Theorem lmodring 20866

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 20862	. 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 1540   ∈ wcel 2108  ∀wral 3061  ‘cfv 6561  (class class class)co 7431  Basecbs 17247  +_gcplusg 17297  ._rcmulr 17298  Scalarcsca 17300   ·_𝑠 cvsca 17301  Grpcgrp 18951  1_rcur 20178  Ringcrg 20230  LModclmod 20858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rab 3437  df-v 3482  df-sbc 3789  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-lmod 20860

This theorem is referenced by:  lmodfgrp  20867  lmodmcl  20871  lmod0cl  20886  lmod1cl  20887  lmod0vs  20893  lmodvs0  20894  lmodvsmmulgdi  20895  lmodvsneg  20904  lmodsubvs  20916  lmodsubdi  20917  lmodsubdir  20918  lssvnegcl  20954  islss3  20957  pwslmod  20968  lmodvsinv  21035  islmhm2  21037  lbsind2  21080  lspsneq  21124  lspexch  21131  ip2subdi  21662  isphld  21672  ocvlss  21690  frlmup1  21818  frlmup2  21819  frlmup3  21820  frlmup4  21821  islindf5  21859  lmisfree  21862  assasca  21882  asclghm  21903  ascl1  21905  ascldimul  21908  tlmtgp  24204  clmring  25103  lmodslmd  33210  imaslmod  33381  linds2eq  33409  lindsadd  37620  lfl0  39066  lfladd  39067  lflsub  39068  lfl0f  39070  lfladdcl  39072  lfladdcom  39073  lfladdass  39074  lfladd0l  39075  lflnegcl  39076  lflnegl  39077  lflvscl  39078  lflvsdi1  39079  lflvsdi2  39080  lflvsass  39082  lfl0sc  39083  lflsc0N  39084  lfl1sc  39085  lkrlss  39096  eqlkr  39100  eqlkr3  39102  lkrlsp  39103  ldualvsass  39142  lduallmodlem  39153  ldualvsubcl  39157  ldualvsubval  39158  lkrin  39165  dochfl1  41478  lcfl7lem  41501  lclkrlem2m  41521  lclkrlem2o  41523  lclkrlem2p  41524  lcfrlem1  41544  lcfrlem2  41545  lcfrlem3  41546  lcfrlem29  41573  lcfrlem33  41577  lcdvsubval  41620  mapdpglem30  41704  baerlem3lem1  41709  baerlem5alem1  41710  baerlem5blem1  41711  baerlem5blem2  41714  hgmapval1  41895  hdmapinvlem3  41922  hdmapinvlem4  41923  hdmapglem5  41924  hgmapvvlem1  41925  hdmapglem7b  41930  hdmapglem7  41931  lvecring  42548  prjspertr  42615  lmod0rng  48145  linc0scn0  48340  linc1  48342  lincscm  48347  lincscmcl  48349  el0ldep  48383  lindsrng01  48385  lindszr  48386  ldepsprlem  48389  ldepspr  48390  lincresunit3lem3  48391  lincresunitlem1  48392  lincresunitlem2  48393  lincresunit2  48395  lincresunit3lem1  48396