mptfzshft

Description: 1-1 onto function in maps-to notation which shifts a finite set of sequential integers. Formerly part of proof for fsumshft . (Contributed by AV, 24-Aug-2019)

	Ref	Expression
Hypotheses	mptfzshft.1	$⊢ φ \to K \in ℤ$
	mptfzshft.2	$⊢ φ \to M \in ℤ$
	mptfzshft.3	$⊢ φ \to N \in ℤ$
Assertion	mptfzshft	$⊢ φ \to (j \in (M + K \dots N + K) ⟼ j - K) : (M + K \dots N + K) \underset{1-1 onto}{⟶} (M \dots N)$

Proof

Step	Hyp	Ref	Expression
1		mptfzshft.1	$⊢ φ \to K \in ℤ$
2		mptfzshft.2	$⊢ φ \to M \in ℤ$
3		mptfzshft.3	$⊢ φ \to N \in ℤ$
4		ovex	$⊢ j - K \in V$
5		eqid	$⊢ (j \in (M + K \dots N + K) ⟼ j - K) = (j \in (M + K \dots N + K) ⟼ j - K)$
6	4 5	fnmpti	$⊢ (j \in (M + K \dots N + K) ⟼ j - K) Fn (M + K \dots N + K)$
7	6	a1i	$⊢ φ \to (j \in (M + K \dots N + K) ⟼ j - K) Fn (M + K \dots N + K)$
8		ovex	$⊢ k + K \in V$
9		eqid	$⊢ (k \in (M \dots N) ⟼ k + K) = (k \in (M \dots N) ⟼ k + K)$
10	8 9	fnmpti	$⊢ (k \in (M \dots N) ⟼ k + K) Fn (M \dots N)$
11		simprr	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to k = j - K$
12	11	oveq1d	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to k + K = j - K + K$
13		elfzelz	$⊢ j \in (M + K \dots N + K) \to j \in ℤ$
14	13	ad2antrl	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to j \in ℤ$
15	1	adantr	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to K \in ℤ$
16		zcn	$⊢ j \in ℤ \to j \in ℂ$
17		zcn	$⊢ K \in ℤ \to K \in ℂ$
18		npcan	$⊢ (j \in ℂ \land K \in ℂ) \to j - K + K = j$
19	16 17 18	syl2an	$⊢ (j \in ℤ \land K \in ℤ) \to j - K + K = j$
20	14 15 19	syl2anc	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to j - K + K = j$
21	12 20	eqtr2d	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to j = k + K$
22		simprl	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to j \in (M + K \dots N + K)$
23	21 22	eqeltrrd	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to k + K \in (M + K \dots N + K)$
24	2	adantr	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to M \in ℤ$
25	3	adantr	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to N \in ℤ$
26	14 15	zsubcld	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to j - K \in ℤ$
27	11 26	eqeltrd	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to k \in ℤ$
28		fzaddel	$⊢ ((M \in ℤ \land N \in ℤ) \land (k \in ℤ \land K \in ℤ)) \to (k \in (M \dots N) \leftrightarrow k + K \in (M + K \dots N + K))$
29	24 25 27 15 28	syl22anc	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to (k \in (M \dots N) \leftrightarrow k + K \in (M + K \dots N + K))$
30	23 29	mpbird	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to k \in (M \dots N)$
31	30 21	jca	$⊢ (φ \land (j \in (M + K \dots N + K) \land k = j - K)) \to (k \in (M \dots N) \land j = k + K)$
32		simprr	$⊢ (φ \land (k \in (M \dots N) \land j = k + K)) \to j = k + K$
33		simprl	$⊢ (φ \land (k \in (M \dots N) \land j = k + K)) \to k \in (M \dots N)$
34	2	adantr	$⊢ (φ \land (k \in (M \dots N) \land j = k + K)) \to M \in ℤ$
35	3	adantr	$⊢ (φ \land (k \in (M \dots N) \land j = k + K)) \to N \in ℤ$
36		elfzelz	$⊢ k \in (M \dots N) \to k \in ℤ$
37	36	ad2antrl	$⊢ (φ \land (k \in (M \dots N) \land j = k + K)) \to k \in ℤ$
38	1	adantr	$⊢ (φ \land (k \in (M \dots N) \land j = k + K)) \to K \in ℤ$
39	34 35 37 38 28	syl22anc	$⊢ (φ \land (k \in (M \dots N) \land j = k + K)) \to (k \in (M \dots N) \leftrightarrow k + K \in (M + K \dots N + K))$
40	33 39	mpbid	$⊢ (φ \land (k \in (M \dots N) \land j = k + K)) \to k + K \in (M + K \dots N + K)$
41	32 40	eqeltrd	$⊢ (φ \land (k \in (M \dots N) \land j = k + K)) \to j \in (M + K \dots N + K)$
42	32	oveq1d	$⊢ (φ \land (k \in (M \dots N) \land j = k + K)) \to j - K = k + K - K$
43		zcn	$⊢ k \in ℤ \to k \in ℂ$
44		pncan	$⊢ (k \in ℂ \land K \in ℂ) \to k + K - K = k$
45	43 17 44	syl2an	$⊢ (k \in ℤ \land K \in ℤ) \to k + K - K = k$
46	37 38 45	syl2anc	$⊢ (φ \land (k \in (M \dots N) \land j = k + K)) \to k + K - K = k$
47	42 46	eqtr2d	$⊢ (φ \land (k \in (M \dots N) \land j = k + K)) \to k = j - K$
48	41 47	jca	$⊢ (φ \land (k \in (M \dots N) \land j = k + K)) \to (j \in (M + K \dots N + K) \land k = j - K)$
49	31 48	impbida	$⊢ φ \to ((j \in (M + K \dots N + K) \land k = j - K) \leftrightarrow (k \in (M \dots N) \land j = k + K))$
50	49	mptcnv	$⊢ φ \to {(j \in (M + K \dots N + K) ⟼ j - K)}^{-1} = (k \in (M \dots N) ⟼ k + K)$
51	50	fneq1d	$⊢ φ \to ({(j \in (M + K \dots N + K) ⟼ j - K)}^{-1} Fn (M \dots N) \leftrightarrow (k \in (M \dots N) ⟼ k + K) Fn (M \dots N))$
52	10 51	mpbiri	$⊢ φ \to {(j \in (M + K \dots N + K) ⟼ j - K)}^{-1} Fn (M \dots N)$
53		dff1o4	$⊢ (j \in (M + K \dots N + K) ⟼ j - K) : (M + K \dots N + K) \underset{1-1 onto}{⟶} (M \dots N) \leftrightarrow ((j \in (M + K \dots N + K) ⟼ j - K) Fn (M + K \dots N + K) \land {(j \in (M + K \dots N + K) ⟼ j - K)}^{-1} Fn (M \dots N))$
54	7 52 53	sylanbrc	$⊢ φ \to (j \in (M + K \dots N + K) ⟼ j - K) : (M + K \dots N + K) \underset{1-1 onto}{⟶} (M \dots N)$

Metamath Proof Explorer

Theorem mptfzshft

Proof