This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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