Metamath Proof Explorer

Theorem metakunt5

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

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

Proof

Step Hyp Ref Expression
1 metakunt5.1 
 |-  ( ph -> M e. NN )
2 metakunt5.2 
 |-  ( ph -> I e. NN )
3 metakunt5.3 
 |-  ( ph -> I <_ M )
4 metakunt5.4 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
5 metakunt5.5 
 |-  C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
6 metakunt5.6 
 |-  ( ph -> X e. ( 1 ... M ) )
7 5 a1i 
 |-  ( ( ph /\ X = I ) -> C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) ) )
8 fveq2 
 |-  ( X = I -> ( A ` X ) = ( A ` I ) )
9 8 adantl 
 |-  ( ( ph /\ X = I ) -> ( A ` X ) = ( A ` I ) )
10 4 a1i 
 |-  ( ph -> A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) )
11 simpr 
 |-  ( ( ph /\ x = I ) -> x = I )
12 11 iftrued 
 |-  ( ( ph /\ x = I ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = M )
13 1zzd 
 |-  ( ph -> 1 e. ZZ )
14 1 nnzd 
 |-  ( ph -> M e. ZZ )
15 2 nnzd 
 |-  ( ph -> I e. ZZ )
16 2 nnge1d 
 |-  ( ph -> 1 <_ I )
17 13 14 15 16 3 elfzd 
 |-  ( ph -> I e. ( 1 ... M ) )
18 10 12 17 1 fvmptd 
 |-  ( ph -> ( A ` I ) = M )
19 18 adantr 
 |-  ( ( ph /\ X = I ) -> ( A ` I ) = M )
20 9 19 eqtrd 
 |-  ( ( ph /\ X = I ) -> ( A ` X ) = M )
21 20 eqeq2d 
 |-  ( ( ph /\ X = I ) -> ( y = ( A ` X ) <-> y = M ) )
22 iftrue 
 |-  ( y = M -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = I )
23 22 3ad2ant3 
 |-  ( ( ph /\ X = I /\ y = M ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = I )
24 simp2 
 |-  ( ( ph /\ X = I /\ y = M ) -> X = I )
25 23 24 eqtr4d 
 |-  ( ( ph /\ X = I /\ y = M ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = X )
26 25 3expia 
 |-  ( ( ph /\ X = I ) -> ( y = M -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = X ) )
27 21 26 sylbid 
 |-  ( ( ph /\ X = I ) -> ( y = ( A ` X ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = X ) )
28 27 imp 
 |-  ( ( ( ph /\ X = I ) /\ y = ( A ` X ) ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = X )
29 1 2 3 4 metakunt1 
 |-  ( ph -> A : ( 1 ... M ) --> ( 1 ... M ) )
30 29 adantr 
 |-  ( ( ph /\ X = I ) -> A : ( 1 ... M ) --> ( 1 ... M ) )
31 6 adantr 
 |-  ( ( ph /\ X = I ) -> X e. ( 1 ... M ) )
32 30 31 ffvelrnd 
 |-  ( ( ph /\ X = I ) -> ( A ` X ) e. ( 1 ... M ) )
33 7 28 32 31 fvmptd 
 |-  ( ( ph /\ X = I ) -> ( C ` ( A ` X ) ) = X )