xmetres

Description: A restriction of an extended metric is an extended metric. (Contributed by Mario Carneiro, 24-Aug-2015)

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

Step	Hyp	Ref	Expression
1		xmetf	$⊢ 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		xmetres2	$⊢ (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