Metamath Proof Explorer

Theorem lveclmod

Description: A left vector space is a left module. (Contributed by NM, 9-Dec-2013)

Ref Expression
Assertion lveclmod 
|- ( W e. LVec -> W e. LMod )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Scalar ` W ) = ( Scalar ` W )
2 1 islvec 
 |-  ( W e. LVec <-> ( W e. LMod /\ ( Scalar ` W ) e. DivRing ) )
3 2 simplbi 
 |-  ( W e. LVec -> W e. LMod )