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	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		df-metu	⊢ metUnif = ( 𝑑 ∈ ∪ ran PsMet ↦ ( ( dom dom 𝑑 × dom dom 𝑑 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝑑 “ ( 0 [,) 𝑎 ) ) ) ) )
2		simpr	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
3	2	dmeqd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom 𝑑 = dom 𝐷 )
4	3	dmeqd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom dom 𝑑 = dom dom 𝐷 )
5		psmetdmdm	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 = dom dom 𝐷 )
6	5	adantr	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑋 = dom dom 𝐷 )
7	4 6	eqtr4d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom dom 𝑑 = 𝑋 )
8	7	sqxpeqd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( dom dom 𝑑 × dom dom 𝑑 ) = ( 𝑋 × 𝑋 ) )
9		simplr	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ℝ+ ) → 𝑑 = 𝐷 )
10	9	cnveqd	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ℝ+ ) → ◡ 𝑑 = ◡ 𝐷 )
11	10	imaeq1d	⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) ∧ 𝑎 ∈ ℝ+ ) → ( ◡ 𝑑 “ ( 0 [,) 𝑎 ) ) = ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) )
12	11	mpteq2dva	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝑑 “ ( 0 [,) 𝑎 ) ) ) = ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
13	12	rneqd	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝑑 “ ( 0 [,) 𝑎 ) ) ) = ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) )
14	8 13	oveq12d	⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( ( dom dom 𝑑 × dom dom 𝑑 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝑑 “ ( 0 [,) 𝑎 ) ) ) ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) )
15		elfvunirn	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 ∈ ∪ ran PsMet )
16		ovexd	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∈ V )
17	1 14 15 16	fvmptd2	⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) )