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 ⁡ I = MetOpen ⁡ f ∈ Base I , g ∈ Base I ⟼ ∑ ℝ fld x ∈ I f ⁡ x − g ⁡ x 2

Proof

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