Metamath Proof Explorer


Theorem pwstps

Description: A structure power of a topological space is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Hypothesis pwstps.y Y=R𝑠I
Assertion pwstps RTopSpIVYTopSp

Proof

Step Hyp Ref Expression
1 pwstps.y Y=R𝑠I
2 eqid ScalarR=ScalarR
3 1 2 pwsval RTopSpIVY=ScalarR𝑠I×R
4 eqid ScalarR𝑠I×R=ScalarR𝑠I×R
5 fvexd RTopSpIVScalarRV
6 simpr RTopSpIVIV
7 fconst6g RTopSpI×R:ITopSp
8 7 adantr RTopSpIVI×R:ITopSp
9 4 5 6 8 prdstps RTopSpIVScalarR𝑠I×RTopSp
10 3 9 eqeltrd RTopSpIVYTopSp