# 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 )
{"found_math": false, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 0, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0, "katex": 0, "math-container": 0, "wp-katex-eq": 0, "align": 0, "equation": 0, "x-ck12": 0, "texerror": 0}