Metamath Proof Explorer

Theorem metakunt8

Description: C is the left inverse for A. (Contributed by metakunt, 24-May-2024)

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

Proof

Step Hyp Ref Expression
1 metakunt8.1 
 |-  ( ph -> M e. NN )
2 metakunt8.2 
 |-  ( ph -> I e. NN )
3 metakunt8.3 
 |-  ( ph -> I <_ M )
4 metakunt8.4 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
5 metakunt8.5 
 |-  C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
6 metakunt8.6 
 |-  ( ph -> X e. ( 1 ... M ) )
7 5 a1i 
 |-  ( ( ph /\ I < X ) -> C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) ) )
8 eqeq1 
 |-  ( y = ( A ` X ) -> ( y = M <-> ( A ` X ) = M ) )
9 breq1 
 |-  ( y = ( A ` X ) -> ( y < I <-> ( A ` X ) < I ) )
10 id 
 |-  ( y = ( A ` X ) -> y = ( A ` X ) )
11 oveq1 
 |-  ( y = ( A ` X ) -> ( y + 1 ) = ( ( A ` X ) + 1 ) )
12 9 10 11 ifbieq12d 
 |-  ( y = ( A ` X ) -> if ( y < I , y , ( y + 1 ) ) = if ( ( A ` X ) < I , ( A ` X ) , ( ( A ` X ) + 1 ) ) )
13 8 12 ifbieq2d 
 |-  ( y = ( A ` X ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = if ( ( A ` X ) = M , I , if ( ( A ` X ) < I , ( A ` X ) , ( ( A ` X ) + 1 ) ) ) )
14 13 adantl 
 |-  ( ( ( ph /\ I < X ) /\ y = ( A ` X ) ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = if ( ( A ` X ) = M , I , if ( ( A ` X ) < I , ( A ` X ) , ( ( A ` X ) + 1 ) ) ) )
15 1 2 3 4 5 6 metakunt7 
 |-  ( ( ph /\ I < X ) -> ( ( A ` X ) = ( X - 1 ) /\ -. ( A ` X ) = M /\ -. ( A ` X ) < I ) )
16 15 simp2d 
 |-  ( ( ph /\ I < X ) -> -. ( A ` X ) = M )
17 iffalse 
 |-  ( -. ( A ` X ) = M -> if ( ( A ` X ) = M , I , if ( ( A ` X ) < I , ( A ` X ) , ( ( A ` X ) + 1 ) ) ) = if ( ( A ` X ) < I , ( A ` X ) , ( ( A ` X ) + 1 ) ) )
18 16 17 syl 
 |-  ( ( ph /\ I < X ) -> if ( ( A ` X ) = M , I , if ( ( A ` X ) < I , ( A ` X ) , ( ( A ` X ) + 1 ) ) ) = if ( ( A ` X ) < I , ( A ` X ) , ( ( A ` X ) + 1 ) ) )
19 15 simp3d 
 |-  ( ( ph /\ I < X ) -> -. ( A ` X ) < I )
20 iffalse 
 |-  ( -. ( A ` X ) < I -> if ( ( A ` X ) < I , ( A ` X ) , ( ( A ` X ) + 1 ) ) = ( ( A ` X ) + 1 ) )
21 19 20 syl 
 |-  ( ( ph /\ I < X ) -> if ( ( A ` X ) < I , ( A ` X ) , ( ( A ` X ) + 1 ) ) = ( ( A ` X ) + 1 ) )
22 18 21 eqtrd 
 |-  ( ( ph /\ I < X ) -> if ( ( A ` X ) = M , I , if ( ( A ` X ) < I , ( A ` X ) , ( ( A ` X ) + 1 ) ) ) = ( ( A ` X ) + 1 ) )
23 15 simp1d 
 |-  ( ( ph /\ I < X ) -> ( A ` X ) = ( X - 1 ) )
24 23 oveq1d 
 |-  ( ( ph /\ I < X ) -> ( ( A ` X ) + 1 ) = ( ( X - 1 ) + 1 ) )
25 elfznn 
 |-  ( X e. ( 1 ... M ) -> X e. NN )
26 6 25 syl 
 |-  ( ph -> X e. NN )
27 26 nncnd 
 |-  ( ph -> X e. CC )
28 1cnd 
 |-  ( ph -> 1 e. CC )
29 27 28 npcand 
 |-  ( ph -> ( ( X - 1 ) + 1 ) = X )
30 29 adantr 
 |-  ( ( ph /\ I < X ) -> ( ( X - 1 ) + 1 ) = X )
31 24 30 eqtrd 
 |-  ( ( ph /\ I < X ) -> ( ( A ` X ) + 1 ) = X )
32 22 31 eqtrd 
 |-  ( ( ph /\ I < X ) -> if ( ( A ` X ) = M , I , if ( ( A ` X ) < I , ( A ` X ) , ( ( A ` X ) + 1 ) ) ) = X )
33 32 adantr 
 |-  ( ( ( ph /\ I < X ) /\ y = ( A ` X ) ) -> if ( ( A ` X ) = M , I , if ( ( A ` X ) < I , ( A ` X ) , ( ( A ` X ) + 1 ) ) ) = X )
34 14 33 eqtrd 
 |-  ( ( ( ph /\ I < X ) /\ y = ( A ` X ) ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = X )
35 1 2 3 4 metakunt1 
 |-  ( ph -> A : ( 1 ... M ) --> ( 1 ... M ) )
36 35 adantr 
 |-  ( ( ph /\ I < X ) -> A : ( 1 ... M ) --> ( 1 ... M ) )
37 6 adantr 
 |-  ( ( ph /\ I < X ) -> X e. ( 1 ... M ) )
38 36 37 ffvelcdmd 
 |-  ( ( ph /\ I < X ) -> ( A ` X ) e. ( 1 ... M ) )
39 7 34 38 37 fvmptd 
 |-  ( ( ph /\ I < X ) -> ( C ` ( A ` X ) ) = X )