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

Metamath Proof Explorer

Theorem hlimi

Description: Express the predicate: The limit of vector sequence F in a Hilbert space is A , i.e. F converges to A . This means that for any real x , no matter how small, there always exists an integer y such that the norm of any later vector in the sequence minus the limit is less than x . Definition of converge in Beran p. 96. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Hypothesis hlim.1 
|- A e. _V
Assertion hlimi 
|- ( F ~~>v A <-> ( ( F : NN --> ~H /\ A e. ~H ) /\ 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 hlim.1 
 |-  A e. _V
2 df-hlim 
 |-  ~~>v = { <. f , 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 ) }
3 2 relopabiv 
 |-  Rel ~~>v
4 3 brrelex1i 
 |-  ( F ~~>v A -> F e. _V )
5 nnex 
 |-  NN e. _V
6 fex 
 |-  ( ( F : NN --> ~H /\ NN e. _V ) -> F e. _V )
7 5 6 mpan2 
 |-  ( F : NN --> ~H -> F e. _V )
8 7 ad2antrr 
 |-  ( ( ( F : NN --> ~H /\ A e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x ) -> F e. _V )
9 feq1 
 |-  ( f = F -> ( f : NN --> ~H <-> F : NN --> ~H ) )
10 eleq1 
 |-  ( w = A -> ( w e. ~H <-> A e. ~H ) )
11 9 10 bi2anan9 
 |-  ( ( f = F /\ w = A ) -> ( ( f : NN --> ~H /\ w e. ~H ) <-> ( F : NN --> ~H /\ A e. ~H ) ) )
12 fveq1 
 |-  ( f = F -> ( f ` z ) = ( F ` z ) )
13 oveq12 
 |-  ( ( ( f ` z ) = ( F ` z ) /\ w = A ) -> ( ( f ` z ) -h w ) = ( ( F ` z ) -h A ) )
14 12 13 sylan 
 |-  ( ( f = F /\ w = A ) -> ( ( f ` z ) -h w ) = ( ( F ` z ) -h A ) )
15 14 fveq2d 
 |-  ( ( f = F /\ w = A ) -> ( normh ` ( ( f ` z ) -h w ) ) = ( normh ` ( ( F ` z ) -h A ) ) )
16 15 breq1d 
 |-  ( ( f = F /\ w = A ) -> ( ( normh ` ( ( f ` z ) -h w ) ) < x <-> ( normh ` ( ( F ` z ) -h A ) ) < x ) )
17 16 rexralbidv 
 |-  ( ( f = F /\ 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 ) )
18 17 ralbidv 
 |-  ( ( f = F /\ 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 ) )
19 11 18 anbi12d 
 |-  ( ( f = F /\ w = A ) -> ( ( ( 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 ) <-> ( ( F : NN --> ~H /\ A e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x ) ) )
20 19 2 brabga 
 |-  ( ( F e. _V /\ A e. _V ) -> ( F ~~>v A <-> ( ( F : NN --> ~H /\ A e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x ) ) )
21 1 20 mpan2 
 |-  ( F e. _V -> ( F ~~>v A <-> ( ( F : NN --> ~H /\ A e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x ) ) )
22 4 8 21 pm5.21nii 
 |-  ( F ~~>v A <-> ( ( F : NN --> ~H /\ A e. ~H ) /\ A. x e. RR+ E. y e. NN A. z e. ( ZZ>= ` y ) ( normh ` ( ( F ` z ) -h A ) ) < x ) )