Theorem lmodring 20882

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105  ∀wral 3058  ‘cfv 6562  (class class class)co 7430  Basecbs 17244  +_gcplusg 17297  ._rcmulr 17298  Scalarcsca 17300   ·_𝑠 cvsca 17301  Grpcgrp 18963  1_rcur 20198  Ringcrg 20250  LModclmod 20874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-nul 5311

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rab 3433  df-v 3479  df-sbc 3791  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-iota 6515  df-fv 6570  df-ov 7433  df-lmod 20876

This theorem is referenced by:  lmodfgrp  20883  lmodmcl  20887  lmod0cl  20902  lmod1cl  20903  lmod0vs  20909  lmodvs0  20910  lmodvsmmulgdi  20911  lmodvsneg  20920  lmodsubvs  20932  lmodsubdi  20933  lmodsubdir  20934  lssvnegcl  20971  islss3  20974  pwslmod  20985  lmodvsinv  21052  islmhm2  21054  lbsind2  21097  lspsneq  21141  lspexch  21148  ip2subdi  21679  isphld  21689  ocvlss  21707  frlmup1  21835  frlmup2  21836  frlmup3  21837  frlmup4  21838  islindf5  21876  lmisfree  21879  assasca  21899  asclghm  21920  ascl1  21922  ascldimul  21925  tlmtgp  24219  clmring  25116  lmodslmd  33192  imaslmod  33360  linds2eq  33388  lindsadd  37599  lfl0  39046  lfladd  39047  lflsub  39048  lfl0f  39050  lfladdcl  39052  lfladdcom  39053  lfladdass  39054  lfladd0l  39055  lflnegcl  39056  lflnegl  39057  lflvscl  39058  lflvsdi1  39059  lflvsdi2  39060  lflvsass  39062  lfl0sc  39063  lflsc0N  39064  lfl1sc  39065  lkrlss  39076  eqlkr  39080  eqlkr3  39082  lkrlsp  39083  ldualvsass  39122  lduallmodlem  39133  ldualvsubcl  39137  ldualvsubval  39138  lkrin  39145  dochfl1  41458  lcfl7lem  41481  lclkrlem2m  41501  lclkrlem2o  41503  lclkrlem2p  41504  lcfrlem1  41524  lcfrlem2  41525  lcfrlem3  41526  lcfrlem29  41553  lcfrlem33  41557  lcdvsubval  41600  mapdpglem30  41684  baerlem3lem1  41689  baerlem5alem1  41690  baerlem5blem1  41691  baerlem5blem2  41694  hgmapval1  41875  hdmapinvlem3  41902  hdmapinvlem4  41903  hdmapglem5  41904  hgmapvvlem1  41905  hdmapglem7b  41910  hdmapglem7  41911  lvecring  42524  prjspertr  42591  lmod0rng  48072  linc0scn0  48268  linc1  48270  lincscm  48275  lincscmcl  48277  el0ldep  48311  lindsrng01  48313  lindszr  48314  ldepsprlem  48317  ldepspr  48318  lincresunit3lem3  48319  lincresunitlem1  48320  lincresunitlem2  48321  lincresunit2  48323  lincresunit3lem1  48324