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	|- CHil = ( Ban i^i CPreHil )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chl	|- CHil
1		cbn	|- Ban
2		ccph	|- CPreHil
3	1 2	cin	|- ( Ban i^i CPreHil )
4	0 3	wceq	|- CHil = ( Ban i^i CPreHil )