Definition df-cvs

Description: Define the class of subcomplex vector spaces, which are the subcomplex modules which are also vector spaces. (Contributed by Thierry Arnoux, 22-May-2019)

	Ref	Expression
Assertion	df-cvs	|- CVec = ( CMod i^i LVec )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccvs	|- CVec
1		cclm	|- CMod
2		clvec	|- LVec
3	1 2	cin	|- ( CMod i^i LVec )
4	0 3	wceq	|- CVec = ( CMod i^i LVec )