Theorem lmodabl

Description: A left module is an abelian group (of vectors, under addition). (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 25-Jun-2014)

	Ref	Expression
Assertion	lmodabl	|- ( W e. LMod -> W e. Abel )

Proof

Step	Hyp	Ref	Expression
1		eqidd	|- ( W e. LMod -> ( Base ` W ) = ( Base ` W ) )
2		eqidd	|- ( W e. LMod -> ( +g ` W ) = ( +g ` W ) )
3		lmodgrp	|- ( W e. LMod -> W e. Grp )
4		eqid	|- ( Base ` W ) = ( Base ` W )
5		eqid	|- ( +g ` W ) = ( +g ` W )
6	4 5	lmodcom	|- ( ( W e. LMod /\ x e. ( Base ` W ) /\ y e. ( Base ` W ) ) -> ( x ( +g ` W ) y ) = ( y ( +g ` W ) x ) )
7	1 2 3 6	isabld	|- ( W e. LMod -> W e. Abel )