pstmfval

Description: Function value of the metric induced by a pseudometric D (Contributed by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Hypothesis	pstmval.1	$⊢ \underset{˙}{\sim} = ~_{Met} (D)$
	Assertion	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$

Proof

Step	Hyp	Ref	Expression
1		pstmval.1	$⊢ \underset{˙}{\sim} = ~_{Met} (D)$
2	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\})$
3	2	3ad2ant1	$⊢ (D \in PsMet (X) \land A \in X \land B \in 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\})$
4	3	oveqd	$⊢ (D \in PsMet (X) \land A \in X \land B \in X) \to [A] \underset{˙}{\sim} pstoMet (D) [B] \underset{˙}{\sim} = [A] \underset{˙}{\sim} (x \in (X / \underset{˙}{\sim}), y \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists a \in x \exists b \in y z = a D b\}) [B] \underset{˙}{\sim}$
5	1	fvexi	$⊢ \underset{˙}{\sim} \in V$
6	5	ecelqsi	$⊢ A \in X \to [A] \underset{˙}{\sim} \in (X / \underset{˙}{\sim})$
7	6	3ad2ant2	$⊢ (D \in PsMet (X) \land A \in X \land B \in X) \to [A] \underset{˙}{\sim} \in (X / \underset{˙}{\sim})$
8	5	ecelqsi	$⊢ B \in X \to [B] \underset{˙}{\sim} \in (X / \underset{˙}{\sim})$
9	8	3ad2ant3	$⊢ (D \in PsMet (X) \land A \in X \land B \in X) \to [B] \underset{˙}{\sim} \in (X / \underset{˙}{\sim})$
10		rexeq	$⊢ x = [A] \underset{˙}{\sim} \to (\exists a \in x \exists b \in y z = a D b \leftrightarrow \exists a \in [A] \underset{˙}{\sim} \exists b \in y z = a D b)$
11	10	abbidv	$⊢ x = [A] \underset{˙}{\sim} \to \{z \| \exists a \in x \exists b \in y z = a D b\} = \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in y z = a D b\}$
12	11	unieqd	$⊢ x = [A] \underset{˙}{\sim} \to ⋃ \{z \| \exists a \in x \exists b \in y z = a D b\} = ⋃ \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in y z = a D b\}$
13		rexeq	$⊢ y = [B] \underset{˙}{\sim} \to (\exists b \in y z = a D b \leftrightarrow \exists b \in [B] \underset{˙}{\sim} z = a D b)$
14	13	rexbidv	$⊢ y = [B] \underset{˙}{\sim} \to (\exists a \in [A] \underset{˙}{\sim} \exists b \in y z = a D b \leftrightarrow \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b)$
15	14	abbidv	$⊢ y = [B] \underset{˙}{\sim} \to \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in y z = a D b\} = \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b\}$
16	15	unieqd	$⊢ y = [B] \underset{˙}{\sim} \to ⋃ \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in y z = a D b\} = ⋃ \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b\}$
17		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\})$
18		ecexg	$⊢ \underset{˙}{\sim} \in V \to [A] \underset{˙}{\sim} \in V$
19	5 18	ax-mp	$⊢ [A] \underset{˙}{\sim} \in V$
20		ecexg	$⊢ \underset{˙}{\sim} \in V \to [B] \underset{˙}{\sim} \in V$
21	5 20	ax-mp	$⊢ [B] \underset{˙}{\sim} \in V$
22	19 21	ab2rexex	$⊢ \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b\} \in V$
23	22	uniex	$⊢ ⋃ \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b\} \in V$
24	12 16 17 23	ovmpo	$⊢ ([A] \underset{˙}{\sim} \in (X / \underset{˙}{\sim}) \land [B] \underset{˙}{\sim} \in (X / \underset{˙}{\sim})) \to [A] \underset{˙}{\sim} (x \in (X / \underset{˙}{\sim}), y \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists a \in x \exists b \in y z = a D b\}) [B] \underset{˙}{\sim} = ⋃ \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b\}$
25	7 9 24	syl2anc	$⊢ (D \in PsMet (X) \land A \in X \land B \in X) \to [A] \underset{˙}{\sim} (x \in (X / \underset{˙}{\sim}), y \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists a \in x \exists b \in y z = a D b\}) [B] \underset{˙}{\sim} = ⋃ \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b\}$
26		simpr3	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to z = e D f$
27		simpl1	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to D \in PsMet (X)$
28		simpr1	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to e \in [A] \underset{˙}{\sim}$
29		metidss	$⊢ D \in PsMet (X) \to ~_{Met} (D) \subseteq X \times X$
30	1 29	eqsstrid	$⊢ D \in PsMet (X) \to \underset{˙}{\sim} \subseteq X \times X$
31		xpss	$⊢ X \times X \subseteq V \times V$
32	30 31	sstrdi	$⊢ D \in PsMet (X) \to \underset{˙}{\sim} \subseteq V \times V$
33		df-rel	$⊢ Rel \underset{˙}{\sim} \leftrightarrow \underset{˙}{\sim} \subseteq V \times V$
34	32 33	sylibr	$⊢ D \in PsMet (X) \to Rel \underset{˙}{\sim}$
35	34	3ad2ant1	$⊢ (D \in PsMet (X) \land A \in X \land B \in X) \to Rel \underset{˙}{\sim}$
36	35	adantr	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to Rel \underset{˙}{\sim}$
37		relelec	$⊢ Rel \underset{˙}{\sim} \to (e \in [A] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{\sim} e)$
38	36 37	syl	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to (e \in [A] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{\sim} e)$
39	28 38	mpbid	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to A \underset{˙}{\sim} e$
40	1	breqi	$⊢ A \underset{˙}{\sim} e \leftrightarrow A ~_{Met} (D) e$
41	39 40	sylib	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to A ~_{Met} (D) e$
42		simpr2	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to f \in [B] \underset{˙}{\sim}$
43		relelec	$⊢ Rel \underset{˙}{\sim} \to (f \in [B] \underset{˙}{\sim} \leftrightarrow B \underset{˙}{\sim} f)$
44	36 43	syl	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to (f \in [B] \underset{˙}{\sim} \leftrightarrow B \underset{˙}{\sim} f)$
45	42 44	mpbid	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to B \underset{˙}{\sim} f$
46	1	breqi	$⊢ B \underset{˙}{\sim} f \leftrightarrow B ~_{Met} (D) f$
47	45 46	sylib	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to B ~_{Met} (D) f$
48		metideq	$⊢ (D \in PsMet (X) \land (A ~_{Met} (D) e \land B ~_{Met} (D) f)) \to A D B = e D f$
49	27 41 47 48	syl12anc	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to A D B = e D f$
50	26 49	eqtr4d	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to z = A D B$
51	50	adantlr	$⊢ (((D \in PsMet (X) \land A \in X \land B \in X) \land \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b) \land (e \in [A] \underset{˙}{\sim} \land f \in [B] \underset{˙}{\sim} \land z = e D f)) \to z = A D B$
52	51	3anassrs	$⊢ (((((D \in PsMet (X) \land A \in X \land B \in X) \land \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b) \land e \in [A] \underset{˙}{\sim}) \land f \in [B] \underset{˙}{\sim}) \land z = e D f) \to z = A D B$
53		oveq1	$⊢ a = e \to a D b = e D b$
54	53	eqeq2d	$⊢ a = e \to (z = a D b \leftrightarrow z = e D b)$
55		oveq2	$⊢ b = f \to e D b = e D f$
56	55	eqeq2d	$⊢ b = f \to (z = e D b \leftrightarrow z = e D f)$
57	54 56	cbvrex2vw	$⊢ \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b \leftrightarrow \exists e \in [A] \underset{˙}{\sim} \exists f \in [B] \underset{˙}{\sim} z = e D f$
58	57	bilani	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b) \to \exists e \in [A] \underset{˙}{\sim} \exists f \in [B] \underset{˙}{\sim} z = e D f$
59	52 58	r19.29vva	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b) \to z = A D B$
60		simpl1	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to D \in PsMet (X)$
61		simpl2	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to A \in X$
62		psmet0	$⊢ (D \in PsMet (X) \land A \in X) \to A D A = 0$
63	60 61 62	syl2anc	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to A D A = 0$
64		relelec	$⊢ Rel \underset{˙}{\sim} \to (A \in [A] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{\sim} A)$
65	60 34 64	3syl	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to (A \in [A] \underset{˙}{\sim} \leftrightarrow A \underset{˙}{\sim} A)$
66	1	a1i	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to \underset{˙}{\sim} = ~_{Met} (D)$
67	66	breqd	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to (A \underset{˙}{\sim} A \leftrightarrow A ~_{Met} (D) A)$
68		metidv	$⊢ (D \in PsMet (X) \land (A \in X \land A \in X)) \to (A ~_{Met} (D) A \leftrightarrow A D A = 0)$
69	60 61 61 68	syl12anc	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to (A ~_{Met} (D) A \leftrightarrow A D A = 0)$
70	65 67 69	3bitrd	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to (A \in [A] \underset{˙}{\sim} \leftrightarrow A D A = 0)$
71	63 70	mpbird	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to A \in [A] \underset{˙}{\sim}$
72		simpl3	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to B \in X$
73		psmet0	$⊢ (D \in PsMet (X) \land B \in X) \to B D B = 0$
74	60 72 73	syl2anc	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to B D B = 0$
75		relelec	$⊢ Rel \underset{˙}{\sim} \to (B \in [B] \underset{˙}{\sim} \leftrightarrow B \underset{˙}{\sim} B)$
76	60 34 75	3syl	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to (B \in [B] \underset{˙}{\sim} \leftrightarrow B \underset{˙}{\sim} B)$
77	66	breqd	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to (B \underset{˙}{\sim} B \leftrightarrow B ~_{Met} (D) B)$
78		metidv	$⊢ (D \in PsMet (X) \land (B \in X \land B \in X)) \to (B ~_{Met} (D) B \leftrightarrow B D B = 0)$
79	60 72 72 78	syl12anc	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to (B ~_{Met} (D) B \leftrightarrow B D B = 0)$
80	76 77 79	3bitrd	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to (B \in [B] \underset{˙}{\sim} \leftrightarrow B D B = 0)$
81	74 80	mpbird	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to B \in [B] \underset{˙}{\sim}$
82		simpr	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to z = A D B$
83		rspceov	$⊢ (A \in [A] \underset{˙}{\sim} \land B \in [B] \underset{˙}{\sim} \land z = A D B) \to \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b$
84	71 81 82 83	syl3anc	$⊢ ((D \in PsMet (X) \land A \in X \land B \in X) \land z = A D B) \to \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b$
85	59 84	impbida	$⊢ (D \in PsMet (X) \land A \in X \land B \in X) \to (\exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b \leftrightarrow z = A D B)$
86	85	abbidv	$⊢ (D \in PsMet (X) \land A \in X \land B \in X) \to \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b\} = \{z \| z = A D B\}$
87		df-sn	$⊢ \{A D B\} = \{z \| z = A D B\}$
88	86 87	eqtr4di	$⊢ (D \in PsMet (X) \land A \in X \land B \in X) \to \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b\} = \{A D B\}$
89	88	unieqd	$⊢ (D \in PsMet (X) \land A \in X \land B \in X) \to ⋃ \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b\} = ⋃ \{A D B\}$
90		ovex	$⊢ A D B \in V$
91	90	unisn	$⊢ ⋃ \{A D B\} = A D B$
92	89 91	eqtrdi	$⊢ (D \in PsMet (X) \land A \in X \land B \in X) \to ⋃ \{z \| \exists a \in [A] \underset{˙}{\sim} \exists b \in [B] \underset{˙}{\sim} z = a D b\} = A D B$
93	4 25 92	3eqtrd	$⊢ (D \in PsMet (X) \land A \in X \land B \in X) \to [A] \underset{˙}{\sim} pstoMet (D) [B] \underset{˙}{\sim} = A D B$

Metamath Proof Explorer

Theorem pstmfval

Proof