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 )