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

Metamath Proof Explorer

Theorem cnmetdval

Description: Value of the distance function of the metric space of complex numbers. (Contributed by NM, 9-Dec-2006) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Hypothesis cnmetdval.1 ⊢ 𝐷 = ( abs ∘ − )
Assertion cnmetdval ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐷 𝐵 ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 cnmetdval.1 ⊢ 𝐷 = ( abs ∘ − )
2 subf ⊢ − : ( ℂ × ℂ ) ⟶ ℂ
3 opelxpi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ℂ × ℂ ) )
4 fvco3 ⊢ ( ( − : ( ℂ × ℂ ) ⟶ ℂ ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ℂ × ℂ ) ) → ( ( abs ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( abs ‘ ( − ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
5 2 3 4 sylancr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( abs ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( abs ‘ ( − ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
6 df-ov ⊢ ( 𝐴 𝐷 𝐵 ) = ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
7 1 fveq1i ⊢ ( 𝐷 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( abs ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
8 6 7 eqtri ⊢ ( 𝐴 𝐷 𝐵 ) = ( ( abs ∘ − ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
9 df-ov ⊢ ( 𝐴 − 𝐵 ) = ( − ‘ ⟨ 𝐴 , 𝐵 ⟩ )
10 9 fveq2i ⊢ ( abs ‘ ( 𝐴 − 𝐵 ) ) = ( abs ‘ ( − ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
11 5 8 10 3eqtr4g ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 𝐷 𝐵 ) = ( abs ‘ ( 𝐴 − 𝐵 ) ) )