Metamath Proof Explorer

Theorem hhcms

Description: The Hilbert space induced metric determines a complete metric space. (Contributed by NM, 10-Apr-2008) (Proof shortened by Mario Carneiro, 14-May-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022) (New usage is discouraged.)

Ref Expression
Hypotheses hhcms.1 
|- U = <. <. +h , .h >. , normh >.
hhcms.2 
|- D = ( IndMet ` U )
Assertion hhcms 
|- D e. ( CMet ` ~H )

Proof

Step Hyp Ref Expression
1 hhcms.1 
 |-  U = <. <. +h , .h >. , normh >.
2 hhcms.2 
 |-  D = ( IndMet ` U )
3 eqid 
 |-  ( MetOpen ` D ) = ( MetOpen ` D )
4 1 2 hhmet 
 |-  D e. ( Met ` ~H )
5 1 2 hhcau 
 |-  Cauchy = ( ( Cau ` D ) i^i ( ~H ^m NN ) )
6 5 eleq2i 
 |-  ( f e. Cauchy <-> f e. ( ( Cau ` D ) i^i ( ~H ^m NN ) ) )
7 elin 
 |-  ( f e. ( ( Cau ` D ) i^i ( ~H ^m NN ) ) <-> ( f e. ( Cau ` D ) /\ f e. ( ~H ^m NN ) ) )
8 ax-hilex 
 |-  ~H e. _V
9 nnex 
 |-  NN e. _V
10 8 9 elmap 
 |-  ( f e. ( ~H ^m NN ) <-> f : NN --> ~H )
11 10 anbi2i 
 |-  ( ( f e. ( Cau ` D ) /\ f e. ( ~H ^m NN ) ) <-> ( f e. ( Cau ` D ) /\ f : NN --> ~H ) )
12 7 11 bitri 
 |-  ( f e. ( ( Cau ` D ) i^i ( ~H ^m NN ) ) <-> ( f e. ( Cau ` D ) /\ f : NN --> ~H ) )
13 6 12 bitri 
 |-  ( f e. Cauchy <-> ( f e. ( Cau ` D ) /\ f : NN --> ~H ) )
14 ax-hcompl 
 |-  ( f e. Cauchy -> E. x e. ~H f ~~>v x )
15 13 14 sylbir 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> ~H ) -> E. x e. ~H f ~~>v x )
16 1 2 3 hhlm 
 |-  ~~>v = ( ( ~~>t ` ( MetOpen ` D ) ) |` ( ~H ^m NN ) )
17 16 breqi 
 |-  ( f ~~>v x <-> f ( ( ~~>t ` ( MetOpen ` D ) ) |` ( ~H ^m NN ) ) x )
18 vex 
 |-  x e. _V
19 18 brresi 
 |-  ( f ( ( ~~>t ` ( MetOpen ` D ) ) |` ( ~H ^m NN ) ) x <-> ( f e. ( ~H ^m NN ) /\ f ( ~~>t ` ( MetOpen ` D ) ) x ) )
20 17 19 bitri 
 |-  ( f ~~>v x <-> ( f e. ( ~H ^m NN ) /\ f ( ~~>t ` ( MetOpen ` D ) ) x ) )
21 vex 
 |-  f e. _V
22 21 18 breldm 
 |-  ( f ( ~~>t ` ( MetOpen ` D ) ) x -> f e. dom ( ~~>t ` ( MetOpen ` D ) ) )
23 20 22 simplbiim 
 |-  ( f ~~>v x -> f e. dom ( ~~>t ` ( MetOpen ` D ) ) )
24 23 rexlimivw 
 |-  ( E. x e. ~H f ~~>v x -> f e. dom ( ~~>t ` ( MetOpen ` D ) ) )
25 15 24 syl 
 |-  ( ( f e. ( Cau ` D ) /\ f : NN --> ~H ) -> f e. dom ( ~~>t ` ( MetOpen ` D ) ) )
26 3 4 25 iscmet3i 
 |-  D e. ( CMet ` ~H )