Theorem vscacn

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

	Ref	Expression
Hypotheses	istlm.s	$$⊢\underset{\dot{}}{·}={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
	istlm.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
	istlm.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
	istlm.k	$$⊢K=\mathrm{TopOpen}\left(F\right)$$
Assertion	vscacn	$$⊢W\in \mathrm{TopMod}\to \underset{\dot{}}{·}\in \left(\left(K{\times }_{t}J\right)\mathrm{Cn}J\right)$$

Proof

Step	Hyp	Ref	Expression
1		istlm.s	$$⊢\underset{\dot{}}{·}={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
2		istlm.j	$$⊢J=\mathrm{TopOpen}\left(W\right)$$
3		istlm.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
4		istlm.k	$$⊢K=\mathrm{TopOpen}\left(F\right)$$
5	1 2 3 4	istlm	$$⊢W\in \mathrm{TopMod}\leftrightarrow \left(\left(W\in \mathrm{TopMnd}\wedge W\in \mathrm{LMod}\wedge F\in \mathrm{TopRing}\right)\wedge \underset{\dot{}}{·}\in \left(\left(K{\times }_{t}J\right)\mathrm{Cn}J\right)\right)$$
6	5	simprbi	$$⊢W\in \mathrm{TopMod}\to \underset{\dot{}}{·}\in \left(\left(K{\times }_{t}J\right)\mathrm{Cn}J\right)$$