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 = Base H
ishil2.s ⊢ ⊕ ˙ = LSSum ⁡ H
ishil2.o ⊢ ⊥ ˙ = ocv ⁡ H
ishil2.c ⊢ C = ClSubSp ⁡ H
Assertion ishil2 ⊢ H ∈ Hil ↔ H ∈ PreHil ∧ ∀ s ∈ C s ⊕ ˙ ⊥ ˙ ⁡ s = V

Proof

Step Hyp Ref Expression
1 ishil2.v ⊢ V = Base H
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 ∈ C s ∈ dom ⁡ proj ⁡ H
12 10 11 bitrdi ⊢ H ∈ PreHil → dom ⁡ proj ⁡ H = C ↔ ∀ s ∈ C s ∈ 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 ∈ C s ∈ dom ⁡ proj ⁡ H ↔ ∀ s ∈ C s ⊕ ˙ ⊥ ˙ ⁡ s = V
19 12 18 bitrd ⊢ H ∈ PreHil → dom ⁡ proj ⁡ H = C ↔ ∀ s ∈ C s ⊕ ˙ ⊥ ˙ ⁡ s = V
20 19 pm5.32i ⊢ H ∈ PreHil ∧ dom ⁡ proj ⁡ H = C ↔ H ∈ PreHil ∧ ∀ s ∈ C s ⊕ ˙ ⊥ ˙ ⁡ s = V
21 6 20 bitri ⊢ H ∈ Hil ↔ H ∈ PreHil ∧ ∀ s ∈ C s ⊕ ˙ ⊥ ˙ ⁡ s = V