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

Theorem lmodgrp 16933
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 2438 . . 3  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2438 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
3 eqid 2438 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
4 eqid 2438 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
5 eqid 2438 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
6 eqid 2438 . . 3  |-  ( +g  `  (Scalar `  W )
)  =  ( +g  `  (Scalar `  W )
)
7 eqid 2438 . . 3  |-  ( .r
`  (Scalar `  W )
)  =  ( .r
`  (Scalar `  W )
)
8 eqid 2438 . . 3  |-  ( 1r
`  (Scalar `  W )
)  =  ( 1r
`  (Scalar `  W )
)
91, 2, 3, 4, 5, 6, 7, 8islmod 16930 . 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 1003 1  |-  ( W  e.  LMod  ->  W  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   A.wral 2710   ` cfv 5413  (class class class)co 6086   Basecbs 14166   +g cplusg 14230   .rcmulr 14231  Scalarcsca 14233   .scvsca 14234   Grpcgrp 15402   1rcur 16591   Ringcrg 16633   LModclmod 16926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-nul 4416
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2715  df-rex 2716  df-rab 2719  df-v 2969  df-sbc 3182  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-lmod 16928
This theorem is referenced by:  lmodbn0  16936  lmodvacl  16940  lmodass  16941  lmodlcan  16942  lmod0vcl  16955  lmod0vlid  16956  lmod0vrid  16957  lmod0vid  16958  lmodvnegcl  16964  lmodvnegid  16965  lmodvsubcl  16968  lmodcom  16969  lmodabl  16970  lmodvpncan  16976  lmodvnpcan  16977  lmodsubeq0  16982  lmodsubid  16983  lmodvsghm  16984  lmodprop2d  16985  lsssubg  17015  islss3  17017  lssacs  17025  prdslmodd  17027  lspsnneg  17064  lspsnsub  17065  lmodindp1  17072  lmodvsinv2  17095  islmhm2  17096  0lmhm  17098  idlmhm  17099  pwsdiaglmhm  17115  pwssplit3  17119  lspexch  17187  lspsolvlem  17200  mplind  17559  ip0l  18040  ipsubdir  18046  ipsubdi  18047  ip2eq  18057  lsmcss  18092  dsmmlss  18144  frlm0  18154  frlmsubgval  18167  frlmup1  18201  islindf4  18242  matrng  18305  tlmtgp  19745  clmgrp  20615  cphtchnm  20720  ipcau2  20724  tchcphlem1  20725  tchcph  20727  rrxnm  20870  rrxds  20872  pjthlem2  20900  kercvrlsm  29389  pwssplit4  29395  pwslnmlem2  29399  mendrng  29502  zlmodzxzsub  30708  lmodvsmdi  30751  lmodvsmmulgdi  30752  lincvalsng  30839  lincvalsc0  30844  linc0scn0  30846  linc1  30848  lcoel0  30851  lindslinindimp2lem4  30884  snlindsntor  30894  lincresunit3  30904  lclkrlem2m  35004  mapdpglem14  35170  baerlem3lem1  35192  baerlem5amN  35201  baerlem5bmN  35202  baerlem5abmN  35203  mapdh6bN  35222  mapdh6cN  35223  hdmap1l6b  35297  hdmap1l6c  35298  hdmap1neglem1N  35313  hdmap11  35336
  Copyright terms: Public domain W3C validator