Definition df-cvs 22924

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.)

Assertion

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

Detailed syntax breakdown of Definition df-cvs

Step	Hyp	Ref	Expression
1		ccvs 22923	. 2 class CVec
2		cclm 22862	. . 3 class CMod
3		clvec 19102	. . 3 class LVec
4	2, 3	cin 3573	. 2 class (CMod i^i LVec )
5	1, 4	wceq 1483	1 wff CVec = (CMod i^i LVec )

This definition is referenced by:  cvslvec  22925  cvsclm  22926  iscvs  22927  cvsi  22930  cnstrcvs  22941  cncvs  22945  recvs  22946  qcvs  22947  zclmncvs  22948