This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdm 
 |-  ( ( 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 ffvelcdm 
 |-  ( ( 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 eqabi 
 |-  ( ( 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 ) )