pstmxmet

Description: The metric induced by a pseudometric is a full-fledged metric on the equivalence classes of the metric identification. (Contributed by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Hypothesis	pstmval.1	$⊢ \underset{˙}{\sim} = ~_{Met} (D)$
	Assertion	pstmxmet	$⊢ D \in PsMet (X) \to pstoMet (D) \in ∞Met (X / \underset{˙}{\sim})$

Proof

Step	Hyp	Ref	Expression
1		pstmval.1	$⊢ \underset{˙}{\sim} = ~_{Met} (D)$
2		eqid	$⊢ (x \in (X / \underset{˙}{\sim}), y \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists a \in x \exists b \in y z = a D b\}) = (x \in (X / \underset{˙}{\sim}), y \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists a \in x \exists b \in y z = a D b\})$
3		vex	$⊢ x \in V$
4		vex	$⊢ y \in V$
5	3 4	ab2rexex	$⊢ \{z \| \exists a \in x \exists b \in y z = a D b\} \in V$
6	5	uniex	$⊢ ⋃ \{z \| \exists a \in x \exists b \in y z = a D b\} \in V$
7	2 6	fnmpoi	$⊢ (x \in (X / \underset{˙}{\sim}), y \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists a \in x \exists b \in y z = a D b\}) Fn ((X / \underset{˙}{\sim}) \times (X / \underset{˙}{\sim}))$
8	1	pstmval	$⊢ D \in PsMet (X) \to pstoMet (D) = (x \in (X / \underset{˙}{\sim}), y \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists a \in x \exists b \in y z = a D b\})$
9	8	fneq1d	$⊢ D \in PsMet (X) \to (pstoMet (D) Fn ((X / \underset{˙}{\sim}) \times (X / \underset{˙}{\sim})) \leftrightarrow (x \in (X / \underset{˙}{\sim}), y \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists a \in x \exists b \in y z = a D b\}) Fn ((X / \underset{˙}{\sim}) \times (X / \underset{˙}{\sim})))$
10	7 9	mpbiri	$⊢ D \in PsMet (X) \to pstoMet (D) Fn ((X / \underset{˙}{\sim}) \times (X / \underset{˙}{\sim}))$
11		simpllr	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to x = [a] \underset{˙}{\sim}$
12		simpr	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to y = [b] \underset{˙}{\sim}$
13	11 12	oveq12d	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to x pstoMet (D) y = [a] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim}$
14		simp-5l	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to D \in PsMet (X)$
15		simp-4r	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to a \in X$
16		simplr	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to b \in X$
17	1	pstmfval	$⊢ (D \in PsMet (X) \land a \in X \land b \in X) \to [a] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim} = a D b$
18	14 15 16 17	syl3anc	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to [a] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim} = a D b$
19	13 18	eqtrd	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to x pstoMet (D) y = a D b$
20		psmetf	$⊢ D \in PsMet (X) \to D : X \times X ⟶ ℝ^{*}$
21	14 20	syl	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to D : X \times X ⟶ ℝ^{*}$
22	21 15 16	fovrnd	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to a D b \in ℝ^{*}$
23	19 22	eqeltrd	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to x pstoMet (D) y \in ℝ^{*}$
24		elqsi	$⊢ y \in (X / \underset{˙}{\sim}) \to \exists b \in X y = [b] \underset{˙}{\sim}$
25	24	ad2antll	$⊢ (D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \to \exists b \in X y = [b] \underset{˙}{\sim}$
26	25	ad2antrr	$⊢ (((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \to \exists b \in X y = [b] \underset{˙}{\sim}$
27	23 26	r19.29a	$⊢ (((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \to x pstoMet (D) y \in ℝ^{*}$
28		elqsi	$⊢ x \in (X / \underset{˙}{\sim}) \to \exists a \in X x = [a] \underset{˙}{\sim}$
29	28	ad2antrl	$⊢ (D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \to \exists a \in X x = [a] \underset{˙}{\sim}$
30	27 29	r19.29a	$⊢ (D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \to x pstoMet (D) y \in ℝ^{*}$
31	30	ralrimivva	$⊢ D \in PsMet (X) \to \forall x \in (X / \underset{˙}{\sim}) \forall y \in (X / \underset{˙}{\sim}) x pstoMet (D) y \in ℝ^{*}$
32		ffnov	$⊢ pstoMet (D) : (X / \underset{˙}{\sim}) \times (X / \underset{˙}{\sim}) ⟶ ℝ^{} \leftrightarrow (pstoMet (D) Fn ((X / \underset{˙}{\sim}) \times (X / \underset{˙}{\sim})) \land \forall x \in (X / \underset{˙}{\sim}) \forall y \in (X / \underset{˙}{\sim}) x pstoMet (D) y \in ℝ^{})$
33	10 31 32	sylanbrc	$⊢ D \in PsMet (X) \to pstoMet (D) : (X / \underset{˙}{\sim}) \times (X / \underset{˙}{\sim}) ⟶ ℝ^{*}$
34	17	3expa	$⊢ ((D \in PsMet (X) \land a \in X) \land b \in X) \to [a] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim} = a D b$
35	34	eqeq1d	$⊢ ((D \in PsMet (X) \land a \in X) \land b \in X) \to ([a] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim} = 0 \leftrightarrow a D b = 0)$
36	1	breqi	$⊢ a \underset{˙}{\sim} b \leftrightarrow a ~_{Met} (D) b$
37		metidv	$⊢ (D \in PsMet (X) \land (a \in X \land b \in X)) \to (a ~_{Met} (D) b \leftrightarrow a D b = 0)$
38	37	anassrs	$⊢ ((D \in PsMet (X) \land a \in X) \land b \in X) \to (a ~_{Met} (D) b \leftrightarrow a D b = 0)$
39	36 38	syl5bb	$⊢ ((D \in PsMet (X) \land a \in X) \land b \in X) \to (a \underset{˙}{\sim} b \leftrightarrow a D b = 0)$
40		metider	$⊢ D \in PsMet (X) \to ~_{Met} (D) Er X$
41	40	ad2antrr	$⊢ ((D \in PsMet (X) \land a \in X) \land b \in X) \to ~_{Met} (D) Er X$
42		ereq1	$⊢ \underset{˙}{\sim} = ~_{Met} (D) \to (\underset{˙}{\sim} Er X \leftrightarrow ~_{Met} (D) Er X)$
43	1 42	ax-mp	$⊢ \underset{˙}{\sim} Er X \leftrightarrow ~_{Met} (D) Er X$
44	41 43	sylibr	$⊢ ((D \in PsMet (X) \land a \in X) \land b \in X) \to \underset{˙}{\sim} Er X$
45		simplr	$⊢ ((D \in PsMet (X) \land a \in X) \land b \in X) \to a \in X$
46	44 45	erth	$⊢ ((D \in PsMet (X) \land a \in X) \land b \in X) \to (a \underset{˙}{\sim} b \leftrightarrow [a] \underset{˙}{\sim} = [b] \underset{˙}{\sim})$
47	35 39 46	3bitr2d	$⊢ ((D \in PsMet (X) \land a \in X) \land b \in X) \to ([a] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim} = 0 \leftrightarrow [a] \underset{˙}{\sim} = [b] \underset{˙}{\sim})$
48	47	adantllr	$⊢ (((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land b \in X) \to ([a] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim} = 0 \leftrightarrow [a] \underset{˙}{\sim} = [b] \underset{˙}{\sim})$
49	48	adantlr	$⊢ ((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \to ([a] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim} = 0 \leftrightarrow [a] \underset{˙}{\sim} = [b] \underset{˙}{\sim})$
50	49	adantr	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to ([a] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim} = 0 \leftrightarrow [a] \underset{˙}{\sim} = [b] \underset{˙}{\sim})$
51	13	eqeq1d	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to (x pstoMet (D) y = 0 \leftrightarrow [a] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim} = 0)$
52	11 12	eqeq12d	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to (x = y \leftrightarrow [a] \underset{˙}{\sim} = [b] \underset{˙}{\sim})$
53	50 51 52	3bitr4d	$⊢ (((((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to (x pstoMet (D) y = 0 \leftrightarrow x = y)$
54	53 26	r19.29a	$⊢ (((D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \land a \in X) \land x = [a] \underset{˙}{\sim}) \to (x pstoMet (D) y = 0 \leftrightarrow x = y)$
55	54 29	r19.29a	$⊢ (D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \to (x pstoMet (D) y = 0 \leftrightarrow x = y)$
56		simp-6l	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to D \in PsMet (X)$
57		simplr	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to c \in X$
58		simp-6r	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to a \in X$
59		simp-4r	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to b \in X$
60		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)$
61	56 57 58 59 60	syl13anc	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to a D b \leq (c D a) +_{𝑒} (c D b)$
62		simp-5r	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to x = [a] \underset{˙}{\sim}$
63		simpllr	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to y = [b] \underset{˙}{\sim}$
64	62 63	oveq12d	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to x pstoMet (D) y = [a] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim}$
65	56 58 59 17	syl3anc	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to [a] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim} = a D b$
66	64 65	eqtrd	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to x pstoMet (D) y = a D b$
67		simpr	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to z = [c] \underset{˙}{\sim}$
68	67 62	oveq12d	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to z pstoMet (D) x = [c] \underset{˙}{\sim} pstoMet (D) [a] \underset{˙}{\sim}$
69	1	pstmfval	$⊢ (D \in PsMet (X) \land c \in X \land a \in X) \to [c] \underset{˙}{\sim} pstoMet (D) [a] \underset{˙}{\sim} = c D a$
70	56 57 58 69	syl3anc	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to [c] \underset{˙}{\sim} pstoMet (D) [a] \underset{˙}{\sim} = c D a$
71	68 70	eqtrd	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to z pstoMet (D) x = c D a$
72	67 63	oveq12d	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to z pstoMet (D) y = [c] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim}$
73	1	pstmfval	$⊢ (D \in PsMet (X) \land c \in X \land b \in X) \to [c] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim} = c D b$
74	56 57 59 73	syl3anc	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to [c] \underset{˙}{\sim} pstoMet (D) [b] \underset{˙}{\sim} = c D b$
75	72 74	eqtrd	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to z pstoMet (D) y = c D b$
76	71 75	oveq12d	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y) = (c D a) +_{𝑒} (c D b)$
77	61 66 76	3brtr4d	$⊢ ((((((D \in PsMet (X) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to x pstoMet (D) y \leq (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y)$
78	77	adantl6r	$⊢ (((((((D \in PsMet (X) \land z \in (X / \underset{˙}{\sim})) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \land c \in X) \land z = [c] \underset{˙}{\sim}) \to x pstoMet (D) y \leq (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y)$
79		elqsi	$⊢ z \in (X / \underset{˙}{\sim}) \to \exists c \in X z = [c] \underset{˙}{\sim}$
80	79	ad5antlr	$⊢ (((((D \in PsMet (X) \land z \in (X / \underset{˙}{\sim})) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to \exists c \in X z = [c] \underset{˙}{\sim}$
81	78 80	r19.29a	$⊢ (((((D \in PsMet (X) \land z \in (X / \underset{˙}{\sim})) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to x pstoMet (D) y \leq (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y)$
82	81	adantl5r	$⊢ ((((((D \in PsMet (X) \land y \in (X / \underset{˙}{\sim})) \land z \in (X / \underset{˙}{\sim})) \land a \in X) \land x = [a] \underset{˙}{\sim}) \land b \in X) \land y = [b] \underset{˙}{\sim}) \to x pstoMet (D) y \leq (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y)$
83	24	ad4antlr	$⊢ ((((D \in PsMet (X) \land y \in (X / \underset{˙}{\sim})) \land z \in (X / \underset{˙}{\sim})) \land a \in X) \land x = [a] \underset{˙}{\sim}) \to \exists b \in X y = [b] \underset{˙}{\sim}$
84	82 83	r19.29a	$⊢ ((((D \in PsMet (X) \land y \in (X / \underset{˙}{\sim})) \land z \in (X / \underset{˙}{\sim})) \land a \in X) \land x = [a] \underset{˙}{\sim}) \to x pstoMet (D) y \leq (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y)$
85	84	adantl4r	$⊢ (((((D \in PsMet (X) \land x \in (X / \underset{˙}{\sim})) \land y \in (X / \underset{˙}{\sim})) \land z \in (X / \underset{˙}{\sim})) \land a \in X) \land x = [a] \underset{˙}{\sim}) \to x pstoMet (D) y \leq (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y)$
86	28	ad3antlr	$⊢ (((D \in PsMet (X) \land x \in (X / \underset{˙}{\sim})) \land y \in (X / \underset{˙}{\sim})) \land z \in (X / \underset{˙}{\sim})) \to \exists a \in X x = [a] \underset{˙}{\sim}$
87	85 86	r19.29a	$⊢ (((D \in PsMet (X) \land x \in (X / \underset{˙}{\sim})) \land y \in (X / \underset{˙}{\sim})) \land z \in (X / \underset{˙}{\sim})) \to x pstoMet (D) y \leq (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y)$
88	87	ralrimiva	$⊢ ((D \in PsMet (X) \land x \in (X / \underset{˙}{\sim})) \land y \in (X / \underset{˙}{\sim})) \to \forall z \in (X / \underset{˙}{\sim}) x pstoMet (D) y \leq (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y)$
89	88	anasss	$⊢ (D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \to \forall z \in (X / \underset{˙}{\sim}) x pstoMet (D) y \leq (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y)$
90	55 89	jca	$⊢ (D \in PsMet (X) \land (x \in (X / \underset{˙}{\sim}) \land y \in (X / \underset{˙}{\sim}))) \to ((x pstoMet (D) y = 0 \leftrightarrow x = y) \land \forall z \in (X / \underset{˙}{\sim}) x pstoMet (D) y \leq (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y))$
91	90	ralrimivva	$⊢ D \in PsMet (X) \to \forall x \in (X / \underset{˙}{\sim}) \forall y \in (X / \underset{˙}{\sim}) ((x pstoMet (D) y = 0 \leftrightarrow x = y) \land \forall z \in (X / \underset{˙}{\sim}) x pstoMet (D) y \leq (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y))$
92		elfvex	$⊢ D \in PsMet (X) \to X \in V$
93		qsexg	$⊢ X \in V \to X / \underset{˙}{\sim} \in V$
94		isxmet	$⊢ X / \underset{˙}{\sim} \in V \to (pstoMet (D) \in ∞Met (X / \underset{˙}{\sim}) \leftrightarrow (pstoMet (D) : (X / \underset{˙}{\sim}) \times (X / \underset{˙}{\sim}) ⟶ ℝ^{*} \land \forall x \in (X / \underset{˙}{\sim}) \forall y \in (X / \underset{˙}{\sim}) ((x pstoMet (D) y = 0 \leftrightarrow x = y) \land \forall z \in (X / \underset{˙}{\sim}) x pstoMet (D) y \leq (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y))))$
95	92 93 94	3syl	$⊢ D \in PsMet (X) \to (pstoMet (D) \in ∞Met (X / \underset{˙}{\sim}) \leftrightarrow (pstoMet (D) : (X / \underset{˙}{\sim}) \times (X / \underset{˙}{\sim}) ⟶ ℝ^{*} \land \forall x \in (X / \underset{˙}{\sim}) \forall y \in (X / \underset{˙}{\sim}) ((x pstoMet (D) y = 0 \leftrightarrow x = y) \land \forall z \in (X / \underset{˙}{\sim}) x pstoMet (D) y \leq (z pstoMet (D) x) +_{𝑒} (z pstoMet (D) y))))$
96	33 91 95	mpbir2and	$⊢ D \in PsMet (X) \to pstoMet (D) \in ∞Met (X / \underset{˙}{\sim})$

Metamath Proof Explorer

Theorem pstmxmet

Proof