Metamath Proof Explorer

Theorem bncssbn

Description: A closed subspace of a Banach space which is also a subcomplex pre-Hilbert space is a Banach space. Remark: the assumption that the Banach space must be a (subcomplex) pre-Hilbert space is required because the definition of ClSubSp is based on an inner product. If ClSubSp was generalized for arbitrary topological spaces, this assuption could be omitted. (Contributed by AV, 8-Oct-2022)

Ref Expression
Hypotheses cmslssbn.x ⊒ 𝑋 = ( π‘Š β†Ύs π‘ˆ )
cmscsscms.s ⊒ 𝑆 = ( ClSubSp β€˜ π‘Š )
Assertion bncssbn ( ( ( π‘Š ∈ Ban ∧ π‘Š ∈ β„‚PreHil ) ∧ π‘ˆ ∈ 𝑆 ) β†’ 𝑋 ∈ Ban )

Proof

Step Hyp Ref Expression
1 cmslssbn.x ⊒ 𝑋 = ( π‘Š β†Ύs π‘ˆ )
2 cmscsscms.s ⊒ 𝑆 = ( ClSubSp β€˜ π‘Š )
3 bnnvc ⊒ ( π‘Š ∈ Ban β†’ π‘Š ∈ NrmVec )
4 eqid ⊒ ( Scalar β€˜ π‘Š ) = ( Scalar β€˜ π‘Š )
5 4 bnsca ⊒ ( π‘Š ∈ Ban β†’ ( Scalar β€˜ π‘Š ) ∈ CMetSp )
6 3 5 jca ⊒ ( π‘Š ∈ Ban β†’ ( π‘Š ∈ NrmVec ∧ ( Scalar β€˜ π‘Š ) ∈ CMetSp ) )
7 6 ad2antrr ⊒ ( ( ( π‘Š ∈ Ban ∧ π‘Š ∈ β„‚PreHil ) ∧ π‘ˆ ∈ 𝑆 ) β†’ ( π‘Š ∈ NrmVec ∧ ( Scalar β€˜ π‘Š ) ∈ CMetSp ) )
8 bncms ⊒ ( π‘Š ∈ Ban β†’ π‘Š ∈ CMetSp )
9 1 2 cmscsscms ⊒ ( ( ( π‘Š ∈ CMetSp ∧ π‘Š ∈ β„‚PreHil ) ∧ π‘ˆ ∈ 𝑆 ) β†’ 𝑋 ∈ CMetSp )
10 8 9 sylanl1 ⊒ ( ( ( π‘Š ∈ Ban ∧ π‘Š ∈ β„‚PreHil ) ∧ π‘ˆ ∈ 𝑆 ) β†’ 𝑋 ∈ CMetSp )
11 cphphl ⊒ ( π‘Š ∈ β„‚PreHil β†’ π‘Š ∈ PreHil )
12 11 adantl ⊒ ( ( π‘Š ∈ Ban ∧ π‘Š ∈ β„‚PreHil ) β†’ π‘Š ∈ PreHil )
13 eqid ⊒ ( LSubSp β€˜ π‘Š ) = ( LSubSp β€˜ π‘Š )
14 2 13 csslss ⊒ ( ( π‘Š ∈ PreHil ∧ π‘ˆ ∈ 𝑆 ) β†’ π‘ˆ ∈ ( LSubSp β€˜ π‘Š ) )
15 12 14 sylan ⊒ ( ( ( π‘Š ∈ Ban ∧ π‘Š ∈ β„‚PreHil ) ∧ π‘ˆ ∈ 𝑆 ) β†’ π‘ˆ ∈ ( LSubSp β€˜ π‘Š ) )
16 1 13 cmslssbn ⊒ ( ( ( π‘Š ∈ NrmVec ∧ ( Scalar β€˜ π‘Š ) ∈ CMetSp ) ∧ ( 𝑋 ∈ CMetSp ∧ π‘ˆ ∈ ( LSubSp β€˜ π‘Š ) ) ) β†’ 𝑋 ∈ Ban )
17 7 10 15 16 syl12anc ⊒ ( ( ( π‘Š ∈ Ban ∧ π‘Š ∈ β„‚PreHil ) ∧ π‘ˆ ∈ 𝑆 ) β†’ 𝑋 ∈ Ban )