Theorem smndex1iidm

Description: The modulo function I is idempotent. (Contributed by AV, 12-Feb-2024)

	Ref	Expression
Hypotheses	smndex1ibas.m	|- M = ( EndoFMnd ` NN0 )
	smndex1ibas.n	|- N e. NN
	smndex1ibas.i	|- I = ( x e. NN0 |-> ( x mod N ) )
Assertion	smndex1iidm	|- ( I o. I ) = I

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	|- M = ( EndoFMnd ` NN0 )
2		smndex1ibas.n	|- N e. NN
3		smndex1ibas.i	|- I = ( x e. NN0 |-> ( x mod N ) )
4		nn0re	|- ( y e. NN0 -> y e. RR )
5		nnrp	|- ( N e. NN -> N e. RR+ )
6	2 5	ax-mp	|- N e. RR+
7		modabs2	|- ( ( y e. RR /\ N e. RR+ ) -> ( ( y mod N ) mod N ) = ( y mod N ) )
8	4 6 7	sylancl	|- ( y e. NN0 -> ( ( y mod N ) mod N ) = ( y mod N ) )
9	8	eqcomd	|- ( y e. NN0 -> ( y mod N ) = ( ( y mod N ) mod N ) )
10	9	mpteq2ia	|- ( y e. NN0 |-> ( y mod N ) ) = ( y e. NN0 |-> ( ( y mod N ) mod N ) )
11		oveq1	|- ( x = y -> ( x mod N ) = ( y mod N ) )
12	11	cbvmptv	|- ( x e. NN0 |-> ( x mod N ) ) = ( y e. NN0 |-> ( y mod N ) )
13	3 12	eqtri	|- I = ( y e. NN0 |-> ( y mod N ) )
14		nn0z	|- ( y e. NN0 -> y e. ZZ )
15	14	anim2i	|- ( ( N e. NN /\ y e. NN0 ) -> ( N e. NN /\ y e. ZZ ) )
16	15	ancomd	|- ( ( N e. NN /\ y e. NN0 ) -> ( y e. ZZ /\ N e. NN ) )
17		zmodcl	|- ( ( y e. ZZ /\ N e. NN ) -> ( y mod N ) e. NN0 )
18	16 17	syl	|- ( ( N e. NN /\ y e. NN0 ) -> ( y mod N ) e. NN0 )
19	13	a1i	|- ( N e. NN -> I = ( y e. NN0 |-> ( y mod N ) ) )
20	3	a1i	|- ( N e. NN -> I = ( x e. NN0 |-> ( x mod N ) ) )
21		oveq1	|- ( x = ( y mod N ) -> ( x mod N ) = ( ( y mod N ) mod N ) )
22	18 19 20 21	fmptco	|- ( N e. NN -> ( I o. I ) = ( y e. NN0 |-> ( ( y mod N ) mod N ) ) )
23	2 22	ax-mp	|- ( I o. I ) = ( y e. NN0 |-> ( ( y mod N ) mod N ) )
24	10 13 23	3eqtr4ri	|- ( I o. I ) = I