Theorem lmodring 20794

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2110  ∀wral 3045  ‘cfv 6477  (class class class)co 7341  Basecbs 17112  +_gcplusg 17153  ._rcmulr 17154  Scalarcsca 17156   ·_𝑠 cvsca 17157  Grpcgrp 18838  1_rcur 20092  Ringcrg 20144  LModclmod 20786

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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702  ax-nul 5242

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rab 3394  df-v 3436  df-sbc 3740  df-dif 3903  df-un 3905  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4858  df-br 5090  df-iota 6433  df-fv 6485  df-ov 7344  df-lmod 20788

This theorem is referenced by:  lmodfgrp  20795  lmodmcl  20799  lmod0cl  20814  lmod1cl  20815  lmod0vs  20821  lmodvs0  20822  lmodvsmmulgdi  20823  lmodvsneg  20832  lmodsubvs  20844  lmodsubdi  20845  lmodsubdir  20846  lssvnegcl  20882  islss3  20885  pwslmod  20896  lmodvsinv  20963  islmhm2  20965  lbsind2  21008  lspsneq  21052  lspexch  21059  ip2subdi  21574  isphld  21584  ocvlss  21602  frlmup1  21728  frlmup2  21729  frlmup3  21730  frlmup4  21731  islindf5  21769  lmisfree  21772  assasca  21792  asclghm  21813  ascl1  21815  ascldimul  21818  tlmtgp  24104  clmring  24990  lmodslmd  33163  imaslmod  33308  linds2eq  33336  lindsadd  37632  lfl0  39083  lfladd  39084  lflsub  39085  lfl0f  39087  lfladdcl  39089  lfladdcom  39090  lfladdass  39091  lfladd0l  39092  lflnegcl  39093  lflnegl  39094  lflvscl  39095  lflvsdi1  39096  lflvsdi2  39097  lflvsass  39099  lfl0sc  39100  lflsc0N  39101  lfl1sc  39102  lkrlss  39113  eqlkr  39117  eqlkr3  39119  lkrlsp  39120  ldualvsass  39159  lduallmodlem  39170  ldualvsubcl  39174  ldualvsubval  39175  lkrin  39182  dochfl1  41494  lcfl7lem  41517  lclkrlem2m  41537  lclkrlem2o  41539  lclkrlem2p  41540  lcfrlem1  41560  lcfrlem2  41561  lcfrlem3  41562  lcfrlem29  41589  lcfrlem33  41593  lcdvsubval  41636  mapdpglem30  41720  baerlem3lem1  41725  baerlem5alem1  41726  baerlem5blem1  41727  baerlem5blem2  41730  hgmapval1  41911  hdmapinvlem3  41938  hdmapinvlem4  41939  hdmapglem5  41940  hgmapvvlem1  41941  hdmapglem7b  41946  hdmapglem7  41947  lvecring  42550  prjspertr  42617  lmod0rng  48239  linc0scn0  48434  linc1  48436  lincscm  48441  lincscmcl  48443  el0ldep  48477  lindsrng01  48479  lindszr  48480  ldepsprlem  48483  ldepspr  48484  lincresunit3lem3  48485  lincresunitlem1  48486  lincresunitlem2  48487  lincresunit2  48489  lincresunit3lem1  48490