Theorem lmodring 19642

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 2821	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2821	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2821	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		lmodring.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
5		eqid 2821	. . 3 ⊢ (Base‘𝐹) = (Base‘𝐹)
6		eqid 2821	. . 3 ⊢ (+g‘𝐹) = (+g‘𝐹)
7		eqid 2821	. . 3 ⊢ (.r‘𝐹) = (.r‘𝐹)
8		eqid 2821	. . 3 ⊢ (1r‘𝐹) = (1r‘𝐹)
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 19638	. 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ (Base‘𝐹)∀𝑟 ∈ (Base‘𝐹)∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠 ‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑥)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = ((𝑞( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = (𝑞( ·𝑠 ‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤)) ∧ ((1r‘𝐹)( ·𝑠 ‘𝑊)𝑤) = 𝑤))))
10	9	simp2bi 1142	1 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  ∀wral 3138  ‘cfv 6355  (class class class)co 7156  Basecbs 16483  +_gcplusg 16565  ._rcmulr 16566  Scalarcsca 16568   ·_𝑠 cvsca 16569  Grpcgrp 18103  1_rcur 19251  Ringcrg 19297  LModclmod 19634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-nul 5210

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159  df-lmod 19636

This theorem is referenced by:  lmodfgrp  19643  lmodmcl  19646  lmod0cl  19660  lmod1cl  19661  lmod0vs  19667  lmodvs0  19668  lmodvsmmulgdi  19669  lmodvsneg  19678  lmodsubvs  19690  lmodsubdi  19691  lmodsubdir  19692  lssvnegcl  19728  islss3  19731  pwslmod  19742  lmodvsinv  19808  islmhm2  19810  lbsind2  19853  lspsneq  19894  lspexch  19901  asclghm  20112  ascldimul  20116  ip2subdi  20788  isphld  20798  ocvlss  20816  frlmup1  20942  frlmup2  20943  frlmup3  20944  frlmup4  20945  islindf5  20983  lmisfree  20986  tlmtgp  22804  clmring  23674  lmodslmd  30832  imaslmod  30922  linds2eq  30941  lindsadd  34900  lfl0  36216  lfladd  36217  lflsub  36218  lfl0f  36220  lfladdcl  36222  lfladdcom  36223  lfladdass  36224  lfladd0l  36225  lflnegcl  36226  lflnegl  36227  lflvscl  36228  lflvsdi1  36229  lflvsdi2  36230  lflvsass  36232  lfl0sc  36233  lflsc0N  36234  lfl1sc  36235  lkrlss  36246  eqlkr  36250  eqlkr3  36252  lkrlsp  36253  ldualvsass  36292  lduallmodlem  36303  ldualvsubcl  36307  ldualvsubval  36308  lkrin  36315  dochfl1  38627  lcfl7lem  38650  lclkrlem2m  38670  lclkrlem2o  38672  lclkrlem2p  38673  lcfrlem1  38693  lcfrlem2  38694  lcfrlem3  38695  lcfrlem29  38722  lcfrlem33  38726  lcdvsubval  38769  mapdpglem30  38853  baerlem3lem1  38858  baerlem5alem1  38859  baerlem5blem1  38860  baerlem5blem2  38863  hgmapval1  39044  hdmapinvlem3  39071  hdmapinvlem4  39072  hdmapglem5  39073  hgmapvvlem1  39074  hdmapglem7b  39079  hdmapglem7  39080  lvecring  39167  prjspertr  39275  lmod0rng  44159  ascl1  44452  linc0scn0  44498  linc1  44500  lincscm  44505  lincscmcl  44507  el0ldep  44541  lindsrng01  44543  lindszr  44544  ldepsprlem  44547  ldepspr  44548  lincresunit3lem3  44549  lincresunitlem1  44550  lincresunitlem2  44551  lincresunit2  44553  lincresunit3lem1  44554