Theorem lmodgrp 18870

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.

Step	Hyp	Ref	Expression
1		eqid 2622	. . 3 |- ( Base ` W ) = ( Base ` W )
2		eqid 2622	. . 3 |- ( +g ` W ) = ( +g ` W )
3		eqid 2622	. . 3 |- ( .s ` W ) = ( .s ` W )
4		eqid 2622	. . 3 |- (Scalar ` W ) = (Scalar ` W )
5		eqid 2622	. . 3 |- ( Base ` (Scalar ` W ) ) = ( Base ` (Scalar ` W ) )
6		eqid 2622	. . 3 |- ( +g ` (Scalar ` W ) ) = ( +g ` (Scalar ` W ) )
7		eqid 2622	. . 3 |- ( .r ` (Scalar ` W ) ) = ( .r ` (Scalar ` W ) )
8		eqid 2622	. . 3 |- ( 1r ` (Scalar ` W ) ) = ( 1r ` (Scalar ` W ) )
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 18867	. 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 ) ) ) )
10	9	simp1bi 1076	1 |- ( W e. LMod -> W e. Grp )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   A.wral 2912   ` cfv 5888  (class class class)co 6650   Basecbs 15857   +g cplusg 15941   .rcmulr 15942  Scalarcsca 15944   .scvsca 15945   Grpcgrp 17422   1rcur 18501   Ringcrg 18547   LModclmod 18863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-lmod 18865

This theorem is referenced by:  lmodbn0  18873  lmodvacl  18877  lmodass  18878  lmodlcan  18879  lmod0vcl  18892  lmod0vlid  18893  lmod0vrid  18894  lmod0vid  18895  lmodvsmmulgdi  18898  lmodfopne  18901  lmodvnegcl  18904  lmodvnegid  18905  lmodvsubcl  18908  lmodcom  18909  lmodabl  18910  lmodvpncan  18916  lmodvnpcan  18917  lmodsubeq0  18922  lmodsubid  18923  lmodvsghm  18924  lmodprop2d  18925  lsssubg  18957  islss3  18959  lssacs  18967  prdslmodd  18969  lspsnneg  19006  lspsnsub  19007  lmodindp1  19014  lmodvsinv2  19037  islmhm2  19038  0lmhm  19040  idlmhm  19041  pwsdiaglmhm  19057  pwssplit3  19061  lspexch  19129  lspsolvlem  19142  mplind  19502  ip0l  19981  ipsubdir  19987  ipsubdi  19988  ip2eq  19998  lsmcss  20036  dsmmlss  20088  frlm0  20098  frlmsubgval  20108  frlmup1  20137  islindf4  20177  matgrp  20236  tlmtgp  21999  clmgrp  22868  ncvspi  22956  cphtchnm  23029  ipcau2  23033  tchcphlem1  23034  tchcph  23036  rrxnm  23179  rrxds  23181  pjthlem2  23209  lclkrlem2m  36808  mapdpglem14  36974  baerlem3lem1  36996  baerlem5amN  37005  baerlem5bmN  37006  baerlem5abmN  37007  mapdh6bN  37026  mapdh6cN  37027  hdmap1l6b  37101  hdmap1l6c  37102  hdmap1neglem1N  37117  hdmap11  37140  kercvrlsm  37653  pwssplit4  37659  pwslnmlem2  37663  mendring  37762  zlmodzxzsub  42138  lmodvsmdi  42163  lincvalsng  42205  lincvalsc0  42210  linc0scn0  42212  linc1  42214  lcoel0  42217  lindslinindimp2lem4  42250  snlindsntor  42260  lincresunit3  42270