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

Theorem lmodgrp 17077
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 17074 . 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 1370    e. wcel 1758   A.wral 2798   ` cfv 5525  (class class class)co 6199   Basecbs 14291   +g cplusg 14356   .rcmulr 14357  Scalarcsca 14359   .scvsca 14360   Grpcgrp 15528   1rcur 16724   Ringcrg 16767   LModclmod 17070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-nul 4528
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-iota 5488  df-fv 5533  df-ov 6202  df-lmod 17072
This theorem is referenced by:  lmodbn0  17080  lmodvacl  17084  lmodass  17085  lmodlcan  17086  lmod0vcl  17099  lmod0vlid  17100  lmod0vrid  17101  lmod0vid  17102  lmodvnegcl  17108  lmodvnegid  17109  lmodvsubcl  17112  lmodcom  17113  lmodabl  17114  lmodvpncan  17120  lmodvnpcan  17121  lmodsubeq0  17126  lmodsubid  17127  lmodvsghm  17128  lmodprop2d  17129  lsssubg  17160  islss3  17162  lssacs  17170  prdslmodd  17172  lspsnneg  17209  lspsnsub  17210  lmodindp1  17217  lmodvsinv2  17240  islmhm2  17241  0lmhm  17243  idlmhm  17244  pwsdiaglmhm  17260  pwssplit3  17264  lspexch  17332  lspsolvlem  17345  mplind  17707  ip0l  18189  ipsubdir  18195  ipsubdi  18196  ip2eq  18206  lsmcss  18241  dsmmlss  18293  frlm0  18303  frlmsubgval  18316  frlmup1  18350  islindf4  18391  matrng  18455  tlmtgp  19901  clmgrp  20771  cphtchnm  20876  ipcau2  20880  tchcphlem1  20881  tchcph  20883  rrxnm  21026  rrxds  21028  pjthlem2  21056  kercvrlsm  29583  pwssplit4  29589  pwslnmlem2  29593  mendrng  29696  zlmodzxzsub  30904  lmodvsmdi  30966  lmodvsmmulgdi  30967  lincvalsng  31068  lincvalsc0  31073  linc0scn0  31075  linc1  31077  lcoel0  31080  lindslinindimp2lem4  31113  snlindsntor  31123  lincresunit3  31133  lclkrlem2m  35487  mapdpglem14  35653  baerlem3lem1  35675  baerlem5amN  35684  baerlem5bmN  35685  baerlem5abmN  35686  mapdh6bN  35705  mapdh6cN  35706  hdmap1l6b  35780  hdmap1l6c  35781  hdmap1neglem1N  35796  hdmap11  35819
  Copyright terms: Public domain W3C validator