Theorem lmodring 20131

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106  ∀wral 3064  ‘cfv 6433  (class class class)co 7275  Basecbs 16912  +_gcplusg 16962  ._rcmulr 16963  Scalarcsca 16965   ·_𝑠 cvsca 16966  Grpcgrp 18577  1_rcur 19737  Ringcrg 19783  LModclmod 20123

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-nul 5230

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-iota 6391  df-fv 6441  df-ov 7278  df-lmod 20125

This theorem is referenced by:  lmodfgrp  20132  lmodmcl  20135  lmod0cl  20149  lmod1cl  20150  lmod0vs  20156  lmodvs0  20157  lmodvsmmulgdi  20158  lmodvsneg  20167  lmodsubvs  20179  lmodsubdi  20180  lmodsubdir  20181  lssvnegcl  20218  islss3  20221  pwslmod  20232  lmodvsinv  20298  islmhm2  20300  lbsind2  20343  lspsneq  20384  lspexch  20391  ip2subdi  20849  isphld  20859  ocvlss  20877  frlmup1  21005  frlmup2  21006  frlmup3  21007  frlmup4  21008  islindf5  21046  lmisfree  21049  asclghm  21087  ascl1  21089  ascldimul  21092  tlmtgp  23347  clmring  24233  lmodslmd  31457  imaslmod  31553  linds2eq  31575  lindsadd  35770  lfl0  37079  lfladd  37080  lflsub  37081  lfl0f  37083  lfladdcl  37085  lfladdcom  37086  lfladdass  37087  lfladd0l  37088  lflnegcl  37089  lflnegl  37090  lflvscl  37091  lflvsdi1  37092  lflvsdi2  37093  lflvsass  37095  lfl0sc  37096  lflsc0N  37097  lfl1sc  37098  lkrlss  37109  eqlkr  37113  eqlkr3  37115  lkrlsp  37116  ldualvsass  37155  lduallmodlem  37166  ldualvsubcl  37170  ldualvsubval  37171  lkrin  37178  dochfl1  39490  lcfl7lem  39513  lclkrlem2m  39533  lclkrlem2o  39535  lclkrlem2p  39536  lcfrlem1  39556  lcfrlem2  39557  lcfrlem3  39558  lcfrlem29  39585  lcfrlem33  39589  lcdvsubval  39632  mapdpglem30  39716  baerlem3lem1  39721  baerlem5alem1  39722  baerlem5blem1  39723  baerlem5blem2  39726  hgmapval1  39907  hdmapinvlem3  39934  hdmapinvlem4  39935  hdmapglem5  39936  hgmapvvlem1  39937  hdmapglem7b  39942  hdmapglem7  39943  lvecring  40260  prjspertr  40444  lmod0rng  45426  linc0scn0  45764  linc1  45766  lincscm  45771  lincscmcl  45773  el0ldep  45807  lindsrng01  45809  lindszr  45810  ldepsprlem  45813  ldepspr  45814  lincresunit3lem3  45815  lincresunitlem1  45816  lincresunitlem2  45817  lincresunit2  45819  lincresunit3lem1  45820