Theorem lmodring 20823

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 2735	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2735	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2735	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		lmodring.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
5		eqid 2735	. . 3 ⊢ (Base‘𝐹) = (Base‘𝐹)
6		eqid 2735	. . 3 ⊢ (+g‘𝐹) = (+g‘𝐹)
7		eqid 2735	. . 3 ⊢ (.r‘𝐹) = (.r‘𝐹)
8		eqid 2735	. . 3 ⊢ (1r‘𝐹) = (1r‘𝐹)
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20819	. 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 1540   ∈ wcel 2108  ∀wral 3051  ‘cfv 6530  (class class class)co 7403  Basecbs 17226  +_gcplusg 17269  ._rcmulr 17270  Scalarcsca 17272   ·_𝑠 cvsca 17273  Grpcgrp 18914  1_rcur 20139  Ringcrg 20191  LModclmod 20815

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 2707  ax-nul 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6483  df-fv 6538  df-ov 7406  df-lmod 20817

This theorem is referenced by:  lmodfgrp  20824  lmodmcl  20828  lmod0cl  20843  lmod1cl  20844  lmod0vs  20850  lmodvs0  20851  lmodvsmmulgdi  20852  lmodvsneg  20861  lmodsubvs  20873  lmodsubdi  20874  lmodsubdir  20875  lssvnegcl  20911  islss3  20914  pwslmod  20925  lmodvsinv  20992  islmhm2  20994  lbsind2  21037  lspsneq  21081  lspexch  21088  ip2subdi  21602  isphld  21612  ocvlss  21630  frlmup1  21756  frlmup2  21757  frlmup3  21758  frlmup4  21759  islindf5  21797  lmisfree  21800  assasca  21820  asclghm  21841  ascl1  21843  ascldimul  21846  tlmtgp  24132  clmring  25019  lmodslmd  33147  imaslmod  33314  linds2eq  33342  lindsadd  37583  lfl0  39029  lfladd  39030  lflsub  39031  lfl0f  39033  lfladdcl  39035  lfladdcom  39036  lfladdass  39037  lfladd0l  39038  lflnegcl  39039  lflnegl  39040  lflvscl  39041  lflvsdi1  39042  lflvsdi2  39043  lflvsass  39045  lfl0sc  39046  lflsc0N  39047  lfl1sc  39048  lkrlss  39059  eqlkr  39063  eqlkr3  39065  lkrlsp  39066  ldualvsass  39105  lduallmodlem  39116  ldualvsubcl  39120  ldualvsubval  39121  lkrin  39128  dochfl1  41441  lcfl7lem  41464  lclkrlem2m  41484  lclkrlem2o  41486  lclkrlem2p  41487  lcfrlem1  41507  lcfrlem2  41508  lcfrlem3  41509  lcfrlem29  41536  lcfrlem33  41540  lcdvsubval  41583  mapdpglem30  41667  baerlem3lem1  41672  baerlem5alem1  41673  baerlem5blem1  41674  baerlem5blem2  41677  hgmapval1  41858  hdmapinvlem3  41885  hdmapinvlem4  41886  hdmapglem5  41887  hgmapvvlem1  41888  hdmapglem7b  41893  hdmapglem7  41894  lvecring  42508  prjspertr  42575  lmod0rng  48152  linc0scn0  48347  linc1  48349  lincscm  48354  lincscmcl  48356  el0ldep  48390  lindsrng01  48392  lindszr  48393  ldepsprlem  48396  ldepspr  48397  lincresunit3lem3  48398  lincresunitlem1  48399  lincresunitlem2  48400  lincresunit2  48402  lincresunit3lem1  48403