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

Theorem lmodgrp 15950
Description: A left module is a group. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 25-Jun-2014.)
Assertion
Ref Expression
lmodgrp  |-  ( W  e.  LMod  ->  W  e. 
Grp )

Proof of Theorem lmodgrp
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 eqid 2436 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
5 eqid 2436 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
6 eqid 2436 . . 3  |-  ( +g  `  (Scalar `  W )
)  =  ( +g  `  (Scalar `  W )
)
7 eqid 2436 . . 3  |-  ( .r
`  (Scalar `  W )
)  =  ( .r
`  (Scalar `  W )
)
8 eqid 2436 . . 3  |-  ( 1r
`  (Scalar `  W )
)  =  ( 1r
`  (Scalar `  W )
)
91, 2, 3, 4, 5, 6, 7, 8islmod 15947 . 2  |-  ( W  e.  LMod  <->  ( W  e. 
Grp  /\  (Scalar `  W
)  e.  Ring  /\  A. q  e.  ( Base `  (Scalar `  W )
) A. r  e.  ( Base `  (Scalar `  W ) ) 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  `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( ( q ( .s `  W
) w ) ( +g  `  W ) ( r ( .s
`  W ) w ) ) )  /\  ( ( ( q ( .r `  (Scalar `  W ) ) r ) ( .s `  W ) w )  =  ( q ( .s `  W ) ( r ( .s
`  W ) w ) )  /\  (
( 1r `  (Scalar `  W ) ) ( .s `  W ) w )  =  w ) ) ) )
109simp1bi 972 1  |-  ( W  e.  LMod  ->  W  e. 
Grp )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936    = wceq 1652    e. wcel 1725   A.wral 2698   ` cfv 5447  (class class class)co 6074   Basecbs 13462   +g cplusg 13522   .rcmulr 13523  Scalarcsca 13525   .scvsca 13526   Grpcgrp 14678   Ringcrg 15653   1rcur 15655   LModclmod 15943
This theorem is referenced by:  lmodbn0  15953  lmodvacl  15957  lmodass  15958  lmodlcan  15959  lmod0vcl  15972  lmod0vlid  15973  lmod0vrid  15974  lmod0vid  15975  lmodvnegcl  15978  lmodvnegid  15979  lmodvsubcl  15982  lmodcom  15983  lmodabl  15984  lmodvpncan  15990  lmodvnpcan  15991  lmodsubeq0  15996  lmodsubid  15997  lmodvsghm  15998  lmodprop2d  15999  lsssubg  16026  islss3  16028  lssacs  16036  prdslmodd  16038  lspsnneg  16075  lspsnsub  16076  lmodindp1  16083  lmodvsinv2  16106  islmhm2  16107  0lmhm  16109  idlmhm  16110  pwsdiaglmhm  16126  lspexch  16194  lspsolvlem  16207  mplind  16555  ip0l  16860  ipsubdir  16866  ipsubdi  16867  ip2eq  16877  lsmcss  16912  tlmtgp  18218  clmgrp  19086  cphtchnm  19181  ipcau2  19184  tchcphlem1  19185  tchcph  19187  pjthlem2  19332  kercvrlsm  27150  pwssplit3  27159  pwssplit4  27160  pwslnmlem2  27164  dsmmlss  27179  frlm0  27191  frlmup1  27219  islindf4  27277  matrng  27449  mendrng  27469  lclkrlem2m  32255  mapdpglem14  32421  baerlem3lem1  32443  baerlem5amN  32452  baerlem5bmN  32453  baerlem5abmN  32454  mapdh6bN  32473  mapdh6cN  32474  hdmap1l6b  32548  hdmap1l6c  32549  hdmap1neglem1N  32564  hdmap11  32587
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 4331
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 2703  df-rex 2704  df-rab 2707  df-v 2951  df-sbc 3155  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-nul 3622  df-if 3733  df-sn 3813  df-pr 3814  df-op 3816  df-uni 4009  df-br 4206  df-iota 5411  df-fv 5455  df-ov 6077  df-lmod 15945
  Copyright terms: Public domain W3C validator