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		psmetdmdm	$⊢ D \in PsMet (X) \to X = dom dom D$
4	3	adantr	$⊢ (D \in PsMet (X) \land d = D) \to X = dom dom D$
5		dmeq	$⊢ d = D \to dom d = dom D$
6	5	dmeqd	$⊢ d = D \to dom dom d = dom dom D$
7	6	adantl	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d = dom dom D$
8	4 7	eqtr4d	$⊢ (D \in PsMet (X) \land d = D) \to X = dom dom d$
9		qseq1	$⊢ X = dom dom d \to X / \underset{˙}{\sim} = dom dom d / \underset{˙}{\sim}$
10	8 9	syl	$⊢ (D \in PsMet (X) \land d = D) \to X / \underset{˙}{\sim} = dom dom d / \underset{˙}{\sim}$
11		fveq2	$⊢ d = D \to ~_{Met} (d) = ~_{Met} (D)$
12	1 11	eqtr4id	$⊢ d = D \to \underset{˙}{\sim} = ~_{Met} (d)$
13	12	qseq2d	$⊢ d = D \to dom dom d / \underset{˙}{\sim} = dom dom d / ~_{Met} (d)$
14	13	adantl	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d / \underset{˙}{\sim} = dom dom d / ~_{Met} (d)$
15	10 14	eqtr2d	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d / ~_{Met} (d) = X / \underset{˙}{\sim}$
16		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\})$
17	15 15 16	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\})$
18		simp1r	$⊢ ((D \in PsMet (X) \land d = D) \land a \in (X / \underset{˙}{\sim}) \land b \in (X / \underset{˙}{\sim})) \to d = D$
19	18	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$
20	19	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)$
21	20	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)$
22	21	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\}$
23	22	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\}$
24	23	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\})$
25	17 24	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\})$
26		elfvunirn	$⊢ D \in PsMet (X) \to D \in ⋃ ran PsMet$
27		elfvex	$⊢ D \in PsMet (X) \to X \in V$
28		qsexg	$⊢ X \in V \to X / \underset{˙}{\sim} \in V$
29	27 28	syl	$⊢ D \in PsMet (X) \to X / \underset{˙}{\sim} \in V$
30		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$
31	29 29 30	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$
32	2 25 26 31	fvmptd2	$⊢ 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