Metamath Proof Explorer

Theorem rrxtps

Description: Generalized Euclidean real spaces are topological spaces. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Assertion rrxtps 
|- ( I e. V -> ( RR^ ` I ) e. TopSp )

Proof

Step Hyp Ref Expression
1 rrxngp 
 |-  ( I e. V -> ( RR^ ` I ) e. NrmGrp )
2 ngptps 
 |-  ( ( RR^ ` I ) e. NrmGrp -> ( RR^ ` I ) e. TopSp )
3 1 2 syl 
 |-  ( I e. V -> ( RR^ ` I ) e. TopSp )