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