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