This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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