Definition df-hlo

Description: Define the class of all complex Hilbert spaces. A Hilbert space is a Banach space which is also an inner product space. (Contributed by Steve Rodriguez, 28-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	df-hlo	|- CHilOLD = ( CBan i^i CPreHilOLD )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chlo	|- CHilOLD
1		ccbn	|- CBan
2		ccphlo	|- CPreHilOLD
3	1 2	cin	|- ( CBan i^i CPreHilOLD )
4	0 3	wceq	|- CHilOLD = ( CBan i^i CPreHilOLD )