Theorem uzmptshftfval

Description: When F is a maps-to function on some set of upper integers Z that returns a set B , ( F shift N ) is another maps-to function on the shifted set of upper integers W . (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	uzmptshftfval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑍 ↦ 𝐵 )
	uzmptshftfval.b	⊢ 𝐵 ∈ V
	uzmptshftfval.c	⊢ ( 𝑥 = ( 𝑦 − 𝑁 ) → 𝐵 = 𝐶 )
	uzmptshftfval.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	uzmptshftfval.w	⊢ 𝑊 = ( ℤ≥ ‘ ( 𝑀 + 𝑁 ) )
	uzmptshftfval.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	uzmptshftfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
Assertion	uzmptshftfval	⊢ ( 𝜑 → ( 𝐹 shift 𝑁 ) = ( 𝑦 ∈ 𝑊 ↦ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		uzmptshftfval.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑍 ↦ 𝐵 )
2		uzmptshftfval.b	⊢ 𝐵 ∈ V
3		uzmptshftfval.c	⊢ ( 𝑥 = ( 𝑦 − 𝑁 ) → 𝐵 = 𝐶 )
4		uzmptshftfval.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
5		uzmptshftfval.w	⊢ 𝑊 = ( ℤ≥ ‘ ( 𝑀 + 𝑁 ) )
6		uzmptshftfval.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
7		uzmptshftfval.n	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
8	2 1	fnmpti	⊢ 𝐹 Fn 𝑍
9	7	zcnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
10	4	fvexi	⊢ 𝑍 ∈ V
11	10	mptex	⊢ ( 𝑥 ∈ 𝑍 ↦ 𝐵 ) ∈ V
12	1 11	eqeltri	⊢ 𝐹 ∈ V
13	12	shftfn	⊢ ( ( 𝐹 Fn 𝑍 ∧ 𝑁 ∈ ℂ ) → ( 𝐹 shift 𝑁 ) Fn { 𝑦 ∈ ℂ ∣ ( 𝑦 − 𝑁 ) ∈ 𝑍 } )
14	8 9 13	sylancr	⊢ ( 𝜑 → ( 𝐹 shift 𝑁 ) Fn { 𝑦 ∈ ℂ ∣ ( 𝑦 − 𝑁 ) ∈ 𝑍 } )
15		shftuz	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → { 𝑦 ∈ ℂ ∣ ( 𝑦 − 𝑁 ) ∈ ( ℤ≥ ‘ 𝑀 ) } = ( ℤ≥ ‘ ( 𝑀 + 𝑁 ) ) )
16	7 6 15	syl2anc	⊢ ( 𝜑 → { 𝑦 ∈ ℂ ∣ ( 𝑦 − 𝑁 ) ∈ ( ℤ≥ ‘ 𝑀 ) } = ( ℤ≥ ‘ ( 𝑀 + 𝑁 ) ) )
17	4	eleq2i	⊢ ( ( 𝑦 − 𝑁 ) ∈ 𝑍 ↔ ( 𝑦 − 𝑁 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
18	17	rabbii	⊢ { 𝑦 ∈ ℂ ∣ ( 𝑦 − 𝑁 ) ∈ 𝑍 } = { 𝑦 ∈ ℂ ∣ ( 𝑦 − 𝑁 ) ∈ ( ℤ≥ ‘ 𝑀 ) }
19	16 18 5	3eqtr4g	⊢ ( 𝜑 → { 𝑦 ∈ ℂ ∣ ( 𝑦 − 𝑁 ) ∈ 𝑍 } = 𝑊 )
20	19	fneq2d	⊢ ( 𝜑 → ( ( 𝐹 shift 𝑁 ) Fn { 𝑦 ∈ ℂ ∣ ( 𝑦 − 𝑁 ) ∈ 𝑍 } ↔ ( 𝐹 shift 𝑁 ) Fn 𝑊 ) )
21	14 20	mpbid	⊢ ( 𝜑 → ( 𝐹 shift 𝑁 ) Fn 𝑊 )
22		dffn5	⊢ ( ( 𝐹 shift 𝑁 ) Fn 𝑊 ↔ ( 𝐹 shift 𝑁 ) = ( 𝑦 ∈ 𝑊 ↦ ( ( 𝐹 shift 𝑁 ) ‘ 𝑦 ) ) )
23	21 22	sylib	⊢ ( 𝜑 → ( 𝐹 shift 𝑁 ) = ( 𝑦 ∈ 𝑊 ↦ ( ( 𝐹 shift 𝑁 ) ‘ 𝑦 ) ) )
24		uzssz	⊢ ( ℤ≥ ‘ ( 𝑀 + 𝑁 ) ) ⊆ ℤ
25	5 24	eqsstri	⊢ 𝑊 ⊆ ℤ
26		zsscn	⊢ ℤ ⊆ ℂ
27	25 26	sstri	⊢ 𝑊 ⊆ ℂ
28	27	sseli	⊢ ( 𝑦 ∈ 𝑊 → 𝑦 ∈ ℂ )
29	12	shftval	⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝐹 shift 𝑁 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑦 − 𝑁 ) ) )
30	9 28 29	syl2an	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑊 ) → ( ( 𝐹 shift 𝑁 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑦 − 𝑁 ) ) )
31	5	eleq2i	⊢ ( 𝑦 ∈ 𝑊 ↔ 𝑦 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝑁 ) ) )
32	6 7	jca	⊢ ( 𝜑 → ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) )
33		eluzsub	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑦 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝑁 ) ) ) → ( 𝑦 − 𝑁 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
34	33	3expa	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑦 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝑁 ) ) ) → ( 𝑦 − 𝑁 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
35	32 34	sylan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ℤ≥ ‘ ( 𝑀 + 𝑁 ) ) ) → ( 𝑦 − 𝑁 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
36	31 35	sylan2b	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑊 ) → ( 𝑦 − 𝑁 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
37	36 4	eleqtrrdi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑊 ) → ( 𝑦 − 𝑁 ) ∈ 𝑍 )
38	3 1 2	fvmpt3i	⊢ ( ( 𝑦 − 𝑁 ) ∈ 𝑍 → ( 𝐹 ‘ ( 𝑦 − 𝑁 ) ) = 𝐶 )
39	37 38	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑊 ) → ( 𝐹 ‘ ( 𝑦 − 𝑁 ) ) = 𝐶 )
40	30 39	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑊 ) → ( ( 𝐹 shift 𝑁 ) ‘ 𝑦 ) = 𝐶 )
41	40	mpteq2dva	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑊 ↦ ( ( 𝐹 shift 𝑁 ) ‘ 𝑦 ) ) = ( 𝑦 ∈ 𝑊 ↦ 𝐶 ) )
42	23 41	eqtrd	⊢ ( 𝜑 → ( 𝐹 shift 𝑁 ) = ( 𝑦 ∈ 𝑊 ↦ 𝐶 ) )