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 ) ) )