Theorem rexmet

Description: The absolute value metric is an extended metric. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypothesis	remet.1	⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
Assertion	rexmet	⊢ 𝐷 ∈ ( ∞Met ‘ ℝ )

Proof

Step	Hyp	Ref	Expression
1		remet.1	⊢ 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
2	1	remet	⊢ 𝐷 ∈ ( Met ‘ ℝ )
3		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ ℝ ) → 𝐷 ∈ ( ∞Met ‘ ℝ ) )
4	2 3	ax-mp	⊢ 𝐷 ∈ ( ∞Met ‘ ℝ )