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=\mathrm{Scalar}\left(W\right)$$
Assertion	tlmscatps	$$⊢W\in \mathrm{TopMod}\to F\in \mathrm{TopSp}$$

Proof

Step	Hyp	Ref	Expression
1		tlmtrg.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2	1	tlmtrg	$$⊢W\in \mathrm{TopMod}\to F\in \mathrm{TopRing}$$
3		trgtps	$$⊢F\in \mathrm{TopRing}\to F\in \mathrm{TopSp}$$
4	2 3	syl	$$⊢W\in \mathrm{TopMod}\to F\in \mathrm{TopSp}$$