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

Metamath Proof Explorer

Theorem cnaddabl

Description: The complex numbers are an Abelian group under addition. This version of cnaddablx hides the explicit structure indices i.e. is "scaffold-independent". Note that the proof also does not reference explicit structure indices. The actual structure is dependent on how Base and +g is defined. This theorem should not be referenced in any proof. For the group/ring properties of the complex numbers, see cnring . (Contributed by NM, 20-Oct-2012) (New usage is discouraged.)

Ref Expression
Hypothesis cnaddabl.g ⊢ G = Base ndx ℂ + ndx +
Assertion cnaddabl ⊢ G ∈ Abel

Proof

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