This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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