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 = { 𝑥 ∈ LMod ∣ ( Scalar ‘ 𝑥 ) ∈ DivRing }
2 ssrab2 { 𝑥 ∈ LMod ∣ ( Scalar ‘ 𝑥 ) ∈ DivRing } ⊆ LMod
3 1 2 eqsstri LVec ⊆ LMod