Description: Real vector spaces are modules. (Contributed by BJ, 6-Jan-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | bj-rvecssmod | |- RRVec C_ LMod |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bj-rvecmod | |- ( x e. RRVec -> x e. LMod ) |
|
2 | 1 | ssriv | |- RRVec C_ LMod |