Metamath Proof Explorer

Theorem metakunt10

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

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

Proof

Step Hyp Ref Expression
1 metakunt10.1 
 |-  ( ph -> M e. NN )
2 metakunt10.2 
 |-  ( ph -> I e. NN )
3 metakunt10.3 
 |-  ( ph -> I <_ M )
4 metakunt10.4 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
5 metakunt10.5 
 |-  C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
6 metakunt10.6 
 |-  ( ph -> X e. ( 1 ... M ) )
7 4 a1i 
 |-  ( ( ph /\ X = M ) -> A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) )
8 eqeq1 
 |-  ( x = ( C ` X ) -> ( x = I <-> ( C ` X ) = I ) )
9 breq1 
 |-  ( x = ( C ` X ) -> ( x < I <-> ( C ` X ) < I ) )
10 id 
 |-  ( x = ( C ` X ) -> x = ( C ` X ) )
11 oveq1 
 |-  ( x = ( C ` X ) -> ( x - 1 ) = ( ( C ` X ) - 1 ) )
12 9 10 11 ifbieq12d 
 |-  ( x = ( C ` X ) -> if ( x < I , x , ( x - 1 ) ) = if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) )
13 8 12 ifbieq2d 
 |-  ( x = ( C ` X ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) )
14 13 adantl 
 |-  ( ( ( ph /\ X = M ) /\ x = ( C ` X ) ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) )
15 fveq2 
 |-  ( X = M -> ( C ` X ) = ( C ` M ) )
16 15 adantl 
 |-  ( ( ph /\ X = M ) -> ( C ` X ) = ( C ` M ) )
17 5 a1i 
 |-  ( ph -> C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) ) )
18 iftrue 
 |-  ( y = M -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = I )
19 18 adantl 
 |-  ( ( ph /\ y = M ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = I )
20 1zzd 
 |-  ( ph -> 1 e. ZZ )
21 1 nnzd 
 |-  ( ph -> M e. ZZ )
22 1 nnge1d 
 |-  ( ph -> 1 <_ M )
23 1 nnred 
 |-  ( ph -> M e. RR )
24 23 leidd 
 |-  ( ph -> M <_ M )
25 20 21 21 22 24 elfzd 
 |-  ( ph -> M e. ( 1 ... M ) )
26 17 19 25 2 fvmptd 
 |-  ( ph -> ( C ` M ) = I )
27 26 adantr 
 |-  ( ( ph /\ X = M ) -> ( C ` M ) = I )
28 16 27 eqtrd 
 |-  ( ( ph /\ X = M ) -> ( C ` X ) = I )
29 iftrue 
 |-  ( ( C ` X ) = I -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = M )
30 28 29 syl 
 |-  ( ( ph /\ X = M ) -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = M )
31 simpr 
 |-  ( ( ph /\ X = M ) -> X = M )
32 31 eqcomd 
 |-  ( ( ph /\ X = M ) -> M = X )
33 30 32 eqtrd 
 |-  ( ( ph /\ X = M ) -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = X )
34 33 adantr 
 |-  ( ( ( ph /\ X = M ) /\ x = ( C ` X ) ) -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = X )
35 14 34 eqtrd 
 |-  ( ( ( ph /\ X = M ) /\ x = ( C ` X ) ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = X )
36 1 2 3 5 metakunt2 
 |-  ( ph -> C : ( 1 ... M ) --> ( 1 ... M ) )
37 36 adantr 
 |-  ( ( ph /\ X = M ) -> C : ( 1 ... M ) --> ( 1 ... M ) )
38 6 adantr 
 |-  ( ( ph /\ X = M ) -> X e. ( 1 ... M ) )
39 37 38 ffvelcdmd 
 |-  ( ( ph /\ X = M ) -> ( C ` X ) e. ( 1 ... M ) )
40 7 35 39 38 fvmptd 
 |-  ( ( ph /\ X = M ) -> ( A ` ( C ` X ) ) = X )