Theorem lmodring 20852

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ‘cfv 6490  (class class class)co 7358  Basecbs 17168  +_gcplusg 17209  ._rcmulr 17210  Scalarcsca 17212   ·_𝑠 cvsca 17213  Grpcgrp 18898  1_rcur 20151  Ringcrg 20203  LModclmod 20844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-iota 6446  df-fv 6498  df-ov 7361  df-lmod 20846

This theorem is referenced by:  lmodfgrp  20853  lmodmcl  20857  lmod0cl  20872  lmod1cl  20873  lmod0vs  20879  lmodvs0  20880  lmodvsmmulgdi  20881  lmodvsneg  20890  lmodsubvs  20902  lmodsubdi  20903  lmodsubdir  20904  lssvnegcl  20940  islss3  20943  pwslmod  20954  lmodvsinv  21021  islmhm2  21023  lbsind2  21066  lspsneq  21110  lspexch  21117  ip2subdi  21632  isphld  21642  ocvlss  21660  frlmup1  21786  frlmup2  21787  frlmup3  21788  frlmup4  21789  islindf5  21827  lmisfree  21830  assasca  21850  asclghm  21870  ascl1  21873  ascldimul  21876  tlmtgp  24170  clmring  25046  lmodslmd  33285  imaslmod  33433  linds2eq  33461  lindsadd  37945  lfl0  39522  lfladd  39523  lflsub  39524  lfl0f  39526  lfladdcl  39528  lfladdcom  39529  lfladdass  39530  lfladd0l  39531  lflnegcl  39532  lflnegl  39533  lflvscl  39534  lflvsdi1  39535  lflvsdi2  39536  lflvsass  39538  lfl0sc  39539  lflsc0N  39540  lfl1sc  39541  lkrlss  39552  eqlkr  39556  eqlkr3  39558  lkrlsp  39559  ldualvsass  39598  lduallmodlem  39609  ldualvsubcl  39613  ldualvsubval  39614  lkrin  39621  dochfl1  41933  lcfl7lem  41956  lclkrlem2m  41976  lclkrlem2o  41978  lclkrlem2p  41979  lcfrlem1  41999  lcfrlem2  42000  lcfrlem3  42001  lcfrlem29  42028  lcfrlem33  42032  lcdvsubval  42075  mapdpglem30  42159  baerlem3lem1  42164  baerlem5alem1  42165  baerlem5blem1  42166  baerlem5blem2  42169  hgmapval1  42350  hdmapinvlem3  42377  hdmapinvlem4  42378  hdmapglem5  42379  hgmapvvlem1  42380  hdmapglem7b  42385  hdmapglem7  42386  lvecring  42994  prjspertr  43049  lmod0rng  48702  linc0scn0  48896  linc1  48898  lincscm  48903  lincscmcl  48905  el0ldep  48939  lindsrng01  48941  lindszr  48942  ldepsprlem  48945  ldepspr  48946  lincresunit3lem3  48947  lincresunitlem1  48948  lincresunitlem2  48949  lincresunit2  48951  lincresunit3lem1  48952