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 )