Metamath Proof Explorer


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 )