Metamath Proof Explorer

Theorem bj-vecssmod

Description: Vector spaces are modules. (Contributed by BJ, 9-Jun-2019) (Proof modification is discouraged.)

Ref Expression
Assertion bj-vecssmod 
|- LVec C_ LMod

Proof

Step Hyp Ref Expression
1 df-lvec 
 |-  LVec = { x e. LMod | ( Scalar ` x ) e. DivRing }
2 ssrab2 
 |-  { x e. LMod | ( Scalar ` x ) e. DivRing } C_ LMod
3 1 2 eqsstri 
 |-  LVec C_ LMod