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	⊢ + ∈ AbelOp

Proof

Step	Hyp	Ref	Expression
1		cnex	⊢ ℂ ∈ V
2		ax-addf	⊢ + : ( ℂ × ℂ ) ⟶ ℂ
3		addass	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
4		0cn	⊢ 0 ∈ ℂ
5		addlid	⊢ ( 𝑥 ∈ ℂ → ( 0 + 𝑥 ) = 𝑥 )
6		negcl	⊢ ( 𝑥 ∈ ℂ → - 𝑥 ∈ ℂ )
7		addcom	⊢ ( ( 𝑥 ∈ ℂ ∧ - 𝑥 ∈ ℂ ) → ( 𝑥 + - 𝑥 ) = ( - 𝑥 + 𝑥 ) )
8	6 7	mpdan	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 + - 𝑥 ) = ( - 𝑥 + 𝑥 ) )
9		negid	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 + - 𝑥 ) = 0 )
10	8 9	eqtr3d	⊢ ( 𝑥 ∈ ℂ → ( - 𝑥 + 𝑥 ) = 0 )
11	1 2 3 4 5 6 10	isgrpoi	⊢ + ∈ GrpOp
12	2	fdmi	⊢ dom + = ( ℂ × ℂ )
13		addcom	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
14	11 12 13	isabloi	⊢ + ∈ AbelOp