Metamath Proof Explorer

Theorem hlim2

Description: The limit of a sequence on a Hilbert space. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( w = A -> ( F ~~>v w <-> F ~~>v A ) )
2 oveq2 
 |-  ( w = A -> ( ( F ` z ) -h w ) = ( ( F ` z ) -h A ) )
3 2 fveq2d 
 |-  ( w = A -> ( normh ` ( ( F ` z ) -h w ) ) = ( normh ` ( ( F ` z ) -h A ) ) )
4 3 breq1d 
 |-  ( w = A -> ( ( normh ` ( ( F ` z ) -h w ) ) < x <-> ( normh ` ( ( F ` z ) -h A ) ) < x ) )
5 4 rexralbidv 
 |-  ( w = A -> ( E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h w ) ) < x <-> E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x ) )
6 5 ralbidv 
 |-  ( w = A -> ( A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h w ) ) < x <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x ) )
7 1 6 bibi12d 
 |-  ( w = A -> ( ( F ~~>v w <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h w ) ) < x ) <-> ( F ~~>v A <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x ) ) )
8 7 imbi2d 
 |-  ( w = A -> ( ( F : NN --> ~H -> ( F ~~>v w <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h w ) ) < x ) ) <-> ( F : NN --> ~H -> ( F ~~>v A <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x ) ) ) )
9 vex 
 |-  w e. _V
10 9 hlimi 
 |-  ( F ~~>v w <-> ( ( F : NN --> ~H /\ w e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h w ) ) < x ) )
11 10 baib 
 |-  ( ( F : NN --> ~H /\ w e. ~H ) -> ( F ~~>v w <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h w ) ) < x ) )
12 11 expcom 
 |-  ( w e. ~H -> ( F : NN --> ~H -> ( F ~~>v w <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h w ) ) < x ) ) )
13 8 12 vtoclga 
 |-  ( A e. ~H -> ( F : NN --> ~H -> ( F ~~>v A <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x ) ) )
14 13 impcom 
 |-  ( ( F : NN --> ~H /\ A e. ~H ) -> ( F ~~>v A <-> A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x ) )