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 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 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 3052  ‘cfv 6499  (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 2709  ax-nul 5242

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 6455  df-fv 6507  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  48699  linc0scn0  48893  linc1  48895  lincscm  48900  lincscmcl  48902  el0ldep  48936  lindsrng01  48938  lindszr  48939  ldepsprlem  48942  ldepspr  48943  lincresunit3lem3  48944  lincresunitlem1  48945  lincresunitlem2  48946  lincresunit2  48948  lincresunit3lem1  48949