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

Theorem lmodgrp 15634
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 2283 . . 3  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2283 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
3 eqid 2283 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
4 eqid 2283 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
5 eqid 2283 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
6 eqid 2283 . . 3  |-  ( +g  `  (Scalar `  W )
)  =  ( +g  `  (Scalar `  W )
)
7 eqid 2283 . . 3  |-  ( .r
`  (Scalar `  W )
)  =  ( .r
`  (Scalar `  W )
)
8 eqid 2283 . . 3  |-  ( 1r
`  (Scalar `  W )
)  =  ( 1r
`  (Scalar `  W )
)
91, 2, 3, 4, 5, 6, 7, 8islmod 15631 . 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 1623    e. wcel 1684   A.wral 2543   ` cfv 5255  (class class class)co 5858   Basecbs 13148   +g cplusg 13208   .rcmulr 13209  Scalarcsca 13211   .scvsca 13212   Grpcgrp 14362   Ringcrg 15337   1rcur 15339   LModclmod 15627
This theorem is referenced by:  lmodbn0  15637  lmodvacl  15641  lmodass  15642  lmodlcan  15643  lmod0vcl  15659  lmod0vlid  15660  lmod0vrid  15661  lmod0vid  15662  lmodvnegcl  15665  lmodvnegid  15666  lmodvsubcl  15670  lmodcom  15671  lmodabl  15672  lmodvpncan  15678  lmodvnpcan  15679  lmodsubeq0  15684  lmodsubid  15685  lmodvsghm  15686  lmodprop2d  15687  lsssubg  15714  islss3  15716  lssacs  15724  prdslmodd  15726  lspsnneg  15763  lspsnsub  15764  lmodindp1  15771  lmodvsinv2  15794  islmhm2  15795  0lmhm  15797  idlmhm  15798  pwsdiaglmhm  15814  lspexch  15882  lspsolvlem  15895  mplind  16243  ip0l  16540  ipsubdir  16546  ipsubdi  16547  ip2eq  16557  lsmcss  16592  tlmtgp  17878  clmgrp  18566  cphtchnm  18661  ipcau2  18664  tchcphlem1  18665  tchcph  18667  pjthlem2  18802  kercvrlsm  26593  pwssplit3  26602  pwssplit4  26603  pwslnmlem2  26607  dsmmlss  26622  frlm0  26634  frlmup1  26662  islindf4  26720  matrng  26892  mendrng  26912  lclkrlem2m  31082  mapdpglem14  31248  baerlem3lem1  31270  baerlem5amN  31279  baerlem5bmN  31280  baerlem5abmN  31281  mapdh6bN  31300  mapdh6cN  31301  hdmap1l6b  31375  hdmap1l6c  31376  hdmap1neglem1N  31391  hdmap11  31414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-nul 4149
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-lmod 15629
  Copyright terms: Public domain W3C validator