Metamath Proof Explorer


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 ‘ ℝ )