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