This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ulmshft

Description: A sequence of functions converges iff the shifted sequence converges. (Contributed by Mario Carneiro, 24-Mar-2015)

Ref Expression
Hypotheses ulmshft.z 
|- Z = ( ZZ>= ` M )
ulmshft.w 
|- W = ( ZZ>= ` ( M + K ) )
ulmshft.m 
|- ( ph -> M e. ZZ )
ulmshft.k 
|- ( ph -> K e. ZZ )
ulmshft.f 
|- ( ph -> F : Z --> ( CC ^m S ) )
ulmshft.h 
|- ( ph -> H = ( n e. W |-> ( F ` ( n - K ) ) ) )
Assertion ulmshft 
|- ( ph -> ( F ( ~~>u ` S ) G <-> H ( ~~>u ` S ) G ) )

Proof

Step Hyp Ref Expression
1 ulmshft.z 
 |-  Z = ( ZZ>= ` M )
2 ulmshft.w 
 |-  W = ( ZZ>= ` ( M + K ) )
3 ulmshft.m 
 |-  ( ph -> M e. ZZ )
4 ulmshft.k 
 |-  ( ph -> K e. ZZ )
5 ulmshft.f 
 |-  ( ph -> F : Z --> ( CC ^m S ) )
6 ulmshft.h 
 |-  ( ph -> H = ( n e. W |-> ( F ` ( n - K ) ) ) )
7 1 2 3 4 5 6 ulmshftlem 
 |-  ( ph -> ( F ( ~~>u ` S ) G -> H ( ~~>u ` S ) G ) )
8 eqid 
 |-  ( ZZ>= ` ( ( M + K ) + -u K ) ) = ( ZZ>= ` ( ( M + K ) + -u K ) )
9 3 4 zaddcld 
 |-  ( ph -> ( M + K ) e. ZZ )
10 4 znegcld 
 |-  ( ph -> -u K e. ZZ )
11 5 adantr 
 |-  ( ( ph /\ n e. W ) -> F : Z --> ( CC ^m S ) )
12 3 adantr 
 |-  ( ( ph /\ n e. W ) -> M e. ZZ )
13 4 adantr 
 |-  ( ( ph /\ n e. W ) -> K e. ZZ )
14 simpr 
 |-  ( ( ph /\ n e. W ) -> n e. W )
15 14 2 eleqtrdi 
 |-  ( ( ph /\ n e. W ) -> n e. ( ZZ>= ` ( M + K ) ) )
16 eluzsub 
 |-  ( ( M e. ZZ /\ K e. ZZ /\ n e. ( ZZ>= ` ( M + K ) ) ) -> ( n - K ) e. ( ZZ>= ` M ) )
17 12 13 15 16 syl3anc 
 |-  ( ( ph /\ n e. W ) -> ( n - K ) e. ( ZZ>= ` M ) )
18 17 1 eleqtrrdi 
 |-  ( ( ph /\ n e. W ) -> ( n - K ) e. Z )
19 11 18 ffvelcdmd 
 |-  ( ( ph /\ n e. W ) -> ( F ` ( n - K ) ) e. ( CC ^m S ) )
20 6 19 fmpt3d 
 |-  ( ph -> H : W --> ( CC ^m S ) )
21 simpr 
 |-  ( ( ph /\ m e. Z ) -> m e. Z )
22 21 1 eleqtrdi 
 |-  ( ( ph /\ m e. Z ) -> m e. ( ZZ>= ` M ) )
23 eluzelz 
 |-  ( m e. ( ZZ>= ` M ) -> m e. ZZ )
24 22 23 syl 
 |-  ( ( ph /\ m e. Z ) -> m e. ZZ )
25 24 zcnd 
 |-  ( ( ph /\ m e. Z ) -> m e. CC )
26 4 zcnd 
 |-  ( ph -> K e. CC )
27 26 adantr 
 |-  ( ( ph /\ m e. Z ) -> K e. CC )
28 25 27 subnegd 
 |-  ( ( ph /\ m e. Z ) -> ( m - -u K ) = ( m + K ) )
29 28 fveq2d 
 |-  ( ( ph /\ m e. Z ) -> ( H ` ( m - -u K ) ) = ( H ` ( m + K ) ) )
30 6 adantr 
 |-  ( ( ph /\ m e. Z ) -> H = ( n e. W |-> ( F ` ( n - K ) ) ) )
31 30 fveq1d 
 |-  ( ( ph /\ m e. Z ) -> ( H ` ( m + K ) ) = ( ( n e. W |-> ( F ` ( n - K ) ) ) ` ( m + K ) ) )
32 4 adantr 
 |-  ( ( ph /\ m e. Z ) -> K e. ZZ )
33 eluzadd 
 |-  ( ( m e. ( ZZ>= ` M ) /\ K e. ZZ ) -> ( m + K ) e. ( ZZ>= ` ( M + K ) ) )
34 22 32 33 syl2anc 
 |-  ( ( ph /\ m e. Z ) -> ( m + K ) e. ( ZZ>= ` ( M + K ) ) )
35 34 2 eleqtrrdi 
 |-  ( ( ph /\ m e. Z ) -> ( m + K ) e. W )
36 fvoveq1 
 |-  ( n = ( m + K ) -> ( F ` ( n - K ) ) = ( F ` ( ( m + K ) - K ) ) )
37 eqid 
 |-  ( n e. W |-> ( F ` ( n - K ) ) ) = ( n e. W |-> ( F ` ( n - K ) ) )
38 fvex 
 |-  ( F ` ( ( m + K ) - K ) ) e. _V
39 36 37 38 fvmpt 
 |-  ( ( m + K ) e. W -> ( ( n e. W |-> ( F ` ( n - K ) ) ) ` ( m + K ) ) = ( F ` ( ( m + K ) - K ) ) )
40 35 39 syl 
 |-  ( ( ph /\ m e. Z ) -> ( ( n e. W |-> ( F ` ( n - K ) ) ) ` ( m + K ) ) = ( F ` ( ( m + K ) - K ) ) )
41 25 27 pncand 
 |-  ( ( ph /\ m e. Z ) -> ( ( m + K ) - K ) = m )
42 41 fveq2d 
 |-  ( ( ph /\ m e. Z ) -> ( F ` ( ( m + K ) - K ) ) = ( F ` m ) )
43 40 42 eqtrd 
 |-  ( ( ph /\ m e. Z ) -> ( ( n e. W |-> ( F ` ( n - K ) ) ) ` ( m + K ) ) = ( F ` m ) )
44 29 31 43 3eqtrd 
 |-  ( ( ph /\ m e. Z ) -> ( H ` ( m - -u K ) ) = ( F ` m ) )
45 44 mpteq2dva 
 |-  ( ph -> ( m e. Z |-> ( H ` ( m - -u K ) ) ) = ( m e. Z |-> ( F ` m ) ) )
46 3 zcnd 
 |-  ( ph -> M e. CC )
47 10 zcnd 
 |-  ( ph -> -u K e. CC )
48 46 26 47 addassd 
 |-  ( ph -> ( ( M + K ) + -u K ) = ( M + ( K + -u K ) ) )
49 26 negidd 
 |-  ( ph -> ( K + -u K ) = 0 )
50 49 oveq2d 
 |-  ( ph -> ( M + ( K + -u K ) ) = ( M + 0 ) )
51 46 addridd 
 |-  ( ph -> ( M + 0 ) = M )
52 48 50 51 3eqtrd 
 |-  ( ph -> ( ( M + K ) + -u K ) = M )
53 52 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( ( M + K ) + -u K ) ) = ( ZZ>= ` M ) )
54 53 1 eqtr4di 
 |-  ( ph -> ( ZZ>= ` ( ( M + K ) + -u K ) ) = Z )
55 54 mpteq1d 
 |-  ( ph -> ( m e. ( ZZ>= ` ( ( M + K ) + -u K ) ) |-> ( H ` ( m - -u K ) ) ) = ( m e. Z |-> ( H ` ( m - -u K ) ) ) )
56 5 feqmptd 
 |-  ( ph -> F = ( m e. Z |-> ( F ` m ) ) )
57 45 55 56 3eqtr4rd 
 |-  ( ph -> F = ( m e. ( ZZ>= ` ( ( M + K ) + -u K ) ) |-> ( H ` ( m - -u K ) ) ) )
58 2 8 9 10 20 57 ulmshftlem 
 |-  ( ph -> ( H ( ~~>u ` S ) G -> F ( ~~>u ` S ) G ) )
59 7 58 impbid 
 |-  ( ph -> ( F ( ~~>u ` S ) G <-> H ( ~~>u ` S ) G ) )