Metamath Proof Explorer

Theorem 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		elfvunirn	$⊢ D \in PsMet (X) \to D \in ⋃ ran PsMet$
16		ovexd	$⊢ D \in PsMet (X) \to (X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)]) \in V$
17	1 14 15 16	fvmptd2	$⊢ D \in PsMet (X) \to metUnif (D) = (X \times X) filGen ran (a \in ℝ^{+} ⟼ D^{-1} [[0, a)])$