Metamath Proof Explorer

Theorem chlcsschl

Description: A closed subspace of a subcomplex Hilbert space is a subcomplex Hilbert space. (Contributed by NM, 10-Apr-2008) (Revised by AV, 8-Oct-2022)

Ref Expression
Hypotheses cmslsschl.x ⊢ X = W ↾ 𝑠 U
chlcsschl.s ⊢ S = ClSubSp ⁡ W
Assertion chlcsschl ⊢ W ∈ ℂHil ∧ U ∈ S → X ∈ ℂHil

Proof

Step Hyp Ref Expression
1 cmslsschl.x ⊢ X = W ↾ 𝑠 U
2 chlcsschl.s ⊢ S = ClSubSp ⁡ W
3 hlbn ⊢ W ∈ ℂHil → W ∈ Ban
4 hlcph ⊢ W ∈ ℂHil → W ∈ CPreHil
5 3 4 jca ⊢ W ∈ ℂHil → W ∈ Ban ∧ W ∈ CPreHil
6 1 2 bncssbn ⊢ W ∈ Ban ∧ W ∈ CPreHil ∧ U ∈ S → X ∈ Ban
7 5 6 sylan ⊢ W ∈ ℂHil ∧ U ∈ S → X ∈ Ban
8 hlphl ⊢ W ∈ ℂHil → W ∈ PreHil
9 eqid ⊢ LSubSp ⁡ W = LSubSp ⁡ W
10 2 9 csslss ⊢ W ∈ PreHil ∧ U ∈ S → U ∈ LSubSp ⁡ W
11 8 10 sylan ⊢ W ∈ ℂHil ∧ U ∈ S → U ∈ LSubSp ⁡ W
12 1 9 cphsscph ⊢ W ∈ CPreHil ∧ U ∈ LSubSp ⁡ W → X ∈ CPreHil
13 4 11 12 syl2an2r ⊢ W ∈ ℂHil ∧ U ∈ S → X ∈ CPreHil
14 ishl ⊢ X ∈ ℂHil ↔ X ∈ Ban ∧ X ∈ CPreHil
15 7 13 14 sylanbrc ⊢ W ∈ ℂHil ∧ U ∈ S → X ∈ ℂHil