Metamath Proof Explorer

Theorem metakunt6

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

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

Proof

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