Metamath Proof Explorer

Theorem tlmlmod

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

Ref Expression
Assertion tlmlmod 
|- ( W e. TopMod -> W e. LMod )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( .sf ` W ) = ( .sf ` W )
2 eqid 
 |-  ( TopOpen ` W ) = ( TopOpen ` W )
3 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
4 eqid 
 |-  ( TopOpen ` ( Scalar ` W ) ) = ( TopOpen ` ( Scalar ` W ) )
5 1 2 3 4 istlm 
 |-  ( W e. TopMod <-> ( ( W e. TopMnd /\ W e. LMod /\ ( Scalar ` W ) e. TopRing ) /\ ( .sf ` W ) e. ( ( ( TopOpen ` ( Scalar ` W ) ) tX ( TopOpen ` W ) ) Cn ( TopOpen ` W ) ) ) )
6 5 simplbi 
 |-  ( W e. TopMod -> ( W e. TopMnd /\ W e. LMod /\ ( Scalar ` W ) e. TopRing ) )
7 6 simp2d 
 |-  ( W e. TopMod -> W e. LMod )