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