Metamath Proof Explorer


Theorem tlmscatps

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 )

Proof

Step Hyp Ref Expression
1 tlmtrg.f 𝐹 = ( Scalar ‘ 𝑊 )
2 1 tlmtrg ( 𝑊 ∈ TopMod → 𝐹 ∈ TopRing )
3 trgtps ( 𝐹 ∈ TopRing → 𝐹 ∈ TopSp )
4 2 3 syl ( 𝑊 ∈ TopMod → 𝐹 ∈ TopSp )