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

Metamath Proof Explorer

Theorem cnaddablx

Description: The complex numbers are an Abelian group under addition. This version of cnaddabl shows the explicit structure "scaffold" we chose for the definition for Abelian groups. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use cnaddabl instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012)

Ref Expression
Hypothesis cnaddablx.g ⊢ G = 1 ℂ 2 +
Assertion cnaddablx ⊢ G ∈ Abel

Proof

Step Hyp Ref Expression
1 cnaddablx.g ⊢ G = 1 ℂ 2 +
2 cnex ⊢ ℂ ∈ V
3 addex ⊢ + ∈ V
4 addcl ⊢ x ∈ ℂ ∧ y ∈ ℂ → x + y ∈ ℂ
5 addass ⊢ x ∈ ℂ ∧ y ∈ ℂ ∧ z ∈ ℂ → x + y + z = x + y + z
6 0cn ⊢ 0 ∈ ℂ
7 addlid ⊢ x ∈ ℂ → 0 + x = x
8 negcl ⊢ x ∈ ℂ → − x ∈ ℂ
9 addcom ⊢ x ∈ ℂ ∧ − x ∈ ℂ → x + − x = - x + x
10 8 9 mpdan ⊢ x ∈ ℂ → x + − x = - x + x
11 negid ⊢ x ∈ ℂ → x + − x = 0
12 10 11 eqtr3d ⊢ x ∈ ℂ → - x + x = 0
13 2 3 1 4 5 6 7 8 12 isgrpix ⊢ G ∈ Grp
14 2 3 1 grpbasex ⊢ ℂ = Base G
15 2 3 1 grpplusgx ⊢ + = + G
16 addcom ⊢ x ∈ ℂ ∧ y ∈ ℂ → x + y = y + x
17 13 14 15 16 isabli ⊢ G ∈ Abel