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 ABA+B=B+A

Proof

Step Hyp Ref Expression
1 eqid Basendx+ndx+=Basendx+ndx+
2 1 cnaddabl Basendx+ndx+Abel
3 cnex V
4 1 grpbase V=BaseBasendx+ndx+
5 3 4 ax-mp =BaseBasendx+ndx+
6 addex +V
7 1 grpplusg +V+=+Basendx+ndx+
8 6 7 ax-mp +=+Basendx+ndx+
9 5 8 ablcom Basendx+ndx+AbelABA+B=B+A
10 2 9 mp3an1 ABA+B=B+A