Theorem lmodring 19071

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

Syntax hints:   → wi 4   ∧ wa 384   ∧ w3a 1100   = wceq 1637   ∈ wcel 2158  ∀wral 3095  ‘cfv 6098  (class class class)co 6871  Basecbs 16064  +_gcplusg 16149  ._rcmulr 16150  Scalarcsca 16152   ·_𝑠 cvsca 16153  Grpcgrp 17623  1_rcur 18699  Ringcrg 18745  LModclmod 19063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-nul 4980

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ral 3100  df-rex 3101  df-rab 3104  df-v 3392  df-sbc 3631  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-uni 4627  df-br 4841  df-iota 6061  df-fv 6106  df-ov 6874  df-lmod 19065

This theorem is referenced by:  lmodfgrp  19072  lmodmcl  19075  lmod0cl  19089  lmod1cl  19090  lmod0vs  19096  lmodvs0  19097  lmodvsmmulgdi  19098  lmodvsneg  19107  lmodsubvs  19119  lmodsubdi  19120  lmodsubdir  19121  lssvnegcl  19159  islss3  19162  pwslmod  19173  lmodvsinv  19239  islmhm2  19241  lbsind2  19284  lspsneq  19325  lspexch  19333  asclghm  19543  ip2subdi  20195  isphld  20205  ocvlss  20222  frlmup1  20343  frlmup2  20344  frlmup3  20345  frlmup4  20346  islindf5  20384  lmisfree  20387  tlmtgp  22208  clmring  23078  lmodslmd  30079  lfl0  34842  lfladd  34843  lflsub  34844  lfl0f  34846  lfladdcl  34848  lfladdcom  34849  lfladdass  34850  lfladd0l  34851  lflnegcl  34852  lflnegl  34853  lflvscl  34854  lflvsdi1  34855  lflvsdi2  34856  lflvsass  34858  lfl0sc  34859  lflsc0N  34860  lfl1sc  34861  lkrlss  34872  eqlkr  34876  eqlkr3  34878  lkrlsp  34879  ldualvsass  34918  lduallmodlem  34929  ldualvsubcl  34933  ldualvsubval  34934  lkrin  34941  dochfl1  37254  lcfl7lem  37277  lclkrlem2m  37297  lclkrlem2o  37299  lclkrlem2p  37300  lcfrlem1  37320  lcfrlem2  37321  lcfrlem3  37322  lcfrlem29  37349  lcfrlem33  37353  lcdvsubval  37396  mapdpglem30  37480  baerlem3lem1  37485  baerlem5alem1  37486  baerlem5blem1  37487  baerlem5blem2  37490  hgmapval1  37671  hdmapinvlem3  37698  hdmapinvlem4  37699  hdmapglem5  37700  hgmapvvlem1  37701  hdmapglem7b  37706  hdmapglem7  37707  lmod0rng  42433  ascl1  42731  linc0scn0  42777  linc1  42779  lincscm  42784  lincscmcl  42786  el0ldep  42820  lindsrng01  42822  lindszr  42823  ldepsprlem  42826  ldepspr  42827  lincresunit3lem3  42828  lincresunitlem1  42829  lincresunitlem2  42830  lincresunit2  42832  lincresunit3lem1  42833