Definition df-hl

Description: Define the class of all subcomplex Hilbert spaces. A subcomplex Hilbert space is a Banach space which is also an inner product space over a subfield of the field of complex numbers closed under square roots of nonnegative reals. (Contributed by Steve Rodriguez, 28-Apr-2007)

	Ref	Expression
Assertion	df-hl	$$⊢\mathrm{ℂHil}=\mathrm{Ban}\cap \mathrm{CPreHil}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chl	$$class\mathrm{ℂHil}$$
1		cbn	$$class\mathrm{Ban}$$
2		ccph	$$class\mathrm{CPreHil}$$
3	1 2	cin	$$class\left(\mathrm{Ban}\cap \mathrm{CPreHil}\right)$$
4	0 3	wceq	$$wff\mathrm{ℂHil}=\mathrm{Ban}\cap \mathrm{CPreHil}$$