Theorem lmodring 20863

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 2736	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2736	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2736	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		lmodring.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
5		eqid 2736	. . 3 ⊢ (Base‘𝐹) = (Base‘𝐹)
6		eqid 2736	. . 3 ⊢ (+g‘𝐹) = (+g‘𝐹)
7		eqid 2736	. . 3 ⊢ (.r‘𝐹) = (.r‘𝐹)
8		eqid 2736	. . 3 ⊢ (1r‘𝐹) = (1r‘𝐹)
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20859	. 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 3051  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  +_gcplusg 17220  ._rcmulr 17221  Scalarcsca 17223   ·_𝑠 cvsca 17224  Grpcgrp 18909  1_rcur 20162  Ringcrg 20214  LModclmod 20855

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 2708  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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3390  df-v 3431  df-sbc 3729  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-lmod 20857

This theorem is referenced by:  lmodfgrp  20864  lmodmcl  20868  lmod0cl  20883  lmod1cl  20884  lmod0vs  20890  lmodvs0  20891  lmodvsmmulgdi  20892  lmodvsneg  20901  lmodsubvs  20913  lmodsubdi  20914  lmodsubdir  20915  lssvnegcl  20951  islss3  20954  pwslmod  20965  lmodvsinv  21031  islmhm2  21033  lbsind2  21076  lspsneq  21120  lspexch  21127  ip2subdi  21624  isphld  21634  ocvlss  21652  frlmup1  21778  frlmup2  21779  frlmup3  21780  frlmup4  21781  islindf5  21819  lmisfree  21822  assasca  21842  asclghm  21862  ascl1  21865  ascldimul  21868  tlmtgp  24161  clmring  25037  lmodslmd  33265  imaslmod  33413  linds2eq  33441  lindsadd  37934  lfl0  39511  lfladd  39512  lflsub  39513  lfl0f  39515  lfladdcl  39517  lfladdcom  39518  lfladdass  39519  lfladd0l  39520  lflnegcl  39521  lflnegl  39522  lflvscl  39523  lflvsdi1  39524  lflvsdi2  39525  lflvsass  39527  lfl0sc  39528  lflsc0N  39529  lfl1sc  39530  lkrlss  39541  eqlkr  39545  eqlkr3  39547  lkrlsp  39548  ldualvsass  39587  lduallmodlem  39598  ldualvsubcl  39602  ldualvsubval  39603  lkrin  39610  dochfl1  41922  lcfl7lem  41945  lclkrlem2m  41965  lclkrlem2o  41967  lclkrlem2p  41968  lcfrlem1  41988  lcfrlem2  41989  lcfrlem3  41990  lcfrlem29  42017  lcfrlem33  42021  lcdvsubval  42064  mapdpglem30  42148  baerlem3lem1  42153  baerlem5alem1  42154  baerlem5blem1  42155  baerlem5blem2  42158  hgmapval1  42339  hdmapinvlem3  42366  hdmapinvlem4  42367  hdmapglem5  42368  hgmapvvlem1  42369  hdmapglem7b  42374  hdmapglem7  42375  lvecring  42983  prjspertr  43038  lmod0rng  48705  linc0scn0  48899  linc1  48901  lincscm  48906  lincscmcl  48908  el0ldep  48942  lindsrng01  48944  lindszr  48945  ldepsprlem  48948  ldepspr  48949  lincresunit3lem3  48950  lincresunitlem1  48951  lincresunitlem2  48952  lincresunit2  48954  lincresunit3lem1  48955