# Metamath Proof Explorer

## Theorem tlmtmd

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

Ref Expression
Assertion tlmtmd ${⊢}{W}\in \mathrm{TopMod}\to {W}\in \mathrm{TopMnd}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}{\cdot }_{\mathrm{𝑠𝑓}}\left({W}\right)={\cdot }_{\mathrm{𝑠𝑓}}\left({W}\right)$
2 eqid ${⊢}\mathrm{TopOpen}\left({W}\right)=\mathrm{TopOpen}\left({W}\right)$
3 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
4 eqid ${⊢}\mathrm{TopOpen}\left(\mathrm{Scalar}\left({W}\right)\right)=\mathrm{TopOpen}\left(\mathrm{Scalar}\left({W}\right)\right)$
5 1 2 3 4 istlm ${⊢}{W}\in \mathrm{TopMod}↔\left(\left({W}\in \mathrm{TopMnd}\wedge {W}\in \mathrm{LMod}\wedge \mathrm{Scalar}\left({W}\right)\in \mathrm{TopRing}\right)\wedge {\cdot }_{\mathrm{𝑠𝑓}}\left({W}\right)\in \left(\left(\mathrm{TopOpen}\left(\mathrm{Scalar}\left({W}\right)\right){×}_{t}\mathrm{TopOpen}\left({W}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({W}\right)\right)\right)$
6 5 simplbi ${⊢}{W}\in \mathrm{TopMod}\to \left({W}\in \mathrm{TopMnd}\wedge {W}\in \mathrm{LMod}\wedge \mathrm{Scalar}\left({W}\right)\in \mathrm{TopRing}\right)$
7 6 simp1d ${⊢}{W}\in \mathrm{TopMod}\to {W}\in \mathrm{TopMnd}$