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	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
Assertion	cnnv	⊢ 𝑈 ∈ NrmCVec

Proof

Step	Hyp	Ref	Expression
1		cnnv.6	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
2		cnaddabloOLD	⊢ + ∈ AbelOp
3		ablogrpo	⊢ ( + ∈ AbelOp → + ∈ GrpOp )
4	2 3	ax-mp	⊢ + ∈ GrpOp
5		ax-addf	⊢ + : ( ℂ × ℂ ) ⟶ ℂ
6	5	fdmi	⊢ dom + = ( ℂ × ℂ )
7	4 6	grporn	⊢ ℂ = ran +
8		cnidOLD	⊢ 0 = ( GId ‘ + )
9		cncvcOLD	⊢ ⟨ + , · ⟩ ∈ CVecOLD
10		absf	⊢ abs : ℂ ⟶ ℝ
11		abs00	⊢ ( 𝑥 ∈ ℂ → ( ( abs ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
12	11	biimpa	⊢ ( ( 𝑥 ∈ ℂ ∧ ( abs ‘ 𝑥 ) = 0 ) → 𝑥 = 0 )
13		absmul	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( abs ‘ ( 𝑦 · 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( abs ‘ 𝑥 ) ) )
14		abstri	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( 𝑥 + 𝑦 ) ) ≤ ( ( abs ‘ 𝑥 ) + ( abs ‘ 𝑦 ) ) )
15	7 8 9 10 12 13 14 1	isnvi	⊢ 𝑈 ∈ NrmCVec