Metamath Proof Explorer


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 Hil H 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 PreHil | dom proj h = ClSubSp h
10 8 9 elrab2 H Hil H PreHil dom K = C