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