Description: The scalar ring of a topological module is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | tlmtrg.f | |
|
Assertion | tlmscatps | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tlmtrg.f | |
|
2 | 1 | tlmtrg | |
3 | trgtps | |
|
4 | 2 3 | syl | |