Metamath Proof Explorer

Theorem hlhil

Description: Corollary of the Projection Theorem: A subcomplex Hilbert space is a Hilbert space (in the algebraic sense, meaning that all algebraically closed subspaces have a projection decomposition). (Contributed by Mario Carneiro, 17-Oct-2015)

Ref Expression
Assertion hlhil ⊢ W ∈ ℂHil → W ∈ Hil

Proof

Step Hyp Ref Expression
1 hlphl ⊢ W ∈ ℂHil → W ∈ PreHil
2 eqid ⊢ proj ⁡ W = proj ⁡ W
3 eqid ⊢ ClSubSp ⁡ W = ClSubSp ⁡ W
4 2 3 pjcss ⊢ W ∈ PreHil → dom ⁡ proj ⁡ W ⊆ ClSubSp ⁡ W
5 1 4 syl ⊢ W ∈ ℂHil → dom ⁡ proj ⁡ W ⊆ ClSubSp ⁡ W
6 eqid ⊢ Base W = Base W
7 eqid ⊢ TopOpen ⁡ W = TopOpen ⁡ W
8 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
9 6 7 8 3 cldcss2 ⊢ W ∈ ℂHil → ClSubSp ⁡ W = LSubSp ⁡ W ∩ Clsd ⁡ TopOpen ⁡ W
10 elin ⊢ x ∈ LSubSp ⁡ W ∩ Clsd ⁡ TopOpen ⁡ W ↔ x ∈ LSubSp ⁡ W ∧ x ∈ Clsd ⁡ TopOpen ⁡ W
11 7 8 2 pjth2 ⊢ W ∈ ℂHil ∧ x ∈ LSubSp ⁡ W ∧ x ∈ Clsd ⁡ TopOpen ⁡ W → x ∈ dom ⁡ proj ⁡ W
12 11 3expib ⊢ W ∈ ℂHil → x ∈ LSubSp ⁡ W ∧ x ∈ Clsd ⁡ TopOpen ⁡ W → x ∈ dom ⁡ proj ⁡ W
13 10 12 biimtrid ⊢ W ∈ ℂHil → x ∈ LSubSp ⁡ W ∩ Clsd ⁡ TopOpen ⁡ W → x ∈ dom ⁡ proj ⁡ W
14 13 ssrdv ⊢ W ∈ ℂHil → LSubSp ⁡ W ∩ Clsd ⁡ TopOpen ⁡ W ⊆ dom ⁡ proj ⁡ W
15 9 14 eqsstrd ⊢ W ∈ ℂHil → ClSubSp ⁡ W ⊆ dom ⁡ proj ⁡ W
16 5 15 eqssd ⊢ W ∈ ℂHil → dom ⁡ proj ⁡ W = ClSubSp ⁡ W
17 2 3 ishil ⊢ W ∈ Hil ↔ W ∈ PreHil ∧ dom ⁡ proj ⁡ W = ClSubSp ⁡ W
18 1 16 17 sylanbrc ⊢ W ∈ ℂHil → W ∈ Hil