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	$$⊢{CHil}_{\mathrm{OLD}}=\mathrm{CBan}\cap {CPreHil}_{\mathrm{OLD}}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chlo	$$class{CHil}_{\mathrm{OLD}}$$
1		ccbn	$$class\mathrm{CBan}$$
2		ccphlo	$$class{CPreHil}_{\mathrm{OLD}}$$
3	1 2	cin	$$class\left(\mathrm{CBan}\cap {CPreHil}_{\mathrm{OLD}}\right)$$
4	0 3	wceq	$$wff{CHil}_{\mathrm{OLD}}=\mathrm{CBan}\cap {CPreHil}_{\mathrm{OLD}}$$