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

Metamath Proof Explorer

Theorem remetdval

Description: Value of the distance function of the metric space of real numbers. (Contributed by NM, 16-May-2007)

Ref Expression
Hypothesis remet.1 ⊢ D = abs ∘ − ↾ ℝ 2
Assertion remetdval ⊢ A ∈ ℝ ∧ B ∈ ℝ → A D B = A − B

Proof

Step Hyp Ref Expression
1 remet.1 ⊢ D = abs ∘ − ↾ ℝ 2
2 df-ov ⊢ A D B = D ⁡ A B
3 1 fveq1i ⊢ D ⁡ A B = abs ∘ − ↾ ℝ 2 ⁡ A B
4 2 3 eqtri ⊢ A D B = abs ∘ − ↾ ℝ 2 ⁡ A B
5 opelxpi ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ∈ ℝ 2
6 5 fvresd ⊢ A ∈ ℝ ∧ B ∈ ℝ → abs ∘ − ↾ ℝ 2 ⁡ A B = abs ∘ − ⁡ A B
7 df-ov ⊢ A abs ∘ − B = abs ∘ − ⁡ A B
8 recn ⊢ A ∈ ℝ → A ∈ ℂ
9 recn ⊢ B ∈ ℝ → B ∈ ℂ
10 eqid ⊢ abs ∘ − = abs ∘ −
11 10 cnmetdval ⊢ A ∈ ℂ ∧ B ∈ ℂ → A abs ∘ − B = A − B
12 8 9 11 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A abs ∘ − B = A − B
13 7 12 eqtr3id ⊢ A ∈ ℝ ∧ B ∈ ℝ → abs ∘ − ⁡ A B = A − B
14 6 13 eqtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → abs ∘ − ↾ ℝ 2 ⁡ A B = A − B
15 4 14 eqtrid ⊢ A ∈ ℝ ∧ B ∈ ℝ → A D B = A − B