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	$$⊢\mathrm{Hil}=\left\{h\in \mathrm{PreHil}|\mathrm{dom}\mathrm{proj}\left(h\right)=\mathrm{ClSubSp}\left(h\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chil	$$class\mathrm{Hil}$$
1		vh	$$setvarh$$
2		cphl	$$class\mathrm{PreHil}$$
3		cpj	$$class\mathrm{proj}$$
4	1	cv	$$setvarh$$
5	4 3	cfv	$$class\mathrm{proj}\left(h\right)$$
6	5	cdm	$$class\mathrm{dom}\mathrm{proj}\left(h\right)$$
7		ccss	$$class\mathrm{ClSubSp}$$
8	4 7	cfv	$$class\mathrm{ClSubSp}\left(h\right)$$
9	6 8	wceq	$$wff\mathrm{dom}\mathrm{proj}\left(h\right)=\mathrm{ClSubSp}\left(h\right)$$
10	9 1 2	crab	$$class\left\{h\in \mathrm{PreHil}|\mathrm{dom}\mathrm{proj}\left(h\right)=\mathrm{ClSubSp}\left(h\right)\right\}$$
11	0 10	wceq	$$wff\mathrm{Hil}=\left\{h\in \mathrm{PreHil}|\mathrm{dom}\mathrm{proj}\left(h\right)=\mathrm{ClSubSp}\left(h\right)\right\}$$