This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐽 ) )