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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	tlmscatps	⊢ ( 𝑊 ∈ TopMod → 𝐹 ∈ TopSp )

Proof

Step	Hyp	Ref	Expression
1		tlmtrg.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2	1	tlmtrg	⊢ ( 𝑊 ∈ TopMod → 𝐹 ∈ TopRing )
3		trgtps	⊢ ( 𝐹 ∈ TopRing → 𝐹 ∈ TopSp )
4	2 3	syl	⊢ ( 𝑊 ∈ TopMod → 𝐹 ∈ TopSp )