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 ⊢ X = W ↾ 𝑠 U
lssbn.s ⊢ S = LSubSp ⁡ W
lssbn.j ⊢ J = TopOpen ⁡ W
Assertion lssbn ⊢ W ∈ Ban ∧ U ∈ S → X ∈ Ban ↔ U ∈ Clsd ⁡ J

Proof

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