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 φ K
mptfzshft.2 φ M
mptfzshft.3 φ N
Assertion mptfzshft φ j M + K N + K j K : M + K N + K 1-1 onto M N

Proof

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