Metamath Proof Explorer

Theorem lssbn

Description: A subspace of a Banach space is a Banach space iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypotheses lssbn.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
lssbn.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lssbn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
Assertion lssbn ( ( 𝑊 ∈ Ban ∧ 𝑈 ∈ 𝑆 ) → ( 𝑋 ∈ Ban ↔ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 lssbn.x ⊢ 𝑋 = ( 𝑊 ↾s 𝑈 )
2 lssbn.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lssbn.j ⊢ 𝐽 = ( TopOpen ‘ 𝑊 )
4 bnnvc ⊢ ( 𝑊 ∈ Ban → 𝑊 ∈ NrmVec )
5 1 2 lssnvc ⊢ ( ( 𝑊 ∈ NrmVec ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ NrmVec )
6 4 5 sylan ⊢ ( ( 𝑊 ∈ Ban ∧ 𝑈 ∈ 𝑆 ) → 𝑋 ∈ NrmVec )
7 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
8 1 7 resssca ⊢ ( 𝑈 ∈ 𝑆 → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
9 8 adantl ⊢ ( ( 𝑊 ∈ Ban ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑋 ) )
10 7 bnsca ⊢ ( 𝑊 ∈ Ban → ( Scalar ‘ 𝑊 ) ∈ CMetSp )
11 10 adantr ⊢ ( ( 𝑊 ∈ Ban ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑊 ) ∈ CMetSp )
12 9 11 eqeltrrd ⊢ ( ( 𝑊 ∈ Ban ∧ 𝑈 ∈ 𝑆 ) → ( Scalar ‘ 𝑋 ) ∈ CMetSp )
13 eqid ⊢ ( Scalar ‘ 𝑋 ) = ( Scalar ‘ 𝑋 )
14 13 isbn ⊢ ( 𝑋 ∈ Ban ↔ ( 𝑋 ∈ NrmVec ∧ 𝑋 ∈ CMetSp ∧ ( Scalar ‘ 𝑋 ) ∈ CMetSp ) )
15 3anan32 ⊢ ( ( 𝑋 ∈ NrmVec ∧ 𝑋 ∈ CMetSp ∧ ( Scalar ‘ 𝑋 ) ∈ CMetSp ) ↔ ( ( 𝑋 ∈ NrmVec ∧ ( Scalar ‘ 𝑋 ) ∈ CMetSp ) ∧ 𝑋 ∈ CMetSp ) )
16 14 15 bitri ⊢ ( 𝑋 ∈ Ban ↔ ( ( 𝑋 ∈ NrmVec ∧ ( Scalar ‘ 𝑋 ) ∈ CMetSp ) ∧ 𝑋 ∈ CMetSp ) )
17 16 baib ⊢ ( ( 𝑋 ∈ NrmVec ∧ ( Scalar ‘ 𝑋 ) ∈ CMetSp ) → ( 𝑋 ∈ Ban ↔ 𝑋 ∈ CMetSp ) )
18 6 12 17 syl2anc ⊢ ( ( 𝑊 ∈ Ban ∧ 𝑈 ∈ 𝑆 ) → ( 𝑋 ∈ Ban ↔ 𝑋 ∈ CMetSp ) )
19 bncms ⊢ ( 𝑊 ∈ Ban → 𝑊 ∈ CMetSp )
20 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
21 20 2 lssss ⊢ ( 𝑈 ∈ 𝑆 → 𝑈 ⊆ ( Base ‘ 𝑊 ) )
22 1 20 3 cmsss ⊢ ( ( 𝑊 ∈ CMetSp ∧ 𝑈 ⊆ ( Base ‘ 𝑊 ) ) → ( 𝑋 ∈ CMetSp ↔ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) )
23 19 21 22 syl2an ⊢ ( ( 𝑊 ∈ Ban ∧ 𝑈 ∈ 𝑆 ) → ( 𝑋 ∈ CMetSp ↔ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) )
24 18 23 bitrd ⊢ ( ( 𝑊 ∈ Ban ∧ 𝑈 ∈ 𝑆 ) → ( 𝑋 ∈ Ban ↔ 𝑈 ∈ ( Clsd ‘ 𝐽 ) ) )