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 elfvdm ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝑋 ∈ dom PsMet )
16 fveq2 ⊢ ( 𝑥 = 𝑋 → ( PsMet ‘ 𝑥 ) = ( PsMet ‘ 𝑋 ) )
17 16 eleq2d ⊢ ( 𝑥 = 𝑋 → ( 𝐷 ∈ ( PsMet ‘ 𝑥 ) ↔ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) )
18 17 rspcev ⊢ ( ( 𝑋 ∈ dom PsMet ∧ 𝐷 ∈ ( PsMet ‘ 𝑋 ) ) → ∃ 𝑥 ∈ dom PsMet 𝐷 ∈ ( PsMet ‘ 𝑥 ) )
19 15 18 mpancom ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ∃ 𝑥 ∈ dom PsMet 𝐷 ∈ ( PsMet ‘ 𝑥 ) )
20 df-psmet ⊢ PsMet = ( 𝑦 ∈ V ↦ { 𝑢 ∈ ( ℝ* ↑m ( 𝑦 × 𝑦 ) ) ∣ ∀ 𝑧 ∈ 𝑦 ( ( 𝑧 𝑢 𝑧 ) = 0 ∧ ∀ 𝑤 ∈ 𝑦 ∀ 𝑣 ∈ 𝑦 ( 𝑧 𝑢 𝑤 ) ≤ ( ( 𝑣 𝑢 𝑧 ) +𝑒 ( 𝑣 𝑢 𝑤 ) ) ) } )
21 20 funmpt2 ⊢ Fun PsMet
22 elunirn ⊢ ( Fun PsMet → ( 𝐷 ∈ ∪ ran PsMet ↔ ∃ 𝑥 ∈ dom PsMet 𝐷 ∈ ( PsMet ‘ 𝑥 ) ) )
23 21 22 ax-mp ⊢ ( 𝐷 ∈ ∪ ran PsMet ↔ ∃ 𝑥 ∈ dom PsMet 𝐷 ∈ ( PsMet ‘ 𝑥 ) )
24 19 23 sylibr ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 ∈ ∪ ran PsMet )
25 ovexd ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) ∈ V )
26 1 14 24 25 fvmptd2 ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( metUnif ‘ 𝐷 ) = ( ( 𝑋 × 𝑋 ) filGen ran ( 𝑎 ∈ ℝ+ ↦ ( ◡ 𝐷 “ ( 0 [,) 𝑎 ) ) ) ) )