This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ D = {(abs \circ -) ↾}_{ℝ^{2}}$
	Assertion	rexmet	$⊢ D \in ∞Met (ℝ)$

Step	Hyp	Ref	Expression
1		remet.1	$⊢ D = {(abs \circ -) ↾}_{ℝ^{2}}$
2	1	remet	$⊢ D \in Met (ℝ)$
3		metxmet	$⊢ D \in Met (ℝ) \to D \in ∞Met (ℝ)$
4	2 3	ax-mp	$⊢ D \in ∞Met (ℝ)$