This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∩ ℂPreHil )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chl	⊢ ℂHil
1		cbn	⊢ Ban
2		ccph	⊢ ℂPreHil
3	1 2	cin	⊢ ( Ban ∩ ℂPreHil )
4	0 3	wceq	⊢ ℂHil = ( Ban ∩ ℂPreHil )