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 ⊢ D = abs ∘ −
Assertion cnmetdval ⊢ A ∈ ℂ ∧ B ∈ ℂ → A D B = A − B

Proof

Step Hyp Ref Expression
1 cnmetdval.1 ⊢ D = abs ∘ −
2 subf ⊢ − : ℂ × ℂ ⟶ ℂ
3 opelxpi ⊢ A ∈ ℂ ∧ B ∈ ℂ → A B ∈ ℂ × ℂ
4 fvco3 ⊢ − : ℂ × ℂ ⟶ ℂ ∧ A B ∈ ℂ × ℂ → abs ∘ − ⁡ A B = − ⁡ A B
5 2 3 4 sylancr ⊢ A ∈ ℂ ∧ B ∈ ℂ → abs ∘ − ⁡ A B = − ⁡ A B
6 df-ov ⊢ A D B = D ⁡ A B
7 1 fveq1i ⊢ D ⁡ A B = abs ∘ − ⁡ A B
8 6 7 eqtri ⊢ A D B = abs ∘ − ⁡ A B
9 df-ov ⊢ A − B = − ⁡ A B
10 9 fveq2i ⊢ A − B = − ⁡ A B
11 5 8 10 3eqtr4g ⊢ A ∈ ℂ ∧ B ∈ ℂ → A D B = A − B