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 ⊒ 𝑋 = ( π‘Š β†Ύs π‘ˆ )
chlcsschl.s ⊒ 𝑆 = ( ClSubSp β€˜ π‘Š )
Assertion chlcsschl ( ( π‘Š ∈ β„‚Hil ∧ π‘ˆ ∈ 𝑆 ) β†’ 𝑋 ∈ β„‚Hil )

Proof

Step Hyp Ref Expression
1 cmslsschl.x ⊒ 𝑋 = ( π‘Š β†Ύs π‘ˆ )
2 chlcsschl.s ⊒ 𝑆 = ( ClSubSp β€˜ π‘Š )
3 hlbn ⊒ ( π‘Š ∈ β„‚Hil β†’ π‘Š ∈ Ban )
4 hlcph ⊒ ( π‘Š ∈ β„‚Hil β†’ π‘Š ∈ β„‚PreHil )
5 3 4 jca ⊒ ( π‘Š ∈ β„‚Hil β†’ ( π‘Š ∈ Ban ∧ π‘Š ∈ β„‚PreHil ) )
6 1 2 bncssbn ⊒ ( ( ( π‘Š ∈ Ban ∧ π‘Š ∈ β„‚PreHil ) ∧ π‘ˆ ∈ 𝑆 ) β†’ 𝑋 ∈ Ban )
7 5 6 sylan ⊒ ( ( π‘Š ∈ β„‚Hil ∧ π‘ˆ ∈ 𝑆 ) β†’ 𝑋 ∈ Ban )
8 hlphl ⊒ ( π‘Š ∈ β„‚Hil β†’ π‘Š ∈ PreHil )
9 eqid ⊒ ( LSubSp β€˜ π‘Š ) = ( LSubSp β€˜ π‘Š )
10 2 9 csslss ⊒ ( ( π‘Š ∈ PreHil ∧ π‘ˆ ∈ 𝑆 ) β†’ π‘ˆ ∈ ( LSubSp β€˜ π‘Š ) )
11 8 10 sylan ⊒ ( ( π‘Š ∈ β„‚Hil ∧ π‘ˆ ∈ 𝑆 ) β†’ π‘ˆ ∈ ( LSubSp β€˜ π‘Š ) )
12 1 9 cphsscph ⊒ ( ( π‘Š ∈ β„‚PreHil ∧ π‘ˆ ∈ ( LSubSp β€˜ π‘Š ) ) β†’ 𝑋 ∈ β„‚PreHil )
13 4 11 12 syl2an2r ⊒ ( ( π‘Š ∈ β„‚Hil ∧ π‘ˆ ∈ 𝑆 ) β†’ 𝑋 ∈ β„‚PreHil )
14 ishl ⊒ ( 𝑋 ∈ β„‚Hil ↔ ( 𝑋 ∈ Ban ∧ 𝑋 ∈ β„‚PreHil ) )
15 7 13 14 sylanbrc ⊒ ( ( π‘Š ∈ β„‚Hil ∧ π‘ˆ ∈ 𝑆 ) β†’ 𝑋 ∈ β„‚Hil )