Theorem lmodring 20831

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 20827	. 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 6500  (class class class)co 7368  Basecbs 17148  +_gcplusg 17189  ._rcmulr 17190  Scalarcsca 17192   ·_𝑠 cvsca 17193  Grpcgrp 18875  1_rcur 20128  Ringcrg 20180  LModclmod 20823

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 5253

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 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-lmod 20825

This theorem is referenced by:  lmodfgrp  20832  lmodmcl  20836  lmod0cl  20851  lmod1cl  20852  lmod0vs  20858  lmodvs0  20859  lmodvsmmulgdi  20860  lmodvsneg  20869  lmodsubvs  20881  lmodsubdi  20882  lmodsubdir  20883  lssvnegcl  20919  islss3  20922  pwslmod  20933  lmodvsinv  21000  islmhm2  21002  lbsind2  21045  lspsneq  21089  lspexch  21096  ip2subdi  21611  isphld  21621  ocvlss  21639  frlmup1  21765  frlmup2  21766  frlmup3  21767  frlmup4  21768  islindf5  21806  lmisfree  21809  assasca  21829  asclghm  21850  ascl1  21853  ascldimul  21856  tlmtgp  24152  clmring  25038  lmodslmd  33297  imaslmod  33445  linds2eq  33473  lindsadd  37853  lfl0  39430  lfladd  39431  lflsub  39432  lfl0f  39434  lfladdcl  39436  lfladdcom  39437  lfladdass  39438  lfladd0l  39439  lflnegcl  39440  lflnegl  39441  lflvscl  39442  lflvsdi1  39443  lflvsdi2  39444  lflvsass  39446  lfl0sc  39447  lflsc0N  39448  lfl1sc  39449  lkrlss  39460  eqlkr  39464  eqlkr3  39466  lkrlsp  39467  ldualvsass  39506  lduallmodlem  39517  ldualvsubcl  39521  ldualvsubval  39522  lkrin  39529  dochfl1  41841  lcfl7lem  41864  lclkrlem2m  41884  lclkrlem2o  41886  lclkrlem2p  41887  lcfrlem1  41907  lcfrlem2  41908  lcfrlem3  41909  lcfrlem29  41936  lcfrlem33  41940  lcdvsubval  41983  mapdpglem30  42067  baerlem3lem1  42072  baerlem5alem1  42073  baerlem5blem1  42074  baerlem5blem2  42077  hgmapval1  42258  hdmapinvlem3  42285  hdmapinvlem4  42286  hdmapglem5  42287  hgmapvvlem1  42288  hdmapglem7b  42293  hdmapglem7  42294  lvecring  42897  prjspertr  42952  lmod0rng  48578  linc0scn0  48772  linc1  48774  lincscm  48779  lincscmcl  48781  el0ldep  48815  lindsrng01  48817  lindszr  48818  ldepsprlem  48821  ldepspr  48822  lincresunit3lem3  48823  lincresunitlem1  48824  lincresunitlem2  48825  lincresunit2  48827  lincresunit3lem1  48828