Theorem bj-rvecsscvec

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

	Ref	Expression
Assertion	bj-rvecsscvec	⊢ ℝ-Vec ⊆ ℂVec

Proof

Step	Hyp	Ref	Expression
1		bj-rvecsscmod	⊢ ℝ-Vec ⊆ ℂMod
2		bj-rvecssvec	⊢ ℝ-Vec ⊆ LVec
3	1 2	ssini	⊢ ℝ-Vec ⊆ ( ℂMod ∩ LVec )
4		df-cvs	⊢ ℂVec = ( ℂMod ∩ LVec )
5	3 4	sseqtrri	⊢ ℝ-Vec ⊆ ℂVec