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

Theorem lmodgrp 15650
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 2296 . . 3  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2296 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
3 eqid 2296 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
4 eqid 2296 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
5 eqid 2296 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
6 eqid 2296 . . 3  |-  ( +g  `  (Scalar `  W )
)  =  ( +g  `  (Scalar `  W )
)
7 eqid 2296 . . 3  |-  ( .r
`  (Scalar `  W )
)  =  ( .r
`  (Scalar `  W )
)
8 eqid 2296 . . 3  |-  ( 1r
`  (Scalar `  W )
)  =  ( 1r
`  (Scalar `  W )
)
91, 2, 3, 4, 5, 6, 7, 8islmod 15647 . 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 970 1  |-  ( W  e.  LMod  ->  W  e. 
Grp )
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:  lmodbn0  15653  lmodvacl  15657  lmodass  15658  lmodlcan  15659  lmod0vcl  15675  lmod0vlid  15676  lmod0vrid  15677  lmod0vid  15678  lmodvnegcl  15681  lmodvnegid  15682  lmodvsubcl  15686  lmodcom  15687  lmodabl  15688  lmodvpncan  15694  lmodvnpcan  15695  lmodsubeq0  15700  lmodsubid  15701  lmodvsghm  15702  lmodprop2d  15703  lsssubg  15730  islss3  15732  lssacs  15740  prdslmodd  15742  lspsnneg  15779  lspsnsub  15780  lmodindp1  15787  lmodvsinv2  15810  islmhm2  15811  0lmhm  15813  idlmhm  15814  pwsdiaglmhm  15830  lspexch  15898  lspsolvlem  15911  mplind  16259  ip0l  16556  ipsubdir  16562  ipsubdi  16563  ip2eq  16573  lsmcss  16608  tlmtgp  17894  clmgrp  18582  cphtchnm  18677  ipcau2  18680  tchcphlem1  18681  tchcph  18683  pjthlem2  18818  kercvrlsm  27284  pwssplit3  27293  pwssplit4  27294  pwslnmlem2  27298  dsmmlss  27313  frlm0  27325  frlmup1  27353  islindf4  27411  matrng  27583  mendrng  27603  lclkrlem2m  32331  mapdpglem14  32497  baerlem3lem1  32519  baerlem5amN  32528  baerlem5bmN  32529  baerlem5abmN  32530  mapdh6bN  32549  mapdh6cN  32550  hdmap1l6b  32624  hdmap1l6c  32625  hdmap1neglem1N  32640  hdmap11  32663
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