Metamath Proof Explorer

Theorem smndex1mnd

Description: The monoid of endofunctions on NN0 restricted to the modulo function I and the constant functions ( GK ) is a monoid. (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 smndex1mnd 
|- S e. Mnd

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 1 2 3 4 5 6 smndex1sgrp 
 |-  S e. Smgrp
8 nn0ex 
 |-  NN0 e. _V
9 8 mptex 
 |-  ( x e. NN0 |-> ( x mod N ) ) e. _V
10 3 9 eqeltri 
 |-  I e. _V
11 10 snid 
 |-  I e. { I }
12 elun1 
 |-  ( I e. { I } -> I e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) )
13 11 12 ax-mp 
 |-  I e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
14 13 5 eleqtrri 
 |-  I e. B
15 id 
 |-  ( I e. B -> I e. B )
16 coeq1 
 |-  ( a = I -> ( a o. b ) = ( I o. b ) )
17 16 eqeq1d 
 |-  ( a = I -> ( ( a o. b ) = b <-> ( I o. b ) = b ) )
18 coeq2 
 |-  ( a = I -> ( b o. a ) = ( b o. I ) )
19 18 eqeq1d 
 |-  ( a = I -> ( ( b o. a ) = b <-> ( b o. I ) = b ) )
20 17 19 anbi12d 
 |-  ( a = I -> ( ( ( a o. b ) = b /\ ( b o. a ) = b ) <-> ( ( I o. b ) = b /\ ( b o. I ) = b ) ) )
21 20 ralbidv 
 |-  ( a = I -> ( A. b e. B ( ( a o. b ) = b /\ ( b o. a ) = b ) <-> A. b e. B ( ( I o. b ) = b /\ ( b o. I ) = b ) ) )
22 21 adantl 
 |-  ( ( I e. B /\ a = I ) -> ( A. b e. B ( ( a o. b ) = b /\ ( b o. a ) = b ) <-> A. b e. B ( ( I o. b ) = b /\ ( b o. I ) = b ) ) )
23 1 2 3 4 5 6 smndex1mndlem 
 |-  ( b e. B -> ( ( I o. b ) = b /\ ( b o. I ) = b ) )
24 23 rgen 
 |-  A. b e. B ( ( I o. b ) = b /\ ( b o. I ) = b )
25 24 a1i 
 |-  ( I e. B -> A. b e. B ( ( I o. b ) = b /\ ( b o. I ) = b ) )
26 15 22 25 rspcedvd 
 |-  ( I e. B -> E. a e. B A. b e. B ( ( a o. b ) = b /\ ( b o. a ) = b ) )
27 14 26 ax-mp 
 |-  E. a e. B A. b e. B ( ( a o. b ) = b /\ ( b o. a ) = b )
28 1 2 3 4 5 smndex1basss 
 |-  B C_ ( Base ` M )
29 ssel 
 |-  ( B C_ ( Base ` M ) -> ( a e. B -> a e. ( Base ` M ) ) )
30 ssel 
 |-  ( B C_ ( Base ` M ) -> ( b e. B -> b e. ( Base ` M ) ) )
31 29 30 anim12d 
 |-  ( B C_ ( Base ` M ) -> ( ( a e. B /\ b e. B ) -> ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) ) )
32 28 31 ax-mp 
 |-  ( ( a e. B /\ b e. B ) -> ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) )
33 eqid 
 |-  ( Base ` M ) = ( Base ` M )
34 snex 
 |-  { I } e. _V
35 ovex 
 |-  ( 0 ..^ N ) e. _V
36 snex 
 |-  { ( G ` n ) } e. _V
37 35 36 iunex 
 |-  U_ n e. ( 0 ..^ N ) { ( G ` n ) } e. _V
38 34 37 unex 
 |-  ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) e. _V
39 5 38 eqeltri 
 |-  B e. _V
40 eqid 
 |-  ( +g ` M ) = ( +g ` M )
41 6 40 ressplusg 
 |-  ( B e. _V -> ( +g ` M ) = ( +g ` S ) )
42 39 41 ax-mp 
 |-  ( +g ` M ) = ( +g ` S )
43 42 eqcomi 
 |-  ( +g ` S ) = ( +g ` M )
44 1 33 43 efmndov 
 |-  ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( a ( +g ` S ) b ) = ( a o. b ) )
45 44 eqeq1d 
 |-  ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( ( a ( +g ` S ) b ) = b <-> ( a o. b ) = b ) )
46 43 oveqi 
 |-  ( b ( +g ` S ) a ) = ( b ( +g ` M ) a )
47 1 33 40 efmndov 
 |-  ( ( b e. ( Base ` M ) /\ a e. ( Base ` M ) ) -> ( b ( +g ` M ) a ) = ( b o. a ) )
48 47 ancoms 
 |-  ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( b ( +g ` M ) a ) = ( b o. a ) )
49 46 48 syl5eq 
 |-  ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( b ( +g ` S ) a ) = ( b o. a ) )
50 49 eqeq1d 
 |-  ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( ( b ( +g ` S ) a ) = b <-> ( b o. a ) = b ) )
51 45 50 anbi12d 
 |-  ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b ) <-> ( ( a o. b ) = b /\ ( b o. a ) = b ) ) )
52 32 51 syl 
 |-  ( ( a e. B /\ b e. B ) -> ( ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b ) <-> ( ( a o. b ) = b /\ ( b o. a ) = b ) ) )
53 52 ralbidva 
 |-  ( a e. B -> ( A. b e. B ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b ) <-> A. b e. B ( ( a o. b ) = b /\ ( b o. a ) = b ) ) )
54 53 rexbiia 
 |-  ( E. a e. B A. b e. B ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b ) <-> E. a e. B A. b e. B ( ( a o. b ) = b /\ ( b o. a ) = b ) )
55 27 54 mpbir 
 |-  E. a e. B A. b e. B ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b )
56 1 2 3 4 5 6 smndex1bas 
 |-  ( Base ` S ) = B
57 56 eqcomi 
 |-  B = ( Base ` S )
58 eqid 
 |-  ( +g ` S ) = ( +g ` S )
59 57 58 ismnddef 
 |-  ( S e. Mnd <-> ( S e. Smgrp /\ E. a e. B A. b e. B ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b ) ) )
60 7 55 59 mpbir2an 
 |-  S e. Mnd