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 = ( Scalar ` W )
Assertion tlmscatps
|- ( W e. TopMod -> F e. TopSp )

Proof

Step Hyp Ref Expression
1 tlmtrg.f
 |-  F = ( Scalar ` W )
2 1 tlmtrg
 |-  ( W e. TopMod -> F e. TopRing )
3 trgtps
 |-  ( F e. TopRing -> F e. TopSp )
4 2 3 syl
 |-  ( W e. TopMod -> F e. TopSp )