Theorem cphssphl

Description: A Banach subspace of a subcomplex pre-Hilbert space is a subcomplex Hilbert space. (Contributed by NM, 11-Apr-2008) (Revised by AV, 25-Sep-2022)

	Ref	Expression
Hypotheses	cphssphl.x	⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
	cphssphl.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
Assertion	cphssphl	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ Ban ) → 𝑋 ∈ ℂHil )

Proof

Step	Hyp	Ref	Expression
1		cphssphl.x	⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2		cphssphl.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		simp3	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ Ban ) → 𝑋 ∈ Ban )
4	1 2	cphsscph	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ ℂPreHil )
5	4	3adant3	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ Ban ) → 𝑋 ∈ ℂPreHil )
6		ishl	⊢ ( 𝑋 ∈ ℂHil ↔ ( 𝑋 ∈ Ban ∧ 𝑋 ∈ ℂPreHil ) )
7	3 5 6	sylanbrc	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ Ban ) → 𝑋 ∈ ℂHil )