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	$⊢ F = (x \in Z ⟼ B)$
	uzmptshftfval.b	$⊢ B \in V$
	uzmptshftfval.c	$⊢ x = y - N \to B = C$
	uzmptshftfval.z	$⊢ Z = ℤ_{\geq M}$
	uzmptshftfval.w	$⊢ W = ℤ_{\geq (M + N)}$
	uzmptshftfval.m	$⊢ φ \to M \in ℤ$
	uzmptshftfval.n	$⊢ φ \to N \in ℤ$
Assertion	uzmptshftfval	$⊢ φ \to F shift N = (y \in W ⟼ C)$

Proof

Step	Hyp	Ref	Expression
1		uzmptshftfval.f	$⊢ F = (x \in Z ⟼ B)$
2		uzmptshftfval.b	$⊢ B \in V$
3		uzmptshftfval.c	$⊢ x = y - N \to B = C$
4		uzmptshftfval.z	$⊢ Z = ℤ_{\geq M}$
5		uzmptshftfval.w	$⊢ W = ℤ_{\geq (M + N)}$
6		uzmptshftfval.m	$⊢ φ \to M \in ℤ$
7		uzmptshftfval.n	$⊢ φ \to N \in ℤ$
8	2 1	fnmpti	$⊢ F Fn Z$
9	7	zcnd	$⊢ φ \to N \in ℂ$
10	4	fvexi	$⊢ Z \in V$
11	10	mptex	$⊢ (x \in Z ⟼ B) \in V$
12	1 11	eqeltri	$⊢ F \in V$
13	12	shftfn	$⊢ (F Fn Z \land N \in ℂ) \to (F shift N) Fn \{y \in ℂ \| y - N \in Z\}$
14	8 9 13	sylancr	$⊢ φ \to (F shift N) Fn \{y \in ℂ \| y - N \in Z\}$
15		shftuz	$⊢ (N \in ℤ \land M \in ℤ) \to \{y \in ℂ \| y - N \in ℤ_{\geq M}\} = ℤ_{\geq (M + N)}$
16	7 6 15	syl2anc	$⊢ φ \to \{y \in ℂ \| y - N \in ℤ_{\geq M}\} = ℤ_{\geq (M + N)}$
17	4	eleq2i	$⊢ y - N \in Z \leftrightarrow y - N \in ℤ_{\geq M}$
18	17	rabbii	$⊢ \{y \in ℂ \| y - N \in Z\} = \{y \in ℂ \| y - N \in ℤ_{\geq M}\}$
19	16 18 5	3eqtr4g	$⊢ φ \to \{y \in ℂ \| y - N \in Z\} = W$
20	19	fneq2d	$⊢ φ \to ((F shift N) Fn \{y \in ℂ \| y - N \in Z\} \leftrightarrow (F shift N) Fn W)$
21	14 20	mpbid	$⊢ φ \to (F shift N) Fn W$
22		dffn5	$⊢ (F shift N) Fn W \leftrightarrow F shift N = (y \in W ⟼ (F shift N) (y))$
23	21 22	sylib	$⊢ φ \to F shift N = (y \in W ⟼ (F shift N) (y))$
24		uzssz	$⊢ ℤ_{\geq (M + N)} \subseteq ℤ$
25	5 24	eqsstri	$⊢ W \subseteq ℤ$
26		zsscn	$⊢ ℤ \subseteq ℂ$
27	25 26	sstri	$⊢ W \subseteq ℂ$
28	27	sseli	$⊢ y \in W \to y \in ℂ$
29	12	shftval	$⊢ (N \in ℂ \land y \in ℂ) \to (F shift N) (y) = F (y - N)$
30	9 28 29	syl2an	$⊢ (φ \land y \in W) \to (F shift N) (y) = F (y - N)$
31	5	eleq2i	$⊢ y \in W \leftrightarrow y \in ℤ_{\geq (M + N)}$
32	6 7	jca	$⊢ φ \to (M \in ℤ \land N \in ℤ)$
33		eluzsub	$⊢ (M \in ℤ \land N \in ℤ \land y \in ℤ_{\geq (M + N)}) \to y - N \in ℤ_{\geq M}$
34	33	3expa	$⊢ ((M \in ℤ \land N \in ℤ) \land y \in ℤ_{\geq (M + N)}) \to y - N \in ℤ_{\geq M}$
35	32 34	sylan	$⊢ (φ \land y \in ℤ_{\geq (M + N)}) \to y - N \in ℤ_{\geq M}$
36	31 35	sylan2b	$⊢ (φ \land y \in W) \to y - N \in ℤ_{\geq M}$
37	36 4	eleqtrrdi	$⊢ (φ \land y \in W) \to y - N \in Z$
38	3 1 2	fvmpt3i	$⊢ y - N \in Z \to F (y - N) = C$
39	37 38	syl	$⊢ (φ \land y \in W) \to F (y - N) = C$
40	30 39	eqtrd	$⊢ (φ \land y \in W) \to (F shift N) (y) = C$
41	40	mpteq2dva	$⊢ φ \to (y \in W ⟼ (F shift N) (y)) = (y \in W ⟼ C)$
42	23 41	eqtrd	$⊢ φ \to F shift N = (y \in W ⟼ C)$

Metamath Proof Explorer

Theorem uzmptshftfval

Proof