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

Metamath Proof Explorer

Theorem cssbn

Description: A complete subspace of a normed vector space with a complete scalar field is a Banach space. Remark: In contrast to ClSubSp , a complete subspace is defined by "a linear subspace in which all Cauchy sequences converge to a point in the subspace". This is closer to the original, but deprecated definition CH ( df-ch ) of closed subspaces of a Hilbert space. It may be superseded by cmslssbn . (Contributed by NM, 10-Apr-2008) (Revised by AV, 6-Oct-2022)

Ref Expression
Hypotheses cssbn.x 
|- X = ( W |`s U )
cssbn.s 
|- S = ( LSubSp ` W )
cssbn.d 
|- D = ( ( dist ` W ) |` ( U X. U ) )
Assertion cssbn 
|- ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> X e. Ban )

Proof

Step Hyp Ref Expression
1 cssbn.x 
 |-  X = ( W |`s U )
2 cssbn.s 
 |-  S = ( LSubSp ` W )
3 cssbn.d 
 |-  D = ( ( dist ` W ) |` ( U X. U ) )
4 simpl1 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> W e. NrmVec )
5 simpl2 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> ( Scalar ` W ) e. CMetSp )
6 nvcnlm 
 |-  ( W e. NrmVec -> W e. NrmMod )
7 nlmngp 
 |-  ( W e. NrmMod -> W e. NrmGrp )
8 6 7 syl 
 |-  ( W e. NrmVec -> W e. NrmGrp )
9 nvclmod 
 |-  ( W e. NrmVec -> W e. LMod )
10 2 lsssubg 
 |-  ( ( W e. LMod /\ U e. S ) -> U e. ( SubGrp ` W ) )
11 9 10 sylan 
 |-  ( ( W e. NrmVec /\ U e. S ) -> U e. ( SubGrp ` W ) )
12 1 subgngp 
 |-  ( ( W e. NrmGrp /\ U e. ( SubGrp ` W ) ) -> X e. NrmGrp )
13 8 11 12 syl2an2r 
 |-  ( ( W e. NrmVec /\ U e. S ) -> X e. NrmGrp )
14 13 3adant2 
 |-  ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) -> X e. NrmGrp )
15 14 adantr 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> X e. NrmGrp )
16 ngpms 
 |-  ( X e. NrmGrp -> X e. MetSp )
17 15 16 syl 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> X e. MetSp )
18 eqid 
 |-  ( dist ` W ) = ( dist ` W )
19 1 18 ressds 
 |-  ( U e. S -> ( dist ` W ) = ( dist ` X ) )
20 19 3ad2ant3 
 |-  ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) -> ( dist ` W ) = ( dist ` X ) )
21 11 3adant2 
 |-  ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) -> U e. ( SubGrp ` W ) )
22 1 subgbas 
 |-  ( U e. ( SubGrp ` W ) -> U = ( Base ` X ) )
23 21 22 syl 
 |-  ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) -> U = ( Base ` X ) )
24 23 sqxpeqd 
 |-  ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) -> ( U X. U ) = ( ( Base ` X ) X. ( Base ` X ) ) )
25 20 24 reseq12d 
 |-  ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) -> ( ( dist ` W ) |` ( U X. U ) ) = ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) )
26 3 25 eqtrid 
 |-  ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) -> D = ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) )
27 26 eqcomd 
 |-  ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) -> ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) = D )
28 27 adantr 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) = D )
29 eqid 
 |-  ( Base ` X ) = ( Base ` X )
30 eqid 
 |-  ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) = ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) )
31 29 30 ngpmet 
 |-  ( X e. NrmGrp -> ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) e. ( Met ` ( Base ` X ) ) )
32 14 31 syl 
 |-  ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) -> ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) e. ( Met ` ( Base ` X ) ) )
33 26 32 eqeltrd 
 |-  ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) -> D e. ( Met ` ( Base ` X ) ) )
34 33 adantr 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> D e. ( Met ` ( Base ` X ) ) )
35 simpr 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) )
36 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
37 36 iscmet2 
 |-  ( D e. ( CMet ` ( Base ` X ) ) <-> ( D e. ( Met ` ( Base ` X ) ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) )
38 34 35 37 sylanbrc 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> D e. ( CMet ` ( Base ` X ) ) )
39 28 38 eqeltrd 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) e. ( CMet ` ( Base ` X ) ) )
40 29 30 iscms 
 |-  ( X e. CMetSp <-> ( X e. MetSp /\ ( ( dist ` X ) |` ( ( Base ` X ) X. ( Base ` X ) ) ) e. ( CMet ` ( Base ` X ) ) ) )
41 17 39 40 sylanbrc 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> X e. CMetSp )
42 simpl3 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> U e. S )
43 1 2 cmslssbn 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp ) /\ ( X e. CMetSp /\ U e. S ) ) -> X e. Ban )
44 4 5 41 42 43 syl22anc 
 |-  ( ( ( W e. NrmVec /\ ( Scalar ` W ) e. CMetSp /\ U e. S ) /\ ( Cau ` D ) C_ dom ( ~~>t ` ( MetOpen ` D ) ) ) -> X e. Ban )