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	⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
Assertion	remet	⊢ 𝐷 ∈ ( Met ‘ ℝ )

Proof

Step	Hyp	Ref	Expression
1		remet.1	⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
2		cnmet	⊢ ( abs ∘ − ) ∈ ( Met ‘ ℂ )
3		ax-resscn	⊢ ℝ ⊆ ℂ
4		metres2	⊢ ( ( ( abs ∘ − ) ∈ ( Met ‘ ℂ ) ∧ ℝ ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( Met ‘ ℝ ) )
5	2 3 4	mp2an	⊢ ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) ) ∈ ( Met ‘ ℝ )
6	1 5	eqeltri	⊢ 𝐷 ∈ ( Met ‘ ℝ )