Metamath Proof Explorer


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