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 )