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	$$⊢+\in \mathrm{AbelOp}$$

Proof

Step	Hyp	Ref	Expression
1		cnex	$$⊢ℂ\in \mathrm{V}$$
2		ax-addf	$$⊢+:ℂ\times ℂ⟶ℂ$$
3		addass	$$⊢\left(x\in ℂ\wedge y\in ℂ\wedge z\in ℂ\right)\to x+y+z=x+y+z$$
4		0cn	$$⊢0\in ℂ$$
5		addlid	$$⊢x\in ℂ\to 0+x=x$$
6		negcl	$$⊢x\in ℂ\to -x\in ℂ$$
7		addcom	$$⊢\left(x\in ℂ\wedge -x\in ℂ\right)\to x+\left(-x\right)=-x+x$$
8	6 7	mpdan	$$⊢x\in ℂ\to x+\left(-x\right)=-x+x$$
9		negid	$$⊢x\in ℂ\to x+\left(-x\right)=0$$
10	8 9	eqtr3d	$$⊢x\in ℂ\to -x+x=0$$
11	1 2 3 4 5 6 10	isgrpoi	$$⊢+\in \mathrm{GrpOp}$$
12	2	fdmi	$$⊢\mathrm{dom}+=ℂ\times ℂ$$
13		addcom	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to x+y=y+x$$
14	11 12 13	isabloi	$$⊢+\in \mathrm{AbelOp}$$