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

Theorem lmodrng 15958
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 2436 . . 3  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2436 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
3 eqid 2436 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
4 lmodrng.1 . . 3  |-  F  =  (Scalar `  W )
5 eqid 2436 . . 3  |-  ( Base `  F )  =  (
Base `  F )
6 eqid 2436 . . 3  |-  ( +g  `  F )  =  ( +g  `  F )
7 eqid 2436 . . 3  |-  ( .r
`  F )  =  ( .r `  F
)
8 eqid 2436 . . 3  |-  ( 1r
`  F )  =  ( 1r `  F
)
91, 2, 3, 4, 5, 6, 7, 8islmod 15954 . 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 973 1  |-  ( W  e.  LMod  ->  F  e. 
Ring )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936    = wceq 1652    e. wcel 1725   A.wral 2705   ` cfv 5454  (class class class)co 6081   Basecbs 13469   +g cplusg 13529   .rcmulr 13530  Scalarcsca 13532   .scvsca 13533   Grpcgrp 14685   Ringcrg 15660   1rcur 15662   LModclmod 15950
This theorem is referenced by:  lmodfgrp  15959  lmodmcl  15962  lmod0cl  15976  lmod1cl  15977  lmod0vs  15983  lmodvs0  15984  lmodvsneg  15988  lmodsubvs  16000  lmodsubdi  16001  lmodsubdir  16002  lssvnegcl  16032  islss3  16035  pwslmod  16046  lmodvsinv  16112  islmhm2  16114  lbsind2  16153  lspsneq  16194  lspexch  16201  asclghm  16397  ip2subdi  16875  isphld  16885  ocvlss  16899  tlmtgp  18225  clmrng  19095  frlmup1  27227  frlmup2  27228  frlmup3  27229  frlmup4  27230  islindf5  27286  lmisfree  27289  lfl0  29863  lfladd  29864  lflsub  29865  lfl0f  29867  lfladdcl  29869  lfladdcom  29870  lfladdass  29871  lfladd0l  29872  lflnegcl  29873  lflnegl  29874  lflvscl  29875  lflvsdi1  29876  lflvsdi2  29877  lflvsass  29879  lfl0sc  29880  lflsc0N  29881  lfl1sc  29882  lkrlss  29893  eqlkr  29897  eqlkr3  29899  lkrlsp  29900  ldualvsass  29939  lduallmodlem  29950  ldualvsubcl  29954  ldualvsubval  29955  lkrin  29962  dochfl1  32274  lcfl7lem  32297  lclkrlem2m  32317  lclkrlem2o  32319  lclkrlem2p  32320  lcfrlem1  32340  lcfrlem2  32341  lcfrlem3  32342  lcfrlem29  32369  lcfrlem33  32373  lcdvsubval  32416  mapdpglem30  32500  baerlem3lem1  32505  baerlem5alem1  32506  baerlem5blem1  32507  baerlem5blem2  32510  hgmapval1  32694  hdmapinvlem3  32721  hdmapinvlem4  32722  hdmapglem5  32723  hgmapvvlem1  32724  hdmapglem7b  32729  hdmapglem7  32730
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-nul 4338
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-sbc 3162  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462  df-ov 6084  df-lmod 15952
  Copyright terms: Public domain W3C validator