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 = { ℎ ∈ PreHil ∣ dom ( proj ‘ ℎ ) = ( ClSubSp ‘ ℎ ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chil	⊢ Hil
1		vh	⊢ ℎ
2		cphl	⊢ PreHil
3		cpj	⊢ proj
4	1	cv	⊢ ℎ
5	4 3	cfv	⊢ ( proj ‘ ℎ )
6	5	cdm	⊢ dom ( proj ‘ ℎ )
7		ccss	⊢ ClSubSp
8	4 7	cfv	⊢ ( ClSubSp ‘ ℎ )
9	6 8	wceq	⊢ dom ( proj ‘ ℎ ) = ( ClSubSp ‘ ℎ )
10	9 1 2	crab	⊢ { ℎ ∈ PreHil ∣ dom ( proj ‘ ℎ ) = ( ClSubSp ‘ ℎ ) }
11	0 10	wceq	⊢ Hil = { ℎ ∈ PreHil ∣ dom ( proj ‘ ℎ ) = ( ClSubSp ‘ ℎ ) }