Metamath Proof Explorer

Theorem cnaddabloOLD

Description: Obsolete version of cnaddabl . Complex number addition is an Abelian group operation. (Contributed by NM, 5-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Assertion cnaddabloOLD 
|- + e. AbelOp

Proof

Step Hyp Ref Expression
1 cnex 
 |-  CC e. _V
2 ax-addf 
 |-  + : ( CC X. CC ) --> CC
3 addass 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) + z ) = ( x + ( y + z ) ) )
4 0cn 
 |-  0 e. CC
5 addid2 
 |-  ( x e. CC -> ( 0 + x ) = x )
6 negcl 
 |-  ( x e. CC -> -u x e. CC )
7 addcom 
 |-  ( ( x e. CC /\ -u x e. CC ) -> ( x + -u x ) = ( -u x + x ) )
8 6 7 mpdan 
 |-  ( x e. CC -> ( x + -u x ) = ( -u x + x ) )
9 negid 
 |-  ( x e. CC -> ( x + -u x ) = 0 )
10 8 9 eqtr3d 
 |-  ( x e. CC -> ( -u x + x ) = 0 )
11 1 2 3 4 5 6 10 isgrpoi 
 |-  + e. GrpOp
12 2 fdmi 
 |-  dom + = ( CC X. CC )
13 addcom 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) = ( y + x ) )
14 11 12 13 isabloi 
 |-  + e. AbelOp