Metamath Proof Explorer

Theorem rrxtopnfi

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

Ref Expression
Hypothesis rrxtopnfi.1 ⊢ ( 𝜑 → 𝐼 ∈ Fin )
Assertion rrxtopnfi ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) = ( MetOpen ‘ ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 rrxtopnfi.1 ⊢ ( 𝜑 → 𝐼 ∈ Fin )
2 1 rrxtopn ⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) = ( MetOpen ‘ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) ) )
3 eqid ⊢ ( ℝ^ ‘ 𝐼 ) = ( ℝ^ ‘ 𝐼 )
4 eqid ⊢ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( Base ‘ ( ℝ^ ‘ 𝐼 ) )
5 1 3 4 rrxbasefi ⊢ ( 𝜑 → ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( ℝ ↑m 𝐼 ) )
6 5 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) → ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( ℝ ↑m 𝐼 ) )
7 simpl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ∧ 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) ) → 𝜑 )
8 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ∧ 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) ) → 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) )
9 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) → 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) )
10 9 6 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) → 𝑓 ∈ ( ℝ ↑m 𝐼 ) )
11 8 10 syldan ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ∧ 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) ) → 𝑓 ∈ ( ℝ ↑m 𝐼 ) )
12 simprr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ∧ 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) ) → 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) )
13 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) → 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) )
14 5 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) → ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( ℝ ↑m 𝐼 ) )
15 13 14 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) → 𝑔 ∈ ( ℝ ↑m 𝐼 ) )
16 12 15 syldan ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ∧ 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) ) → 𝑔 ∈ ( ℝ ↑m 𝐼 ) )
17 elmapi ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) → 𝑓 : 𝐼 ⟶ ℝ )
18 17 adantr ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → 𝑓 : 𝐼 ⟶ ℝ )
19 18 ffvelrnda ⊢ ( ( ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℝ )
20 elmapi ⊢ ( 𝑔 ∈ ( ℝ ↑m 𝐼 ) → 𝑔 : 𝐼 ⟶ ℝ )
21 20 adantl ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → 𝑔 : 𝐼 ⟶ ℝ )
22 21 ffvelrnda ⊢ ( ( ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑥 ) ∈ ℝ )
23 19 22 resubcld ⊢ ( ( ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ∈ ℝ )
24 23 resqcld ⊢ ( ( ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ∈ ℝ )
25 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) )
26 24 25 fmptd ⊢ ( ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) : 𝐼 ⟶ ℝ )
27 26 3adant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) : 𝐼 ⟶ ℝ )
28 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → 𝐼 ∈ Fin )
29 0red ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → 0 ∈ ℝ )
30 27 28 29 fidmfisupp ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) finSupp 0 )
31 regsumsupp ⊢ ( ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) : 𝐼 ⟶ ℝ ∧ ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) finSupp 0 ∧ 𝐼 ∈ Fin ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) = Σ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) )
32 27 30 28 31 syl3anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) = Σ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) )
33 ax-resscn ⊢ ℝ ⊆ ℂ
34 33 a1i ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) → ℝ ⊆ ℂ )
35 17 34 fssd ⊢ ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) → 𝑓 : 𝐼 ⟶ ℂ )
36 35 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → 𝑓 : 𝐼 ⟶ ℂ )
37 36 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑓 ‘ 𝑥 ) ∈ ℂ )
38 33 a1i ⊢ ( 𝑔 ∈ ( ℝ ↑m 𝐼 ) → ℝ ⊆ ℂ )
39 20 38 fssd ⊢ ( 𝑔 ∈ ( ℝ ↑m 𝐼 ) → 𝑔 : 𝐼 ⟶ ℂ )
40 39 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → 𝑔 : 𝐼 ⟶ ℂ )
41 40 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( 𝑔 ‘ 𝑥 ) ∈ ℂ )
42 37 41 subcld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ∈ ℂ )
43 42 sqcld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑥 ∈ 𝐼 ) → ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ∈ ℂ )
44 43 25 fmptd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) : 𝐼 ⟶ ℂ )
45 28 44 fsumsupp0 ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → Σ 𝑘 ∈ ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) supp 0 ) ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) = Σ 𝑘 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) )
46 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) )
47 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑘 ) )
48 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑘 ) )
49 47 48 oveq12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) = ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) )
50 49 oveq1d ⊢ ( 𝑥 = 𝑘 → ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) = ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) )
51 50 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑘 ∈ 𝐼 ) ∧ 𝑥 = 𝑘 ) → ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) = ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) )
52 simpr ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑘 ∈ 𝐼 ) → 𝑘 ∈ 𝐼 )
53 ovexd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ∈ V )
54 46 51 52 53 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) ∧ 𝑘 ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) = ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) )
55 54 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → Σ 𝑘 ∈ 𝐼 ( ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ‘ 𝑘 ) = Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) )
56 32 45 55 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) = Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) )
57 56 fveq2d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( ℝ ↑m 𝐼 ) ∧ 𝑔 ∈ ( ℝ ↑m 𝐼 ) ) → ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) )
58 7 11 16 57 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ∧ 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ) ) → ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) = ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) )
59 5 6 58 mpoeq123dva ⊢ ( 𝜑 → ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) = ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
60 59 fveq2d ⊢ ( 𝜑 → ( MetOpen ‘ ( 𝑓 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) , 𝑔 ∈ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) ↦ ( √ ‘ ( ℝfld Σg ( 𝑥 ∈ 𝐼 ↦ ( ( ( 𝑓 ‘ 𝑥 ) − ( 𝑔 ‘ 𝑥 ) ) ↑ 2 ) ) ) ) ) ) = ( MetOpen ‘ ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) )
61 2 60 eqtrd ⊢ ( 𝜑 → ( TopOpen ‘ ( ℝ^ ‘ 𝐼 ) ) = ( MetOpen ‘ ( 𝑓 ∈ ( ℝ ↑m 𝐼 ) , 𝑔 ∈ ( ℝ ↑m 𝐼 ) ↦ ( √ ‘ Σ 𝑘 ∈ 𝐼 ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) ) )