Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
mptfzshft.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
mptfzshft.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
Assertion mptfzshft ( 𝜑 → ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) : ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )

Proof

Step Hyp Ref Expression
1 mptfzshft.1 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2 mptfzshft.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 mptfzshft.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4 ovex ⊢ ( 𝑗 − 𝐾 ) ∈ V
5 eqid ⊢ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) = ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) )
6 4 5 fnmpti ⊢ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) Fn ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) )
7 6 a1i ⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) Fn ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) )
8 ovex ⊢ ( 𝑘 + 𝐾 ) ∈ V
9 eqid ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑘 + 𝐾 ) ) = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑘 + 𝐾 ) )
10 8 9 fnmpti ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑘 + 𝐾 ) ) Fn ( 𝑀 ... 𝑁 )
11 simprr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → 𝑘 = ( 𝑗 − 𝐾 ) )
12 11 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → ( 𝑘 + 𝐾 ) = ( ( 𝑗 − 𝐾 ) + 𝐾 ) )
13 elfzelz ⊢ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) → 𝑗 ∈ ℤ )
14 13 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → 𝑗 ∈ ℤ )
15 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → 𝐾 ∈ ℤ )
16 zcn ⊢ ( 𝑗 ∈ ℤ → 𝑗 ∈ ℂ )
17 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
18 npcan ⊢ ( ( 𝑗 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( 𝑗 − 𝐾 ) + 𝐾 ) = 𝑗 )
19 16 17 18 syl2an ⊢ ( ( 𝑗 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑗 − 𝐾 ) + 𝐾 ) = 𝑗 )
20 14 15 19 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → ( ( 𝑗 − 𝐾 ) + 𝐾 ) = 𝑗 )
21 12 20 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → 𝑗 = ( 𝑘 + 𝐾 ) )
22 simprl ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) )
23 21 22 eqeltrrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → ( 𝑘 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) )
24 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → 𝑀 ∈ ℤ )
25 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → 𝑁 ∈ ℤ )
26 14 15 zsubcld ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → ( 𝑗 − 𝐾 ) ∈ ℤ )
27 11 26 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → 𝑘 ∈ ℤ )
28 fzaddel ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑘 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) )
29 24 25 27 15 28 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑘 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) )
30 23 29 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
31 30 21 jca ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) )
32 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) → 𝑗 = ( 𝑘 + 𝐾 ) )
33 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) → 𝑘 ∈ ( 𝑀 ... 𝑁 ) )
34 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) → 𝑀 ∈ ℤ )
35 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) → 𝑁 ∈ ℤ )
36 elfzelz ⊢ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) → 𝑘 ∈ ℤ )
37 36 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) → 𝑘 ∈ ℤ )
38 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) → 𝐾 ∈ ℤ )
39 34 35 37 38 28 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) → ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑘 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) )
40 33 39 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) → ( 𝑘 + 𝐾 ) ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) )
41 32 40 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) → 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) )
42 32 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) → ( 𝑗 − 𝐾 ) = ( ( 𝑘 + 𝐾 ) − 𝐾 ) )
43 zcn ⊢ ( 𝑘 ∈ ℤ → 𝑘 ∈ ℂ )
44 pncan ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( 𝑘 + 𝐾 ) − 𝐾 ) = 𝑘 )
45 43 17 44 syl2an ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝑘 + 𝐾 ) − 𝐾 ) = 𝑘 )
46 37 38 45 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) → ( ( 𝑘 + 𝐾 ) − 𝐾 ) = 𝑘 )
47 42 46 eqtr2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) → 𝑘 = ( 𝑗 − 𝐾 ) )
48 41 47 jca ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) → ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) )
49 31 48 impbida ⊢ ( 𝜑 → ( ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ 𝑘 = ( 𝑗 − 𝐾 ) ) ↔ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ∧ 𝑗 = ( 𝑘 + 𝐾 ) ) ) )
50 49 mptcnv ⊢ ( 𝜑 → ◡ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) = ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑘 + 𝐾 ) ) )
51 50 fneq1d ⊢ ( 𝜑 → ( ◡ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) Fn ( 𝑀 ... 𝑁 ) ↔ ( 𝑘 ∈ ( 𝑀 ... 𝑁 ) ↦ ( 𝑘 + 𝐾 ) ) Fn ( 𝑀 ... 𝑁 ) ) )
52 10 51 mpbiri ⊢ ( 𝜑 → ◡ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) Fn ( 𝑀 ... 𝑁 ) )
53 dff1o4 ⊢ ( ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) : ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) –1-1-onto→ ( 𝑀 ... 𝑁 ) ↔ ( ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) Fn ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ∧ ◡ ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) Fn ( 𝑀 ... 𝑁 ) ) )
54 7 52 53 sylanbrc ⊢ ( 𝜑 → ( 𝑗 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ↦ ( 𝑗 − 𝐾 ) ) : ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) –1-1-onto→ ( 𝑀 ... 𝑁 ) )