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 
|- ( ph -> I e. V )
Assertion 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 ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 rrxtopn.1 
 |-  ( ph -> I e. V )
2 eqid 
 |-  ( RR^ ` I ) = ( RR^ ` I )
3 2 rrxval 
 |-  ( I e. V -> ( RR^ ` I ) = ( toCPreHil ` ( RRfld freeLMod I ) ) )
4 1 3 syl 
 |-  ( ph -> ( RR^ ` I ) = ( toCPreHil ` ( RRfld freeLMod I ) ) )
5 4 fveq2d 
 |-  ( ph -> ( TopOpen ` ( RR^ ` I ) ) = ( TopOpen ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
6 ovex 
 |-  ( RRfld freeLMod I ) e. _V
7 eqid 
 |-  ( toCPreHil ` ( RRfld freeLMod I ) ) = ( toCPreHil ` ( RRfld freeLMod I ) )
8 eqid 
 |-  ( dist ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( dist ` ( toCPreHil ` ( RRfld freeLMod I ) ) )
9 eqid 
 |-  ( TopOpen ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( TopOpen ` ( toCPreHil ` ( RRfld freeLMod I ) ) )
10 7 8 9 tcphtopn 
 |-  ( ( RRfld freeLMod I ) e. _V -> ( TopOpen ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( MetOpen ` ( dist ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) ) )
11 6 10 ax-mp 
 |-  ( TopOpen ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( MetOpen ` ( dist ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) )
12 11 a1i 
 |-  ( ph -> ( TopOpen ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( MetOpen ` ( dist ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) ) )
13 4 eqcomd 
 |-  ( ph -> ( toCPreHil ` ( RRfld freeLMod I ) ) = ( RR^ ` I ) )
14 13 fveq2d 
 |-  ( ph -> ( dist ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) = ( dist ` ( RR^ ` I ) ) )
15 14 fveq2d 
 |-  ( ph -> ( MetOpen ` ( dist ` ( toCPreHil ` ( RRfld freeLMod I ) ) ) ) = ( MetOpen ` ( dist ` ( RR^ ` I ) ) ) )
16 5 12 15 3eqtrd 
 |-  ( ph -> ( TopOpen ` ( RR^ ` I ) ) = ( MetOpen ` ( dist ` ( RR^ ` I ) ) ) )
17 eqid 
 |-  ( Base ` ( RR^ ` I ) ) = ( Base ` ( RR^ ` I ) )
18 2 17 rrxds 
 |-  ( I e. V -> ( f e. ( Base ` ( RR^ ` I ) ) , g e. ( Base ` ( RR^ ` I ) ) |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) = ( dist ` ( RR^ ` I ) ) )
19 1 18 syl 
 |-  ( ph -> ( f e. ( Base ` ( RR^ ` I ) ) , g e. ( Base ` ( RR^ ` I ) ) |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) = ( dist ` ( RR^ ` I ) ) )
20 19 eqcomd 
 |-  ( ph -> ( dist ` ( RR^ ` I ) ) = ( f e. ( Base ` ( RR^ ` I ) ) , g e. ( Base ` ( RR^ ` I ) ) |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) )
21 20 fveq2d 
 |-  ( ph -> ( MetOpen ` ( dist ` ( RR^ ` I ) ) ) = ( MetOpen ` ( f e. ( Base ` ( RR^ ` I ) ) , g e. ( Base ` ( RR^ ` I ) ) |-> ( sqrt ` ( RRfld gsum ( x e. I |-> ( ( ( f ` x ) - ( g ` x ) ) ^ 2 ) ) ) ) ) ) )
22 16 21 eqtrd 
 |-  ( 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 ) ) ) ) ) ) )