metres2

Description: Lemma for metres . (Contributed by FL, 12-Oct-2006) (Proof shortened by Mario Carneiro, 14-Aug-2015)

		Ref	Expression
	Assertion	metres2	$⊢ (D \in Met (X) \land R \subseteq X) \to {D ↾}_{(R \times R)} \in Met (R)$

Step	Hyp	Ref	Expression
1		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
2		xmetres2	$⊢ (D \in ∞Met (X) \land R \subseteq X) \to {D ↾}_{(R \times R)} \in ∞Met (R)$
3	1 2	sylan	$⊢ (D \in Met (X) \land R \subseteq X) \to {D ↾}_{(R \times R)} \in ∞Met (R)$
4		metf	$⊢ D \in Met (X) \to D : X \times X ⟶ ℝ$
5	4	adantr	$⊢ (D \in Met (X) \land R \subseteq X) \to D : X \times X ⟶ ℝ$
6		simpr	$⊢ (D \in Met (X) \land R \subseteq X) \to R \subseteq X$
7		xpss12	$⊢ (R \subseteq X \land R \subseteq X) \to R \times R \subseteq X \times X$
8	6 7	sylancom	$⊢ (D \in Met (X) \land R \subseteq X) \to R \times R \subseteq X \times X$
9	5 8	fssresd	$⊢ (D \in Met (X) \land R \subseteq X) \to ({D ↾}_{(R \times R)}) : R \times R ⟶ ℝ$
10		ismet2	$⊢ {D ↾}_{(R \times R)} \in Met (R) \leftrightarrow ({D ↾}_{(R \times R)} \in ∞Met (R) \land ({D ↾}_{(R \times R)}) : R \times R ⟶ ℝ)$
11	3 9 10	sylanbrc	$⊢ (D \in Met (X) \land R \subseteq X) \to {D ↾}_{(R \times R)} \in Met (R)$

Metamath Proof Explorer