Theorem lmodring 18871

Description: The scalar component of a left module is a ring. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)

Hypothesis

Ref	Expression
lmodring.1	⊢ 𝐹 = (Scalar‘𝑊)

Assertion

Ref	Expression
lmodring	⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)

Proof of Theorem lmodring

Dummy variables 𝑟 𝑞 𝑤 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2622	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2622	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2622	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		lmodring.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
5		eqid 2622	. . 3 ⊢ (Base‘𝐹) = (Base‘𝐹)
6		eqid 2622	. . 3 ⊢ (+g‘𝐹) = (+g‘𝐹)
7		eqid 2622	. . 3 ⊢ (.r‘𝐹) = (.r‘𝐹)
8		eqid 2622	. . 3 ⊢ (1r‘𝐹) = (1r‘𝐹)
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 18867	. 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ (Base‘𝐹)∀𝑟 ∈ (Base‘𝐹)∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠 ‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑥)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = ((𝑞( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = (𝑞( ·𝑠 ‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤)) ∧ ((1r‘𝐹)( ·𝑠 ‘𝑊)𝑤) = 𝑤))))
10	9	simp2bi 1077	1 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1037   = wceq 1483   ∈ wcel 1990  ∀wral 2912  ‘cfv 5888  (class class class)co 6650  Basecbs 15857  +_gcplusg 15941  ._rcmulr 15942  Scalarcsca 15944   ·_𝑠 cvsca 15945  Grpcgrp 17422  1_rcur 18501  Ringcrg 18547  LModclmod 18863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-lmod 18865

This theorem is referenced by:  lmodfgrp  18872  lmodmcl  18875  lmod0cl  18889  lmod1cl  18890  lmod0vs  18896  lmodvs0  18897  lmodvsmmulgdi  18898  lmodvsneg  18907  lmodsubvs  18919  lmodsubdi  18920  lmodsubdir  18921  lssvnegcl  18956  islss3  18959  pwslmod  18970  lmodvsinv  19036  islmhm2  19038  lbsind2  19081  lspsneq  19122  lspexch  19129  asclghm  19338  ip2subdi  19989  isphld  19999  ocvlss  20016  frlmup1  20137  frlmup2  20138  frlmup3  20139  frlmup4  20140  islindf5  20178  lmisfree  20181  tlmtgp  21999  clmring  22870  lmodslmd  29757  lfl0  34352  lfladd  34353  lflsub  34354  lfl0f  34356  lfladdcl  34358  lfladdcom  34359  lfladdass  34360  lfladd0l  34361  lflnegcl  34362  lflnegl  34363  lflvscl  34364  lflvsdi1  34365  lflvsdi2  34366  lflvsass  34368  lfl0sc  34369  lflsc0N  34370  lfl1sc  34371  lkrlss  34382  eqlkr  34386  eqlkr3  34388  lkrlsp  34389  ldualvsass  34428  lduallmodlem  34439  ldualvsubcl  34443  ldualvsubval  34444  lkrin  34451  dochfl1  36765  lcfl7lem  36788  lclkrlem2m  36808  lclkrlem2o  36810  lclkrlem2p  36811  lcfrlem1  36831  lcfrlem2  36832  lcfrlem3  36833  lcfrlem29  36860  lcfrlem33  36864  lcdvsubval  36907  mapdpglem30  36991  baerlem3lem1  36996  baerlem5alem1  36997  baerlem5blem1  36998  baerlem5blem2  37001  hgmapval1  37185  hdmapinvlem3  37212  hdmapinvlem4  37213  hdmapglem5  37214  hgmapvvlem1  37215  hdmapglem7b  37220  hdmapglem7  37221  lmod0rng  41868  ascl1  42166  linc0scn0  42212  linc1  42214  lincscm  42219  lincscmcl  42221  el0ldep  42255  lindsrng01  42257  lindszr  42258  ldepsprlem  42261  ldepspr  42262  lincresunit3lem3  42263  lincresunitlem1  42264  lincresunitlem2  42265  lincresunit2  42267  lincresunit3lem1  42268