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