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=\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)$$
Assertion	cncvs	$$⊢C\in \mathrm{ℂVec}$$

Proof

Step	Hyp	Ref	Expression
1		cnrlmod.c	$$⊢C=\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)$$
2	1	cnrlmod	$$⊢C\in \mathrm{LMod}$$
3		cnfldex	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{V}$$
4		cnfldbas	$$⊢ℂ={\mathrm{Base}}_{{ℂ}_{\mathrm{fld}}}$$
5	4	ressid	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{V}\to {ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℂ={ℂ}_{\mathrm{fld}}$$
6	3 5	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℂ={ℂ}_{\mathrm{fld}}$$
7	6	eqcomi	$$⊢{ℂ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℂ$$
8		id	$$⊢x\in ℂ\to x\in ℂ$$
9		addcl	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to x+y\in ℂ$$
10		negcl	$$⊢x\in ℂ\to -x\in ℂ$$
11		ax-1cn	$$⊢1\in ℂ$$
12		mulcl	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to xy\in ℂ$$
13	8 9 10 11 12	cnsubrglem	$$⊢ℂ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
14		rlmsca	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{V}\to {ℂ}_{\mathrm{fld}}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
15	3 14	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}=\mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
16	1	eqcomi	$$⊢\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)=C$$
17	16	fveq2i	$$⊢\mathrm{Scalar}\left(\mathrm{ringLMod}\left({ℂ}_{\mathrm{fld}}\right)\right)=\mathrm{Scalar}\left(C\right)$$
18	15 17	eqtri	$$⊢{ℂ}_{\mathrm{fld}}=\mathrm{Scalar}\left(C\right)$$
19	18	isclmi	$$⊢\left(C\in \mathrm{LMod}\wedge {ℂ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℂ\wedge ℂ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to C\in \mathrm{CMod}$$
20	2 7 13 19	mp3an	$$⊢C\in \mathrm{CMod}$$
21	1	cnrlvec	$$⊢C\in \mathrm{LVec}$$
22	20 21	elini	$$⊢C\in \left(\mathrm{CMod}\cap \mathrm{LVec}\right)$$
23		df-cvs	$$⊢\mathrm{ℂVec}=\mathrm{CMod}\cap \mathrm{LVec}$$
24	22 23	eleqtrri	$$⊢C\in \mathrm{ℂVec}$$