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 
|- ( ph -> I e. Fin )
Assertion rrxtopnfi 
|- ( ph -> ( TopOpen ` ( RR^ ` I ) ) = ( MetOpen ` ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 rrxtopnfi.1 
 |-  ( ph -> I e. Fin )
2 1 rrxtopn 
 |-  ( ph -> ( TopOpen ` ( RR^ ` I ) ) = ( MetOpen ` ( f e. ( Base ` ( RR^ ` I ) ) , g e. ( Base ` ( RR^ ` I ) ) |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) ) )
3 eqid 
 |-  ( RR^ ` I ) = ( RR^ ` I )
4 eqid 
 |-  ( Base ` ( RR^ ` I ) ) = ( Base ` ( RR^ ` I ) )
5 1 3 4 rrxbasefi 
 |-  ( ph -> ( Base ` ( RR^ ` I ) ) = ( RR ^m I ) )
6 5 adantr 
 |-  ( ( ph /\ f e. ( Base ` ( RR^ ` I ) ) ) -> ( Base ` ( RR^ ` I ) ) = ( RR ^m I ) )
7 simpl 
 |-  ( ( ph /\ ( f e. ( Base ` ( RR^ ` I ) ) /\ g e. ( Base ` ( RR^ ` I ) ) ) ) -> ph )
8 simprl 
 |-  ( ( ph /\ ( f e. ( Base ` ( RR^ ` I ) ) /\ g e. ( Base ` ( RR^ ` I ) ) ) ) -> f e. ( Base ` ( RR^ ` I ) ) )
9 simpr 
 |-  ( ( ph /\ f e. ( Base ` ( RR^ ` I ) ) ) -> f e. ( Base ` ( RR^ ` I ) ) )
10 9 6 eleqtrd 
 |-  ( ( ph /\ f e. ( Base ` ( RR^ ` I ) ) ) -> f e. ( RR ^m I ) )
11 8 10 syldan 
 |-  ( ( ph /\ ( f e. ( Base ` ( RR^ ` I ) ) /\ g e. ( Base ` ( RR^ ` I ) ) ) ) -> f e. ( RR ^m I ) )
12 simprr 
 |-  ( ( ph /\ ( f e. ( Base ` ( RR^ ` I ) ) /\ g e. ( Base ` ( RR^ ` I ) ) ) ) -> g e. ( Base ` ( RR^ ` I ) ) )
13 simpr 
 |-  ( ( ph /\ g e. ( Base ` ( RR^ ` I ) ) ) -> g e. ( Base ` ( RR^ ` I ) ) )
14 5 adantr 
 |-  ( ( ph /\ g e. ( Base ` ( RR^ ` I ) ) ) -> ( Base ` ( RR^ ` I ) ) = ( RR ^m I ) )
15 13 14 eleqtrd 
 |-  ( ( ph /\ g e. ( Base ` ( RR^ ` I ) ) ) -> g e. ( RR ^m I ) )
16 12 15 syldan 
 |-  ( ( ph /\ ( f e. ( Base ` ( RR^ ` I ) ) /\ g e. ( Base ` ( RR^ ` I ) ) ) ) -> g e. ( RR ^m I ) )
17 elmapi 
 |-  ( f e. ( RR ^m I ) -> f : I --> RR )
18 17 adantr 
 |-  ( ( f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> f : I --> RR )
19 18 ffvelcdmda 
 |-  ( ( ( f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) /\ x e. I ) -> ( f ` x ) e. RR )
20 elmapi 
 |-  ( g e. ( RR ^m I ) -> g : I --> RR )
21 20 adantl 
 |-  ( ( f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> g : I --> RR )
22 21 ffvelcdmda 
 |-  ( ( ( f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) /\ x e. I ) -> ( g ` x ) e. RR )
23 19 22 resubcld 
 |-  ( ( ( f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) /\ x e. I ) -> ( ( f ` x ) - ( g ` x ) ) e. RR )
24 23 resqcld 
 |-  ( ( ( f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) /\ x e. I ) -> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) e. RR )
25 eqid 
 |-  ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) = ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) )
26 24 25 fmptd 
 |-  ( ( f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) : I --> RR )
27 26 3adant1 
 |-  ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) : I --> RR )
28 1 3ad2ant1 
 |-  ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> I e. Fin )
29 0red 
 |-  ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> 0 e. RR )
30 27 28 29 fidmfisupp 
 |-  ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) finSupp 0 )
31 regsumsupp 
 |-  ( ( ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) : I --> RR /\ ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) finSupp 0 /\ I e. Fin ) -> ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) = sum_ k e. ( ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) supp 0 ) ( ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ` k ) )
32 27 30 28 31 syl3anc 
 |-  ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) = sum_ k e. ( ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) supp 0 ) ( ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ` k ) )
33 ax-resscn 
 |-  RR C_ CC
34 33 a1i 
 |-  ( f e. ( RR ^m I ) -> RR C_ CC )
35 17 34 fssd 
 |-  ( f e. ( RR ^m I ) -> f : I --> CC )
36 35 3ad2ant2 
 |-  ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> f : I --> CC )
37 36 ffvelcdmda 
 |-  ( ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) /\ x e. I ) -> ( f ` x ) e. CC )
38 33 a1i 
 |-  ( g e. ( RR ^m I ) -> RR C_ CC )
39 20 38 fssd 
 |-  ( g e. ( RR ^m I ) -> g : I --> CC )
40 39 3ad2ant3 
 |-  ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> g : I --> CC )
41 40 ffvelcdmda 
 |-  ( ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) /\ x e. I ) -> ( g ` x ) e. CC )
42 37 41 subcld 
 |-  ( ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) /\ x e. I ) -> ( ( f ` x ) - ( g ` x ) ) e. CC )
43 42 sqcld 
 |-  ( ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) /\ x e. I ) -> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) e. CC )
44 43 25 fmptd 
 |-  ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) : I --> CC )
45 28 44 fsumsupp0 
 |-  ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> sum_ k e. ( ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) supp 0 ) ( ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ` k ) = sum_ k e. I ( ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ` k ) )
46 eqidd 
 |-  ( ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) /\ k e. I ) -> ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) = ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) )
47 fveq2 
 |-  ( x = k -> ( f ` x ) = ( f ` k ) )
48 fveq2 
 |-  ( x = k -> ( g ` x ) = ( g ` k ) )
49 47 48 oveq12d 
 |-  ( x = k -> ( ( f ` x ) - ( g ` x ) ) = ( ( f ` k ) - ( g ` k ) ) )
50 49 oveq1d 
 |-  ( x = k -> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) = ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) )
51 50 adantl 
 |-  ( ( ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) /\ k e. I ) /\ x = k ) -> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) = ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) )
52 simpr 
 |-  ( ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) /\ k e. I ) -> k e. I )
53 ovexd 
 |-  ( ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) /\ k e. I ) -> ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) e. _V )
54 46 51 52 53 fvmptd 
 |-  ( ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) /\ k e. I ) -> ( ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ` k ) = ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) )
55 54 sumeq2dv 
 |-  ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> sum_ k e. I ( ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ` k ) = sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) )
56 32 45 55 3eqtrd 
 |-  ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) = sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) )
57 56 fveq2d 
 |-  ( ( ph /\ f e. ( RR ^m I ) /\ g e. ( RR ^m I ) ) -> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) = ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )
58 7 11 16 57 syl3anc 
 |-  ( ( ph /\ ( f e. ( Base ` ( RR^ ` I ) ) /\ g e. ( Base ` ( RR^ ` I ) ) ) ) -> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) = ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) )
59 5 6 58 mpoeq123dva 
 |-  ( ph -> ( f e. ( Base ` ( RR^ ` I ) ) , g e. ( Base ` ( RR^ ` I ) ) |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) = ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) )
60 59 fveq2d 
 |-  ( ph -> ( MetOpen ` ( f e. ( Base ` ( RR^ ` I ) ) , g e. ( Base ` ( RR^ ` I ) ) |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) ) = ( MetOpen ` ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) ) )
61 2 60 eqtrd 
 |-  ( ph -> ( TopOpen ` ( RR^ ` I ) ) = ( MetOpen ` ( f e. ( RR ^m I ) , g e. ( RR ^m I ) |-> ( sqrt ` sum_ k e. I ( ( ( f ` k ) - ( g ` k ) ) ^ 2 ) ) ) ) )