Metamath Proof Explorer

Theorem metakunt11

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

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

Proof

Step Hyp Ref Expression
1 metakunt11.1 
 |-  ( ph -> M e. NN )
2 metakunt11.2 
 |-  ( ph -> I e. NN )
3 metakunt11.3 
 |-  ( ph -> I <_ M )
4 metakunt11.4 
 |-  A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
5 metakunt11.5 
 |-  C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
6 metakunt11.6 
 |-  ( ph -> X e. ( 1 ... M ) )
7 4 a1i 
 |-  ( ( ph /\ X < I ) -> 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 < 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 ) ) ) )
15 5 a1i 
 |-  ( ( ph /\ X < I ) -> C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) ) )
16 eqeq1 
 |-  ( y = X -> ( y = M <-> X = M ) )
17 breq1 
 |-  ( y = X -> ( y < I <-> X < I ) )
18 id 
 |-  ( y = X -> y = X )
19 oveq1 
 |-  ( y = X -> ( y + 1 ) = ( X + 1 ) )
20 17 18 19 ifbieq12d 
 |-  ( y = X -> if ( y < I , y , ( y + 1 ) ) = if ( X < I , X , ( X + 1 ) ) )
21 16 20 ifbieq2d 
 |-  ( y = X -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) )
22 21 adantl 
 |-  ( ( ( ph /\ X < I ) /\ y = X ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) )
23 elfznn 
 |-  ( X e. ( 1 ... M ) -> X e. NN )
24 6 23 syl 
 |-  ( ph -> X e. NN )
25 24 nnred 
 |-  ( ph -> X e. RR )
26 25 adantr 
 |-  ( ( ph /\ X < I ) -> X e. RR )
27 2 nnred 
 |-  ( ph -> I e. RR )
28 27 adantr 
 |-  ( ( ph /\ X < I ) -> I e. RR )
29 1 nnred 
 |-  ( ph -> M e. RR )
30 29 adantr 
 |-  ( ( ph /\ X < I ) -> M e. RR )
31 simpr 
 |-  ( ( ph /\ X < I ) -> X < I )
32 3 adantr 
 |-  ( ( ph /\ X < I ) -> I <_ M )
33 26 28 30 31 32 ltletrd 
 |-  ( ( ph /\ X < I ) -> X < M )
34 26 33 ltned 
 |-  ( ( ph /\ X < I ) -> X =/= M )
35 df-ne 
 |-  ( X =/= M <-> -. X = M )
36 34 35 sylib 
 |-  ( ( ph /\ X < I ) -> -. X = M )
37 iffalse 
 |-  ( -. X = M -> if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) = if ( X < I , X , ( X + 1 ) ) )
38 36 37 syl 
 |-  ( ( ph /\ X < I ) -> if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) = if ( X < I , X , ( X + 1 ) ) )
39 iftrue 
 |-  ( X < I -> if ( X < I , X , ( X + 1 ) ) = X )
40 39 adantl 
 |-  ( ( ph /\ X < I ) -> if ( X < I , X , ( X + 1 ) ) = X )
41 38 40 eqtrd 
 |-  ( ( ph /\ X < I ) -> if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) = X )
42 41 adantr 
 |-  ( ( ( ph /\ X < I ) /\ y = X ) -> if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) = X )
43 22 42 eqtrd 
 |-  ( ( ( ph /\ X < I ) /\ y = X ) -> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) = X )
44 6 adantr 
 |-  ( ( ph /\ X < I ) -> X e. ( 1 ... M ) )
45 15 43 44 44 fvmptd 
 |-  ( ( ph /\ X < I ) -> ( C ` X ) = X )
46 eqeq1 
 |-  ( ( C ` X ) = X -> ( ( C ` X ) = I <-> X = I ) )
47 46 ifbid 
 |-  ( ( C ` X ) = X -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = if ( X = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) )
48 45 47 syl 
 |-  ( ( ph /\ X < I ) -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = if ( X = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) )
49 26 31 ltned 
 |-  ( ( ph /\ X < I ) -> X =/= I )
50 49 neneqd 
 |-  ( ( ph /\ X < I ) -> -. X = I )
51 iffalse 
 |-  ( -. X = I -> if ( X = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) )
52 50 51 syl 
 |-  ( ( ph /\ X < I ) -> if ( X = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) )
53 45 eqcomd 
 |-  ( ( ph /\ X < I ) -> X = ( C ` X ) )
54 breq1 
 |-  ( X = ( C ` X ) -> ( X < I <-> ( C ` X ) < I ) )
55 id 
 |-  ( X = ( C ` X ) -> X = ( C ` X ) )
56 oveq1 
 |-  ( X = ( C ` X ) -> ( X - 1 ) = ( ( C ` X ) - 1 ) )
57 54 55 56 ifbieq12d 
 |-  ( X = ( C ` X ) -> if ( X < I , X , ( X - 1 ) ) = if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) )
58 53 57 syl 
 |-  ( ( ph /\ X < I ) -> if ( X < I , X , ( X - 1 ) ) = if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) )
59 58 eqcomd 
 |-  ( ( ph /\ X < I ) -> if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) = if ( X < I , X , ( X - 1 ) ) )
60 31 iftrued 
 |-  ( ( ph /\ X < I ) -> if ( X < I , X , ( X - 1 ) ) = X )
61 59 60 eqtrd 
 |-  ( ( ph /\ X < I ) -> if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) = X )
62 52 61 eqtrd 
 |-  ( ( ph /\ X < I ) -> if ( X = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = X )
63 48 62 eqtrd 
 |-  ( ( ph /\ X < I ) -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = X )
64 63 adantr 
 |-  ( ( ( ph /\ X < I ) /\ x = ( C ` X ) ) -> if ( ( C ` X ) = I , M , if ( ( C ` X ) < I , ( C ` X ) , ( ( C ` X ) - 1 ) ) ) = X )
65 14 64 eqtrd 
 |-  ( ( ( ph /\ X < I ) /\ x = ( C ` X ) ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = X )
66 1 2 3 5 metakunt2 
 |-  ( ph -> C : ( 1 ... M ) --> ( 1 ... M ) )
67 66 adantr 
 |-  ( ( ph /\ X < I ) -> C : ( 1 ... M ) --> ( 1 ... M ) )
68 67 44 ffvelrnd 
 |-  ( ( ph /\ X < I ) -> ( C ` X ) e. ( 1 ... M ) )
69 7 65 68 44 fvmptd 
 |-  ( ( ph /\ X < I ) -> ( A ` ( C ` X ) ) = X )