Metamath Proof Explorer

Theorem metakunt14

Description: A is a primitive permutation that moves the I-th element to the end and C is its inverse that moves the last element back to the I-th position. (Contributed by metakunt, 25-May-2024)

Ref Expression
Hypotheses metakunt14.1 
|- ( ph -> M e. NN )
metakunt14.2 
|- ( ph -> I e. NN )
metakunt14.3 
|- ( ph -> I <_ M )
metakunt14.4 
|- A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
metakunt14.5 
|- C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
Assertion metakunt14 
|- ( ph -> ( A : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) /\ `' A = C ) )

Proof

Step Hyp Ref Expression
1 metakunt14.1 
 |-  ( ph -> M e. NN )
2 metakunt14.2 
 |-  ( ph -> I e. NN )
3 metakunt14.3 
 |-  ( ph -> I <_ M )
4 metakunt14.4 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
5 metakunt14.5 
 |-  C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
6 1 2 3 4 metakunt1 
 |-  ( ph -> A : ( 1 ... M ) --> ( 1 ... M ) )
7 1 2 3 5 metakunt2 
 |-  ( ph -> C : ( 1 ... M ) --> ( 1 ... M ) )
8 1 adantr 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> M e. NN )
9 2 adantr 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> I e. NN )
10 3 adantr 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> I <_ M )
11 simpr 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> a e. ( 1 ... M ) )
12 8 9 10 4 5 11 metakunt9 
 |-  ( ( ph /\ a e. ( 1 ... M ) ) -> ( C ` ( A ` a ) ) = a )
13 12 ralrimiva 
 |-  ( ph -> A. a e. ( 1 ... M ) ( C ` ( A ` a ) ) = a )
14 1 adantr 
 |-  ( ( ph /\ b e. ( 1 ... M ) ) -> M e. NN )
15 2 adantr 
 |-  ( ( ph /\ b e. ( 1 ... M ) ) -> I e. NN )
16 3 adantr 
 |-  ( ( ph /\ b e. ( 1 ... M ) ) -> I <_ M )
17 simpr 
 |-  ( ( ph /\ b e. ( 1 ... M ) ) -> b e. ( 1 ... M ) )
18 14 15 16 4 5 17 metakunt13 
 |-  ( ( ph /\ b e. ( 1 ... M ) ) -> ( A ` ( C ` b ) ) = b )
19 18 ralrimiva 
 |-  ( ph -> A. b e. ( 1 ... M ) ( A ` ( C ` b ) ) = b )
20 6 7 13 19 2fvidf1od 
 |-  ( ph -> A : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
21 6 7 13 19 2fvidinvd 
 |-  ( ph -> `' A = C )
22 20 21 jca 
 |-  ( ph -> ( A : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) /\ `' A = C ) )