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 F=ScalarW
Assertion tlmscatps WTopModFTopSp

Proof

Step Hyp Ref Expression
1 tlmtrg.f F=ScalarW
2 1 tlmtrg WTopModFTopRing
3 trgtps FTopRingFTopSp
4 2 3 syl WTopModFTopSp