Metamath Proof Explorer


Theorem h2hcau

Description: The Cauchy sequences of Hilbert space. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 13-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses h2hc.1
|- U = <. <. +h , .h >. , normh >.
h2hc.2
|- U e. NrmCVec
h2hc.3
|- ~H = ( BaseSet ` U )
h2hc.4
|- D = ( IndMet ` U )
Assertion h2hcau
|- Cauchy = ( ( Cau ` D ) i^i ( ~H ^m NN ) )

Proof

Step Hyp Ref Expression
1 h2hc.1
 |-  U = <. <. +h , .h >. , normh >.
2 h2hc.2
 |-  U e. NrmCVec
3 h2hc.3
 |-  ~H = ( BaseSet ` U )
4 h2hc.4
 |-  D = ( IndMet ` U )
5 df-rab
 |-  { f e. ( ~H ^m NN ) | A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x } = { f | ( f e. ( ~H ^m NN ) /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) }
6 df-hcau
 |-  Cauchy = { f e. ( ~H ^m NN ) | A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x }
7 elin
 |-  ( f e. ( ( Cau ` D ) i^i ( ~H ^m NN ) ) <-> ( f e. ( Cau ` D ) /\ f e. ( ~H ^m NN ) ) )
8 ancom
 |-  ( ( f e. ( Cau ` D ) /\ f e. ( ~H ^m NN ) ) <-> ( f e. ( ~H ^m NN ) /\ f e. ( Cau ` D ) ) )
9 3 hlex
 |-  ~H e. _V
10 nnex
 |-  NN e. _V
11 9 10 elmap
 |-  ( f e. ( ~H ^m NN ) <-> f : NN --> ~H )
12 nnuz
 |-  NN = ( ZZ>= ` 1 )
13 3 4 imsxmet
 |-  ( U e. NrmCVec -> D e. ( *Met ` ~H ) )
14 2 13 mp1i
 |-  ( f : NN --> ~H -> D e. ( *Met ` ~H ) )
15 1zzd
 |-  ( f : NN --> ~H -> 1 e. ZZ )
16 eqidd
 |-  ( ( f : NN --> ~H /\ k e. NN ) -> ( f ` k ) = ( f ` k ) )
17 eqidd
 |-  ( ( f : NN --> ~H /\ j e. NN ) -> ( f ` j ) = ( f ` j ) )
18 id
 |-  ( f : NN --> ~H -> f : NN --> ~H )
19 12 14 15 16 17 18 iscauf
 |-  ( f : NN --> ~H -> ( f e. ( Cau ` D ) <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( f ` j ) D ( f ` k ) ) < x ) )
20 ffvelrn
 |-  ( ( f : NN --> ~H /\ j e. NN ) -> ( f ` j ) e. ~H )
21 20 adantr
 |-  ( ( ( f : NN --> ~H /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( f ` j ) e. ~H )
22 eluznn
 |-  ( ( j e. NN /\ k e. ( ZZ>= ` j ) ) -> k e. NN )
23 ffvelrn
 |-  ( ( f : NN --> ~H /\ k e. NN ) -> ( f ` k ) e. ~H )
24 22 23 sylan2
 |-  ( ( f : NN --> ~H /\ ( j e. NN /\ k e. ( ZZ>= ` j ) ) ) -> ( f ` k ) e. ~H )
25 24 anassrs
 |-  ( ( ( f : NN --> ~H /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( f ` k ) e. ~H )
26 1 2 3 4 h2hmetdval
 |-  ( ( ( f ` j ) e. ~H /\ ( f ` k ) e. ~H ) -> ( ( f ` j ) D ( f ` k ) ) = ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) )
27 21 25 26 syl2anc
 |-  ( ( ( f : NN --> ~H /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( f ` j ) D ( f ` k ) ) = ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) )
28 27 breq1d
 |-  ( ( ( f : NN --> ~H /\ j e. NN ) /\ k e. ( ZZ>= ` j ) ) -> ( ( ( f ` j ) D ( f ` k ) ) < x <-> ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) )
29 28 ralbidva
 |-  ( ( f : NN --> ~H /\ j e. NN ) -> ( A. k e. ( ZZ>= ` j ) ( ( f ` j ) D ( f ` k ) ) < x <-> A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) )
30 29 rexbidva
 |-  ( f : NN --> ~H -> ( E. j e. NN A. k e. ( ZZ>= ` j ) ( ( f ` j ) D ( f ` k ) ) < x <-> E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) )
31 30 ralbidv
 |-  ( f : NN --> ~H -> ( A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( ( f ` j ) D ( f ` k ) ) < x <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) )
32 19 31 bitrd
 |-  ( f : NN --> ~H -> ( f e. ( Cau ` D ) <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) )
33 11 32 sylbi
 |-  ( f e. ( ~H ^m NN ) -> ( f e. ( Cau ` D ) <-> A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) )
34 33 pm5.32i
 |-  ( ( f e. ( ~H ^m NN ) /\ f e. ( Cau ` D ) ) <-> ( f e. ( ~H ^m NN ) /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) )
35 7 8 34 3bitri
 |-  ( f e. ( ( Cau ` D ) i^i ( ~H ^m NN ) ) <-> ( f e. ( ~H ^m NN ) /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) )
36 35 abbi2i
 |-  ( ( Cau ` D ) i^i ( ~H ^m NN ) ) = { f | ( f e. ( ~H ^m NN ) /\ A. x e. RR+ E. j e. NN A. k e. ( ZZ>= ` j ) ( normh ` ( ( f ` j ) -h ( f ` k ) ) ) < x ) }
37 5 6 36 3eqtr4i
 |-  Cauchy = ( ( Cau ` D ) i^i ( ~H ^m NN ) )