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	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑊 ) → ( 𝐹 ‘ ( 𝑛 − 𝐾 ) ) ∈ ( ℂ ↑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	addid1d	⊢ ( 𝜑 → ( 𝑀 + 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	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ↔ 𝐻 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) )