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

Theorem lmodrng 15651
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 2296 . . 3  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2296 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
3 eqid 2296 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
4 lmodrng.1 . . 3  |-  F  =  (Scalar `  W )
5 eqid 2296 . . 3  |-  ( Base `  F )  =  (
Base `  F )
6 eqid 2296 . . 3  |-  ( +g  `  F )  =  ( +g  `  F )
7 eqid 2296 . . 3  |-  ( .r
`  F )  =  ( .r `  F
)
8 eqid 2296 . . 3  |-  ( 1r
`  F )  =  ( 1r `  F
)
91, 2, 3, 4, 5, 6, 7, 8islmod 15647 . 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 1632    e. wcel 1696   A.wral 2556   ` cfv 5271  (class class class)co 5874   Basecbs 13164   +g cplusg 13224   .rcmulr 13225  Scalarcsca 13227   .scvsca 13228   Grpcgrp 14378   Ringcrg 15353   1rcur 15355   LModclmod 15643
This theorem is referenced by:  lmodfgrp  15652  lmodmcl  15655  lmod0cl  15672  lmod1cl  15673  lmod0vs  15679  lmodvs0  15680  lmodvsnegOLD  15684  lmodvsneg  15685  lmodsubvs  15697  lmodsubdi  15698  lmodsubdir  15699  lssvnegcl  15729  islss3  15732  pwslmod  15743  lmodvsinv  15809  islmhm2  15811  lbsind2  15850  lspsneq  15891  lspexch  15898  asclghm  16094  ip2subdi  16564  isphld  16574  ocvlss  16588  tlmtgp  17894  clmrng  18584  frlmup1  27353  frlmup2  27354  frlmup3  27355  frlmup4  27356  islindf5  27412  lmisfree  27415  lfl0  29877  lfladd  29878  lflsub  29879  lfl0f  29881  lfladdcl  29883  lfladdcom  29884  lfladdass  29885  lfladd0l  29886  lflnegcl  29887  lflnegl  29888  lflvscl  29889  lflvsdi1  29890  lflvsdi2  29891  lflvsass  29893  lfl0sc  29894  lflsc0N  29895  lfl1sc  29896  lkrlss  29907  eqlkr  29911  eqlkr3  29913  lkrlsp  29914  ldualvsass  29953  lduallmodlem  29964  ldualvsubcl  29968  ldualvsubval  29969  lkrin  29976  dochfl1  32288  lcfl7lem  32311  lclkrlem2m  32331  lclkrlem2o  32333  lclkrlem2p  32334  lcfrlem1  32354  lcfrlem2  32355  lcfrlem3  32356  lcfrlem29  32383  lcfrlem33  32387  lcdvsubval  32430  mapdpglem30  32514  baerlem3lem1  32519  baerlem5alem1  32520  baerlem5blem1  32521  baerlem5blem2  32524  hgmapval1  32708  hdmapinvlem3  32735  hdmapinvlem4  32736  hdmapglem5  32737  hgmapvvlem1  32738  hdmapglem7b  32743  hdmapglem7  32744
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-nul 4165
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-lmod 15645
  Copyright terms: Public domain W3C validator