Metamath Proof Explorer

Theorem metakunt25

Description: B is a permutation. (Contributed by metakunt, 28-May-2024)

Ref Expression
Hypotheses metakunt25.1 
|- ( ph -> M e. NN )
metakunt25.2 
|- ( ph -> I e. NN )
metakunt25.3 
|- ( ph -> I <_ M )
metakunt25.4 
|- B = ( x e. ( 1 ... M ) |-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) )
Assertion metakunt25 
|- ( ph -> B : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )

Proof

Step Hyp Ref Expression
1 metakunt25.1 
 |-  ( ph -> M e. NN )
2 metakunt25.2 
 |-  ( ph -> I e. NN )
3 metakunt25.3 
 |-  ( ph -> I <_ M )
4 metakunt25.4 
 |-  B = ( x e. ( 1 ... M ) |-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) )
5 eqid 
 |-  ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) ) = ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) )
6 1 2 3 5 metakunt15 
 |-  ( ph -> ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) ) : ( 1 ... ( I - 1 ) ) -1-1-onto-> ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) )
7 eqid 
 |-  ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) ) = ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) )
8 1 2 3 7 metakunt16 
 |-  ( ph -> ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) ) : ( I ... ( M - 1 ) ) -1-1-onto-> ( 1 ... ( M - I ) ) )
9 f1osng 
 |-  ( ( M e. NN /\ M e. NN ) -> { <. M , M >. } : { M } -1-1-onto-> { M } )
10 1 1 9 syl2anc 
 |-  ( ph -> { <. M , M >. } : { M } -1-1-onto-> { M } )
11 1 2 3 metakunt18 
 |-  ( ph -> ( ( ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) /\ ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) /\ ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) ) /\ ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( 1 ... ( M - I ) ) ) = (/) /\ ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i { M } ) = (/) /\ ( ( 1 ... ( M - I ) ) i^i { M } ) = (/) ) ) )
12 11 simpld 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) /\ ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) /\ ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) ) )
13 12 simp1d 
 |-  ( ph -> ( ( 1 ... ( I - 1 ) ) i^i ( I ... ( M - 1 ) ) ) = (/) )
14 12 simp2d 
 |-  ( ph -> ( ( 1 ... ( I - 1 ) ) i^i { M } ) = (/) )
15 12 simp3d 
 |-  ( ph -> ( ( I ... ( M - 1 ) ) i^i { M } ) = (/) )
16 11 simprd 
 |-  ( ph -> ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( 1 ... ( M - I ) ) ) = (/) /\ ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i { M } ) = (/) /\ ( ( 1 ... ( M - I ) ) i^i { M } ) = (/) ) )
17 16 simp1d 
 |-  ( ph -> ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i ( 1 ... ( M - I ) ) ) = (/) )
18 16 simp2d 
 |-  ( ph -> ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) i^i { M } ) = (/) )
19 16 simp3d 
 |-  ( ph -> ( ( 1 ... ( M - I ) ) i^i { M } ) = (/) )
20 eleq1 
 |-  ( M = if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) -> ( M e. ZZ <-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) e. ZZ ) )
21 eleq1 
 |-  ( if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) = if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) -> ( if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) e. ZZ <-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) e. ZZ ) )
22 1 nnzd 
 |-  ( ph -> M e. ZZ )
23 22 adantr 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> M e. ZZ )
24 23 adantr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ x = M ) -> M e. ZZ )
25 eleq1 
 |-  ( ( x + ( M - I ) ) = if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) -> ( ( x + ( M - I ) ) e. ZZ <-> if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) e. ZZ ) )
26 eleq1 
 |-  ( ( x + ( 1 - I ) ) = if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) -> ( ( x + ( 1 - I ) ) e. ZZ <-> if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) e. ZZ ) )
27 elfzelz 
 |-  ( x e. ( 1 ... M ) -> x e. ZZ )
28 27 adantl 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> x e. ZZ )
29 28 adantr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) -> x e. ZZ )
30 29 adantr 
 |-  ( ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) /\ x < I ) -> x e. ZZ )
31 23 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) /\ x < I ) -> M e. ZZ )
32 2 nnzd 
 |-  ( ph -> I e. ZZ )
33 32 adantr 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> I e. ZZ )
34 33 adantr 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) -> I e. ZZ )
35 34 adantr 
 |-  ( ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) /\ x < I ) -> I e. ZZ )
36 31 35 zsubcld 
 |-  ( ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) /\ x < I ) -> ( M - I ) e. ZZ )
37 30 36 zaddcld 
 |-  ( ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) /\ x < I ) -> ( x + ( M - I ) ) e. ZZ )
38 29 adantr 
 |-  ( ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) /\ -. x < I ) -> x e. ZZ )
39 1zzd 
 |-  ( ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) /\ -. x < I ) -> 1 e. ZZ )
40 34 adantr 
 |-  ( ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) /\ -. x < I ) -> I e. ZZ )
41 39 40 zsubcld 
 |-  ( ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) /\ -. x < I ) -> ( 1 - I ) e. ZZ )
42 38 41 zaddcld 
 |-  ( ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) /\ -. x < I ) -> ( x + ( 1 - I ) ) e. ZZ )
43 25 26 37 42 ifbothda 
 |-  ( ( ( ph /\ x e. ( 1 ... M ) ) /\ -. x = M ) -> if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) e. ZZ )
44 20 21 24 43 ifbothda 
 |-  ( ( ph /\ x e. ( 1 ... M ) ) -> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) e. ZZ )
45 44 4 fmptd 
 |-  ( ph -> B : ( 1 ... M ) --> ZZ )
46 45 ffnd 
 |-  ( ph -> B Fn ( 1 ... M ) )
47 1 2 3 4 5 7 metakunt19 
 |-  ( ph -> ( ( ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) ) Fn ( 1 ... ( I - 1 ) ) /\ ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) ) Fn ( I ... ( M - 1 ) ) /\ ( ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) ) u. ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) ) ) Fn ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) ) /\ { <. M , M >. } Fn { M } ) )
48 47 simpld 
 |-  ( ph -> ( ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) ) Fn ( 1 ... ( I - 1 ) ) /\ ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) ) Fn ( I ... ( M - 1 ) ) /\ ( ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) ) u. ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) ) ) Fn ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) ) )
49 48 simp3d 
 |-  ( ph -> ( ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) ) u. ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) ) ) Fn ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) )
50 47 simprd 
 |-  ( ph -> { <. M , M >. } Fn { M } )
51 1 2 3 metakunt24 
 |-  ( ph -> ( ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = (/) /\ ( 1 ... M ) = ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. { M } ) /\ ( 1 ... M ) = ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) u. ( 1 ... ( M - I ) ) ) u. { M } ) ) )
52 51 simp1d 
 |-  ( ph -> ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) i^i { M } ) = (/) )
53 49 50 52 fnund 
 |-  ( ph -> ( ( ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) ) u. ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) ) ) u. { <. M , M >. } ) Fn ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. { M } ) )
54 51 simp2d 
 |-  ( ph -> ( 1 ... M ) = ( ( ( 1 ... ( I - 1 ) ) u. ( I ... ( M - 1 ) ) ) u. { M } ) )
55 1 adantr 
 |-  ( ( ph /\ y e. ( 1 ... M ) ) -> M e. NN )
56 2 adantr 
 |-  ( ( ph /\ y e. ( 1 ... M ) ) -> I e. NN )
57 3 adantr 
 |-  ( ( ph /\ y e. ( 1 ... M ) ) -> I <_ M )
58 simpr 
 |-  ( ( ph /\ y e. ( 1 ... M ) ) -> y e. ( 1 ... M ) )
59 55 56 57 4 5 7 58 metakunt23 
 |-  ( ( ph /\ y e. ( 1 ... M ) ) -> ( B ` y ) = ( ( ( ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) ) u. ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) ) ) u. { <. M , M >. } ) ` y ) )
60 46 53 54 59 eqfnfv2d2 
 |-  ( ph -> B = ( ( ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) ) u. ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) ) ) u. { <. M , M >. } ) )
61 51 simp3d 
 |-  ( ph -> ( 1 ... M ) = ( ( ( ( ( M - I ) + 1 ) ... ( M - 1 ) ) u. ( 1 ... ( M - I ) ) ) u. { M } ) )
62 6 8 10 13 14 15 17 18 19 60 54 61 metakunt17 
 |-  ( ph -> B : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )