Theorem lmodring 19636

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083   = wceq 1533   ∈ wcel 2110  ∀wral 3138  ‘cfv 6350  (class class class)co 7150  Basecbs 16477  +_gcplusg 16559  ._rcmulr 16560  Scalarcsca 16562   ·_𝑠 cvsca 16563  Grpcgrp 18097  1_rcur 19245  Ringcrg 19291  LModclmod 19628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-nul 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-iota 6309  df-fv 6358  df-ov 7153  df-lmod 19630

This theorem is referenced by:  lmodfgrp  19637  lmodmcl  19640  lmod0cl  19654  lmod1cl  19655  lmod0vs  19661  lmodvs0  19662  lmodvsmmulgdi  19663  lmodvsneg  19672  lmodsubvs  19684  lmodsubdi  19685  lmodsubdir  19686  lssvnegcl  19722  islss3  19725  pwslmod  19736  lmodvsinv  19802  islmhm2  19804  lbsind2  19847  lspsneq  19888  lspexch  19895  asclghm  20106  ascldimul  20110  ip2subdi  20782  isphld  20792  ocvlss  20810  frlmup1  20936  frlmup2  20937  frlmup3  20938  frlmup4  20939  islindf5  20977  lmisfree  20980  tlmtgp  22798  clmring  23668  lmodslmd  30827  imaslmod  30917  linds2eq  30936  lindsadd  34879  lfl0  36195  lfladd  36196  lflsub  36197  lfl0f  36199  lfladdcl  36201  lfladdcom  36202  lfladdass  36203  lfladd0l  36204  lflnegcl  36205  lflnegl  36206  lflvscl  36207  lflvsdi1  36208  lflvsdi2  36209  lflvsass  36211  lfl0sc  36212  lflsc0N  36213  lfl1sc  36214  lkrlss  36225  eqlkr  36229  eqlkr3  36231  lkrlsp  36232  ldualvsass  36271  lduallmodlem  36282  ldualvsubcl  36286  ldualvsubval  36287  lkrin  36294  dochfl1  38606  lcfl7lem  38629  lclkrlem2m  38649  lclkrlem2o  38651  lclkrlem2p  38652  lcfrlem1  38672  lcfrlem2  38673  lcfrlem3  38674  lcfrlem29  38701  lcfrlem33  38705  lcdvsubval  38748  mapdpglem30  38832  baerlem3lem1  38837  baerlem5alem1  38838  baerlem5blem1  38839  baerlem5blem2  38842  hgmapval1  39023  hdmapinvlem3  39050  hdmapinvlem4  39051  hdmapglem5  39052  hgmapvvlem1  39053  hdmapglem7b  39058  hdmapglem7  39059  lvecring  39140  prjspertr  39248  lmod0rng  44132  ascl1  44425  linc0scn0  44471  linc1  44473  lincscm  44478  lincscmcl  44480  el0ldep  44514  lindsrng01  44516  lindszr  44517  ldepsprlem  44520  ldepspr  44521  lincresunit3lem3  44522  lincresunitlem1  44523  lincresunitlem2  44524  lincresunit2  44526  lincresunit3lem1  44527