Metamath Proof Explorer

Theorem hhsscms

Description: The induced metric of a closed subspace is complete. (Contributed by NM, 10-Apr-2008) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses hhssims2.1 
|- W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
hhssims2.3 
|- D = ( IndMet ` W )
hhsscms.3 
|- H e. CH
Assertion hhsscms 
|- D e. ( CMet ` H )

Proof

Step Hyp Ref Expression
1 hhssims2.1 
 |-  W = <. <. ( +h |` ( H X. H ) ) , ( .h |` ( CC X. H ) ) >. , ( normh |` H ) >.
2 hhssims2.3 
 |-  D = ( IndMet ` W )
3 hhsscms.3 
 |-  H e. CH
4 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
5 3 chshii 
 |-  H e. SH
6 1 2 5 hhssmet 
 |-  D e. ( Met ` H )
7 simpl 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> f e. ( Cau ` D ) )
8 1 2 5 hhssims2 
 |-  D = ( ( normh o. -h ) |` ( H X. H ) )
9 8 fveq2i 
 |-  ( Cau ` D ) = ( Cau ` ( ( normh o. -h ) |` ( H X. H ) ) )
10 7 9 eleqtrdi 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> f e. ( Cau ` ( ( normh o. -h ) |` ( H X. H ) ) ) )
11 eqid 
 |-  ( normh o. -h ) = ( normh o. -h )
12 11 hilxmet 
 |-  ( normh o. -h ) e. ( *Met ` ~H )
13 simpr 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> f : NN --> H )
14 causs 
 |-  ( ( ( normh o. -h ) e. ( *Met ` ~H ) /\ f : NN --> H ) -> ( f e. ( Cau ` ( normh o. -h ) ) <-> f e. ( Cau ` ( ( normh o. -h ) |` ( H X. H ) ) ) ) )
15 12 13 14 sylancr 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> ( f e. ( Cau ` ( normh o. -h ) ) <-> f e. ( Cau ` ( ( normh o. -h ) |` ( H X. H ) ) ) ) )
16 10 15 mpbird 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> f e. ( Cau ` ( normh o. -h ) ) )
17 3 chssii 
 |-  H C_ ~H
18 fss 
 |-  ( ( f : NN --> H /\ H C_ ~H ) -> f : NN --> ~H )
19 13 17 18 sylancl 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> f : NN --> ~H )
20 ax-hilex 
 |-  ~H e. _V
21 nnex 
 |-  NN e. _V
22 20 21 elmap 
 |-  ( f e. ( ~H ^m NN ) <-> f : NN --> ~H )
23 19 22 sylibr 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> f e. ( ~H ^m NN ) )
24 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
25 24 11 hhims 
 |-  ( normh o. -h ) = ( IndMet ` <. <. +h , .h >. , normh >. )
26 24 25 hhcau 
 |-  Cauchy = ( ( Cau ` ( normh o. -h ) ) i^i ( ~H ^m NN ) )
27 26 elin2 
 |-  ( f e. Cauchy <-> ( f e. ( Cau ` ( normh o. -h ) ) /\ f e. ( ~H ^m NN ) ) )
28 16 23 27 sylanbrc 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> f e. Cauchy )
29 ax-hcompl 
 |-  ( f e. Cauchy -> E. x e. ~H f ~~>v x )
30 vex 
 |-  f e. _V
31 vex 
 |-  x e. _V
32 30 31 breldm 
 |-  ( f ~~>v x -> f e. dom ~~>v )
33 32 rexlimivw 
 |-  ( E. x e. ~H f ~~>v x -> f e. dom ~~>v )
34 28 29 33 3syl 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> f e. dom ~~>v )
35 hlimf 
 |-  ~~>v : dom ~~>v --> ~H
36 ffun 
 |-  ( ~~>v : dom ~~>v --> ~H -> Fun ~~>v )
37 funfvbrb 
 |-  ( Fun ~~>v -> ( f e. dom ~~>v <-> f ~~>v ( ~~>v ` f ) ) )
38 35 36 37 mp2b 
 |-  ( f e. dom ~~>v <-> f ~~>v ( ~~>v ` f ) )
39 34 38 sylib 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> f ~~>v ( ~~>v ` f ) )
40 eqid 
 |-  ( MetOpen ` ( normh o. -h ) ) = ( MetOpen ` ( normh o. -h ) )
41 24 25 40 hhlm 
 |-  ~~>v = ( ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) |` ( ~H ^m NN ) )
42 resss 
 |-  ( ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) |` ( ~H ^m NN ) ) C_ ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) )
43 41 42 eqsstri 
 |-  ~~>v C_ ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) )
44 43 ssbri 
 |-  ( f ~~>v ( ~~>v ` f ) -> f ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) ( ~~>v ` f ) )
45 39 44 syl 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> f ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) ( ~~>v ` f ) )
46 8 40 4 metrest 
 |-  ( ( ( normh o. -h ) e. ( *Met ` ~H ) /\ H C_ ~H ) -> ( ( MetOpen ` ( normh o. -h ) ) |`t H ) = ( MetOpen ` D ) )
47 12 17 46 mp2an 
 |-  ( ( MetOpen ` ( normh o. -h ) ) |`t H ) = ( MetOpen ` D )
48 47 eqcomi 
 |-  ( MetOpen ` D ) = ( ( MetOpen ` ( normh o. -h ) ) |`t H )
49 nnuz 
 |-  NN = ( ZZ>= ` 1 )
50 3 a1i 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> H e. CH )
51 40 mopntop 
 |-  ( ( normh o. -h ) e. ( *Met ` ~H ) -> ( MetOpen ` ( normh o. -h ) ) e. Top )
52 12 51 mp1i 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> ( MetOpen ` ( normh o. -h ) ) e. Top )
53 fvex 
 |-  ( ~~>v ` f ) e. _V
54 53 chlimi 
 |-  ( ( H e. CH /\ f : NN --> H /\ f ~~>v ( ~~>v ` f ) ) -> ( ~~>v ` f ) e. H )
55 50 13 39 54 syl3anc 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> ( ~~>v ` f ) e. H )
56 1zzd 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> 1 e. ZZ )
57 48 49 50 52 55 56 13 lmss 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> ( f ( ~~>t ` ( MetOpen ` ( normh o. -h ) ) ) ( ~~>v ` f ) <-> f ( ~~>t ` ( MetOpen ` D ) ) ( ~~>v ` f ) ) )
58 45 57 mpbid 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> f ( ~~>t ` ( MetOpen ` D ) ) ( ~~>v ` f ) )
59 30 53 breldm 
 |-  ( f ( ~~>t ` ( MetOpen ` D ) ) ( ~~>v ` f ) -> f e. dom ( ~~>t ` ( MetOpen ` D ) ) )
60 58 59 syl 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> H ) -> f e. dom ( ~~>t ` ( MetOpen ` D ) ) )
61 4 6 60 iscmet3i 
 |-  D e. ( CMet ` H )