Metamath Proof Explorer


Theorem smndex1sgrp

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

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 smndex1mgm
 |-  S e. Mgm
8 eqid
 |-  ( Base ` S ) = ( Base ` S )
9 eqid
 |-  ( +g ` S ) = ( +g ` S )
10 8 9 mgmcl
 |-  ( ( S e. Mgm /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
11 7 10 mp3an1
 |-  ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) )
12 snex
 |-  { I } e. _V
13 ovex
 |-  ( 0 ..^ N ) e. _V
14 snex
 |-  { ( G ` n ) } e. _V
15 13 14 iunex
 |-  U_ n e. ( 0 ..^ N ) { ( G ` n ) } e. _V
16 12 15 unex
 |-  ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) e. _V
17 5 16 eqeltri
 |-  B e. _V
18 eqid
 |-  ( +g ` M ) = ( +g ` M )
19 6 18 ressplusg
 |-  ( B e. _V -> ( +g ` M ) = ( +g ` S ) )
20 17 19 ax-mp
 |-  ( +g ` M ) = ( +g ` S )
21 20 eqcomi
 |-  ( +g ` S ) = ( +g ` M )
22 21 oveqi
 |-  ( x ( +g ` S ) y ) = ( x ( +g ` M ) y )
23 1 2 3 4 5 6 smndex1bas
 |-  ( Base ` S ) = B
24 1 2 3 4 5 smndex1basss
 |-  B C_ ( Base ` M )
25 23 24 eqsstri
 |-  ( Base ` S ) C_ ( Base ` M )
26 ssel
 |-  ( ( Base ` S ) C_ ( Base ` M ) -> ( x e. ( Base ` S ) -> x e. ( Base ` M ) ) )
27 ssel
 |-  ( ( Base ` S ) C_ ( Base ` M ) -> ( y e. ( Base ` S ) -> y e. ( Base ` M ) ) )
28 26 27 anim12d
 |-  ( ( Base ` S ) C_ ( Base ` M ) -> ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) )
29 25 28 ax-mp
 |-  ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) )
30 eqid
 |-  ( Base ` M ) = ( Base ` M )
31 1 30 18 efmndov
 |-  ( ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) -> ( x ( +g ` M ) y ) = ( x o. y ) )
32 29 31 syl
 |-  ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` M ) y ) = ( x o. y ) )
33 22 32 syl5eq
 |-  ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` S ) y ) = ( x o. y ) )
34 11 33 symggrplem
 |-  ( ( a e. ( Base ` S ) /\ b e. ( Base ` S ) /\ c e. ( Base ` S ) ) -> ( ( a ( +g ` S ) b ) ( +g ` S ) c ) = ( a ( +g ` S ) ( b ( +g ` S ) c ) ) )
35 34 rgen3
 |-  A. a e. ( Base ` S ) A. b e. ( Base ` S ) A. c e. ( Base ` S ) ( ( a ( +g ` S ) b ) ( +g ` S ) c ) = ( a ( +g ` S ) ( b ( +g ` S ) c ) )
36 8 9 issgrp
 |-  ( S e. Smgrp <-> ( S e. Mgm /\ A. a e. ( Base ` S ) A. b e. ( Base ` S ) A. c e. ( Base ` S ) ( ( a ( +g ` S ) b ) ( +g ` S ) c ) = ( a ( +g ` S ) ( b ( +g ` S ) c ) ) ) )
37 7 35 36 mpbir2an
 |-  S e. Smgrp