Metamath Proof Explorer

Theorem bj-rvecsscmod

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

Ref Expression
Assertion bj-rvecsscmod 
|- RRVec C_ CMod

Proof

Step Hyp Ref Expression
1 bj-rveccmod 
 |-  ( x e. RRVec -> x e. CMod )
2 1 ssriv 
 |-  RRVec C_ CMod