Theorem lssbn

Description: A subspace of a Banach space is a Banach space iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypotheses	lssbn.x	|- X = ( W |`s U )
	lssbn.s	|- S = ( LSubSp ` W )
	lssbn.j	|- J = ( TopOpen ` W )
Assertion	lssbn	|- ( ( W e. Ban /\ U e. S ) -> ( X e. Ban <-> U e. ( Clsd ` J ) ) )

Proof

Step	Hyp	Ref	Expression
1		lssbn.x	|- X = ( W |`s U )
2		lssbn.s	|- S = ( LSubSp ` W )
3		lssbn.j	|- J = ( TopOpen ` W )
4		bnnvc	|- ( W e. Ban -> W e. NrmVec )
5	1 2	lssnvc	|- ( ( W e. NrmVec /\ U e. S ) -> X e. NrmVec )
6	4 5	sylan	|- ( ( W e. Ban /\ U e. S ) -> X e. NrmVec )
7		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
8	1 7	resssca	|- ( U e. S -> ( Scalar ` W ) = ( Scalar ` X ) )
9	8	adantl	|- ( ( W e. Ban /\ U e. S ) -> ( Scalar ` W ) = ( Scalar ` X ) )
10	7	bnsca	|- ( W e. Ban -> ( Scalar ` W ) e. CMetSp )
11	10	adantr	|- ( ( W e. Ban /\ U e. S ) -> ( Scalar ` W ) e. CMetSp )
12	9 11	eqeltrrd	|- ( ( W e. Ban /\ U e. S ) -> ( Scalar ` X ) e. CMetSp )
13		eqid	|- ( Scalar ` X ) = ( Scalar ` X )
14	13	isbn	|- ( X e. Ban <-> ( X e. NrmVec /\ X e. CMetSp /\ ( Scalar ` X ) e. CMetSp ) )
15		3anan32	|- ( ( X e. NrmVec /\ X e. CMetSp /\ ( Scalar ` X ) e. CMetSp ) <-> ( ( X e. NrmVec /\ ( Scalar ` X ) e. CMetSp ) /\ X e. CMetSp ) )
16	14 15	bitri	|- ( X e. Ban <-> ( ( X e. NrmVec /\ ( Scalar ` X ) e. CMetSp ) /\ X e. CMetSp ) )
17	16	baib	|- ( ( X e. NrmVec /\ ( Scalar ` X ) e. CMetSp ) -> ( X e. Ban <-> X e. CMetSp ) )
18	6 12 17	syl2anc	|- ( ( W e. Ban /\ U e. S ) -> ( X e. Ban <-> X e. CMetSp ) )
19		bncms	|- ( W e. Ban -> W e. CMetSp )
20		eqid	|- ( Base ` W ) = ( Base ` W )
21	20 2	lssss	|- ( U e. S -> U C_ ( Base ` W ) )
22	1 20 3	cmsss	|- ( ( W e. CMetSp /\ U C_ ( Base ` W ) ) -> ( X e. CMetSp <-> U e. ( Clsd ` J ) ) )
23	19 21 22	syl2an	|- ( ( W e. Ban /\ U e. S ) -> ( X e. CMetSp <-> U e. ( Clsd ` J ) ) )
24	18 23	bitrd	|- ( ( W e. Ban /\ U e. S ) -> ( X e. Ban <-> U e. ( Clsd ` J ) ) )