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 ⊢ ( ( 𝑥 ∈ ℂ ∧ 0 ∈ ℂ ) → ( 𝑥 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑥 − 0 ) ) )
4 1 3 mpan2 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ( abs ∘ − ) 0 ) = ( abs ‘ ( 𝑥 − 0 ) ) )
5 subid1 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 − 0 ) = 𝑥 )
6 5 fveq2d ⊢ ( 𝑥 ∈ ℂ → ( abs ‘ ( 𝑥 − 0 ) ) = ( abs ‘ 𝑥 ) )
7 4 6 eqtrd ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ( abs ∘ − ) 0 ) = ( abs ‘ 𝑥 ) )
8 7 mpteq2ia ⊢ ( 𝑥 ∈ ℂ ↦ ( 𝑥 ( abs ∘ − ) 0 ) ) = ( 𝑥 ∈ ℂ ↦ ( abs ‘ 𝑥 ) )
9 eqid ⊢ ( norm ‘ ℂfld ) = ( norm ‘ ℂfld )
10 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
11 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
12 cnfldds ⊢ ( abs ∘ − ) = ( dist ‘ ℂfld )
13 9 10 11 12 nmfval ⊢ ( norm ‘ ℂfld ) = ( 𝑥 ∈ ℂ ↦ ( 𝑥 ( abs ∘ − ) 0 ) )
14 absf ⊢ abs : ℂ ⟶ ℝ
15 14 a1i ⊢ ( ⊤ → abs : ℂ ⟶ ℝ )
16 15 feqmptd ⊢ ( ⊤ → abs = ( 𝑥 ∈ ℂ ↦ ( abs ‘ 𝑥 ) ) )
17 16 mptru ⊢ abs = ( 𝑥 ∈ ℂ ↦ ( abs ‘ 𝑥 ) )
18 8 13 17 3eqtr4ri ⊢ abs = ( norm ‘ ℂfld )