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 6 elfzelzd 
 |-  ( ph -> X e. ZZ )
35 34 3ad2ant1 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> X e. ZZ )
36 35 peano2zd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( X + 1 ) e. ZZ )
37 16 32 33 36 fvmptd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( C ` X ) = ( X + 1 ) )
38 eqeq1 
 |-  ( ( C ` X ) = ( X + 1 ) -> ( ( C ` X ) = I <-> ( X + 1 ) = I ) )
39 breq1 
 |-  ( ( C ` X ) = ( X + 1 ) -> ( ( C ` X ) < I <-> ( X + 1 ) < I ) )
40 id 
 |-  ( ( C ` X ) = ( X + 1 ) -> ( C ` X ) = ( X + 1 ) )
41 oveq1 
 |-  ( ( C ` X ) = ( X + 1 ) -> ( ( C ` X ) - 1 ) = ( ( X + 1 ) - 1 ) )
42 39 40 41 ifbieq12d 
 |-  ( ( C ` X ) = ( X + 1 ) -> if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) = if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) )
43 38 42 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 ) ) ) )
44 37 43 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 ) ) ) )
45 2 nnred 
 |-  ( ph -> I e. RR )
46 45 3ad2ant1 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> I e. RR )
47 35 zred 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> X e. RR )
48 36 zred 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( X + 1 ) e. RR )
49 46 47 lenltd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( I <_ X <-> -. X < I ) )
50 27 49 mpbird 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> I <_ X )
51 47 ltp1d 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> X < ( X + 1 ) )
52 46 47 48 50 51 lelttrd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> I < ( X + 1 ) )
53 46 52 ltned 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> I =/= ( X + 1 ) )
54 53 necomd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( X + 1 ) =/= I )
55 54 neneqd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> -. ( X + 1 ) = I )
56 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 ) ) )
57 55 56 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 ) ) )
58 47 lep1d 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> X <_ ( X + 1 ) )
59 46 47 48 50 58 letrd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> I <_ ( X + 1 ) )
60 46 48 lenltd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( I <_ ( X + 1 ) <-> -. ( X + 1 ) < I ) )
61 59 60 mpbid 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> -. ( X + 1 ) < I )
62 iffalse 
 |-  ( -. ( X + 1 ) < I -> if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) = ( ( X + 1 ) - 1 ) )
63 61 62 syl 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) = ( ( X + 1 ) - 1 ) )
64 35 zcnd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> X e. CC )
65 1cnd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> 1 e. CC )
66 64 65 pncand 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( ( X + 1 ) - 1 ) = X )
67 57 63 66 3eqtrd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> if ( ( X + 1 ) = I , M , if ( ( X + 1 ) < I , ( X + 1 ) , ( ( X + 1 ) - 1 ) ) ) = X )
68 44 67 eqtrd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = X )
69 68 adantr 
 |-  ( ( ( ph /\ -. X = M /\ -. X < I ) /\ x = ( C ` X ) ) -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = X )
70 15 69 eqtrd 
 |-  ( ( ( ph /\ -. X = M /\ -. X < I ) /\ x = ( C ` X ) ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = X )
71 1 2 3 5 metakunt2 
 |-  ( ph -> C : ( 1 ... M ) --> ( 1 ... M ) )
72 71 3ad2ant1 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> C : ( 1 ... M ) --> ( 1 ... M ) )
73 72 33 ffvelrnd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( C ` X ) e. ( 1 ... M ) )
74 8 70 73 33 fvmptd 
 |-  ( ( ph /\ -. X = M /\ -. X < I ) -> ( A ` ( C ` X ) ) = X )
75 74 3expb 
 |-  ( ( ph /\ ( -. X = M /\ -. X < I ) ) -> ( A ` ( C ` X ) ) = X )
76 7 75 sylan2b 
 |-  ( ( ph /\ -. ( X = M \/ X < I ) ) -> ( A ` ( C ` X ) ) = X )