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

Metamath Proof Explorer

Theorem cnfld0

Description: Zero is the zero element of the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Assertion cnfld0 ⊢ 0 = 0 ℂ fld

Proof

Step Hyp Ref Expression
1 00id ⊢ 0 + 0 = 0
2 cnring ⊢ ℂ fld ∈ Ring
3 ringgrp ⊢ ℂ fld ∈ Ring → ℂ fld ∈ Grp
4 2 3 ax-mp ⊢ ℂ fld ∈ Grp
5 0cn ⊢ 0 ∈ ℂ
6 cnfldbas ⊢ ℂ = Base ℂ fld
7 cnfldadd ⊢ + = + ℂ fld
8 eqid ⊢ 0 ℂ fld = 0 ℂ fld
9 6 7 8 grpid ⊢ ℂ fld ∈ Grp ∧ 0 ∈ ℂ → 0 + 0 = 0 ↔ 0 ℂ fld = 0
10 4 5 9 mp2an ⊢ 0 + 0 = 0 ↔ 0 ℂ fld = 0
11 1 10 mpbi ⊢ 0 ℂ fld = 0
12 11 eqcomi ⊢ 0 = 0 ℂ fld