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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
ulmshft.w ⊢ 𝑊 = ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) )
ulmshft.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
ulmshft.k ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
ulmshft.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
ulmshft.h ⊢ ( 𝜑 → 𝐻 = ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) )
Assertion ulmshft ( 𝜑 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) )

Proof

Step Hyp Ref Expression
1 ulmshft.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 ulmshft.w ⊢ 𝑊 = ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) )
3 ulmshft.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 ulmshft.k ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
5 ulmshft.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
6 ulmshft.h ⊢ ( 𝜑 → 𝐻 = ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) )
7 1 2 3 4 5 6 ulmshftlem ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) )
8 eqid ⊢ ( ℤ≥ ‘ ( ( 𝑀 + 𝐾 ) + - 𝐾 ) ) = ( ℤ≥ ‘ ( ( 𝑀 + 𝐾 ) + - 𝐾 ) )
9 3 4 zaddcld ⊢ ( 𝜑 → ( 𝑀 + 𝐾 ) ∈ ℤ )
10 4 znegcld ⊢ ( 𝜑 → - 𝐾 ∈ ℤ )
11 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
12 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → 𝑀 ∈ ℤ )
13 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → 𝐾 ∈ ℤ )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → 𝑛 ∈ 𝑊 )
15 14 2 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
16 eluzsub ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑛 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) ) → ( 𝑛 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
17 12 13 15 16 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → ( 𝑛 − 𝐾 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
18 17 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → ( 𝑛 − 𝐾 ) ∈ 𝑍 )
19 11 18 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ∈ ( ℂ ↑m 𝑆 ) )
20 6 19 fmpt3d ⊢ ( 𝜑 → 𝐻 : 𝑊 ⟶ ( ℂ ↑m 𝑆 ) )
21 simpr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ 𝑍 )
22 21 1 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) )
23 eluzelz ⊢ ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑚 ∈ ℤ )
24 22 23 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ ℤ )
25 24 zcnd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝑚 ∈ ℂ )
26 4 zcnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝐾 ∈ ℂ )
28 25 27 subnegd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 − - 𝐾 ) = ( 𝑚 + 𝐾 ) )
29 28 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐻 ‘ ( 𝑚 − - 𝐾 ) ) = ( 𝐻 ‘ ( 𝑚 + 𝐾 ) ) )
30 6 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝐻 = ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) )
31 30 fveq1d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐻 ‘ ( 𝑚 + 𝐾 ) ) = ( ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) ‘ ( 𝑚 + 𝐾 ) ) )
32 4 adantr ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → 𝐾 ∈ ℤ )
33 eluzadd ⊢ ( ( 𝑚 ∈ ( ℤ≥ ‘ 𝑀 ) ∧ 𝐾 ∈ ℤ ) → ( 𝑚 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
34 22 32 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 + 𝐾 ) ∈ ( ℤ≥ ‘ ( 𝑀 + 𝐾 ) ) )
35 34 2 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝑚 + 𝐾 ) ∈ 𝑊 )
36 fvoveq1 ⊢ ( 𝑛 = ( 𝑚 + 𝐾 ) → ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) = ( 𝐹 ‘ ( ( 𝑚 + 𝐾 ) − 𝐾 ) ) )
37 eqid ⊢ ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) = ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) )
38 fvex ⊢ ( 𝐹 ‘ ( ( 𝑚 + 𝐾 ) − 𝐾 ) ) ∈ V
39 36 37 38 fvmpt ⊢ ( ( 𝑚 + 𝐾 ) ∈ 𝑊 → ( ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) ‘ ( 𝑚 + 𝐾 ) ) = ( 𝐹 ‘ ( ( 𝑚 + 𝐾 ) − 𝐾 ) ) )
40 35 39 syl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) ‘ ( 𝑚 + 𝐾 ) ) = ( 𝐹 ‘ ( ( 𝑚 + 𝐾 ) − 𝐾 ) ) )
41 25 27 pncand ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑚 + 𝐾 ) − 𝐾 ) = 𝑚 )
42 41 fveq2d ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐹 ‘ ( ( 𝑚 + 𝐾 ) − 𝐾 ) ) = ( 𝐹 ‘ 𝑚 ) )
43 40 42 eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( ( 𝑛 ∈ 𝑊 ↦ ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ) ‘ ( 𝑚 + 𝐾 ) ) = ( 𝐹 ‘ 𝑚 ) )
44 29 31 43 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ 𝑍 ) → ( 𝐻 ‘ ( 𝑚 − - 𝐾 ) ) = ( 𝐹 ‘ 𝑚 ) )
45 44 mpteq2dva ⊢ ( 𝜑 → ( 𝑚 ∈ 𝑍 ↦ ( 𝐻 ‘ ( 𝑚 − - 𝐾 ) ) ) = ( 𝑚 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑚 ) ) )
46 3 zcnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
47 10 zcnd ⊢ ( 𝜑 → - 𝐾 ∈ ℂ )
48 46 26 47 addassd ⊢ ( 𝜑 → ( ( 𝑀 + 𝐾 ) + - 𝐾 ) = ( 𝑀 + ( 𝐾 + - 𝐾 ) ) )
49 26 negidd ⊢ ( 𝜑 → ( 𝐾 + - 𝐾 ) = 0 )
50 49 oveq2d ⊢ ( 𝜑 → ( 𝑀 + ( 𝐾 + - 𝐾 ) ) = ( 𝑀 + 0 ) )
51 46 addridd ⊢ ( 𝜑 → ( 𝑀 + 0 ) = 𝑀 )
52 48 50 51 3eqtrd ⊢ ( 𝜑 → ( ( 𝑀 + 𝐾 ) + - 𝐾 ) = 𝑀 )
53 52 fveq2d ⊢ ( 𝜑 → ( ℤ≥ ‘ ( ( 𝑀 + 𝐾 ) + - 𝐾 ) ) = ( ℤ≥ ‘ 𝑀 ) )
54 53 1 eqtr4di ⊢ ( 𝜑 → ( ℤ≥ ‘ ( ( 𝑀 + 𝐾 ) + - 𝐾 ) ) = 𝑍 )
55 54 mpteq1d ⊢ ( 𝜑 → ( 𝑚 ∈ ( ℤ≥ ‘ ( ( 𝑀 + 𝐾 ) + - 𝐾 ) ) ↦ ( 𝐻 ‘ ( 𝑚 − - 𝐾 ) ) ) = ( 𝑚 ∈ 𝑍 ↦ ( 𝐻 ‘ ( 𝑚 − - 𝐾 ) ) ) )
56 5 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑚 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑚 ) ) )
57 45 55 56 3eqtr4rd ⊢ ( 𝜑 → 𝐹 = ( 𝑚 ∈ ( ℤ≥ ‘ ( ( 𝑀 + 𝐾 ) + - 𝐾 ) ) ↦ ( 𝐻 ‘ ( 𝑚 − - 𝐾 ) ) ) )
58 2 8 9 10 20 57 ulmshftlem ⊢ ( 𝜑 → ( 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) )
59 7 58 impbid ⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) )