Theorem lmodring 20241

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 20237	. 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ (Base‘𝐹)∀𝑟 ∈ (Base‘𝐹)∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠 ‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑥)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = ((𝑞( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = (𝑞( ·𝑠 ‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤)) ∧ ((1r‘𝐹)( ·𝑠 ‘𝑊)𝑤) = 𝑤))))
10	9	simp2bi 1146	1 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∀wral 3062  ‘cfv 6488  (class class class)co 7346  Basecbs 17014  +_gcplusg 17064  ._rcmulr 17065  Scalarcsca 17067   ·_𝑠 cvsca 17068  Grpcgrp 18678  1_rcur 19836  Ringcrg 19882  LModclmod 20233

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708  ax-nul 5258

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-ral 3063  df-rab 3406  df-v 3445  df-sbc 3735  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4278  df-if 4482  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4861  df-br 5101  df-iota 6440  df-fv 6496  df-ov 7349  df-lmod 20235

This theorem is referenced by:  lmodfgrp  20242  lmodmcl  20245  lmod0cl  20259  lmod1cl  20260  lmod0vs  20266  lmodvs0  20267  lmodvsmmulgdi  20268  lmodvsneg  20277  lmodsubvs  20289  lmodsubdi  20290  lmodsubdir  20291  lssvnegcl  20328  islss3  20331  pwslmod  20342  lmodvsinv  20408  islmhm2  20410  lbsind2  20453  lspsneq  20494  lspexch  20501  ip2subdi  20959  isphld  20969  ocvlss  20987  frlmup1  21115  frlmup2  21116  frlmup3  21117  frlmup4  21118  islindf5  21156  lmisfree  21159  asclghm  21197  ascl1  21199  ascldimul  21202  tlmtgp  23457  clmring  24343  lmodslmd  31808  imaslmod  31913  linds2eq  31936  lindsadd  35926  lfl0  37383  lfladd  37384  lflsub  37385  lfl0f  37387  lfladdcl  37389  lfladdcom  37390  lfladdass  37391  lfladd0l  37392  lflnegcl  37393  lflnegl  37394  lflvscl  37395  lflvsdi1  37396  lflvsdi2  37397  lflvsass  37399  lfl0sc  37400  lflsc0N  37401  lfl1sc  37402  lkrlss  37413  eqlkr  37417  eqlkr3  37419  lkrlsp  37420  ldualvsass  37459  lduallmodlem  37470  ldualvsubcl  37474  ldualvsubval  37475  lkrin  37482  dochfl1  39795  lcfl7lem  39818  lclkrlem2m  39838  lclkrlem2o  39840  lclkrlem2p  39841  lcfrlem1  39861  lcfrlem2  39862  lcfrlem3  39863  lcfrlem29  39890  lcfrlem33  39894  lcdvsubval  39937  mapdpglem30  40021  baerlem3lem1  40026  baerlem5alem1  40027  baerlem5blem1  40028  baerlem5blem2  40031  hgmapval1  40212  hdmapinvlem3  40239  hdmapinvlem4  40240  hdmapglem5  40241  hgmapvvlem1  40242  hdmapglem7b  40247  hdmapglem7  40248  lvecring  40571  prjspertr  40755  lmod0rng  45844  linc0scn0  46182  linc1  46184  lincscm  46189  lincscmcl  46191  el0ldep  46225  lindsrng01  46227  lindszr  46228  ldepsprlem  46231  ldepspr  46232  lincresunit3lem3  46233  lincresunitlem1  46234  lincresunitlem2  46235  lincresunit2  46237  lincresunit3lem1  46238