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

Proof

Step	Hyp	Ref	Expression
1		cnex	$⊢ ℂ \in V$
2		ax-addf	$⊢ + : ℂ \times ℂ ⟶ ℂ$
3		addass	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \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	$⊢ (x \in ℂ \land - x \in ℂ) \to x + (- x) = - x + x$
8	6 7	mpdan	$⊢ x \in ℂ \to x + (- x) = - x + x$
9		negid	$⊢ x \in ℂ \to x + (- x) = 0$
10	8 9	eqtr3d	$⊢ x \in ℂ \to - x + x = 0$
11	1 2 3 4 5 6 10	isgrpoi	$⊢ + \in GrpOp$
12	2	fdmi	$⊢ dom + = ℂ \times ℂ$
13		addcom	$⊢ (x \in ℂ \land y \in ℂ) \to x + y = y + x$
14	11 12 13	isabloi	$⊢ + \in AbelOp$