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→ ( 𝑀 ... 𝑁 ) )