Metamath Proof Explorer


Theorem vscacn

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

Ref Expression
Hypotheses istlm.s ·˙=𝑠𝑓W
istlm.j J=TopOpenW
istlm.f F=ScalarW
istlm.k K=TopOpenF
Assertion vscacn WTopMod·˙K×tJCnJ

Proof

Step Hyp Ref Expression
1 istlm.s ·˙=𝑠𝑓W
2 istlm.j J=TopOpenW
3 istlm.f F=ScalarW
4 istlm.k K=TopOpenF
5 1 2 3 4 istlm WTopModWTopMndWLModFTopRing·˙K×tJCnJ
6 5 simprbi WTopMod·˙K×tJCnJ