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 ) |
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 ) |