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 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
Assertion rrxtopn ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) = ( MetOpen ‘ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 rrxtopn.1 ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
2 eqid ⊢ ( ℝ^ ‘ 𝐼 ) = ( ℝ^ ‘ 𝐼 )
3 2 rrxval ⊢ ( 𝐼 ∈ 𝑉 → ( ℝ^ ‘ 𝐼 ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
4 1 3 syl ⊢ ( 𝜑 → ( ℝ^ ‘ 𝐼 ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
5 4 fveq2d ⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) = ( TopOpen ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
6 ovex ⊢ ( ℝfld freeLMod 𝐼 ) ∈ V
7 eqid ⊢ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) = ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) )
8 eqid ⊢ ( dist ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( dist ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
9 eqid ⊢ ( TopOpen ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( TopOpen ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) )
10 7 8 9 tcphtopn ⊢ ( ( ℝfld freeLMod 𝐼 ) ∈ V → ( TopOpen ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( MetOpen ‘ ( dist ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) ) )
11 6 10 ax-mp ⊢ ( TopOpen ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( MetOpen ‘ ( dist ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) )
12 11 a1i ⊢ ( 𝜑 → ( TopOpen ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( MetOpen ‘ ( dist ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) ) )
13 4 eqcomd ⊢ ( 𝜑 → ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) = ( ℝ^ ‘ 𝐼 ) )
14 13 fveq2d ⊢ ( 𝜑 → ( dist ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) = ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) )
15 14 fveq2d ⊢ ( 𝜑 → ( MetOpen ‘ ( dist ‘ ( toℂPreHil ‘ ( ℝfld freeLMod 𝐼 ) ) ) ) = ( MetOpen ‘ ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) ) )
16 5 12 15 3eqtrd ⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) = ( MetOpen ‘ ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) ) )
17 eqid ⊢ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( Base ‘ ( ℝ^ ‘ 𝐼 ) )
18 2 17 rrxds ⊢ ( 𝐼 ∈ 𝑉 → ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) = ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) )
19 1 18 syl ⊢ ( 𝜑 → ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) = ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) )
20 19 eqcomd ⊢ ( 𝜑 → ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) = ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) )
21 20 fveq2d ⊢ ( 𝜑 → ( MetOpen ‘ ( dist ‘ ( ℝ^ ‘ 𝐼 ) ) ) = ( MetOpen ‘ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) ) )
22 16 21 eqtrd ⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) = ( MetOpen ‘ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) ) )