Theorem lmodring 20958

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1563   ∈ wcel 2145  ∀wral 3079  ‘cfv 6525  (class class class)co 7400  Basecbs 17259  +_gcplusg 17300  ._rcmulr 17301  Scalarcsca 17303   ·_𝑠 cvsca 17304  Grpcgrp 18990  1_rcur 20254  Ringcrg 20306  LModclmod 20950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3080  df-rab 3418  df-v 3459  df-sbc 3748  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4869  df-br 5106  df-iota 6481  df-fv 6533  df-ov 7403  df-lmod 20952

This theorem is referenced by:  lmodfgrp  20959  lmodmcl  20963  lmod0cl  20978  lmod1cl  20979  lmod0vs  20985  lmodvs0  20986  lmodvsmmulgdi  20987  lmodvsneg  20996  lmodsubvs  21008  lmodsubdi  21009  lmodsubdir  21010  lssvnegcl  21046  islss3  21049  pwslmod  21060  lmodvsinv  21126  islmhm2  21128  lbsind2  21171  lspsneq  21215  lspexch  21222  ip2subdi  21754  isphld  21764  ocvlss  21782  frlmup1  21908  frlmup2  21909  frlmup3  21910  frlmup4  21911  islindf5  21949  lmisfree  21952  assasca  21972  asclghm  21992  ascl1  21995  ascldimul  21998  tlmtgp  24314  clmring  25190  lmodslmd  33437  imaslmod  33588  linds2eq  33610  lindsadd  38124  lfl0  39701  lfladd  39702  lflsub  39703  lfl0f  39705  lfladdcl  39707  lfladdcom  39708  lfladdass  39709  lfladd0l  39710  lflnegcl  39711  lflnegl  39712  lflvscl  39713  lflvsdi1  39714  lflvsdi2  39715  lflvsass  39717  lfl0sc  39718  lflsc0N  39719  lfl1sc  39720  lkrlss  39731  eqlkr  39735  eqlkr3  39737  lkrlsp  39738  ldualvsass  39777  lduallmodlem  39788  ldualvsubcl  39792  ldualvsubval  39793  lkrin  39800  dochfl1  42112  lcfl7lem  42135  lclkrlem2m  42155  lclkrlem2o  42157  lclkrlem2p  42158  lcfrlem1  42178  lcfrlem2  42179  lcfrlem3  42180  lcfrlem29  42207  lcfrlem33  42211  lcdvsubval  42254  mapdpglem30  42338  baerlem3lem1  42343  baerlem5alem1  42344  baerlem5blem1  42345  baerlem5blem2  42348  hgmapval1  42529  hdmapinvlem3  42556  hdmapinvlem4  42557  hdmapglem5  42558  hgmapvvlem1  42559  hdmapglem7b  42564  hdmapglem7  42565  lvecring  43168  prjspertr  43199  lmod0rng  48849  linc0scn0  49054  linc1  49056  lincscm  49061  lincscmcl  49063  el0ldep  49097  lindsrng01  49099  lindszr  49100  ldepsprlem  49103  ldepspr  49104  lincresunit3lem3  49105  lincresunitlem1  49106  lincresunitlem2  49107  lincresunit2  49109  lincresunit3lem1  49110