Theorem cnstrcvs

Description: The set 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, 20-Sep-2021)

	Ref	Expression
Hypothesis	cnlmod.w	|- W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. ( Scalar ` ndx ) , CCfld >. , <. ( .s ` ndx ) , x. >. } )
Assertion	cnstrcvs	|- W e. CVec

Proof

Step	Hyp	Ref	Expression
1		cnlmod.w	|- W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. ( Scalar ` ndx ) , CCfld >. , <. ( .s ` ndx ) , x. >. } )
2	1	cnlmod	|- W 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		qdass	|- ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. } u. { <. ( Scalar ` ndx ) , CCfld >. , <. ( .s ` ndx ) , x. >. } ) = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( Scalar ` ndx ) , CCfld >. } u. { <. ( .s ` ndx ) , x. >. } )
15	1 14	eqtri	|- W = ( { <. ( Base ` ndx ) , CC >. , <. ( +g ` ndx ) , + >. , <. ( Scalar ` ndx ) , CCfld >. } u. { <. ( .s ` ndx ) , x. >. } )
16	15	lmodsca	|- ( CCfld e. _V -> CCfld = ( Scalar ` W ) )
17	3 16	ax-mp	|- CCfld = ( Scalar ` W )
18	17	isclmi	|- ( ( W e. LMod /\ CCfld = ( CCfld |`s CC ) /\ CC e. ( SubRing ` CCfld ) ) -> W e. CMod )
19	2 7 13 18	mp3an	|- W e. CMod
20		cndrng	|- CCfld e. DivRing
21	17	islvec	|- ( W e. LVec <-> ( W e. LMod /\ CCfld e. DivRing ) )
22	2 20 21	mpbir2an	|- W e. LVec
23	19 22	elini	|- W e. ( CMod i^i LVec )
24		df-cvs	|- CVec = ( CMod i^i LVec )
25	23 24	eleqtrri	|- W e. CVec