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

Metamath Proof Explorer

Theorem cnfldnm

Description: The norm of the field of complex numbers. (Contributed by Mario Carneiro, 4-Oct-2015)

Ref Expression
Assertion cnfldnm ⊢ abs = norm ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 0cn ⊢ 0 ∈ ℂ
2 eqid ⊢ abs ∘ − = abs ∘ −
3 2 cnmetdval ⊢ x ∈ ℂ ∧ 0 ∈ ℂ → x abs ∘ − 0 = x − 0
4 1 3 mpan2 ⊢ x ∈ ℂ → x abs ∘ − 0 = x − 0
5 subid1 ⊢ x ∈ ℂ → x − 0 = x
6 5 fveq2d ⊢ x ∈ ℂ → x − 0 = x
7 4 6 eqtrd ⊢ x ∈ ℂ → x abs ∘ − 0 = x
8 7 mpteq2ia ⊢ x ∈ ℂ ⟼ x abs ∘ − 0 = x ∈ ℂ ⟼ x
9 eqid ⊢ norm ⁡ ℂ fld = norm ⁡ ℂ fld
10 cnfldbas ⊢ ℂ = Base ℂ fld
11 cnfld0 ⊢ 0 = 0 ℂ fld
12 cnfldds ⊢ abs ∘ − = dist ⁡ ℂ fld
13 9 10 11 12 nmfval ⊢ norm ⁡ ℂ fld = x ∈ ℂ ⟼ x abs ∘ − 0
14 absf ⊢ abs : ℂ ⟶ ℝ
15 14 a1i ⊢ ⊤ → abs : ℂ ⟶ ℝ
16 15 feqmptd ⊢ ⊤ → abs = x ∈ ℂ ⟼ x
17 16 mptru ⊢ abs = x ∈ ℂ ⟼ x
18 8 13 17 3eqtr4ri ⊢ abs = norm ⁡ ℂ fld