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

Metamath Proof Explorer

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 )