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 
|- ( ph -> K e. ZZ )
mptfzshft.2 
|- ( ph -> M e. ZZ )
mptfzshft.3 
|- ( ph -> N e. ZZ )
Assertion mptfzshft 
|- ( ph -> ( j e. ( ( M + K ) ... ( N + K ) ) |-> ( j - K ) ) : ( ( M + K ) ... ( N + K ) ) -1-1-onto-> ( M ... N ) )

Proof

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