Theorem lmodring 21173

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ‘cfv 6558  (class class class)co 7443  Basecbs 17416  +_gcplusg 17457  ._rcmulr 17458  Scalarcsca 17460   ·_𝑠 cvsca 17461  Grpcgrp 19173  1_rcur 20437  Ringcrg 20489  LModclmod 21165

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5263

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-iota 6512  df-fv 6566  df-ov 7446  df-lmod 21167

This theorem is used by:  lmodfgrp  21174  lmodmcl  21178  lmod0cl  21193  lmod1cl  21194  lmod0vs  21200  lmodvs0  21201  lmodvsmmulgdi  21202  lmodvsneg  21211  lmodsubvs  21223  lmodsubdi  21224  lmodsubdir  21225  lssvnegcl  21261  islss3  21264  pwslmod  21275  lmodvsinv  21341  islmhm2  21343  lbsind2  21386  lspsneq  21430  lspexch  21437  ip2subdi  21980  isphld  21990  ocvlss  22008  frlmup1  22134  frlmup2  22135  frlmup3  22136  frlmup4  22137  islindf5  22175  lmisfree  22178  assasca  22200  asclghm  22220  ascl1  22223  tlmtgp  24545  clmring  25421  lmodslmd  33835  imaslmod  33984  linds2eq  34006  lindsadd  38728  lfl0  40314  lfladd  40315  lflsub  40316  lfl0f  40318  lfladdcl  40320  lfladdcom  40321  lfladdass  40322  lfladd0l  40323  lflnegcl  40324  lflnegl  40325  lflvscl  40326  lflvsdi1  40327  lflvsdi2  40328  lflvsass  40330  lfl0sc  40331  lflsc0N  40332  lfl1sc  40333  lkrlss  40344  eqlkr  40348  eqlkr3  40350  lkrlsp  40351  ldualvsass  40390  lduallmodlem  40401  ldualvsubcl  40405  ldualvsubval  40406  lkrin  40413  dochfl1  42725  lcfl7lem  42748  lclkrlem2m  42768  lclkrlem2o  42770  lclkrlem2p  42771  lcfrlem1  42791  lcfrlem2  42792  lcfrlem3  42793  lcfrlem29  42820  lcfrlem33  42824  lcdvsubval  42867  mapdpglem30  42951  baerlem3lem1  42956  baerlem5alem1  42957  baerlem5blem1  42958  baerlem5blem2  42961  hgmapval1  43142  hdmapinvlem3  43169  hdmapinvlem4  43170  hdmapglem5  43171  hgmapvvlem1  43172  hdmapglem7b  43177  hdmapglem7  43178  lvecring  43795  prjspertr  43826  lmod0rng  49531  linc0scn0  49740  linc1  49742  lincscm  49747  lincscmcl  49749  el0ldep  49783  lindsrng01  49785  lindszr  49786  ldepsprlem  49789  ldepspr  49790  lincresunit3lem3  49791  lincresunitlem1  49792  lincresunitlem2  49793  lincresunit2  49795  lincresunit3lem1  49796