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

Metamath Proof Explorer

Theorem cnaddid

Description: The group identity element of complex number addition is zero. See also cnfld0 . (Contributed by Steve Rodriguez, 3-Dec-2006) (Revised by AV, 26-Aug-2021) (New usage is discouraged.)

Ref Expression
Hypothesis cnaddabl.g ⊢ G = Base ndx ℂ + ndx +
Assertion cnaddid ⊢ 0 G = 0

Proof

Step Hyp Ref Expression
1 cnaddabl.g ⊢ G = Base ndx ℂ + ndx +
2 0cn ⊢ 0 ∈ ℂ
3 cnex ⊢ ℂ ∈ V
4 1 grpbase ⊢ ℂ ∈ V → ℂ = Base G
5 3 4 ax-mp ⊢ ℂ = Base G
6 eqid ⊢ 0 G = 0 G
7 addex ⊢ + ∈ V
8 1 grpplusg ⊢ + ∈ V → + = + G
9 7 8 ax-mp ⊢ + = + G
10 id ⊢ 0 ∈ ℂ → 0 ∈ ℂ
11 addlid ⊢ x ∈ ℂ → 0 + x = x
12 11 adantl ⊢ 0 ∈ ℂ ∧ x ∈ ℂ → 0 + x = x
13 addrid ⊢ x ∈ ℂ → x + 0 = x
14 13 adantl ⊢ 0 ∈ ℂ ∧ x ∈ ℂ → x + 0 = x
15 5 6 9 10 12 14 ismgmid2 ⊢ 0 ∈ ℂ → 0 = 0 G
16 2 15 ax-mp ⊢ 0 = 0 G
17 16 eqcomi ⊢ 0 G = 0