Theorem lmodring 20811

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 2733	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2733	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2733	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		lmodring.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
5		eqid 2733	. . 3 ⊢ (Base‘𝐹) = (Base‘𝐹)
6		eqid 2733	. . 3 ⊢ (+g‘𝐹) = (+g‘𝐹)
7		eqid 2733	. . 3 ⊢ (.r‘𝐹) = (.r‘𝐹)
8		eqid 2733	. . 3 ⊢ (1r‘𝐹) = (1r‘𝐹)
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20807	. 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 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ∀wral 3049  ‘cfv 6489  (class class class)co 7355  Basecbs 17130  +_gcplusg 17171  ._rcmulr 17172  Scalarcsca 17174   ·_𝑠 cvsca 17175  Grpcgrp 18856  1_rcur 20109  Ringcrg 20161  LModclmod 20803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2931  df-ral 3050  df-rab 3398  df-v 3440  df-sbc 3739  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-iota 6445  df-fv 6497  df-ov 7358  df-lmod 20805

This theorem is referenced by:  lmodfgrp  20812  lmodmcl  20816  lmod0cl  20831  lmod1cl  20832  lmod0vs  20838  lmodvs0  20839  lmodvsmmulgdi  20840  lmodvsneg  20849  lmodsubvs  20861  lmodsubdi  20862  lmodsubdir  20863  lssvnegcl  20899  islss3  20902  pwslmod  20913  lmodvsinv  20980  islmhm2  20982  lbsind2  21025  lspsneq  21069  lspexch  21076  ip2subdi  21591  isphld  21601  ocvlss  21619  frlmup1  21745  frlmup2  21746  frlmup3  21747  frlmup4  21748  islindf5  21786  lmisfree  21789  assasca  21809  asclghm  21830  ascl1  21832  ascldimul  21835  tlmtgp  24121  clmring  25007  lmodslmd  33184  imaslmod  33329  linds2eq  33357  lindsadd  37663  lfl0  39174  lfladd  39175  lflsub  39176  lfl0f  39178  lfladdcl  39180  lfladdcom  39181  lfladdass  39182  lfladd0l  39183  lflnegcl  39184  lflnegl  39185  lflvscl  39186  lflvsdi1  39187  lflvsdi2  39188  lflvsass  39190  lfl0sc  39191  lflsc0N  39192  lfl1sc  39193  lkrlss  39204  eqlkr  39208  eqlkr3  39210  lkrlsp  39211  ldualvsass  39250  lduallmodlem  39261  ldualvsubcl  39265  ldualvsubval  39266  lkrin  39273  dochfl1  41585  lcfl7lem  41608  lclkrlem2m  41628  lclkrlem2o  41630  lclkrlem2p  41631  lcfrlem1  41651  lcfrlem2  41652  lcfrlem3  41653  lcfrlem29  41680  lcfrlem33  41684  lcdvsubval  41727  mapdpglem30  41811  baerlem3lem1  41816  baerlem5alem1  41817  baerlem5blem1  41818  baerlem5blem2  41821  hgmapval1  42002  hdmapinvlem3  42029  hdmapinvlem4  42030  hdmapglem5  42031  hgmapvvlem1  42032  hdmapglem7b  42037  hdmapglem7  42038  lvecring  42646  prjspertr  42713  lmod0rng  48343  linc0scn0  48538  linc1  48540  lincscm  48545  lincscmcl  48547  el0ldep  48581  lindsrng01  48583  lindszr  48584  ldepsprlem  48587  ldepspr  48588  lincresunit3lem3  48589  lincresunitlem1  48590  lincresunitlem2  48591  lincresunit2  48593  lincresunit3lem1  48594