Definition df-hil

Description: Define class of all Hilbert spaces. Based on Proposition 4.5, p. 176, Gudrun Kalmbach, Quantum Measures and Spaces, Kluwer, Dordrecht, 1998. (Contributed by NM, 7-Oct-2011) (Revised by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Assertion	df-hil	|- Hil = { h e. PreHil | dom ( proj ` h ) = ( ClSubSp ` h ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chil	|- Hil
1		vh	|- h
2		cphl	|- PreHil
3		cpj	|- proj
4	1	cv	|- h
5	4 3	cfv	|- ( proj ` h )
6	5	cdm	|- dom ( proj ` h )
7		ccss	|- ClSubSp
8	4 7	cfv	|- ( ClSubSp ` h )
9	6 8	wceq	|- dom ( proj ` h ) = ( ClSubSp ` h )
10	9 1 2	crab	|- { h e. PreHil | dom ( proj ` h ) = ( ClSubSp ` h ) }
11	0 10	wceq	|- Hil = { h e. PreHil | dom ( proj ` h ) = ( ClSubSp ` h ) }