Metamath Proof Explorer

Theorem bj-rvecsscvec

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

		Ref	Expression
	Assertion	bj-rvecsscvec	\|- RRVec C_ CVec


 |-  RRVec C_ CMod
 |-  RRVec C_ LVec
 |-  RRVec C_ ( CMod i^i LVec )
 |-  CVec = ( CMod i^i LVec )
 |-  RRVec C_ CVec

Step	Hyp	Ref	Expression
1		bj-rvecsscmod	\|- RRVec C_ CMod
2		bj-rvecssvec	\|- RRVec C_ LVec
3	1 2	ssini	\|- RRVec C_ ( CMod i^i LVec )
4		df-cvs	\|- CVec = ( CMod i^i LVec )
5	3 4	sseqtrri	\|- RRVec C_ CVec