metres

Description: A restriction of a metric is a metric. (Contributed by NM, 26-Aug-2007) (Revised by Mario Carneiro, 14-Aug-2015)

		Ref	Expression
	Assertion	metres	$⊢ D \in Met (X) \to {D ↾}_{(R \times R)} \in Met (X \cap R)$

Step	Hyp	Ref	Expression
1		metf	$⊢ D \in Met (X) \to D : X \times X ⟶ ℝ$
2		fdm	$⊢ D : X \times X ⟶ ℝ \to dom D = X \times X$
3		metreslem	$⊢ dom D = X \times X \to {D ↾}_{(R \times R)} = {D ↾}_{((X \cap R) \times (X \cap R))}$
4	1 2 3	3syl	$⊢ D \in Met (X) \to {D ↾}_{(R \times R)} = {D ↾}_{((X \cap R) \times (X \cap R))}$
5		inss1	$⊢ X \cap R \subseteq X$
6		metres2	$⊢ (D \in Met (X) \land X \cap R \subseteq X) \to {D ↾}_{((X \cap R) \times (X \cap R))} \in Met (X \cap R)$
7	5 6	mpan2	$⊢ D \in Met (X) \to {D ↾}_{((X \cap R) \times (X \cap R))} \in Met (X \cap R)$
8	4 7	eqeltrd	$⊢ D \in Met (X) \to {D ↾}_{(R \times R)} \in Met (X \cap R)$

Metamath Proof Explorer