Metamath Proof Explorer


Theorem ulmclm

Description: A uniform limit of functions converges pointwise. (Contributed by Mario Carneiro, 27-Feb-2015)

Ref Expression
Hypotheses ulmclm.z
|- Z = ( ZZ>= ` M )
ulmclm.m
|- ( ph -> M e. ZZ )
ulmclm.f
|- ( ph -> F : Z --> ( CC ^m S ) )
ulmclm.a
|- ( ph -> A e. S )
ulmclm.h
|- ( ph -> H e. W )
ulmclm.e
|- ( ( ph /\ k e. Z ) -> ( ( F ` k ) ` A ) = ( H ` k ) )
ulmclm.u
|- ( ph -> F ( ~~>u ` S ) G )
Assertion ulmclm
|- ( ph -> H ~~> ( G ` A ) )

Proof

Step Hyp Ref Expression
1 ulmclm.z
 |-  Z = ( ZZ>= ` M )
2 ulmclm.m
 |-  ( ph -> M e. ZZ )
3 ulmclm.f
 |-  ( ph -> F : Z --> ( CC ^m S ) )
4 ulmclm.a
 |-  ( ph -> A e. S )
5 ulmclm.h
 |-  ( ph -> H e. W )
6 ulmclm.e
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) ` A ) = ( H ` k ) )
7 ulmclm.u
 |-  ( ph -> F ( ~~>u ` S ) G )
8 fveq2
 |-  ( z = A -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` A ) )
9 fveq2
 |-  ( z = A -> ( G ` z ) = ( G ` A ) )
10 8 9 oveq12d
 |-  ( z = A -> ( ( ( F ` k ) ` z ) - ( G ` z ) ) = ( ( ( F ` k ) ` A ) - ( G ` A ) ) )
11 10 fveq2d
 |-  ( z = A -> ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) = ( abs ` ( ( ( F ` k ) ` A ) - ( G ` A ) ) ) )
12 11 breq1d
 |-  ( z = A -> ( ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x <-> ( abs ` ( ( ( F ` k ) ` A ) - ( G ` A ) ) ) < x ) )
13 12 rspcv
 |-  ( A e. S -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x -> ( abs ` ( ( ( F ` k ) ` A ) - ( G ` A ) ) ) < x ) )
14 4 13 syl
 |-  ( ph -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x -> ( abs ` ( ( ( F ` k ) ` A ) - ( G ` A ) ) ) < x ) )
15 14 ralimdv
 |-  ( ph -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x -> A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` A ) - ( G ` A ) ) ) < x ) )
16 15 reximdv
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x -> E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` A ) - ( G ` A ) ) ) < x ) )
17 16 ralimdv
 |-  ( ph -> ( A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` A ) - ( G ` A ) ) ) < x ) )
18 eqidd
 |-  ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` z ) )
19 eqidd
 |-  ( ( ph /\ z e. S ) -> ( G ` z ) = ( G ` z ) )
20 ulmcl
 |-  ( F ( ~~>u ` S ) G -> G : S --> CC )
21 7 20 syl
 |-  ( ph -> G : S --> CC )
22 ulmscl
 |-  ( F ( ~~>u ` S ) G -> S e. _V )
23 7 22 syl
 |-  ( ph -> S e. _V )
24 1 2 3 18 19 21 23 ulm2
 |-  ( ph -> ( F ( ~~>u ` S ) G <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) )
25 6 eqcomd
 |-  ( ( ph /\ k e. Z ) -> ( H ` k ) = ( ( F ` k ) ` A ) )
26 21 4 ffvelrnd
 |-  ( ph -> ( G ` A ) e. CC )
27 3 ffvelrnda
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. ( CC ^m S ) )
28 elmapi
 |-  ( ( F ` k ) e. ( CC ^m S ) -> ( F ` k ) : S --> CC )
29 27 28 syl
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) : S --> CC )
30 4 adantr
 |-  ( ( ph /\ k e. Z ) -> A e. S )
31 29 30 ffvelrnd
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) ` A ) e. CC )
32 1 2 5 25 26 31 clim2c
 |-  ( ph -> ( H ~~> ( G ` A ) <-> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) ( abs ` ( ( ( F ` k ) ` A ) - ( G ` A ) ) ) < x ) )
33 17 24 32 3imtr4d
 |-  ( ph -> ( F ( ~~>u ` S ) G -> H ~~> ( G ` A ) ) )
34 7 33 mpd
 |-  ( ph -> H ~~> ( G ` A ) )