Theorem lmodring 20046

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ∀wral 3063  ‘cfv 6418  (class class class)co 7255  Basecbs 16840  +_gcplusg 16888  ._rcmulr 16889  Scalarcsca 16891   ·_𝑠 cvsca 16892  Grpcgrp 18492  1_rcur 19652  Ringcrg 19698  LModclmod 20038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-nul 5225

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426  df-ov 7258  df-lmod 20040

This theorem is referenced by:  lmodfgrp  20047  lmodmcl  20050  lmod0cl  20064  lmod1cl  20065  lmod0vs  20071  lmodvs0  20072  lmodvsmmulgdi  20073  lmodvsneg  20082  lmodsubvs  20094  lmodsubdi  20095  lmodsubdir  20096  lssvnegcl  20133  islss3  20136  pwslmod  20147  lmodvsinv  20213  islmhm2  20215  lbsind2  20258  lspsneq  20299  lspexch  20306  ip2subdi  20761  isphld  20771  ocvlss  20789  frlmup1  20915  frlmup2  20916  frlmup3  20917  frlmup4  20918  islindf5  20956  lmisfree  20959  asclghm  20997  ascl1  20999  ascldimul  21002  tlmtgp  23255  clmring  24139  lmodslmd  31359  imaslmod  31455  linds2eq  31477  lindsadd  35697  lfl0  37006  lfladd  37007  lflsub  37008  lfl0f  37010  lfladdcl  37012  lfladdcom  37013  lfladdass  37014  lfladd0l  37015  lflnegcl  37016  lflnegl  37017  lflvscl  37018  lflvsdi1  37019  lflvsdi2  37020  lflvsass  37022  lfl0sc  37023  lflsc0N  37024  lfl1sc  37025  lkrlss  37036  eqlkr  37040  eqlkr3  37042  lkrlsp  37043  ldualvsass  37082  lduallmodlem  37093  ldualvsubcl  37097  ldualvsubval  37098  lkrin  37105  dochfl1  39417  lcfl7lem  39440  lclkrlem2m  39460  lclkrlem2o  39462  lclkrlem2p  39463  lcfrlem1  39483  lcfrlem2  39484  lcfrlem3  39485  lcfrlem29  39512  lcfrlem33  39516  lcdvsubval  39559  mapdpglem30  39643  baerlem3lem1  39648  baerlem5alem1  39649  baerlem5blem1  39650  baerlem5blem2  39653  hgmapval1  39834  hdmapinvlem3  39861  hdmapinvlem4  39862  hdmapglem5  39863  hgmapvvlem1  39864  hdmapglem7b  39869  hdmapglem7  39870  lvecring  40185  prjspertr  40365  lmod0rng  45314  linc0scn0  45652  linc1  45654  lincscm  45659  lincscmcl  45661  el0ldep  45695  lindsrng01  45697  lindszr  45698  ldepsprlem  45701  ldepspr  45702  lincresunit3lem3  45703  lincresunitlem1  45704  lincresunitlem2  45705  lincresunit2  45707  lincresunit3lem1  45708