Metamath Proof Explorer

Theorem smndex1id

Description: The modulo function I is the identity of the monoid of endofunctions on NN0 restricted to the modulo function I and the constant functions ( GK ) . (Contributed by AV, 16-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 ) )
smndex1mgm.b 
|- B = ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
smndex1mgm.s 
|- S = ( M |`s B )
Assertion smndex1id 
|- I = ( 0g ` S )

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 smndex1mgm.b 
 |-  B = ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
6 smndex1mgm.s 
 |-  S = ( M |`s B )
7 nn0ex 
 |-  NN0 e. _V
8 7 mptex 
 |-  ( x e. NN0 |-> ( x mod N ) ) e. _V
9 3 8 eqeltri 
 |-  I e. _V
10 9 snid 
 |-  I e. { I }
11 elun1 
 |-  ( I e. { I } -> I e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) )
12 10 11 ax-mp 
 |-  I e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
13 12 5 eleqtrri 
 |-  I e. B
14 1 2 3 4 5 6 smndex1bas 
 |-  ( Base ` S ) = B
15 14 eqcomi 
 |-  B = ( Base ` S )
16 15 a1i 
 |-  ( I e. B -> B = ( Base ` S ) )
17 snex 
 |-  { I } e. _V
18 ovex 
 |-  ( 0 ..^ N ) e. _V
19 snex 
 |-  { ( G ` n ) } e. _V
20 18 19 iunex 
 |-  U_ n e. ( 0 ..^ N ) { ( G ` n ) } e. _V
21 17 20 unex 
 |-  ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) e. _V
22 5 21 eqeltri 
 |-  B e. _V
23 eqid 
 |-  ( +g ` M ) = ( +g ` M )
24 6 23 ressplusg 
 |-  ( B e. _V -> ( +g ` M ) = ( +g ` S ) )
25 22 24 mp1i 
 |-  ( I e. B -> ( +g ` M ) = ( +g ` S ) )
26 id 
 |-  ( I e. B -> I e. B )
27 1 2 3 smndex1ibas 
 |-  I e. ( Base ` M )
28 27 a1i 
 |-  ( I e. B -> I e. ( Base ` M ) )
29 1 2 3 4 5 smndex1basss 
 |-  B C_ ( Base ` M )
30 29 sseli 
 |-  ( a e. B -> a e. ( Base ` M ) )
31 eqid 
 |-  ( Base ` M ) = ( Base ` M )
32 1 31 23 efmndov 
 |-  ( ( I e. ( Base ` M ) /\ a e. ( Base ` M ) ) -> ( I ( +g ` M ) a ) = ( I o. a ) )
33 28 30 32 syl2an 
 |-  ( ( I e. B /\ a e. B ) -> ( I ( +g ` M ) a ) = ( I o. a ) )
34 1 2 3 4 5 6 smndex1mndlem 
 |-  ( a e. B -> ( ( I o. a ) = a /\ ( a o. I ) = a ) )
35 34 simpld 
 |-  ( a e. B -> ( I o. a ) = a )
36 35 adantl 
 |-  ( ( I e. B /\ a e. B ) -> ( I o. a ) = a )
37 33 36 eqtrd 
 |-  ( ( I e. B /\ a e. B ) -> ( I ( +g ` M ) a ) = a )
38 1 31 23 efmndov 
 |-  ( ( a e. ( Base ` M ) /\ I e. ( Base ` M ) ) -> ( a ( +g ` M ) I ) = ( a o. I ) )
39 30 28 38 syl2anr 
 |-  ( ( I e. B /\ a e. B ) -> ( a ( +g ` M ) I ) = ( a o. I ) )
40 34 simprd 
 |-  ( a e. B -> ( a o. I ) = a )
41 40 adantl 
 |-  ( ( I e. B /\ a e. B ) -> ( a o. I ) = a )
42 39 41 eqtrd 
 |-  ( ( I e. B /\ a e. B ) -> ( a ( +g ` M ) I ) = a )
43 16 25 26 37 42 grpidd 
 |-  ( I e. B -> I = ( 0g ` S ) )
44 13 43 ax-mp 
 |-  I = ( 0g ` S )