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 ( 𝑥 ∈ ℝ-Vec → 𝑥 ∈ LMod )
2 1 ssriv ℝ-Vec ⊆ LMod