Metamath Proof Explorer

Theorem lmodgrp

Description: A left module is a group. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 25-Jun-2014)

Ref Expression
Assertion lmodgrp 
|- ( W e. LMod -> W e. Grp )

Proof

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