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