Metamath Proof Explorer

Theorem bnsscmcl

Description: A subspace of a Banach space is a Banach space iff it is closed in the norm-induced metric of the parent space. (Contributed by NM, 1-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses bnsscmcl.x ⊢ X = BaseSet ⁡ U
bnsscmcl.d ⊢ D = IndMet ⁡ U
bnsscmcl.j ⊢ J = MetOpen ⁡ D
bnsscmcl.h ⊢ H = SubSp ⁡ U
bnsscmcl.y ⊢ Y = BaseSet ⁡ W
Assertion bnsscmcl ⊢ U ∈ CBan ∧ W ∈ H → W ∈ CBan ↔ Y ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 bnsscmcl.x ⊢ X = BaseSet ⁡ U
2 bnsscmcl.d ⊢ D = IndMet ⁡ U
3 bnsscmcl.j ⊢ J = MetOpen ⁡ D
4 bnsscmcl.h ⊢ H = SubSp ⁡ U
5 bnsscmcl.y ⊢ Y = BaseSet ⁡ W
6 bnnv ⊢ U ∈ CBan → U ∈ NrmCVec
7 4 sspnv ⊢ U ∈ NrmCVec ∧ W ∈ H → W ∈ NrmCVec
8 6 7 sylan ⊢ U ∈ CBan ∧ W ∈ H → W ∈ NrmCVec
9 eqid ⊢ IndMet ⁡ W = IndMet ⁡ W
10 5 9 iscbn ⊢ W ∈ CBan ↔ W ∈ NrmCVec ∧ IndMet ⁡ W ∈ CMet ⁡ Y
11 10 baib ⊢ W ∈ NrmCVec → W ∈ CBan ↔ IndMet ⁡ W ∈ CMet ⁡ Y
12 8 11 syl ⊢ U ∈ CBan ∧ W ∈ H → W ∈ CBan ↔ IndMet ⁡ W ∈ CMet ⁡ Y
13 5 2 9 4 sspims ⊢ U ∈ NrmCVec ∧ W ∈ H → IndMet ⁡ W = D ↾ Y × Y
14 6 13 sylan ⊢ U ∈ CBan ∧ W ∈ H → IndMet ⁡ W = D ↾ Y × Y
15 14 eleq1d ⊢ U ∈ CBan ∧ W ∈ H → IndMet ⁡ W ∈ CMet ⁡ Y ↔ D ↾ Y × Y ∈ CMet ⁡ Y
16 1 2 cbncms ⊢ U ∈ CBan → D ∈ CMet ⁡ X
17 16 adantr ⊢ U ∈ CBan ∧ W ∈ H → D ∈ CMet ⁡ X
18 3 cmetss ⊢ D ∈ CMet ⁡ X → D ↾ Y × Y ∈ CMet ⁡ Y ↔ Y ∈ Clsd ⁡ J
19 17 18 syl ⊢ U ∈ CBan ∧ W ∈ H → D ↾ Y × Y ∈ CMet ⁡ Y ↔ Y ∈ Clsd ⁡ J
20 12 15 19 3bitrd ⊢ U ∈ CBan ∧ W ∈ H → W ∈ CBan ↔ Y ∈ Clsd ⁡ J