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

Theorem lmodgrp 17714
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 2454 . . 3  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2454 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
3 eqid 2454 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
4 eqid 2454 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
5 eqid 2454 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
6 eqid 2454 . . 3  |-  ( +g  `  (Scalar `  W )
)  =  ( +g  `  (Scalar `  W )
)
7 eqid 2454 . . 3  |-  ( .r
`  (Scalar `  W )
)  =  ( .r
`  (Scalar `  W )
)
8 eqid 2454 . . 3  |-  ( 1r
`  (Scalar `  W )
)  =  ( 1r
`  (Scalar `  W )
)
91, 2, 3, 4, 5, 6, 7, 8islmod 17711 . 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 1009 1  |-  ( W  e.  LMod  ->  W  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971    = wceq 1398    e. wcel 1823   A.wral 2804   ` cfv 5570  (class class class)co 6270   Basecbs 14716   +g cplusg 14784   .rcmulr 14785  Scalarcsca 14787   .scvsca 14788   Grpcgrp 16252   1rcur 17348   Ringcrg 17393   LModclmod 17707
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273  df-lmod 17709
This theorem is referenced by:  lmodbn0  17717  lmodvacl  17721  lmodass  17722  lmodlcan  17723  lmod0vcl  17736  lmod0vlid  17737  lmod0vrid  17738  lmod0vid  17739  lmodvsmmulgdi  17742  lmodvnegcl  17746  lmodvnegid  17747  lmodvsubcl  17750  lmodcom  17751  lmodabl  17752  lmodvpncan  17758  lmodvnpcan  17759  lmodsubeq0  17764  lmodsubid  17765  lmodvsghm  17766  lmodprop2d  17767  lsssubg  17798  islss3  17800  lssacs  17808  prdslmodd  17810  lspsnneg  17847  lspsnsub  17848  lmodindp1  17855  lmodvsinv2  17878  islmhm2  17879  0lmhm  17881  idlmhm  17882  pwsdiaglmhm  17898  pwssplit3  17902  lspexch  17970  lspsolvlem  17983  mplind  18362  ip0l  18844  ipsubdir  18850  ipsubdi  18851  ip2eq  18861  lsmcss  18896  dsmmlss  18948  frlm0  18958  frlmsubgval  18969  frlmup1  19000  islindf4  19040  matgrp  19099  tlmtgp  20864  clmgrp  21734  cphtchnm  21839  ipcau2  21843  tchcphlem1  21844  tchcph  21846  rrxnm  21989  rrxds  21991  pjthlem2  22019  kercvrlsm  31268  pwssplit4  31274  pwslnmlem2  31278  mendring  31382  zlmodzxzsub  33203  lmodvsmdi  33229  lincvalsng  33271  lincvalsc0  33276  linc0scn0  33278  linc1  33280  lcoel0  33283  lindslinindimp2lem4  33316  snlindsntor  33326  lincresunit3  33336  lclkrlem2m  37643  mapdpglem14  37809  baerlem3lem1  37831  baerlem5amN  37840  baerlem5bmN  37841  baerlem5abmN  37842  mapdh6bN  37861  mapdh6cN  37862  hdmap1l6b  37936  hdmap1l6c  37937  hdmap1neglem1N  37952  hdmap11  37975
  Copyright terms: Public domain W3C validator