pstmval

Description: Value of the metric induced by a pseudometric D . (Contributed by Thierry Arnoux, 7-Feb-2018)

		Ref	Expression
	Hypothesis	pstmval.1	$⊢ \underset{˙}{\sim} = ~_{Met} (D)$
	Assertion	pstmval	$⊢ D \in PsMet (X) \to pstoMet (D) = (a \in (X / \underset{˙}{\sim}), b \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x D y\})$

Proof

Step	Hyp	Ref	Expression
1		pstmval.1	$⊢ \underset{˙}{\sim} = ~_{Met} (D)$
2		df-pstm	$⊢ pstoMet = (d \in ⋃ ran PsMet ⟼ (a \in (dom dom d / ~_{Met} (d)), b \in (dom dom d / ~_{Met} (d)) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x d y\}))$
3	2	a1i	$⊢ D \in PsMet (X) \to pstoMet = (d \in ⋃ ran PsMet ⟼ (a \in (dom dom d / ~_{Met} (d)), b \in (dom dom d / ~_{Met} (d)) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x d y\}))$
4		psmetdmdm	$⊢ D \in PsMet (X) \to X = dom dom D$
5	4	adantr	$⊢ (D \in PsMet (X) \land d = D) \to X = dom dom D$
6		dmeq	$⊢ d = D \to dom d = dom D$
7	6	dmeqd	$⊢ d = D \to dom dom d = dom dom D$
8	7	adantl	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d = dom dom D$
9	5 8	eqtr4d	$⊢ (D \in PsMet (X) \land d = D) \to X = dom dom d$
10		qseq1	$⊢ X = dom dom d \to X / \underset{˙}{\sim} = dom dom d / \underset{˙}{\sim}$
11	9 10	syl	$⊢ (D \in PsMet (X) \land d = D) \to X / \underset{˙}{\sim} = dom dom d / \underset{˙}{\sim}$
12		fveq2	$⊢ d = D \to ~_{Met} (d) = ~_{Met} (D)$
13	1 12	eqtr4id	$⊢ d = D \to \underset{˙}{\sim} = ~_{Met} (d)$
14		qseq2	$⊢ \underset{˙}{\sim} = ~_{Met} (d) \to dom dom d / \underset{˙}{\sim} = dom dom d / ~_{Met} (d)$
15	13 14	syl	$⊢ d = D \to dom dom d / \underset{˙}{\sim} = dom dom d / ~_{Met} (d)$
16	15	adantl	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d / \underset{˙}{\sim} = dom dom d / ~_{Met} (d)$
17	11 16	eqtr2d	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d / ~_{Met} (d) = X / \underset{˙}{\sim}$
18		mpoeq12	$⊢ (dom dom d / ~_{Met} (d) = X / \underset{˙}{\sim} \land dom dom d / ~_{Met} (d) = X / \underset{˙}{\sim}) \to (a \in (dom dom d / ~_{Met} (d)), b \in (dom dom d / ~_{Met} (d)) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x d y\}) = (a \in (X / \underset{˙}{\sim}), b \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x d y\})$
19	17 17 18	syl2anc	$⊢ (D \in PsMet (X) \land d = D) \to (a \in (dom dom d / ~_{Met} (d)), b \in (dom dom d / ~_{Met} (d)) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x d y\}) = (a \in (X / \underset{˙}{\sim}), b \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x d y\})$
20		simp1r	$⊢ ((D \in PsMet (X) \land d = D) \land a \in (X / \underset{˙}{\sim}) \land b \in (X / \underset{˙}{\sim})) \to d = D$
21	20	oveqd	$⊢ ((D \in PsMet (X) \land d = D) \land a \in (X / \underset{˙}{\sim}) \land b \in (X / \underset{˙}{\sim})) \to x d y = x D y$
22	21	eqeq2d	$⊢ ((D \in PsMet (X) \land d = D) \land a \in (X / \underset{˙}{\sim}) \land b \in (X / \underset{˙}{\sim})) \to (z = x d y \leftrightarrow z = x D y)$
23	22	2rexbidv	$⊢ ((D \in PsMet (X) \land d = D) \land a \in (X / \underset{˙}{\sim}) \land b \in (X / \underset{˙}{\sim})) \to (\exists x \in a \exists y \in b z = x d y \leftrightarrow \exists x \in a \exists y \in b z = x D y)$
24	23	abbidv	$⊢ ((D \in PsMet (X) \land d = D) \land a \in (X / \underset{˙}{\sim}) \land b \in (X / \underset{˙}{\sim})) \to \{z \| \exists x \in a \exists y \in b z = x d y\} = \{z \| \exists x \in a \exists y \in b z = x D y\}$
25	24	unieqd	$⊢ ((D \in PsMet (X) \land d = D) \land a \in (X / \underset{˙}{\sim}) \land b \in (X / \underset{˙}{\sim})) \to ⋃ \{z \| \exists x \in a \exists y \in b z = x d y\} = ⋃ \{z \| \exists x \in a \exists y \in b z = x D y\}$
26	25	mpoeq3dva	$⊢ (D \in PsMet (X) \land d = D) \to (a \in (X / \underset{˙}{\sim}), b \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x d y\}) = (a \in (X / \underset{˙}{\sim}), b \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x D y\})$
27	19 26	eqtrd	$⊢ (D \in PsMet (X) \land d = D) \to (a \in (dom dom d / ~_{Met} (d)), b \in (dom dom d / ~_{Met} (d)) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x d y\}) = (a \in (X / \underset{˙}{\sim}), b \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x D y\})$
28		elfvdm	$⊢ D \in PsMet (X) \to X \in dom PsMet$
29		fveq2	$⊢ x = X \to PsMet (x) = PsMet (X)$
30	29	eleq2d	$⊢ x = X \to (D \in PsMet (x) \leftrightarrow D \in PsMet (X))$
31	30	rspcev	$⊢ (X \in dom PsMet \land D \in PsMet (X)) \to \exists x \in dom PsMet D \in PsMet (x)$
32	28 31	mpancom	$⊢ D \in PsMet (X) \to \exists x \in dom PsMet D \in PsMet (x)$
33		df-psmet	$⊢ PsMet = (x \in V ⟼ \{d \in ({ℝ^{*}}^{(x \times x)}) \| \forall a \in x (a d a = 0 \land \forall b \in x \forall c \in x a d b \leq (c d a) +_{𝑒} (c d b))\})$
34	33	funmpt2	$⊢ Fun PsMet$
35		elunirn	$⊢ Fun PsMet \to (D \in ⋃ ran PsMet \leftrightarrow \exists x \in dom PsMet D \in PsMet (x))$
36	34 35	ax-mp	$⊢ D \in ⋃ ran PsMet \leftrightarrow \exists x \in dom PsMet D \in PsMet (x)$
37	32 36	sylibr	$⊢ D \in PsMet (X) \to D \in ⋃ ran PsMet$
38		elfvex	$⊢ D \in PsMet (X) \to X \in V$
39		qsexg	$⊢ X \in V \to X / \underset{˙}{\sim} \in V$
40	38 39	syl	$⊢ D \in PsMet (X) \to X / \underset{˙}{\sim} \in V$
41		mpoexga	$⊢ (X / \underset{˙}{\sim} \in V \land X / \underset{˙}{\sim} \in V) \to (a \in (X / \underset{˙}{\sim}), b \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x D y\}) \in V$
42	40 40 41	syl2anc	$⊢ D \in PsMet (X) \to (a \in (X / \underset{˙}{\sim}), b \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x D y\}) \in V$
43	3 27 37 42	fvmptd	$⊢ D \in PsMet (X) \to pstoMet (D) = (a \in (X / \underset{˙}{\sim}), b \in (X / \underset{˙}{\sim}) ⟼ ⋃ \{z \| \exists x \in a \exists y \in b z = x D y\})$

Metamath Proof Explorer

Theorem pstmval

Proof