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

Metamath Proof Explorer

Theorem hhnv

Description: Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypothesis hhnv.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
Assertion hhnv 𝑈 ∈ NrmCVec

Proof

Step Hyp Ref Expression
1 hhnv.1 ⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2 hilablo ⊢ +ℎ ∈ AbelOp
3 ablogrpo ⊢ ( +ℎ ∈ AbelOp → +ℎ ∈ GrpOp )
4 2 3 ax-mp ⊢ +ℎ ∈ GrpOp
5 ax-hfvadd ⊢ +ℎ : ( ℋ × ℋ ) ⟶ ℋ
6 5 fdmi ⊢ dom +ℎ = ( ℋ × ℋ )
7 4 6 grporn ⊢ ℋ = ran +ℎ
8 hilid ⊢ ( GId ‘ +ℎ ) = 0ℎ
9 8 eqcomi ⊢ 0ℎ = ( GId ‘ +ℎ )
10 hilvc ⊢ ⟨ +ℎ , ·ℎ ⟩ ∈ CVecOLD
11 normf ⊢ normℎ : ℋ ⟶ ℝ
12 norm-i ⊢ ( 𝑥 ∈ ℋ → ( ( normℎ ‘ 𝑥 ) = 0 ↔ 𝑥 = 0ℎ ) )
13 12 biimpa ⊢ ( ( 𝑥 ∈ ℋ ∧ ( normℎ ‘ 𝑥 ) = 0 ) → 𝑥 = 0ℎ )
14 norm-iii ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℋ ) → ( normℎ ‘ ( 𝑦 ·ℎ 𝑥 ) ) = ( ( abs ‘ 𝑦 ) · ( normℎ ‘ 𝑥 ) ) )
15 norm-ii ⊢ ( ( 𝑥 ∈ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑥 +ℎ 𝑦 ) ) ≤ ( ( normℎ ‘ 𝑥 ) + ( normℎ ‘ 𝑦 ) ) )
16 7 9 10 11 13 14 15 1 isnvi ⊢ 𝑈 ∈ NrmCVec