Theorem ishil

Description: The predicate "is a Hilbert space" (over a *-division ring). A Hilbert space is a pre-Hilbert space such that all closed subspaces have a projection decomposition. (Contributed by NM, 7-Oct-2011) (Revised by Mario Carneiro, 22-Jun-2014)

	Ref	Expression
Hypotheses	ishil.k	|- K = ( proj ` H )
	ishil.c	|- C = ( ClSubSp ` H )
Assertion	ishil	|- ( H e. Hil <-> ( H e. PreHil /\ dom K = C ) )

Proof

Step	Hyp	Ref	Expression
1		ishil.k	|- K = ( proj ` H )
2		ishil.c	|- C = ( ClSubSp ` H )
3		fveq2	|- ( h = H -> ( proj ` h ) = ( proj ` H ) )
4	3 1	eqtr4di	|- ( h = H -> ( proj ` h ) = K )
5	4	dmeqd	|- ( h = H -> dom ( proj ` h ) = dom K )
6		fveq2	|- ( h = H -> ( ClSubSp ` h ) = ( ClSubSp ` H ) )
7	6 2	eqtr4di	|- ( h = H -> ( ClSubSp ` h ) = C )
8	5 7	eqeq12d	|- ( h = H -> ( dom ( proj ` h ) = ( ClSubSp ` h ) <-> dom K = C ) )
9		df-hil	|- Hil = { h e. PreHil | dom ( proj ` h ) = ( ClSubSp ` h ) }
10	8 9	elrab2	|- ( H e. Hil <-> ( H e. PreHil /\ dom K = C ) )