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 
|- U = <. <. +h , .h >. , normh >.
Assertion hhnv 
|- U e. NrmCVec

Proof

Step Hyp Ref Expression
1 hhnv.1 
 |-  U = <. <. +h , .h >. , normh >.
2 hilablo 
 |-  +h e. AbelOp
3 ablogrpo 
 |-  ( +h e. AbelOp -> +h e. GrpOp )
4 2 3 ax-mp 
 |-  +h e. GrpOp
5 ax-hfvadd 
 |-  +h : ( ~H X. ~H ) --> ~H
6 5 fdmi 
 |-  dom +h = ( ~H X. ~H )
7 4 6 grporn 
 |-  ~H = ran +h
8 hilid 
 |-  ( GId ` +h ) = 0h
9 8 eqcomi 
 |-  0h = ( GId ` +h )
10 hilvc 
 |-  <. +h , .h >. e. CVecOLD
11 normf 
 |-  normh : ~H --> RR
12 norm-i 
 |-  ( x e. ~H -> ( ( normh ` x ) = 0 <-> x = 0h ) )
13 12 biimpa 
 |-  ( ( x e. ~H /\ ( normh ` x ) = 0 ) -> x = 0h )
14 norm-iii 
 |-  ( ( y e. CC /\ x e. ~H ) -> ( normh ` ( y .h x ) ) = ( ( abs ` y ) x. ( normh ` x ) ) )
15 norm-ii 
 |-  ( ( x e. ~H /\ y e. ~H ) -> ( normh ` ( x +h y ) ) <_ ( ( normh ` x ) + ( normh ` y ) ) )
16 7 9 10 11 13 14 15 1 isnvi 
 |-  U e. NrmCVec