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

Theorem lmodgrp 15912
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 2404 . . 3  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2404 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
3 eqid 2404 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
4 eqid 2404 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
5 eqid 2404 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
6 eqid 2404 . . 3  |-  ( +g  `  (Scalar `  W )
)  =  ( +g  `  (Scalar `  W )
)
7 eqid 2404 . . 3  |-  ( .r
`  (Scalar `  W )
)  =  ( .r
`  (Scalar `  W )
)
8 eqid 2404 . . 3  |-  ( 1r
`  (Scalar `  W )
)  =  ( 1r
`  (Scalar `  W )
)
91, 2, 3, 4, 5, 6, 7, 8islmod 15909 . 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 1649    e. wcel 1721   A.wral 2666   ` cfv 5413  (class class class)co 6040   Basecbs 13424   +g cplusg 13484   .rcmulr 13485  Scalarcsca 13487   .scvsca 13488   Grpcgrp 14640   Ringcrg 15615   1rcur 15617   LModclmod 15905
This theorem is referenced by:  lmodbn0  15915  lmodvacl  15919  lmodass  15920  lmodlcan  15921  lmod0vcl  15934  lmod0vlid  15935  lmod0vrid  15936  lmod0vid  15937  lmodvnegcl  15940  lmodvnegid  15941  lmodvsubcl  15944  lmodcom  15945  lmodabl  15946  lmodvpncan  15952  lmodvnpcan  15953  lmodsubeq0  15958  lmodsubid  15959  lmodvsghm  15960  lmodprop2d  15961  lsssubg  15988  islss3  15990  lssacs  15998  prdslmodd  16000  lspsnneg  16037  lspsnsub  16038  lmodindp1  16045  lmodvsinv2  16068  islmhm2  16069  0lmhm  16071  idlmhm  16072  pwsdiaglmhm  16088  lspexch  16156  lspsolvlem  16169  mplind  16517  ip0l  16822  ipsubdir  16828  ipsubdi  16829  ip2eq  16839  lsmcss  16874  tlmtgp  18178  clmgrp  19046  cphtchnm  19141  ipcau2  19144  tchcphlem1  19145  tchcph  19147  pjthlem2  19292  kercvrlsm  27049  pwssplit3  27058  pwssplit4  27059  pwslnmlem2  27063  dsmmlss  27078  frlm0  27090  frlmup1  27118  islindf4  27176  matrng  27348  mendrng  27368  lclkrlem2m  32002  mapdpglem14  32168  baerlem3lem1  32190  baerlem5amN  32199  baerlem5bmN  32200  baerlem5abmN  32201  mapdh6bN  32220  mapdh6cN  32221  hdmap1l6b  32295  hdmap1l6c  32296  hdmap1neglem1N  32311  hdmap11  32334
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-nul 4298
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-sbc 3122  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-lmod 15907
  Copyright terms: Public domain W3C validator