Metamath Proof Explorer

Theorem metakunt12

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

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

Proof

Step Hyp Ref Expression
1 metakunt12.1 
 |-  ( ph -> M e. NN )
2 metakunt12.2 
 |-  ( ph -> I e. NN )
3 metakunt12.3 
 |-  ( ph -> I <_ M )
4 metakunt12.4 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
5 metakunt12.5 
 |-  C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
6 metakunt12.6 
 |-  ( ph -> X e. ( 1 ... M ) )
7 ioran 
 |-  ( -. ( X = M \/ X < I ) <-> ( -. X = M /\ -. X < I ) )
8 4 a1i 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) )
9 eqeq1 
 |-  ( x = ( C ` X ) -> ( x = I <-> ( C ` X ) = I ) )
10 breq1 
 |-  ( x = ( C ` X ) -> ( x < I <-> ( C ` X ) < I ) )
11 id 
 |-  ( x = ( C ` X ) -> x = ( C ` X ) )
12 oveq1 
 |-  ( x = ( C ` X ) -> ( x - 1 ) = ( ( C ` X ) - 1 ) )
13 10 11 12 ifbieq12d 
 |-  ( x = ( C ` X ) -> if ( x < I , x , ( x - 1 ) ) = if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) )
14 9 13 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 ) ) ) )
15 14 adantl 
 |-  ( ( ( ph /\ -. X = M /\ -. X < I ) /\ 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 ) ) ) )
16 5 a1i 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) ) )
17 eqeq1 
 |-  ( y = X -> ( y = M <-> X = M ) )
18 breq1 
 |-  ( y = X -> ( y < I <-> X < I ) )
19 id 
 |-  ( y = X -> y = X )
20 oveq1 
 |-  ( y = X -> ( y + 1 ) = ( X + 1 ) )
21 18 19 20 ifbieq12d 
 |-  ( y = X -> if ( y < I , y , ( y + 1 ) ) = if ( X < I , X , ( X + 1 ) ) )
22 17 21 ifbieq2d 
 |-  ( y = X -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) )
23 22 adantl 
 |-  ( ( ( ph /\ -. X = M /\ -. X < I ) /\ y = X ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) )
24 simp2 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> -. X = M )
25 iffalse 
 |-  ( -. X = M -> if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) = if ( X < I , X , ( X + 1 ) ) )
26 24 25 syl 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) = if ( X < I , X , ( X + 1 ) ) )
27 simp3 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> -. X < I )
28 iffalse 
 |-  ( -. X < I -> if ( X < I , X , ( X + 1 ) ) = ( X + 1 ) )
29 27 28 syl 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> if ( X < I , X , ( X + 1 ) ) = ( X + 1 ) )
30 26 29 eqtrd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) = ( X + 1 ) )
31 30 adantr 
 |-  ( ( ( ph /\ -. X = M /\ -. X < I ) /\ y = X ) -> if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) = ( X + 1 ) )
32 23 31 eqtrd 
 |-  ( ( ( ph /\ -. X = M /\ -. X < I ) /\ y = X ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = ( X + 1 ) )
33 6 3ad2ant1 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> X e. ( 1 ... M ) )
34 elfznn 
 |-  ( X e. ( 1 ... M ) -> X e. NN )
35 6 34 syl 
 |-  ( ph -> X e. NN )
36 35 nnzd 
 |-  ( ph -> X e. ZZ )
37 36 3ad2ant1 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> X e. ZZ )
38 37 peano2zd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( X + 1 ) e. ZZ )
39 16 32 33 38 fvmptd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( C ` X ) = ( X + 1 ) )
40 eqeq1 
 |-  ( ( C ` X ) = ( X + 1 ) -> ( ( C ` X ) = I <-> ( X + 1 ) = I ) )
41 breq1 
 |-  ( ( C ` X ) = ( X + 1 ) -> ( ( C ` X ) < I <-> ( X + 1 ) < I ) )
42 id 
 |-  ( ( C ` X ) = ( X + 1 ) -> ( C ` X ) = ( X + 1 ) )
43 oveq1 
 |-  ( ( C ` X ) = ( X + 1 ) -> ( ( C ` X ) - 1 ) = ( ( X + 1 ) - 1 ) )
44 41 42 43 ifbieq12d 
 |-  ( ( C ` X ) = ( X + 1 ) -> if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) = if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) )
45 40 44 ifbieq2d 
 |-  ( ( C ` X ) = ( X + 1 ) -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = if ( ( X + 1 ) = I , M , if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) ) )
46 39 45 syl 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = if ( ( X + 1 ) = I , M , if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) ) )
47 2 nnred 
 |-  ( ph -> I e. RR )
48 47 3ad2ant1 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> I e. RR )
49 37 zred 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> X e. RR )
50 38 zred 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( X + 1 ) e. RR )
51 48 49 lenltd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( I <_ X <-> -. X < I ) )
52 27 51 mpbird 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> I <_ X )
53 49 ltp1d 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> X < ( X + 1 ) )
54 48 49 50 52 53 lelttrd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> I < ( X + 1 ) )
55 48 54 ltned 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> I =/= ( X + 1 ) )
56 55 necomd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( X + 1 ) =/= I )
57 56 neneqd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> -. ( X + 1 ) = I )
58 iffalse 
 |-  ( -. ( X + 1 ) = I -> if ( ( X + 1 ) = I , M , if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) ) = if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) )
59 57 58 syl 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> if ( ( X + 1 ) = I , M , if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) ) = if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) )
60 49 lep1d 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> X <_ ( X + 1 ) )
61 48 49 50 52 60 letrd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> I <_ ( X + 1 ) )
62 48 50 lenltd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( I <_ ( X + 1 ) <-> -. ( X + 1 ) < I ) )
63 61 62 mpbid 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> -. ( X + 1 ) < I )
64 iffalse 
 |-  ( -. ( X + 1 ) < I -> if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) = ( ( X + 1 ) - 1 ) )
65 63 64 syl 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) = ( ( X + 1 ) - 1 ) )
66 37 zcnd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> X e. CC )
67 1cnd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> 1 e. CC )
68 66 67 pncand 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( ( X + 1 ) - 1 ) = X )
69 59 65 68 3eqtrd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> if ( ( X + 1 ) = I , M , if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) ) = X )
70 46 69 eqtrd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = X )
71 70 adantr 
 |-  ( ( ( ph /\ -. X = M /\ -. X < I ) /\ x = ( C ` X ) ) -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = X )
72 15 71 eqtrd 
 |-  ( ( ( ph /\ -. X = M /\ -. X < I ) /\ x = ( C ` X ) ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = X )
73 1 2 3 5 metakunt2 
 |-  ( ph -> C : ( 1 ... M ) --> ( 1 ... M ) )
74 73 3ad2ant1 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> C : ( 1 ... M ) --> ( 1 ... M ) )
75 74 33 ffvelrnd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( C ` X ) e. ( 1 ... M ) )
76 8 72 75 33 fvmptd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( A ` ( C ` X ) ) = X )
77 76 3expb 
 |-  ( ( ph /\ ( -. X = M /\ -. X < I ) ) -> ( A ` ( C ` X ) ) = X )
78 7 77 sylan2b 
 |-  ( ( ph /\ -. ( X = M \/ X < I ) ) -> ( A ` ( C ` X ) ) = X )