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⟩, abs⟩$
	Assertion	cnnv	$⊢ U \in NrmCVec$

Proof

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

Metamath Proof Explorer

Theorem cnnv

Proof