Metamath Proof Explorer

Theorem metakunt23

Description: B coincides on the union of bijections of functions. (Contributed by metakunt, 28-May-2024)

Ref Expression
Hypotheses metakunt23.1 
|- ( ph -> M e. NN )
metakunt23.2 
|- ( ph -> I e. NN )
metakunt23.3 
|- ( ph -> I <_ M )
metakunt23.4 
|- B = ( x e. ( 1 ... M ) |-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) )
metakunt23.5 
|- C = ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) )
metakunt23.6 
|- D = ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) )
metakunt23.7 
|- ( ph -> X e. ( 1 ... M ) )
Assertion metakunt23 
|- ( ph -> ( B ` X ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )

Proof

Step Hyp Ref Expression
1 metakunt23.1 
 |-  ( ph -> M e. NN )
2 metakunt23.2 
 |-  ( ph -> I e. NN )
3 metakunt23.3 
 |-  ( ph -> I <_ M )
4 metakunt23.4 
 |-  B = ( x e. ( 1 ... M ) |-> if ( x = M , M , if ( x < I , ( x + ( M - I ) ) , ( x + ( 1 - I ) ) ) ) )
5 metakunt23.5 
 |-  C = ( x e. ( 1 ... ( I - 1 ) ) |-> ( x + ( M - I ) ) )
6 metakunt23.6 
 |-  D = ( x e. ( I ... ( M - 1 ) ) |-> ( x + ( 1 - I ) ) )
7 metakunt23.7 
 |-  ( ph -> X e. ( 1 ... M ) )
8 1 adantr 
 |-  ( ( ph /\ X = M ) -> M e. NN )
9 2 adantr 
 |-  ( ( ph /\ X = M ) -> I e. NN )
10 3 adantr 
 |-  ( ( ph /\ X = M ) -> I <_ M )
11 7 adantr 
 |-  ( ( ph /\ X = M ) -> X e. ( 1 ... M ) )
12 simpr 
 |-  ( ( ph /\ X = M ) -> X = M )
13 8 9 10 4 5 6 11 12 metakunt20 
 |-  ( ( ph /\ X = M ) -> ( B ` X ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )
14 1 ad2antrr 
 |-  ( ( ( ph /\ -. X = M ) /\ X < I ) -> M e. NN )
15 2 ad2antrr 
 |-  ( ( ( ph /\ -. X = M ) /\ X < I ) -> I e. NN )
16 3 ad2antrr 
 |-  ( ( ( ph /\ -. X = M ) /\ X < I ) -> I <_ M )
17 7 ad2antrr 
 |-  ( ( ( ph /\ -. X = M ) /\ X < I ) -> X e. ( 1 ... M ) )
18 simplr 
 |-  ( ( ( ph /\ -. X = M ) /\ X < I ) -> -. X = M )
19 simpr 
 |-  ( ( ( ph /\ -. X = M ) /\ X < I ) -> X < I )
20 14 15 16 4 5 6 17 18 19 metakunt21 
 |-  ( ( ( ph /\ -. X = M ) /\ X < I ) -> ( B ` X ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )
21 1 ad2antrr 
 |-  ( ( ( ph /\ -. X = M ) /\ -. X < I ) -> M e. NN )
22 2 ad2antrr 
 |-  ( ( ( ph /\ -. X = M ) /\ -. X < I ) -> I e. NN )
23 3 ad2antrr 
 |-  ( ( ( ph /\ -. X = M ) /\ -. X < I ) -> I <_ M )
24 7 ad2antrr 
 |-  ( ( ( ph /\ -. X = M ) /\ -. X < I ) -> X e. ( 1 ... M ) )
25 simplr 
 |-  ( ( ( ph /\ -. X = M ) /\ -. X < I ) -> -. X = M )
26 simpr 
 |-  ( ( ( ph /\ -. X = M ) /\ -. X < I ) -> -. X < I )
27 21 22 23 4 5 6 24 25 26 metakunt22 
 |-  ( ( ( ph /\ -. X = M ) /\ -. X < I ) -> ( B ` X ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )
28 20 27 pm2.61dan 
 |-  ( ( ph /\ -. X = M ) -> ( B ` X ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )
29 13 28 pm2.61dan 
 |-  ( ph -> ( B ` X ) = ( ( ( C u. D ) u. { <. M , M >. } ) ` X ) )