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

Metamath Proof Explorer

Theorem tlmtmd

Description: A topological module is a topological monoid. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Assertion tlmtmd ( 𝑊 ∈ TopMod → 𝑊 ∈ TopMnd )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( ·sf ‘ 𝑊 ) = ( ·sf ‘ 𝑊 )
2 eqid ⊢ ( TopOpen ‘ 𝑊 ) = ( TopOpen ‘ 𝑊 )
3 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
4 eqid ⊢ ( TopOpen ‘ ( Scalar ‘ 𝑊 ) ) = ( TopOpen ‘ ( Scalar ‘ 𝑊 ) )
5 1 2 3 4 istlm ⊢ ( 𝑊 ∈ TopMod ↔ ( ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) ∈ TopRing ) ∧ ( ·sf ‘ 𝑊 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑊 ) ) ×t ( TopOpen ‘ 𝑊 ) ) Cn ( TopOpen ‘ 𝑊 ) ) ) )
6 5 simplbi ⊢ ( 𝑊 ∈ TopMod → ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) ∈ TopRing ) )
7 6 simp1d ⊢ ( 𝑊 ∈ TopMod → 𝑊 ∈ TopMnd )