Theorem vscacn

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

	Ref	Expression
Hypotheses	istlm.s	|- .x. = ( .sf ` W )
	istlm.j	|- J = ( TopOpen ` W )
	istlm.f	|- F = ( Scalar ` W )
	istlm.k	|- K = ( TopOpen ` F )
Assertion	vscacn	|- ( W e. TopMod -> .x. e. ( ( K tX J ) Cn J ) )

Proof

Step	Hyp	Ref	Expression
1		istlm.s	|- .x. = ( .sf ` W )
2		istlm.j	|- J = ( TopOpen ` W )
3		istlm.f	|- F = ( Scalar ` W )
4		istlm.k	|- K = ( TopOpen ` F )
5	1 2 3 4	istlm	|- ( W e. TopMod <-> ( ( W e. TopMnd /\ W e. LMod /\ F e. TopRing ) /\ .x. e. ( ( K tX J ) Cn J ) ) )
6	5	simprbi	|- ( W e. TopMod -> .x. e. ( ( K tX J ) Cn J ) )