# 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}={\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}$
Assertion remetdval ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{D}{B}=\left|{A}-{B}\right|$

### Proof

Step Hyp Ref Expression
1 remet.1 ${⊢}{D}={\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}$
2 df-ov ${⊢}{A}{D}{B}={D}\left(⟨{A},{B}⟩\right)$
3 1 fveq1i ${⊢}{D}\left(⟨{A},{B}⟩\right)=\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\left(⟨{A},{B}⟩\right)$
4 2 3 eqtri ${⊢}{A}{D}{B}=\left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\left(⟨{A},{B}⟩\right)$
5 opelxpi ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to ⟨{A},{B}⟩\in {ℝ}^{2}$
6 5 fvresd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\left(⟨{A},{B}⟩\right)=\left(\mathrm{abs}\circ -\right)\left(⟨{A},{B}⟩\right)$
7 df-ov ${⊢}{A}\left(\mathrm{abs}\circ -\right){B}=\left(\mathrm{abs}\circ -\right)\left(⟨{A},{B}⟩\right)$
8 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
9 recn ${⊢}{B}\in ℝ\to {B}\in ℂ$
10 eqid ${⊢}\mathrm{abs}\circ -=\mathrm{abs}\circ -$
11 10 cnmetdval ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}\left(\mathrm{abs}\circ -\right){B}=\left|{A}-{B}\right|$
12 8 9 11 syl2an ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}\left(\mathrm{abs}\circ -\right){B}=\left|{A}-{B}\right|$
13 7 12 syl5eqr ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left(\mathrm{abs}\circ -\right)\left(⟨{A},{B}⟩\right)=\left|{A}-{B}\right|$
14 6 13 eqtrd ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({\left(\mathrm{abs}\circ -\right)↾}_{{ℝ}^{2}}\right)\left(⟨{A},{B}⟩\right)=\left|{A}-{B}\right|$
15 4 14 syl5eq ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{D}{B}=\left|{A}-{B}\right|$