Theorem cncvs

Description: The complex left module of complex numbers is a subcomplex vector space. The vector operation is + , and the scalar product is x. . (Contributed by NM, 5-Nov-2006) (Revised by AV, 21-Sep-2021)

	Ref	Expression
Hypothesis	cnrlmod.c	|- C = ( ringLMod ` CCfld )
Assertion	cncvs	|- C e. CVec

Proof

Step	Hyp	Ref	Expression
1		cnrlmod.c	|- C = ( ringLMod ` CCfld )
2	1	cnrlmod	|- C e. LMod
3		cnfldex	|- CCfld e. _V
4		cnfldbas	|- CC = ( Base ` CCfld )
5	4	ressid	|- ( CCfld e. _V -> ( CCfld |`s CC ) = CCfld )
6	3 5	ax-mp	|- ( CCfld |`s CC ) = CCfld
7	6	eqcomi	|- CCfld = ( CCfld |`s CC )
8		id	|- ( x e. CC -> x e. CC )
9		addcl	|- ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
10		negcl	|- ( x e. CC -> -u x e. CC )
11		ax-1cn	|- 1 e. CC
12		mulcl	|- ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
13	8 9 10 11 12	cnsubrglem	|- CC e. ( SubRing ` CCfld )
14		rlmsca	|- ( CCfld e. _V -> CCfld = ( Scalar ` ( ringLMod ` CCfld ) ) )
15	3 14	ax-mp	|- CCfld = ( Scalar ` ( ringLMod ` CCfld ) )
16	1	eqcomi	|- ( ringLMod ` CCfld ) = C
17	16	fveq2i	|- ( Scalar ` ( ringLMod ` CCfld ) ) = ( Scalar ` C )
18	15 17	eqtri	|- CCfld = ( Scalar ` C )
19	18	isclmi	|- ( ( C e. LMod /\ CCfld = ( CCfld |`s CC ) /\ CC e. ( SubRing ` CCfld ) ) -> C e. CMod )
20	2 7 13 19	mp3an	|- C e. CMod
21	1	cnrlvec	|- C e. LVec
22	20 21	elini	|- C e. ( CMod i^i LVec )
23		df-cvs	|- CVec = ( CMod i^i LVec )
24	22 23	eleqtrri	|- C e. CVec