This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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)

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