This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )