Metamath Proof Explorer

Theorem smndex1igid

Description: The composition of the modulo function I and a constant function ( GK ) results in ( GK ) itself. (Contributed by AV, 14-Feb-2024) Avoid ax-rep . (Revised by GG, 2-Apr-2026)

Ref Expression
Hypotheses smndex1ibas.m 
|- M = ( EndoFMnd ` NN0 )
smndex1ibas.n 
|- N e. NN
smndex1ibas.i 
|- I = ( x e. NN0 |-> ( x mod N ) )
smndex1ibas.g 
|- G = ( n e. ( 0 ..^ N ) |-> ( x e. NN0 |-> n ) )
Assertion smndex1igid 
|- ( K e. ( 0 ..^ N ) -> ( I o. ( G ` K ) ) = ( G ` K ) )

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 smndex1ibas.g 
 |-  G = ( n e. ( 0 ..^ N ) |-> ( x e. NN0 |-> n ) )
5 fconstmpt 
 |-  ( NN0 X. { K } ) = ( x e. NN0 |-> K )
6 5 eqcomi 
 |-  ( x e. NN0 |-> K ) = ( NN0 X. { K } )
7 6 a1i 
 |-  ( K e. ( 0 ..^ N ) -> ( x e. NN0 |-> K ) = ( NN0 X. { K } ) )
8 7 coeq2d 
 |-  ( K e. ( 0 ..^ N ) -> ( I o. ( x e. NN0 |-> K ) ) = ( I o. ( NN0 X. { K } ) ) )
9 id 
 |-  ( n = K -> n = K )
10 9 mpteq2dv 
 |-  ( n = K -> ( x e. NN0 |-> n ) = ( x e. NN0 |-> K ) )
11 nn0ex 
 |-  NN0 e. _V
12 snex 
 |-  { K } e. _V
13 11 12 xpex 
 |-  ( NN0 X. { K } ) e. _V
14 5 13 eqeltrri 
 |-  ( x e. NN0 |-> K ) e. _V
15 10 4 14 fvmpt 
 |-  ( K e. ( 0 ..^ N ) -> ( G ` K ) = ( x e. NN0 |-> K ) )
16 15 coeq2d 
 |-  ( K e. ( 0 ..^ N ) -> ( I o. ( G ` K ) ) = ( I o. ( x e. NN0 |-> K ) ) )
17 oveq1 
 |-  ( x = K -> ( x mod N ) = ( K mod N ) )
18 zmodidfzoimp 
 |-  ( K e. ( 0 ..^ N ) -> ( K mod N ) = K )
19 17 18 sylan9eqr 
 |-  ( ( K e. ( 0 ..^ N ) /\ x = K ) -> ( x mod N ) = K )
20 elfzonn0 
 |-  ( K e. ( 0 ..^ N ) -> K e. NN0 )
21 3 19 20 20 fvmptd2 
 |-  ( K e. ( 0 ..^ N ) -> ( I ` K ) = K )
22 21 eqcomd 
 |-  ( K e. ( 0 ..^ N ) -> K = ( I ` K ) )
23 22 sneqd 
 |-  ( K e. ( 0 ..^ N ) -> { K } = { ( I ` K ) } )
24 23 xpeq2d 
 |-  ( K e. ( 0 ..^ N ) -> ( NN0 X. { K } ) = ( NN0 X. { ( I ` K ) } ) )
25 15 5 eqtr4di 
 |-  ( K e. ( 0 ..^ N ) -> ( G ` K ) = ( NN0 X. { K } ) )
26 ovex 
 |-  ( x mod N ) e. _V
27 26 3 fnmpti 
 |-  I Fn NN0
28 fcoconst 
 |-  ( ( I Fn NN0 /\ K e. NN0 ) -> ( I o. ( NN0 X. { K } ) ) = ( NN0 X. { ( I ` K ) } ) )
29 27 20 28 sylancr 
 |-  ( K e. ( 0 ..^ N ) -> ( I o. ( NN0 X. { K } ) ) = ( NN0 X. { ( I ` K ) } ) )
30 24 25 29 3eqtr4d 
 |-  ( K e. ( 0 ..^ N ) -> ( G ` K ) = ( I o. ( NN0 X. { K } ) ) )
31 8 16 30 3eqtr4d 
 |-  ( K e. ( 0 ..^ N ) -> ( I o. ( G ` K ) ) = ( G ` K ) )