Description: The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | tlmtrg.f | ⊢ 𝐹 = ( Scalar ‘ 𝑊 ) | |
Assertion | tlmscatps | ⊢ ( 𝑊 ∈ TopMod → 𝐹 ∈ TopSp ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tlmtrg.f | ⊢ 𝐹 = ( Scalar ‘ 𝑊 ) | |
2 | 1 | tlmtrg | ⊢ ( 𝑊 ∈ TopMod → 𝐹 ∈ TopRing ) |
3 | trgtps | ⊢ ( 𝐹 ∈ TopRing → 𝐹 ∈ TopSp ) | |
4 | 2 3 | syl | ⊢ ( 𝑊 ∈ TopMod → 𝐹 ∈ TopSp ) |