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

Metamath Proof Explorer

Theorem hilvc

Description: Hilbert space is a complex vector space. Vector addition is +h , and scalar product is .h . (Contributed by NM, 15-Apr-2007) (New usage is discouraged.)

Ref Expression
Assertion hilvc 
|- <. +h , .h >. e. CVecOLD

Proof

Step Hyp Ref Expression
1 hilablo 
 |-  +h e. AbelOp
2 ax-hfvadd 
 |-  +h : ( ~H X. ~H ) --> ~H
3 2 fdmi 
 |-  dom +h = ( ~H X. ~H )
4 ax-hfvmul 
 |-  .h : ( CC X. ~H ) --> ~H
5 ax-hvmulid 
 |-  ( x e. ~H -> ( 1 .h x ) = x )
6 ax-hvdistr1 
 |-  ( ( y e. CC /\ x e. ~H /\ z e. ~H ) -> ( y .h ( x +h z ) ) = ( ( y .h x ) +h ( y .h z ) ) )
7 ax-hvdistr2 
 |-  ( ( y e. CC /\ z e. CC /\ x e. ~H ) -> ( ( y + z ) .h x ) = ( ( y .h x ) +h ( z .h x ) ) )
8 ax-hvmulass 
 |-  ( ( y e. CC /\ z e. CC /\ x e. ~H ) -> ( ( y x. z ) .h x ) = ( y .h ( z .h x ) ) )
9 eqid 
 |-  <. +h , .h >. = <. +h , .h >.
10 1 3 4 5 6 7 8 9 isvciOLD 
 |-  <. +h , .h >. e. CVecOLD