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

Theorem lmodgrp 17393
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 2443 . . 3  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2443 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
3 eqid 2443 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
4 eqid 2443 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
5 eqid 2443 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
6 eqid 2443 . . 3  |-  ( +g  `  (Scalar `  W )
)  =  ( +g  `  (Scalar `  W )
)
7 eqid 2443 . . 3  |-  ( .r
`  (Scalar `  W )
)  =  ( .r
`  (Scalar `  W )
)
8 eqid 2443 . . 3  |-  ( 1r
`  (Scalar `  W )
)  =  ( 1r
`  (Scalar `  W )
)
91, 2, 3, 4, 5, 6, 7, 8islmod 17390 . 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 1012 1  |-  ( W  e.  LMod  ->  W  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974    = wceq 1383    e. wcel 1804   A.wral 2793   ` cfv 5578  (class class class)co 6281   Basecbs 14509   +g cplusg 14574   .rcmulr 14575  Scalarcsca 14577   .scvsca 14578   Grpcgrp 15927   1rcur 17027   Ringcrg 17072   LModclmod 17386
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-nul 4566
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-iota 5541  df-fv 5586  df-ov 6284  df-lmod 17388
This theorem is referenced by:  lmodbn0  17396  lmodvacl  17400  lmodass  17401  lmodlcan  17402  lmod0vcl  17415  lmod0vlid  17416  lmod0vrid  17417  lmod0vid  17418  lmodvsmmulgdi  17421  lmodvnegcl  17425  lmodvnegid  17426  lmodvsubcl  17429  lmodcom  17430  lmodabl  17431  lmodvpncan  17437  lmodvnpcan  17438  lmodsubeq0  17443  lmodsubid  17444  lmodvsghm  17445  lmodprop2d  17446  lsssubg  17477  islss3  17479  lssacs  17487  prdslmodd  17489  lspsnneg  17526  lspsnsub  17527  lmodindp1  17534  lmodvsinv2  17557  islmhm2  17558  0lmhm  17560  idlmhm  17561  pwsdiaglmhm  17577  pwssplit3  17581  lspexch  17649  lspsolvlem  17662  mplind  18041  ip0l  18544  ipsubdir  18550  ipsubdi  18551  ip2eq  18561  lsmcss  18596  dsmmlss  18648  frlm0  18658  frlmsubgval  18671  frlmup1  18705  islindf4  18746  matgrp  18805  tlmtgp  20571  clmgrp  21441  cphtchnm  21546  ipcau2  21550  tchcphlem1  21551  tchcph  21553  rrxnm  21696  rrxds  21698  pjthlem2  21726  kercvrlsm  31004  pwssplit4  31010  pwslnmlem2  31014  mendring  31117  zlmodzxzsub  32682  lmodvsmdi  32710  lincvalsng  32752  lincvalsc0  32757  linc0scn0  32759  linc1  32761  lcoel0  32764  lindslinindimp2lem4  32797  snlindsntor  32807  lincresunit3  32817  lclkrlem2m  36986  mapdpglem14  37152  baerlem3lem1  37174  baerlem5amN  37183  baerlem5bmN  37184  baerlem5abmN  37185  mapdh6bN  37204  mapdh6cN  37205  hdmap1l6b  37279  hdmap1l6c  37280  hdmap1neglem1N  37295  hdmap11  37318
  Copyright terms: Public domain W3C validator