Theorem cnnv

Description: The set of complex numbers is a normed complex vector space. The vector operation is + , the scalar product is x. , and the norm function is abs . (Contributed by Steve Rodriguez, 3-Dec-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	cnnv.6	$$⊢U=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
Assertion	cnnv	$$⊢U\in \mathrm{NrmCVec}$$

Proof

Step	Hyp	Ref	Expression
1		cnnv.6	$$⊢U=⟨⟨+,\times ⟩,\mathrm{abs}⟩$$
2		cnaddabloOLD	$$⊢+\in \mathrm{AbelOp}$$
3		ablogrpo	$$⊢+\in \mathrm{AbelOp}\to +\in \mathrm{GrpOp}$$
4	2 3	ax-mp	$$⊢+\in \mathrm{GrpOp}$$
5		ax-addf	$$⊢+:ℂ\times ℂ⟶ℂ$$
6	5	fdmi	$$⊢\mathrm{dom}+=ℂ\times ℂ$$
7	4 6	grporn	$$⊢ℂ=\mathrm{ran}+$$
8		cnidOLD	$$⊢0=\mathrm{GId}\left(+\right)$$
9		cncvcOLD	$$⊢⟨+,\times ⟩\in {CVec}_{\mathrm{OLD}}$$
10		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
11		abs00	$$⊢x\in ℂ\to \left(\left|x\right|=0\leftrightarrow x=0\right)$$
12	11	biimpa	$$⊢\left(x\in ℂ\wedge \left|x\right|=0\right)\to x=0$$
13		absmul	$$⊢\left(y\in ℂ\wedge x\in ℂ\right)\to \left|yx\right|=\left|y\right|\left|x\right|$$
14		abstri	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to \left|x+y\right|\le \left|x\right|+\left|y\right|$$
15	7 8 9 10 12 13 14 1	isnvi	$$⊢U\in \mathrm{NrmCVec}$$