Theorem remet

Description: The absolute value metric determines a metric space on the reals. (Contributed by NM, 10-Feb-2007)

	Ref	Expression
Hypothesis	remet.1	$$⊢D={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
Assertion	remet	$$⊢D\in \mathrm{Met}\left(ℝ\right)$$

Proof

Step	Hyp	Ref	Expression
1		remet.1	$$⊢D={\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}$$
2		cnmet	$$⊢\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)$$
3		ax-resscn	$$⊢ℝ\subseteq ℂ$$
4		metres2	$$⊢\left(\mathrm{abs}\circ -\in \mathrm{Met}\left(ℂ\right)\wedge ℝ\subseteq ℂ\right)\to {\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{Met}\left(ℝ\right)$$
5	2 3 4	mp2an	$$⊢{\left(\mathrm{abs}\circ -\right)\upharpoonright }_{{ℝ}^2}\in \mathrm{Met}\left(ℝ\right)$$
6	1 5	eqeltri	$$⊢D\in \mathrm{Met}\left(ℝ\right)$$