Definition df-cvs 22732

Description: Define a complex vector space, which is just a complex left module and a vector space. (Contributed by Thierry Arnoux, 22-May-2019.)

Assertion

Ref	Expression
df-cvs	⊢ ℂVec = (ℂMod ∩ LVec)

Detailed syntax breakdown of Definition df-cvs

Step	Hyp	Ref	Expression
1		ccvs 22731	. 2 class ℂVec
2		cclm 22670	. . 3 class ℂMod
3		clvec 18923	. . 3 class LVec
4	2, 3	cin 3539	. 2 class (ℂMod ∩ LVec)
5	1, 4	wceq 1475	1 wff ℂVec = (ℂMod ∩ LVec)

This definition is referenced by:  cvslvec  22733  cvsclm  22734  iscvs  22735  cvsi  22738  cnstrcvs  22749  cncvs  22753  recvs  22754  qcvs  22755  zclmncvs  22756