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 · = ( ·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 𝐽 ) )