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