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 LMod

Proof

Step Hyp Ref Expression
1 df-lvec LVec = x LMod | Scalar x DivRing
2 ssrab2 x LMod | Scalar x DivRing LMod
3 1 2 eqsstri LVec LMod