Metamath Proof Explorer

Theorem cnaddcom

Description: Recover the commutative law of addition for complex numbers from the Abelian group structure. (Contributed by NM, 17-Mar-2013) (Proof modification is discouraged.)

Ref Expression
Assertion cnaddcom 
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } = { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. }
2 1 cnaddabl 
 |-  { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } e. Abel
3 cnex 
 |-  CC e. _V
4 1 grpbase 
 |-  ( CC e. _V -> CC = ( Base ` { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } ) )
5 3 4 ax-mp 
 |-  CC = ( Base ` { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } )
6 addex 
 |-  + e. _V
7 1 grpplusg 
 |-  ( + e. _V -> + = ( +g ` { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } ) )
8 6 7 ax-mp 
 |-  + = ( +g ` { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } )
9 5 8 ablcom 
 |-  ( ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } e. Abel /\ A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )
10 2 9 mp3an1 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) = ( B + A ) )