Theorem hhhl

Description: The Hilbert space structure is a complex Hilbert space. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhhl.1	|- U = <. <. +h , .h >. , normh >.
Assertion	hhhl	|- U e. CHilOLD

Proof

Step	Hyp	Ref	Expression
1		hhhl.1	|- U = <. <. +h , .h >. , normh >.
2	1	hhnv	|- U e. NrmCVec
3		eqid	|- ( IndMet ` U ) = ( IndMet ` U )
4	1 3	hhcms	|- ( IndMet ` U ) e. ( CMet ` ~H )
5	1	hhba	|- ~H = ( BaseSet ` U )
6	5 3	iscbn	|- ( U e. CBan <-> ( U e. NrmCVec /\ ( IndMet ` U ) e. ( CMet ` ~H ) ) )
7	2 4 6	mpbir2an	|- U e. CBan
8	1	hhph	|- U e. CPreHilOLD
9		ishlo	|- ( U e. CHilOLD <-> ( U e. CBan /\ U e. CPreHilOLD ) )
10	7 8 9	mpbir2an	|- U e. CHilOLD