Metamath Proof Explorer


Theorem ulm0

Description: Every function converges uniformly on the empty set. (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses ulm0.z
|- Z = ( ZZ>= ` M )
ulm0.m
|- ( ph -> M e. ZZ )
ulm0.f
|- ( ph -> F : Z --> ( CC ^m S ) )
ulm0.g
|- ( ph -> G : S --> CC )
Assertion ulm0
|- ( ( ph /\ S = (/) ) -> F ( ~~>u ` S ) G )

Proof

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 )