Theorem lmodring 20781

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 20777	. 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 1540   ∈ wcel 2109  ∀wral 3045  ‘cfv 6514  (class class class)co 7390  Basecbs 17186  +_gcplusg 17227  ._rcmulr 17228  Scalarcsca 17230   ·_𝑠 cvsca 17231  Grpcgrp 18872  1_rcur 20097  Ringcrg 20149  LModclmod 20773

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-lmod 20775

This theorem is referenced by:  lmodfgrp  20782  lmodmcl  20786  lmod0cl  20801  lmod1cl  20802  lmod0vs  20808  lmodvs0  20809  lmodvsmmulgdi  20810  lmodvsneg  20819  lmodsubvs  20831  lmodsubdi  20832  lmodsubdir  20833  lssvnegcl  20869  islss3  20872  pwslmod  20883  lmodvsinv  20950  islmhm2  20952  lbsind2  20995  lspsneq  21039  lspexch  21046  ip2subdi  21560  isphld  21570  ocvlss  21588  frlmup1  21714  frlmup2  21715  frlmup3  21716  frlmup4  21717  islindf5  21755  lmisfree  21758  assasca  21778  asclghm  21799  ascl1  21801  ascldimul  21804  tlmtgp  24090  clmring  24977  lmodslmd  33164  imaslmod  33331  linds2eq  33359  lindsadd  37614  lfl0  39065  lfladd  39066  lflsub  39067  lfl0f  39069  lfladdcl  39071  lfladdcom  39072  lfladdass  39073  lfladd0l  39074  lflnegcl  39075  lflnegl  39076  lflvscl  39077  lflvsdi1  39078  lflvsdi2  39079  lflvsass  39081  lfl0sc  39082  lflsc0N  39083  lfl1sc  39084  lkrlss  39095  eqlkr  39099  eqlkr3  39101  lkrlsp  39102  ldualvsass  39141  lduallmodlem  39152  ldualvsubcl  39156  ldualvsubval  39157  lkrin  39164  dochfl1  41477  lcfl7lem  41500  lclkrlem2m  41520  lclkrlem2o  41522  lclkrlem2p  41523  lcfrlem1  41543  lcfrlem2  41544  lcfrlem3  41545  lcfrlem29  41572  lcfrlem33  41576  lcdvsubval  41619  mapdpglem30  41703  baerlem3lem1  41708  baerlem5alem1  41709  baerlem5blem1  41710  baerlem5blem2  41713  hgmapval1  41894  hdmapinvlem3  41921  hdmapinvlem4  41922  hdmapglem5  41923  hgmapvvlem1  41924  hdmapglem7b  41929  hdmapglem7  41930  lvecring  42533  prjspertr  42600  lmod0rng  48221  linc0scn0  48416  linc1  48418  lincscm  48423  lincscmcl  48425  el0ldep  48459  lindsrng01  48461  lindszr  48462  ldepsprlem  48465  ldepspr  48466  lincresunit3lem3  48467  lincresunitlem1  48468  lincresunitlem2  48469  lincresunit2  48471  lincresunit3lem1  48472