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