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	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B=B+A$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}$$
2	1	cnaddabl	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}\in \mathrm{Abel}$$
3		cnex	$$⊢ℂ\in \mathrm{V}$$
4	1	grpbase	$$⊢ℂ\in \mathrm{V}\to ℂ={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}}$$
5	3 4	ax-mp	$$⊢ℂ={\mathrm{Base}}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}}$$
6		addex	$$⊢+\in \mathrm{V}$$
7	1	grpplusg	$$⊢+\in \mathrm{V}\to +={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}}$$
8	6 7	ax-mp	$$⊢+={+}_{\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}}$$
9	5 8	ablcom	$$⊢\left(\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}\in \mathrm{Abel}\wedge A\in ℂ\wedge B\in ℂ\right)\to A+B=B+A$$
10	2 9	mp3an1	$$⊢\left(A\in ℂ\wedge B\in ℂ\right)\to A+B=B+A$$