metuval

Description: Value of the uniform structure generated by metric D . (Contributed by Thierry Arnoux, 1-Dec-2017) (Revised by Thierry Arnoux, 11-Feb-2018)

		Ref	Expression
	Assertion	metuval	$⊢ D \in PsMet (X) \to metUnif (D) = (X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$

Proof

Step	Hyp	Ref	Expression
1		df-metu	$⊢ metUnif = (d \in ⋃ ran PsMet ⟼ (dom dom d \times dom dom d) filGen ran (a \in ℝ^{+} ⟼ d^{-1} [[0, a)]))$
2		simpr	$⊢ (D \in PsMet (X) \land d = D) \to d = D$
3	2	dmeqd	$⊢ (D \in PsMet (X) \land d = D) \to dom d = dom D$
4	3	dmeqd	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d = dom dom D$
5		psmetdmdm	$⊢ D \in PsMet (X) \to X = dom dom D$
6	5	adantr	$⊢ (D \in PsMet (X) \land d = D) \to X = dom dom D$
7	4 6	eqtr4d	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d = X$
8	7	sqxpeqd	$⊢ (D \in PsMet (X) \land d = D) \to dom dom d \times dom dom d = X \times X$
9		simplr	$⊢ ((D \in PsMet (X) \land d = D) \land a \in ℝ^{+}) \to d = D$
10	9	cnveqd	$⊢ ((D \in PsMet (X) \land d = D) \land a \in ℝ^{+}) \to d^{-1} = D^{-1}$
11	10	imaeq1d	$⊢ ((D \in PsMet (X) \land d = D) \land a \in ℝ^{+}) \to d^{-1} [[0, a)] = D^{-1} [[0, a)]$
12	11	mpteq2dva	$⊢ (D \in PsMet (X) \land d = D) \to (a \in ℝ^{+} ⟼ d^{-1} [[0, a)]) = (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
13	12	rneqd	$⊢ (D \in PsMet (X) \land d = D) \to ran (a \in ℝ^{+} ⟼ d^{-1} [[0, a)]) = ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
14	8 13	oveq12d	$⊢ (D \in PsMet (X) \land d = D) \to (dom dom d \times dom dom d) filGen ran (a \in ℝ^{+} ⟼ d^{-1} [[0, a)]) = (X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$
15		elfvdm	$⊢ D \in PsMet (X) \to X \in dom PsMet$
16		fveq2	$⊢ x = X \to PsMet (x) = PsMet (X)$
17	16	eleq2d	$⊢ x = X \to (D \in PsMet (x) \leftrightarrow D \in PsMet (X))$
18	17	rspcev	$⊢ (X \in dom PsMet \land D \in PsMet (X)) \to \exists x \in dom PsMet D \in PsMet (x)$
19	15 18	mpancom	$⊢ D \in PsMet (X) \to \exists x \in dom PsMet D \in PsMet (x)$
20		df-psmet	$⊢ PsMet = (y \in V ⟼ \{u \in ({ℝ^{*}}^{(y \times y)}) \| \forall z \in y (z u z = 0 \land \forall w \in y \forall v \in y z u w \leq (v u z) +_{𝑒} (v u w))\})$
21	20	funmpt2	$⊢ Fun PsMet$
22		elunirn	$⊢ Fun PsMet \to (D \in ⋃ ran PsMet \leftrightarrow \exists x \in dom PsMet D \in PsMet (x))$
23	21 22	ax-mp	$⊢ D \in ⋃ ran PsMet \leftrightarrow \exists x \in dom PsMet D \in PsMet (x)$
24	19 23	sylibr	$⊢ D \in PsMet (X) \to D \in ⋃ ran PsMet$
25		ovexd	$⊢ D \in PsMet (X) \to (X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \in V$
26	1 14 24 25	fvmptd2	$⊢ D \in PsMet (X) \to metUnif (D) = (X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$

Metamath Proof Explorer

Theorem metuval

Proof