Theorem vcablo

Description: Vector addition is an Abelian group operation. (Contributed by NM, 3-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	vcabl.1	|- G = ( 1st ` W )
Assertion	vcablo	|- ( W e. CVecOLD -> G e. AbelOp )

Proof

Step	Hyp	Ref	Expression
1		vcabl.1	|- G = ( 1st ` W )
2		eqid	|- ( 2nd ` W ) = ( 2nd ` W )
3		eqid	|- ran G = ran G
4	1 2 3	vciOLD	|- ( W e. CVecOLD -> ( G e. AbelOp /\ ( 2nd ` W ) : ( CC X. ran G ) --> ran G /\ A. x e. ran G ( ( 1 ( 2nd ` W ) x ) = x /\ A. y e. CC ( A. z e. ran G ( y ( 2nd ` W ) ( x G z ) ) = ( ( y ( 2nd ` W ) x ) G ( y ( 2nd ` W ) z ) ) /\ A. z e. CC ( ( ( y + z ) ( 2nd ` W ) x ) = ( ( y ( 2nd ` W ) x ) G ( z ( 2nd ` W ) x ) ) /\ ( ( y x. z ) ( 2nd ` W ) x ) = ( y ( 2nd ` W ) ( z ( 2nd ` W ) x ) ) ) ) ) ) )
5	4	simp1d	|- ( W e. CVecOLD -> G e. AbelOp )