Theorem metakunt13

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt13.1	|- ( ph -> M e. NN )
2		metakunt13.2	|- ( ph -> I e. NN )
3		metakunt13.3	|- ( ph -> I <_ M )
4		metakunt13.4	|- A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
5		metakunt13.5	|- C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
6		metakunt13.6	|- ( ph -> X e. ( 1 ... M ) )
7	1 2 3 4 5 6	metakunt10	|- ( ( ph /\ X = M ) -> ( A ` ( C ` X ) ) = X )
8	7	ex	|- ( ph -> ( X = M -> ( A ` ( C ` X ) ) = X ) )
9	1 2 3 4 5 6	metakunt11	|- ( ( ph /\ X < I ) -> ( A ` ( C ` X ) ) = X )
10	9	ex	|- ( ph -> ( X < I -> ( A ` ( C ` X ) ) = X ) )
11	1 2 3 4 5 6	metakunt12	|- ( ( ph /\ -. ( X = M \/ X < I ) ) -> ( A ` ( C ` X ) ) = X )
12	11	ex	|- ( ph -> ( -. ( X = M \/ X < I ) -> ( A ` ( C ` X ) ) = X ) )
13	8 10 12	ecase3d	|- ( ph -> ( A ` ( C ` X ) ) = X )