psmetres2

Description: Restriction of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018)

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

Proof

Step	Hyp	Ref	Expression
1		psmetf	$⊢ D \in PsMet (X) \to D : X \times X ⟶ ℝ^{*}$
2	1	adantr	$⊢ (D \in PsMet (X) \land R \subseteq X) \to D : X \times X ⟶ ℝ^{*}$
3		simpr	$⊢ (D \in PsMet (X) \land R \subseteq X) \to R \subseteq X$
4		xpss12	$⊢ (R \subseteq X \land R \subseteq X) \to R \times R \subseteq X \times X$
5	3 3 4	syl2anc	$⊢ (D \in PsMet (X) \land R \subseteq X) \to R \times R \subseteq X \times X$
6	2 5	fssresd	$⊢ (D \in PsMet (X) \land R \subseteq X) \to ({D ↾}_{(R \times R)}) : R \times R ⟶ ℝ^{*}$
7		simpr	$⊢ ((D \in PsMet (X) \land R \subseteq X) \land a \in R) \to a \in R$
8	7 7	ovresd	$⊢ ((D \in PsMet (X) \land R \subseteq X) \land a \in R) \to a ({D ↾}_{(R \times R)}) a = a D a$
9		simpll	$⊢ ((D \in PsMet (X) \land R \subseteq X) \land a \in R) \to D \in PsMet (X)$
10	3	sselda	$⊢ ((D \in PsMet (X) \land R \subseteq X) \land a \in R) \to a \in X$
11		psmet0	$⊢ (D \in PsMet (X) \land a \in X) \to a D a = 0$
12	9 10 11	syl2anc	$⊢ ((D \in PsMet (X) \land R \subseteq X) \land a \in R) \to a D a = 0$
13	8 12	eqtrd	$⊢ ((D \in PsMet (X) \land R \subseteq X) \land a \in R) \to a ({D ↾}_{(R \times R)}) a = 0$
14	9	ad2antrr	$⊢ ((((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \land c \in R) \to D \in PsMet (X)$
15	3	ad2antrr	$⊢ (((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \to R \subseteq X$
16	15	sselda	$⊢ ((((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \land c \in R) \to c \in X$
17	10	ad2antrr	$⊢ ((((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \land c \in R) \to a \in X$
18	3	adantr	$⊢ ((D \in PsMet (X) \land R \subseteq X) \land a \in R) \to R \subseteq X$
19	18	sselda	$⊢ (((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \to b \in X$
20	19	adantr	$⊢ ((((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \land c \in R) \to b \in X$
21		psmettri2	$⊢ (D \in PsMet (X) \land (c \in X \land a \in X \land b \in X)) \to a D b \leq (c D a) +_{𝑒} (c D b)$
22	14 16 17 20 21	syl13anc	$⊢ ((((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \land c \in R) \to a D b \leq (c D a) +_{𝑒} (c D b)$
23	7	adantr	$⊢ (((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \to a \in R$
24		simpr	$⊢ (((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \to b \in R$
25	23 24	ovresd	$⊢ (((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \to a ({D ↾}_{(R \times R)}) b = a D b$
26	25	adantr	$⊢ ((((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \land c \in R) \to a ({D ↾}_{(R \times R)}) b = a D b$
27		simpr	$⊢ ((((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \land c \in R) \to c \in R$
28	7	ad2antrr	$⊢ ((((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \land c \in R) \to a \in R$
29	27 28	ovresd	$⊢ ((((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \land c \in R) \to c ({D ↾}_{(R \times R)}) a = c D a$
30	24	adantr	$⊢ ((((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \land c \in R) \to b \in R$
31	27 30	ovresd	$⊢ ((((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \land c \in R) \to c ({D ↾}_{(R \times R)}) b = c D b$
32	29 31	oveq12d	$⊢ ((((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \land c \in R) \to (c ({D ↾}_{(R \times R)}) a) +_{𝑒} (c ({D ↾}_{(R \times R)}) b) = (c D a) +_{𝑒} (c D b)$
33	22 26 32	3brtr4d	$⊢ ((((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \land c \in R) \to a ({D ↾}_{(R \times R)}) b \leq (c ({D ↾}_{(R \times R)}) a) +_{𝑒} (c ({D ↾}_{(R \times R)}) b)$
34	33	ralrimiva	$⊢ (((D \in PsMet (X) \land R \subseteq X) \land a \in R) \land b \in R) \to \forall c \in R a ({D ↾}_{(R \times R)}) b \leq (c ({D ↾}_{(R \times R)}) a) +_{𝑒} (c ({D ↾}_{(R \times R)}) b)$
35	34	ralrimiva	$⊢ ((D \in PsMet (X) \land R \subseteq X) \land a \in R) \to \forall b \in R \forall c \in R a ({D ↾}_{(R \times R)}) b \leq (c ({D ↾}_{(R \times R)}) a) +_{𝑒} (c ({D ↾}_{(R \times R)}) b)$
36	13 35	jca	$⊢ ((D \in PsMet (X) \land R \subseteq X) \land a \in R) \to (a ({D ↾}_{(R \times R)}) a = 0 \land \forall b \in R \forall c \in R a ({D ↾}_{(R \times R)}) b \leq (c ({D ↾}_{(R \times R)}) a) +_{𝑒} (c ({D ↾}_{(R \times R)}) b))$
37	36	ralrimiva	$⊢ (D \in PsMet (X) \land R \subseteq X) \to \forall a \in R (a ({D ↾}_{(R \times R)}) a = 0 \land \forall b \in R \forall c \in R a ({D ↾}_{(R \times R)}) b \leq (c ({D ↾}_{(R \times R)}) a) +_{𝑒} (c ({D ↾}_{(R \times R)}) b))$
38		elfvex	$⊢ D \in PsMet (X) \to X \in V$
39	38	adantr	$⊢ (D \in PsMet (X) \land R \subseteq X) \to X \in V$
40	39 3	ssexd	$⊢ (D \in PsMet (X) \land R \subseteq X) \to R \in V$
41		ispsmet	$⊢ R \in V \to ({D ↾}_{(R \times R)} \in PsMet (R) \leftrightarrow (({D ↾}_{(R \times R)}) : R \times R ⟶ ℝ^{*} \land \forall a \in R (a ({D ↾}_{(R \times R)}) a = 0 \land \forall b \in R \forall c \in R a ({D ↾}_{(R \times R)}) b \leq (c ({D ↾}_{(R \times R)}) a) +_{𝑒} (c ({D ↾}_{(R \times R)}) b))))$
42	40 41	syl	$⊢ (D \in PsMet (X) \land R \subseteq X) \to ({D ↾}_{(R \times R)} \in PsMet (R) \leftrightarrow (({D ↾}_{(R \times R)}) : R \times R ⟶ ℝ^{*} \land \forall a \in R (a ({D ↾}_{(R \times R)}) a = 0 \land \forall b \in R \forall c \in R a ({D ↾}_{(R \times R)}) b \leq (c ({D ↾}_{(R \times R)}) a) +_{𝑒} (c ({D ↾}_{(R \times R)}) b))))$
43	6 37 42	mpbir2and	$⊢ (D \in PsMet (X) \land R \subseteq X) \to {D ↾}_{(R \times R)} \in PsMet (R)$

Metamath Proof Explorer

Theorem psmetres2

Proof