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 ∩ CPreHilOLD )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chlo	⊢ CHilOLD
1		ccbn	⊢ CBan
2		ccphlo	⊢ CPreHilOLD
3	1 2	cin	⊢ ( CBan ∩ CPreHilOLD )
4	0 3	wceq	⊢ CHilOLD = ( CBan ∩ CPreHilOLD )