Theorem lmodring 20968

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1568   ∈ wcel 2141  ∀wral 3077  ‘cfv 6536  (class class class)co 7410  Basecbs 17268  +_gcplusg 17309  ._rcmulr 17310  Scalarcsca 17312   ·_𝑠 cvsca 17313  Grpcgrp 18999  1_rcur 20262  Ringcrg 20314  LModclmod 20960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5268

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rab 3415  df-v 3455  df-sbc 3744  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7413  df-lmod 20962

This theorem is referenced by:  lmodfgrp  20969  lmodmcl  20973  lmod0cl  20988  lmod1cl  20989  lmod0vs  20995  lmodvs0  20996  lmodvsmmulgdi  20997  lmodvsneg  21006  lmodsubvs  21018  lmodsubdi  21019  lmodsubdir  21020  lssvnegcl  21056  islss3  21059  pwslmod  21070  lmodvsinv  21136  islmhm2  21138  lbsind2  21181  lspsneq  21225  lspexch  21232  ip2subdi  21773  isphld  21783  ocvlss  21801  frlmup1  21927  frlmup2  21928  frlmup3  21929  frlmup4  21930  islindf5  21968  lmisfree  21971  assasca  21991  asclghm  22011  ascl1  22014  tlmtgp  24332  clmring  25208  lmodslmd  33490  imaslmod  33639  linds2eq  33660  lindsadd  38230  lfl0  39807  lfladd  39808  lflsub  39809  lfl0f  39811  lfladdcl  39813  lfladdcom  39814  lfladdass  39815  lfladd0l  39816  lflnegcl  39817  lflnegl  39818  lflvscl  39819  lflvsdi1  39820  lflvsdi2  39821  lflvsass  39823  lfl0sc  39824  lflsc0N  39825  lfl1sc  39826  lkrlss  39837  eqlkr  39841  eqlkr3  39843  lkrlsp  39844  ldualvsass  39883  lduallmodlem  39894  ldualvsubcl  39898  ldualvsubval  39899  lkrin  39906  dochfl1  42218  lcfl7lem  42241  lclkrlem2m  42261  lclkrlem2o  42263  lclkrlem2p  42264  lcfrlem1  42284  lcfrlem2  42285  lcfrlem3  42286  lcfrlem29  42313  lcfrlem33  42317  lcdvsubval  42360  mapdpglem30  42444  baerlem3lem1  42449  baerlem5alem1  42450  baerlem5blem1  42451  baerlem5blem2  42454  hgmapval1  42635  hdmapinvlem3  42662  hdmapinvlem4  42663  hdmapglem5  42664  hgmapvvlem1  42665  hdmapglem7b  42670  hdmapglem7  42671  lvecring  43276  prjspertr  43307  lmod0rng  48961  linc0scn0  49170  linc1  49172  lincscm  49177  lincscmcl  49179  el0ldep  49213  lindsrng01  49215  lindszr  49216  ldepsprlem  49219  ldepspr  49220  lincresunit3lem3  49221  lincresunitlem1  49222  lincresunitlem2  49223  lincresunit2  49225  lincresunit3lem1  49226