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 ) )