Metamath Proof Explorer


Theorem bj-rvecssmod

Description: Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024)

Ref Expression
Assertion bj-rvecssmod ℝVec LMod

Proof

Step Hyp Ref Expression
1 bj-rvecmod x ℝVec x LMod
2 1 ssriv ℝVec LMod