Theorem cncvcOLD

Description: Obsolete version of cncvs . The set of complex numbers is a complex vector space. The vector operation is + , and the scalar product is x. . (Contributed by NM, 5-Nov-2006) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Assertion	cncvcOLD	$$⊢⟨+,\times ⟩\in {CVec}_{\mathrm{OLD}}$$

Proof

Step	Hyp	Ref	Expression
1		cnaddabloOLD	$$⊢+\in \mathrm{AbelOp}$$
2		ax-addf	$$⊢+:ℂ\times ℂ⟶ℂ$$
3	2	fdmi	$$⊢\mathrm{dom}+=ℂ\times ℂ$$
4		ax-mulf	$$⊢\times :ℂ\times ℂ⟶ℂ$$
5		mullid	$$⊢x\in ℂ\to 1x=x$$
6		adddi	$$⊢\left(y\in ℂ\wedge x\in ℂ\wedge z\in ℂ\right)\to y\left(x+z\right)=yx+yz$$
7		adddir	$$⊢\left(y\in ℂ\wedge z\in ℂ\wedge x\in ℂ\right)\to \left(y+z\right)x=yx+zx$$
8		mulass	$$⊢\left(y\in ℂ\wedge z\in ℂ\wedge x\in ℂ\right)\to yzx=yzx$$
9		eqid	$$⊢⟨+,\times ⟩=⟨+,\times ⟩$$
10	1 3 4 5 6 7 8 9	isvciOLD	$$⊢⟨+,\times ⟩\in {CVec}_{\mathrm{OLD}}$$