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

Metamath Proof Explorer

Theorem bnsscmcl

Proof