Metamath Proof Explorer

Theorem rrxtopn

Description: The topology of the generalized real Euclidean space. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypothesis rrxtopn.1 ⊢φ→I∈V
Assertion rrxtopn ⊢φ→TopOpen⁡msup=MetOpen⁡f∈Basemsup,g∈Basemsup⟼∑ℝfldx∈If⁡x−g⁡x2

Proof

Step Hyp Ref Expression
1 rrxtopn.1 ⊢φ→I∈V
2 eqid ⊢msup=msup
3 2 rrxval ⊢I∈V→msup=toCPreHil⁡ℝfldfreeLModI
4 1 3 syl ⊢φ→msup=toCPreHil⁡ℝfldfreeLModI
5 4 fveq2d ⊢φ→TopOpen⁡msup=TopOpen⁡toCPreHil⁡ℝfldfreeLModI
6 ovex ⊢ℝfldfreeLModI∈V
7 eqid ⊢toCPreHil⁡ℝfldfreeLModI=toCPreHil⁡ℝfldfreeLModI
8 eqid ⊢dist⁡toCPreHil⁡ℝfldfreeLModI=dist⁡toCPreHil⁡ℝfldfreeLModI
9 eqid ⊢TopOpen⁡toCPreHil⁡ℝfldfreeLModI=TopOpen⁡toCPreHil⁡ℝfldfreeLModI
10 7 8 9 tcphtopn ⊢ℝfldfreeLModI∈V→TopOpen⁡toCPreHil⁡ℝfldfreeLModI=MetOpen⁡dist⁡toCPreHil⁡ℝfldfreeLModI
11 6 10 ax-mp ⊢TopOpen⁡toCPreHil⁡ℝfldfreeLModI=MetOpen⁡dist⁡toCPreHil⁡ℝfldfreeLModI
12 11 a1i ⊢φ→TopOpen⁡toCPreHil⁡ℝfldfreeLModI=MetOpen⁡dist⁡toCPreHil⁡ℝfldfreeLModI
13 4 eqcomd ⊢φ→toCPreHil⁡ℝfldfreeLModI=msup
14 13 fveq2d ⊢φ→dist⁡toCPreHil⁡ℝfldfreeLModI=dist⁡msup
15 14 fveq2d ⊢φ→MetOpen⁡dist⁡toCPreHil⁡ℝfldfreeLModI=MetOpen⁡dist⁡msup
16 5 12 15 3eqtrd ⊢φ→TopOpen⁡msup=MetOpen⁡dist⁡msup
17 eqid ⊢Basemsup=Basemsup
18 2 17 rrxds ⊢I∈V→f∈Basemsup,g∈Basemsup⟼∑ℝfldx∈If⁡x−g⁡x2=dist⁡msup
19 1 18 syl ⊢φ→f∈Basemsup,g∈Basemsup⟼∑ℝfldx∈If⁡x−g⁡x2=dist⁡msup
20 19 eqcomd ⊢φ→dist⁡msup=f∈Basemsup,g∈Basemsup⟼∑ℝfldx∈If⁡x−g⁡x2
21 20 fveq2d ⊢φ→MetOpen⁡dist⁡msup=MetOpen⁡f∈Basemsup,g∈Basemsup⟼∑ℝfldx∈If⁡x−g⁡x2
22 16 21 eqtrd ⊢φ→TopOpen⁡msup=MetOpen⁡f∈Basemsup,g∈Basemsup⟼∑ℝfldx∈If⁡x−g⁡x2