MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lmodrng Unicode version

Theorem lmodrng 15635
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
lmodrng.1  |-  F  =  (Scalar `  W )
Assertion
Ref Expression
lmodrng  |-  ( W  e.  LMod  ->  F  e. 
Ring )

Proof of Theorem lmodrng
Dummy variables  r 
q  w  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2283 . . 3  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2283 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
3 eqid 2283 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
4 lmodrng.1 . . 3  |-  F  =  (Scalar `  W )
5 eqid 2283 . . 3  |-  ( Base `  F )  =  (
Base `  F )
6 eqid 2283 . . 3  |-  ( +g  `  F )  =  ( +g  `  F )
7 eqid 2283 . . 3  |-  ( .r
`  F )  =  ( .r `  F
)
8 eqid 2283 . . 3  |-  ( 1r
`  F )  =  ( 1r `  F
)
91, 2, 3, 4, 5, 6, 7, 8islmod 15631 . 2  |-  ( W  e.  LMod  <->  ( W  e. 
Grp  /\  F  e.  Ring  /\  A. q  e.  (
Base `  F ) A. r  e.  ( Base `  F ) A. x  e.  ( Base `  W ) A. w  e.  ( Base `  W
) ( ( ( r ( .s `  W ) w )  e.  ( Base `  W
)  /\  ( r
( .s `  W
) ( w ( +g  `  W ) x ) )  =  ( ( r ( .s `  W ) w ) ( +g  `  W ) ( r ( .s `  W
) x ) )  /\  ( ( q ( +g  `  F
) r ) ( .s `  W ) w )  =  ( ( q ( .s
`  W ) w ) ( +g  `  W
) ( r ( .s `  W ) w ) ) )  /\  ( ( ( q ( .r `  F ) r ) ( .s `  W
) w )  =  ( q ( .s
`  W ) ( r ( .s `  W ) w ) )  /\  ( ( 1r `  F ) ( .s `  W
) w )  =  w ) ) ) )
109simp2bi 971 1  |-  ( W  e.  LMod  ->  F  e. 
Ring )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934    = wceq 1623    e. wcel 1684   A.wral 2543   ` cfv 5255  (class class class)co 5858   Basecbs 13148   +g cplusg 13208   .rcmulr 13209  Scalarcsca 13211   .scvsca 13212   Grpcgrp 14362   Ringcrg 15337   1rcur 15339   LModclmod 15627
This theorem is referenced by:  lmodfgrp  15636  lmodmcl  15639  lmod0cl  15656  lmod1cl  15657  lmod0vs  15663  lmodvs0  15664  lmodvsnegOLD  15668  lmodvsneg  15669  lmodsubvs  15681  lmodsubdi  15682  lmodsubdir  15683  lssvnegcl  15713  islss3  15716  pwslmod  15727  lmodvsinv  15793  islmhm2  15795  lbsind2  15834  lspsneq  15875  lspexch  15882  asclghm  16078  ip2subdi  16548  isphld  16558  ocvlss  16572  tlmtgp  17878  clmrng  18568  frlmup1  27250  frlmup2  27251  frlmup3  27252  frlmup4  27253  islindf5  27309  lmisfree  27312  lfl0  29255  lfladd  29256  lflsub  29257  lfl0f  29259  lfladdcl  29261  lfladdcom  29262  lfladdass  29263  lfladd0l  29264  lflnegcl  29265  lflnegl  29266  lflvscl  29267  lflvsdi1  29268  lflvsdi2  29269  lflvsass  29271  lfl0sc  29272  lflsc0N  29273  lfl1sc  29274  lkrlss  29285  eqlkr  29289  eqlkr3  29291  lkrlsp  29292  ldualvsass  29331  lduallmodlem  29342  ldualvsubcl  29346  ldualvsubval  29347  lkrin  29354  dochfl1  31666  lcfl7lem  31689  lclkrlem2m  31709  lclkrlem2o  31711  lclkrlem2p  31712  lcfrlem1  31732  lcfrlem2  31733  lcfrlem3  31734  lcfrlem29  31761  lcfrlem33  31765  lcdvsubval  31808  mapdpglem30  31892  baerlem3lem1  31897  baerlem5alem1  31898  baerlem5blem1  31899  baerlem5blem2  31902  hgmapval1  32086  hdmapinvlem3  32113  hdmapinvlem4  32114  hdmapglem5  32115  hgmapvvlem1  32116  hdmapglem7b  32121  hdmapglem7  32122
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-lmod 15629
  Copyright terms: Public domain W3C validator