Metamath Proof Explorer


Theorem tlmtmd

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

Ref Expression
Assertion tlmtmd WTopModWTopMnd

Proof

Step Hyp Ref Expression
1 eqid 𝑠𝑓W=𝑠𝑓W
2 eqid TopOpenW=TopOpenW
3 eqid ScalarW=ScalarW
4 eqid TopOpenScalarW=TopOpenScalarW
5 1 2 3 4 istlm WTopModWTopMndWLModScalarWTopRing𝑠𝑓WTopOpenScalarW×tTopOpenWCnTopOpenW
6 5 simplbi WTopModWTopMndWLModScalarWTopRing
7 6 simp1d WTopModWTopMnd