Metamath Proof Explorer

Theorem ulmss

Description: A uniform limit of functions is still a uniform limit if restricted to a subset. (Contributed by Mario Carneiro, 3-Mar-2015)

Ref Expression
Hypotheses ulmss.z 
|- Z = ( ZZ>= ` M )
ulmss.t 
|- ( ph -> T C_ S )
ulmss.a 
|- ( ( ph /\ x e. Z ) -> A e. W )
ulmss.u 
|- ( ph -> ( x e. Z |-> A ) ( ~~>u ` S ) G )
Assertion ulmss 
|- ( ph -> ( x e. Z |-> ( A |` T ) ) ( ~~>u ` T ) ( G |` T ) )

Proof

Step Hyp Ref Expression
1 ulmss.z 
 |-  Z = ( ZZ>= ` M )
2 ulmss.t 
 |-  ( ph -> T C_ S )
3 ulmss.a 
 |-  ( ( ph /\ x e. Z ) -> A e. W )
4 ulmss.u 
 |-  ( ph -> ( x e. Z |-> A ) ( ~~>u ` S ) G )
5 1 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
6 2 adantr 
 |-  ( ( ph /\ k e. Z ) -> T C_ S )
7 ssralv 
 |-  ( T C_ S -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
8 6 7 syl 
 |-  ( ( ph /\ k e. Z ) -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
9 fvres 
 |-  ( z e. T -> ( ( A |` T ) ` z ) = ( A ` z ) )
10 9 ad2antll 
 |-  ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( A |` T ) ` z ) = ( A ` z ) )
11 simprl 
 |-  ( ( ph /\ ( x e. Z /\ z e. T ) ) -> x e. Z )
12 3 adantrr 
 |-  ( ( ph /\ ( x e. Z /\ z e. T ) ) -> A e. W )
13 12 resexd 
 |-  ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( A |` T ) e. _V )
14 eqid 
 |-  ( x e. Z |-> ( A |` T ) ) = ( x e. Z |-> ( A |` T ) )
15 14 fvmpt2 
 |-  ( ( x e. Z /\ ( A |` T ) e. _V ) -> ( ( x e. Z |-> ( A |` T ) ) ` x ) = ( A |` T ) )
16 11 13 15 syl2anc 
 |-  ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( x e. Z |-> ( A |` T ) ) ` x ) = ( A |` T ) )
17 16 fveq1d 
 |-  ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( A |` T ) ` z ) )
18 eqid 
 |-  ( x e. Z |-> A ) = ( x e. Z |-> A )
19 18 fvmpt2 
 |-  ( ( x e. Z /\ A e. W ) -> ( ( x e. Z |-> A ) ` x ) = A )
20 11 12 19 syl2anc 
 |-  ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( x e. Z |-> A ) ` x ) = A )
21 20 fveq1d 
 |-  ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( ( x e. Z |-> A ) ` x ) ` z ) = ( A ` z ) )
22 10 17 21 3eqtr4d 
 |-  ( ( ph /\ ( x e. Z /\ z e. T ) ) -> ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) )
23 22 ralrimivva 
 |-  ( ph -> A. x e. Z A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) )
24 nfv 
 |-  F/ k A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z )
25 nfcv 
 |-  F/_ x T
26 nffvmpt1 
 |-  F/_ x ( ( x e. Z |-> ( A |` T ) ) ` k )
27 nfcv 
 |-  F/_ x z
28 26 27 nffv 
 |-  F/_ x ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z )
29 nffvmpt1 
 |-  F/_ x ( ( x e. Z |-> A ) ` k )
30 29 27 nffv 
 |-  F/_ x ( ( ( x e. Z |-> A ) ` k ) ` z )
31 28 30 nfeq 
 |-  F/ x ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z )
32 25 31 nfralw 
 |-  F/ x A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z )
33 fveq2 
 |-  ( x = k -> ( ( x e. Z |-> ( A |` T ) ) ` x ) = ( ( x e. Z |-> ( A |` T ) ) ` k ) )
34 33 fveq1d 
 |-  ( x = k -> ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) )
35 fveq2 
 |-  ( x = k -> ( ( x e. Z |-> A ) ` x ) = ( ( x e. Z |-> A ) ` k ) )
36 35 fveq1d 
 |-  ( x = k -> ( ( ( x e. Z |-> A ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) )
37 34 36 eqeq12d 
 |-  ( x = k -> ( ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) <-> ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) ) )
38 37 ralbidv 
 |-  ( x = k -> ( A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) <-> A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) ) )
39 24 32 38 cbvralw 
 |-  ( A. x e. Z A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` x ) ` z ) = ( ( ( x e. Z |-> A ) ` x ) ` z ) <-> A. k e. Z A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) )
40 23 39 sylib 
 |-  ( ph -> A. k e. Z A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) )
41 40 r19.21bi 
 |-  ( ( ph /\ k e. Z ) -> A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) )
42 fvoveq1 
 |-  ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) -> ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) = ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) )
43 42 breq1d 
 |-  ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) -> ( ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
44 43 ralimi 
 |-  ( A. z e. T ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) -> A. z e. T ( ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
45 ralbi 
 |-  ( A. z e. T ( ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) -> ( A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> A. z e. T ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
46 41 44 45 3syl 
 |-  ( ( ph /\ k e. Z ) -> ( A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r <-> A. z e. T ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
47 8 46 sylibrd 
 |-  ( ( ph /\ k e. Z ) -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
48 5 47 sylan2 
 |-  ( ( ph /\ ( j e. Z /\ k e. ( ZZ>= ` j ) ) ) -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
49 48 anassrs 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
50 49 ralimdva 
 |-  ( ( ph /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. k e. ( ZZ>= ` j ) A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
51 50 reximdva 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
52 51 ralimdv 
 |-  ( ph -> ( A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r -> A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
53 ulmf 
 |-  ( ( x e. Z |-> A ) ( ~~>u ` S ) G -> E. m e. ZZ ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) )
54 4 53 syl 
 |-  ( ph -> E. m e. ZZ ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) )
55 fdm 
 |-  ( ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> dom ( x e. Z |-> A ) = ( ZZ>= ` m ) )
56 18 dmmptss 
 |-  dom ( x e. Z |-> A ) C_ Z
57 55 56 eqsstrrdi 
 |-  ( ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> ( ZZ>= ` m ) C_ Z )
58 uzid 
 |-  ( m e. ZZ -> m e. ( ZZ>= ` m ) )
59 58 adantl 
 |-  ( ( ph /\ m e. ZZ ) -> m e. ( ZZ>= ` m ) )
60 ssel 
 |-  ( ( ZZ>= ` m ) C_ Z -> ( m e. ( ZZ>= ` m ) -> m e. Z ) )
61 eluzel2 
 |-  ( m e. ( ZZ>= ` M ) -> M e. ZZ )
62 61 1 eleq2s 
 |-  ( m e. Z -> M e. ZZ )
63 60 62 syl6 
 |-  ( ( ZZ>= ` m ) C_ Z -> ( m e. ( ZZ>= ` m ) -> M e. ZZ ) )
64 57 59 63 syl2imc 
 |-  ( ( ph /\ m e. ZZ ) -> ( ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> M e. ZZ ) )
65 64 rexlimdva 
 |-  ( ph -> ( E. m e. ZZ ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> M e. ZZ ) )
66 54 65 mpd 
 |-  ( ph -> M e. ZZ )
67 3 ralrimiva 
 |-  ( ph -> A. x e. Z A e. W )
68 18 fnmpt 
 |-  ( A. x e. Z A e. W -> ( x e. Z |-> A ) Fn Z )
69 67 68 syl 
 |-  ( ph -> ( x e. Z |-> A ) Fn Z )
70 frn 
 |-  ( ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> ran ( x e. Z |-> A ) C_ ( CC ^m S ) )
71 70 rexlimivw 
 |-  ( E. m e. ZZ ( x e. Z |-> A ) : ( ZZ>= ` m ) --> ( CC ^m S ) -> ran ( x e. Z |-> A ) C_ ( CC ^m S ) )
72 54 71 syl 
 |-  ( ph -> ran ( x e. Z |-> A ) C_ ( CC ^m S ) )
73 df-f 
 |-  ( ( x e. Z |-> A ) : Z --> ( CC ^m S ) <-> ( ( x e. Z |-> A ) Fn Z /\ ran ( x e. Z |-> A ) C_ ( CC ^m S ) ) )
74 69 72 73 sylanbrc 
 |-  ( ph -> ( x e. Z |-> A ) : Z --> ( CC ^m S ) )
75 eqidd 
 |-  ( ( ph /\ ( k e. Z /\ z e. S ) ) -> ( ( ( x e. Z |-> A ) ` k ) ` z ) = ( ( ( x e. Z |-> A ) ` k ) ` z ) )
76 eqidd 
 |-  ( ( ph /\ z e. S ) -> ( G ` z ) = ( G ` z ) )
77 ulmcl 
 |-  ( ( x e. Z |-> A ) ( ~~>u ` S ) G -> G : S --> CC )
78 4 77 syl 
 |-  ( ph -> G : S --> CC )
79 ulmscl 
 |-  ( ( x e. Z |-> A ) ( ~~>u ` S ) G -> S e. _V )
80 4 79 syl 
 |-  ( ph -> S e. _V )
81 1 66 74 75 76 78 80 ulm2 
 |-  ( ph -> ( ( x e. Z |-> A ) ( ~~>u ` S ) G <-> A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. S ( abs ` ( ( ( ( x e. Z |-> A ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
82 74 fvmptelcdm 
 |-  ( ( ph /\ x e. Z ) -> A e. ( CC ^m S ) )
83 elmapi 
 |-  ( A e. ( CC ^m S ) -> A : S --> CC )
84 82 83 syl 
 |-  ( ( ph /\ x e. Z ) -> A : S --> CC )
85 2 adantr 
 |-  ( ( ph /\ x e. Z ) -> T C_ S )
86 84 85 fssresd 
 |-  ( ( ph /\ x e. Z ) -> ( A |` T ) : T --> CC )
87 cnex 
 |-  CC e. _V
88 80 2 ssexd 
 |-  ( ph -> T e. _V )
89 88 adantr 
 |-  ( ( ph /\ x e. Z ) -> T e. _V )
90 elmapg 
 |-  ( ( CC e. _V /\ T e. _V ) -> ( ( A |` T ) e. ( CC ^m T ) <-> ( A |` T ) : T --> CC ) )
91 87 89 90 sylancr 
 |-  ( ( ph /\ x e. Z ) -> ( ( A |` T ) e. ( CC ^m T ) <-> ( A |` T ) : T --> CC ) )
92 86 91 mpbird 
 |-  ( ( ph /\ x e. Z ) -> ( A |` T ) e. ( CC ^m T ) )
93 92 fmpttd 
 |-  ( ph -> ( x e. Z |-> ( A |` T ) ) : Z --> ( CC ^m T ) )
94 eqidd 
 |-  ( ( ph /\ ( k e. Z /\ z e. T ) ) -> ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) = ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) )
95 fvres 
 |-  ( z e. T -> ( ( G |` T ) ` z ) = ( G ` z ) )
96 95 adantl 
 |-  ( ( ph /\ z e. T ) -> ( ( G |` T ) ` z ) = ( G ` z ) )
97 78 2 fssresd 
 |-  ( ph -> ( G |` T ) : T --> CC )
98 1 66 93 94 96 97 88 ulm2 
 |-  ( ph -> ( ( x e. Z |-> ( A |` T ) ) ( ~~>u ` T ) ( G |` T ) <-> A. r e. RR+ E. j e. Z A. k e. ( ZZ>= ` j ) A. z e. T ( abs ` ( ( ( ( x e. Z |-> ( A |` T ) ) ` k ) ` z ) - ( G ` z ) ) ) < r ) )
99 52 81 98 3imtr4d 
 |-  ( ph -> ( ( x e. Z |-> A ) ( ~~>u ` S ) G -> ( x e. Z |-> ( A |` T ) ) ( ~~>u ` T ) ( G |` T ) ) )
100 4 99 mpd 
 |-  ( ph -> ( x e. Z |-> ( A |` T ) ) ( ~~>u ` T ) ( G |` T ) )