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 ⊢ R ∈ TopSp ∧ I ∈ V → Y ∈ TopSp

Proof

Step Hyp Ref Expression
1 pwstps.y ⊢ Y = R ↑ 𝑠 I
2 eqid ⊢ Scalar ⁡ R = Scalar ⁡ R
3 1 2 pwsval ⊢ R ∈ TopSp ∧ I ∈ V → Y = Scalar ⁡ R ⨉ 𝑠 I × R
4 eqid ⊢ Scalar ⁡ R ⨉ 𝑠 I × R = Scalar ⁡ R ⨉ 𝑠 I × R
5 fvexd ⊢ R ∈ TopSp ∧ I ∈ V → Scalar ⁡ R ∈ V
6 simpr ⊢ R ∈ TopSp ∧ I ∈ V → I ∈ V
7 fconst6g ⊢ R ∈ TopSp → I × R : I ⟶ TopSp
8 7 adantr ⊢ R ∈ TopSp ∧ I ∈ V → I × R : I ⟶ TopSp
9 4 5 6 8 prdstps ⊢ R ∈ TopSp ∧ I ∈ V → Scalar ⁡ R ⨉ 𝑠 I × R ∈ TopSp
10 3 9 eqeltrd ⊢ R ∈ TopSp ∧ I ∈ V → Y ∈ TopSp