Description: Obsolete version of cssbn : Banach space property of a closed subspace. (Contributed by NM, 10-Apr-2008) (New usage is discouraged.) (Proof modification is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | hhssbnOLD.1 | |- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. |
|
| hhssbnOLD.2 | |- H e. CH |
||
| Assertion | hhssbnOLD | |- W e. CBan |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hhssbnOLD.1 | |- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >. |
|
| 2 | hhssbnOLD.2 | |- H e. CH |
|
| 3 | 2 | chshii | |- H e. SH |
| 4 | 1 3 | hhssnv | |- W e. NrmCVec |
| 5 | eqid | |- ( IndMet ` W ) = ( IndMet ` W ) |
|
| 6 | 1 5 2 | hhsscms | |- ( IndMet ` W ) e. ( CMet ` H ) |
| 7 | 1 3 | hhssba | |- H = ( BaseSet ` W ) |
| 8 | 7 5 | iscbn | |- ( W e. CBan <-> ( W e. NrmCVec /\ ( IndMet ` W ) e. ( CMet ` H ) ) ) |
| 9 | 4 6 8 | mpbir2an | |- W e. CBan |