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

Theorem lmodgrp 16879
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 2433 . . 3  |-  ( Base `  W )  =  (
Base `  W )
2 eqid 2433 . . 3  |-  ( +g  `  W )  =  ( +g  `  W )
3 eqid 2433 . . 3  |-  ( .s
`  W )  =  ( .s `  W
)
4 eqid 2433 . . 3  |-  (Scalar `  W )  =  (Scalar `  W )
5 eqid 2433 . . 3  |-  ( Base `  (Scalar `  W )
)  =  ( Base `  (Scalar `  W )
)
6 eqid 2433 . . 3  |-  ( +g  `  (Scalar `  W )
)  =  ( +g  `  (Scalar `  W )
)
7 eqid 2433 . . 3  |-  ( .r
`  (Scalar `  W )
)  =  ( .r
`  (Scalar `  W )
)
8 eqid 2433 . . 3  |-  ( 1r
`  (Scalar `  W )
)  =  ( 1r
`  (Scalar `  W )
)
91, 2, 3, 4, 5, 6, 7, 8islmod 16876 . 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 996 1  |-  ( W  e.  LMod  ->  W  e. 
Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958    = wceq 1362    e. wcel 1755   A.wral 2705   ` cfv 5406  (class class class)co 6080   Basecbs 14157   +g cplusg 14221   .rcmulr 14222  Scalarcsca 14224   .scvsca 14225   Grpcgrp 15393   Ringcrg 16577   1rcur 16579   LModclmod 16872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-nul 4409
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-lmod 16874
This theorem is referenced by:  lmodbn0  16882  lmodvacl  16886  lmodass  16887  lmodlcan  16888  lmod0vcl  16901  lmod0vlid  16902  lmod0vrid  16903  lmod0vid  16904  lmodvnegcl  16910  lmodvnegid  16911  lmodvsubcl  16914  lmodcom  16915  lmodabl  16916  lmodvpncan  16922  lmodvnpcan  16923  lmodsubeq0  16928  lmodsubid  16929  lmodvsghm  16930  lmodprop2d  16931  lsssubg  16960  islss3  16962  lssacs  16970  prdslmodd  16972  lspsnneg  17009  lspsnsub  17010  lmodindp1  17017  lmodvsinv2  17040  islmhm2  17041  0lmhm  17043  idlmhm  17044  pwsdiaglmhm  17060  pwssplit3  17064  lspexch  17132  lspsolvlem  17145  mplind  17516  ip0l  17907  ipsubdir  17913  ipsubdi  17914  ip2eq  17924  lsmcss  17959  dsmmlss  18011  frlm0  18021  frlmsubgval  18034  frlmup1  18068  islindf4  18109  matrng  18172  tlmtgp  19612  clmgrp  20482  cphtchnm  20587  ipcau2  20591  tchcphlem1  20592  tchcph  20594  rrxnm  20737  rrxds  20739  pjthlem2  20767  kercvrlsm  29281  pwssplit4  29287  pwslnmlem2  29291  mendrng  29394  zlmodzxzsub  30592  lincvalsng  30680  lincvalsc0  30685  linc0scn0  30687  linc1  30689  lcoel0  30692  lindslinindimp2lem4  30725  snlindsntor  30735  lincresunit3  30745  lclkrlem2m  34758  mapdpglem14  34924  baerlem3lem1  34946  baerlem5amN  34955  baerlem5bmN  34956  baerlem5abmN  34957  mapdh6bN  34976  mapdh6cN  34977  hdmap1l6b  35051  hdmap1l6c  35052  hdmap1neglem1N  35067  hdmap11  35090
  Copyright terms: Public domain W3C validator