xmetres2

Description: Restriction of an extended metric. (Contributed by Mario Carneiro, 20-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$⊢ D \in ∞Met (X) \to X \in dom ∞Met$
2	1	adantr	$⊢ (D \in ∞Met (X) \land R \subseteq X) \to X \in dom ∞Met$
3		simpr	$⊢ (D \in ∞Met (X) \land R \subseteq X) \to R \subseteq X$
4	2 3	ssexd	$⊢ (D \in ∞Met (X) \land R \subseteq X) \to R \in V$
5		xmetf	$⊢ D \in ∞Met (X) \to D : X \times X ⟶ ℝ^{*}$
6	5	adantr	$⊢ (D \in ∞Met (X) \land R \subseteq X) \to D : X \times X ⟶ ℝ^{*}$
7		xpss12	$⊢ (R \subseteq X \land R \subseteq X) \to R \times R \subseteq X \times X$
8	3 7	sylancom	$⊢ (D \in ∞Met (X) \land R \subseteq X) \to R \times R \subseteq X \times X$
9	6 8	fssresd	$⊢ (D \in ∞Met (X) \land R \subseteq X) \to ({D ↾}_{(R \times R)}) : R \times R ⟶ ℝ^{*}$
10		ovres	$⊢ (x \in R \land y \in R) \to x ({D ↾}_{(R \times R)}) y = x D y$
11	10	adantl	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R)) \to x ({D ↾}_{(R \times R)}) y = x D y$
12	11	eqeq1d	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R)) \to (x ({D ↾}_{(R \times R)}) y = 0 \leftrightarrow x D y = 0)$
13		simpll	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R)) \to D \in ∞Met (X)$
14		simplr	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R)) \to R \subseteq X$
15		simprl	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R)) \to x \in R$
16	14 15	sseldd	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R)) \to x \in X$
17		simprr	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R)) \to y \in R$
18	14 17	sseldd	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R)) \to y \in X$
19		xmeteq0	$⊢ (D \in ∞Met (X) \land x \in X \land y \in X) \to (x D y = 0 \leftrightarrow x = y)$
20	13 16 18 19	syl3anc	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R)) \to (x D y = 0 \leftrightarrow x = y)$
21	12 20	bitrd	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R)) \to (x ({D ↾}_{(R \times R)}) y = 0 \leftrightarrow x = y)$
22		simpll	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to D \in ∞Met (X)$
23		simplr	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to R \subseteq X$
24		simpr3	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to z \in R$
25	23 24	sseldd	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to z \in X$
26	16	3adantr3	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to x \in X$
27	18	3adantr3	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to y \in X$
28		xmettri2	$⊢ (D \in ∞Met (X) \land (z \in X \land x \in X \land y \in X)) \to x D y \leq (z D x) +_{𝑒} (z D y)$
29	22 25 26 27 28	syl13anc	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to x D y \leq (z D x) +_{𝑒} (z D y)$
30	11	3adantr3	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to x ({D ↾}_{(R \times R)}) y = x D y$
31		simpr1	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to x \in R$
32	24 31	ovresd	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to z ({D ↾}_{(R \times R)}) x = z D x$
33		simpr2	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to y \in R$
34	24 33	ovresd	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to z ({D ↾}_{(R \times R)}) y = z D y$
35	32 34	oveq12d	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to (z ({D ↾}_{(R \times R)}) x) +_{𝑒} (z ({D ↾}_{(R \times R)}) y) = (z D x) +_{𝑒} (z D y)$
36	29 30 35	3brtr4d	$⊢ ((D \in ∞Met (X) \land R \subseteq X) \land (x \in R \land y \in R \land z \in R)) \to x ({D ↾}_{(R \times R)}) y \leq (z ({D ↾}_{(R \times R)}) x) +_{𝑒} (z ({D ↾}_{(R \times R)}) y)$
37	4 9 21 36	isxmetd	$⊢ (D \in ∞Met (X) \land R \subseteq X) \to {D ↾}_{(R \times R)} \in ∞Met (R)$

Metamath Proof Explorer

Theorem xmetres2

Proof