Step |
Hyp |
Ref |
Expression |
1 |
|
ulm0.z |
|- Z = ( ZZ>= ` M ) |
2 |
|
ulm0.m |
|- ( ph -> M e. ZZ ) |
3 |
|
ulm0.f |
|- ( ph -> F : Z --> ( CC ^m S ) ) |
4 |
|
ulm0.g |
|- ( ph -> G : S --> CC ) |
5 |
|
uzid |
|- ( M e. ZZ -> M e. ( ZZ>= ` M ) ) |
6 |
2 5
|
syl |
|- ( ph -> M e. ( ZZ>= ` M ) ) |
7 |
6 1
|
eleqtrrdi |
|- ( ph -> M e. Z ) |
8 |
7
|
ne0d |
|- ( ph -> Z =/= (/) ) |
9 |
|
ral0 |
|- A. z e. (/) ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x |
10 |
|
simpr |
|- ( ( ph /\ S = (/) ) -> S = (/) ) |
11 |
10
|
raleqdv |
|- ( ( ph /\ S = (/) ) -> ( A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x <-> A. z e. (/) ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) ) |
12 |
9 11
|
mpbiri |
|- ( ( ph /\ S = (/) ) -> A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) |
13 |
12
|
ralrimivw |
|- ( ( ph /\ S = (/) ) -> A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) |
14 |
13
|
ralrimivw |
|- ( ( ph /\ S = (/) ) -> A. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) |
15 |
|
r19.2z |
|- ( ( Z =/= (/) /\ A. 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 ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) |
16 |
8 14 15
|
syl2an2r |
|- ( ( ph /\ S = (/) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) |
17 |
16
|
ralrimivw |
|- ( ( ph /\ S = (/) ) -> A. x e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( F ` k ) ` z ) - ( G ` z ) ) ) < x ) |
18 |
2
|
adantr |
|- ( ( ph /\ S = (/) ) -> M e. ZZ ) |
19 |
3
|
adantr |
|- ( ( ph /\ S = (/) ) -> F : Z --> ( CC ^m S ) ) |
20 |
|
eqidd |
|- ( ( ( ph /\ S = (/) ) /\ ( k e. Z /\ z e. S ) ) -> ( ( F ` k ) ` z ) = ( ( F ` k ) ` z ) ) |
21 |
|
eqidd |
|- ( ( ( ph /\ S = (/) ) /\ z e. S ) -> ( G ` z ) = ( G ` z ) ) |
22 |
4
|
adantr |
|- ( ( ph /\ S = (/) ) -> G : S --> CC ) |
23 |
|
0ex |
|- (/) e. _V |
24 |
10 23
|
eqeltrdi |
|- ( ( ph /\ S = (/) ) -> S e. _V ) |
25 |
1 18 19 20 21 22 24
|
ulm2 |
|- ( ( ph /\ S = (/) ) -> ( 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 ) ) |
26 |
17 25
|
mpbird |
|- ( ( ph /\ S = (/) ) -> F ( ~~>u ` S ) G ) |