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 )