Theorem vscacn

Description: The scalar multiplication is continuous in a topological module. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypotheses	istlm.s	⊢ · = ( ·sf ‘ 𝑊 )
	istlm.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
	istlm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	istlm.k	⊢ 𝐾 = ( TopOpen ‘ 𝐹 )
Assertion	vscacn	⊢ ( 𝑊 ∈ TopMod → · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )

Proof

Step	Hyp	Ref	Expression
1		istlm.s	⊢ · = ( ·sf ‘ 𝑊 )
2		istlm.j	⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
3		istlm.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4		istlm.k	⊢ 𝐾 = ( TopOpen ‘ 𝐹 )
5	1 2 3 4	istlm	⊢ ( 𝑊 ∈ TopMod ↔ ( ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ TopRing ) ∧ · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ) )
6	5	simprbi	⊢ ( 𝑊 ∈ TopMod → · ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) )