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

Metamath Proof Explorer

Theorem hcau

Description: Member of the set of Cauchy sequences on a Hilbert space. Definition for Cauchy sequence in Beran p. 96. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Assertion hcau 
|- ( F e. Cauchy <-> ( F : NN --> ~H /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )

Proof

Step Hyp Ref Expression
1 fveq1 
 |-  ( f = F -> ( f ` y ) = ( F ` y ) )
2 fveq1 
 |-  ( f = F -> ( f ` z ) = ( F ` z ) )
3 1 2 oveq12d 
 |-  ( f = F -> ( ( f ` y ) -h ( f ` z ) ) = ( ( F ` y ) -h ( F ` z ) ) )
4 3 fveq2d 
 |-  ( f = F -> ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) = ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) )
5 4 breq1d 
 |-  ( f = F -> ( ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x <-> ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )
6 5 rexralbidv 
 |-  ( f = F -> ( E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x <-> E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )
7 6 ralbidv 
 |-  ( f = F -> ( A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )
8 df-hcau 
 |-  Cauchy = { f e. ( ~H ^m NN ) | A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( f ` y ) -h ( f ` z ) ) ) < x }
9 7 8 elrab2 
 |-  ( F e. Cauchy <-> ( F e. ( ~H ^m NN ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )
10 ax-hilex 
 |-  ~H e. _V
11 nnex 
 |-  NN e. _V
12 10 11 elmap 
 |-  ( F e. ( ~H ^m NN ) <-> F : NN --> ~H )
13 12 anbi1i 
 |-  ( ( F e. ( ~H ^m NN ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) <-> ( F : NN --> ~H /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )
14 9 13 bitri 
 |-  ( F e. Cauchy <-> ( F : NN --> ~H /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` y ) -h ( F ` z ) ) ) < x ) )