Metamath Proof Explorer


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 ℂHil = Ban CPreHil

Detailed syntax breakdown

Step Hyp Ref Expression
0 chl class ℂHil
1 cbn class Ban
2 ccph class CPreHil
3 1 2 cin class Ban CPreHil
4 0 3 wceq wff ℂHil = Ban CPreHil