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