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 fvmptelrn
 |-  ( ( 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 ) )