This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐷 ∈ ( 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 [,) 𝑎 ) ) ) ) )