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=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℂ}_{\mathrm{fld}}⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}$$
Assertion	cnstrcvs	$$⊢W\in \mathrm{ℂVec}$$

Proof

Step	Hyp	Ref	Expression
1		cnlmod.w	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℂ}_{\mathrm{fld}}⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}$$
2	1	cnlmod	$$⊢W\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		qdass	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩\right\}\cup \left\{⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℂ}_{\mathrm{fld}}⟩,⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℂ}_{\mathrm{fld}}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}$$
15	1 14	eqtri	$$⊢W=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},ℂ⟩,⟨{+}_{\mathrm{ndx}},+⟩,⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{ℂ}_{\mathrm{fld}}⟩\right\}\cup \left\{⟨{\cdot }_{\mathrm{ndx}},\times ⟩\right\}$$
16	15	lmodsca	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{V}\to {ℂ}_{\mathrm{fld}}=\mathrm{Scalar}\left(W\right)$$
17	3 16	ax-mp	$$⊢{ℂ}_{\mathrm{fld}}=\mathrm{Scalar}\left(W\right)$$
18	17	isclmi	$$⊢\left(W\in \mathrm{LMod}\wedge {ℂ}_{\mathrm{fld}}={ℂ}_{\mathrm{fld}}{\upharpoonright }_{𝑠}ℂ\wedge ℂ\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)\right)\to W\in \mathrm{CMod}$$
19	2 7 13 18	mp3an	$$⊢W\in \mathrm{CMod}$$
20		cndrng	$$⊢{ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}$$
21	17	islvec	$$⊢W\in \mathrm{LVec}\leftrightarrow \left(W\in \mathrm{LMod}\wedge {ℂ}_{\mathrm{fld}}\in \mathrm{DivRing}\right)$$
22	2 20 21	mpbir2an	$$⊢W\in \mathrm{LVec}$$
23	19 22	elini	$$⊢W\in \left(\mathrm{CMod}\cap \mathrm{LVec}\right)$$
24		df-cvs	$$⊢\mathrm{ℂVec}=\mathrm{CMod}\cap \mathrm{LVec}$$
25	23 24	eleqtrri	$$⊢W\in \mathrm{ℂVec}$$