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 e. CBan /\ W e. H ) -> ( W e. CBan <-> Y e. ( 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 e. CBan -> U e. NrmCVec )
7 4 sspnv
 |-  ( ( U e. NrmCVec /\ W e. H ) -> W e. NrmCVec )
8 6 7 sylan
 |-  ( ( U e. CBan /\ W e. H ) -> W e. NrmCVec )
9 eqid
 |-  ( IndMet ` W ) = ( IndMet ` W )
10 5 9 iscbn
 |-  ( W e. CBan <-> ( W e. NrmCVec /\ ( IndMet ` W ) e. ( CMet ` Y ) ) )
11 10 baib
 |-  ( W e. NrmCVec -> ( W e. CBan <-> ( IndMet ` W ) e. ( CMet ` Y ) ) )
12 8 11 syl
 |-  ( ( U e. CBan /\ W e. H ) -> ( W e. CBan <-> ( IndMet ` W ) e. ( CMet ` Y ) ) )
13 5 2 9 4 sspims
 |-  ( ( U e. NrmCVec /\ W e. H ) -> ( IndMet ` W ) = ( D |` ( Y X. Y ) ) )
14 6 13 sylan
 |-  ( ( U e. CBan /\ W e. H ) -> ( IndMet ` W ) = ( D |` ( Y X. Y ) ) )
15 14 eleq1d
 |-  ( ( U e. CBan /\ W e. H ) -> ( ( IndMet ` W ) e. ( CMet ` Y ) <-> ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) ) )
16 1 2 cbncms
 |-  ( U e. CBan -> D e. ( CMet ` X ) )
17 16 adantr
 |-  ( ( U e. CBan /\ W e. H ) -> D e. ( CMet ` X ) )
18 3 cmetss
 |-  ( D e. ( CMet ` X ) -> ( ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) <-> Y e. ( Clsd ` J ) ) )
19 17 18 syl
 |-  ( ( U e. CBan /\ W e. H ) -> ( ( D |` ( Y X. Y ) ) e. ( CMet ` Y ) <-> Y e. ( Clsd ` J ) ) )
20 12 15 19 3bitrd
 |-  ( ( U e. CBan /\ W e. H ) -> ( W e. CBan <-> Y e. ( Clsd ` J ) ) )