Metamath Proof Explorer


Theorem hhssbnOLD

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 × H norm H
hhssbnOLD.2 H C
Assertion hhssbnOLD W CBan

Proof

Step Hyp Ref Expression
1 hhssbnOLD.1 W = + H × H × H norm H
2 hhssbnOLD.2 H C
3 2 chshii H S
4 1 3 hhssnv W NrmCVec
5 eqid IndMet W = IndMet W
6 1 5 2 hhsscms IndMet W CMet H
7 1 3 hhssba H = BaseSet W
8 7 5 iscbn W CBan W NrmCVec IndMet W CMet H
9 4 6 8 mpbir2an W CBan