Theorem cmslsschl

Description: A complete linear subspace of a subcomplex Hilbert space is a subcomplex Hilbert space. (Contributed by AV, 8-Oct-2022)

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

Proof

Step	Hyp	Ref	Expression
1		cmslsschl.x	⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2		cmslsschl.s	⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3		hlbn	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ Ban )
4		bnnvc	⊢ ( 𝑊 ∈ Ban → 𝑊 ∈ NrmVec )
5	3 4	syl	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ NrmVec )
6	5	3ad2ant1	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → 𝑊 ∈ NrmVec )
7		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
8	7	bnsca	⊢ ( 𝑊 ∈ Ban → ( Scalar ‘ 𝑊 ) ∈ CMetSp )
9	3 8	syl	⊢ ( 𝑊 ∈ ℂHil → ( Scalar ‘ 𝑊 ) ∈ CMetSp )
10	9	3ad2ant1	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑊 ) ∈ CMetSp )
11		3simpc	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → ( 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) )
12	1 2	cmslssbn	⊢ ( ( ( 𝑊 ∈ NrmVec ∧ ( Scalar ‘ 𝑊 ) ∈ CMetSp ) ∧ ( 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) ) → 𝑋 ∈ Ban )
13	6 10 11 12	syl21anc	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ Ban )
14		hlcph	⊢ ( 𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil )
15	1 2	cphsscph	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ ℂPreHil )
16	14 15	sylan	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ ℂPreHil )
17	16	3adant2	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ ℂPreHil )
18		ishl	⊢ ( 𝑋 ∈ ℂHil ↔ ( 𝑋 ∈ Ban ∧ 𝑋 ∈ ℂPreHil ) )
19	13 17 18	sylanbrc	⊢ ( ( 𝑊 ∈ ℂHil ∧ 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ ℂHil )