text: # 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 )
metadata: {"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}