Metamath Proof Explorer

Theorem ishil2

Description: The predicate "is a Hilbert space" (over a *-division ring). (Contributed by NM, 7-Oct-2011) (Revised by Mario Carneiro, 22-Jun-2014)

Ref Expression
Hypotheses ishil2.v ⊢V=BaseH
ishil2.s ⊢⊕˙=LSSum⁡H
ishil2.o ⊢⊥˙=ocv⁡H
ishil2.c ⊢C=ClSubSp⁡H
Assertion ishil2 ⊢H∈Hil↔H∈PreHil∧∀s∈Cs⊕˙⊥˙⁡s=V

Proof

Step Hyp Ref Expression
1 ishil2.v ⊢V=BaseH
2 ishil2.s ⊢⊕˙=LSSum⁡H
3 ishil2.o ⊢⊥˙=ocv⁡H
4 ishil2.c ⊢C=ClSubSp⁡H
5 eqid ⊢proj⁡H=proj⁡H
6 5 4 ishil ⊢H∈Hil↔H∈PreHil∧dom⁡proj⁡H=C
7 5 4 pjcss ⊢H∈PreHil→dom⁡proj⁡H⊆C
8 eqss ⊢dom⁡proj⁡H=C↔dom⁡proj⁡H⊆C∧C⊆dom⁡proj⁡H
9 8 baib ⊢dom⁡proj⁡H⊆C→dom⁡proj⁡H=C↔C⊆dom⁡proj⁡H
10 7 9 syl ⊢H∈PreHil→dom⁡proj⁡H=C↔C⊆dom⁡proj⁡H
11 dfss3 ⊢C⊆dom⁡proj⁡H↔∀s∈Cs∈dom⁡proj⁡H
12 10 11 bitrdi ⊢H∈PreHil→dom⁡proj⁡H=C↔∀s∈Cs∈dom⁡proj⁡H
13 eqid ⊢LSubSp⁡H=LSubSp⁡H
14 4 13 csslss ⊢H∈PreHil∧s∈C→s∈LSubSp⁡H
15 1 13 3 2 5 pjdm2 ⊢H∈PreHil→s∈dom⁡proj⁡H↔s∈LSubSp⁡H∧s⊕˙⊥˙⁡s=V
16 15 baibd ⊢H∈PreHil∧s∈LSubSp⁡H→s∈dom⁡proj⁡H↔s⊕˙⊥˙⁡s=V
17 14 16 syldan ⊢H∈PreHil∧s∈C→s∈dom⁡proj⁡H↔s⊕˙⊥˙⁡s=V
18 17 ralbidva ⊢H∈PreHil→∀s∈Cs∈dom⁡proj⁡H↔∀s∈Cs⊕˙⊥˙⁡s=V
19 12 18 bitrd ⊢H∈PreHil→dom⁡proj⁡H=C↔∀s∈Cs⊕˙⊥˙⁡s=V
20 19 pm5.32i ⊢H∈PreHil∧dom⁡proj⁡H=C↔H∈PreHil∧∀s∈Cs⊕˙⊥˙⁡s=V
21 6 20 bitri ⊢H∈Hil↔H∈PreHil∧∀s∈Cs⊕˙⊥˙⁡s=V