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 ) |
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 ) |