Theorem metakunt9

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt9.1	|- ( ph -> M e. NN )
2		metakunt9.2	|- ( ph -> I e. NN )
3		metakunt9.3	|- ( ph -> I <_ M )
4		metakunt9.4	|- A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
5		metakunt9.5	|- C = ( y e. ( 1 ... M ) |-> if ( y = M , I , if ( y < I , y , ( y + 1 ) ) ) )
6		metakunt9.6	|- ( ph -> X e. ( 1 ... M ) )
7	1 2 3 4 5 6	metakunt8	|- ( ( ph /\ I < X ) -> ( C ` ( A ` X ) ) = X )
8		elfznn	|- ( X e. ( 1 ... M ) -> X e. NN )
9	6 8	syl	|- ( ph -> X e. NN )
10	9	nnred	|- ( ph -> X e. RR )
11	2	nnred	|- ( ph -> I e. RR )
12	10 11	leloed	|- ( ph -> ( X <_ I <-> ( X < I \/ X = I ) ) )
13	1 2 3 4 5 6	metakunt6	|- ( ( ph /\ X < I ) -> ( C ` ( A ` X ) ) = X )
14	1 2 3 4 5 6	metakunt5	|- ( ( ph /\ X = I ) -> ( C ` ( A ` X ) ) = X )
15	13 14	jaodan	|- ( ( ph /\ ( X < I \/ X = I ) ) -> ( C ` ( A ` X ) ) = X )
16	15	ex	|- ( ph -> ( ( X < I \/ X = I ) -> ( C ` ( A ` X ) ) = X ) )
17	12 16	sylbid	|- ( ph -> ( X <_ I -> ( C ` ( A ` X ) ) = X ) )
18	17	imp	|- ( ( ph /\ X <_ I ) -> ( C ` ( A ` X ) ) = X )
19	7 18 11 10	ltlecasei	|- ( ph -> ( C ` ( A ` X ) ) = X )