Metamath Proof Explorer


Theorem tlmlmod

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

Ref Expression
Assertion tlmlmod WTopModWLMod

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 simp2d WTopModWLMod