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 No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
smndex1ibas.n N
smndex1ibas.i I = x 0 x mod N
smndex1ibas.g G = n 0 ..^ N x 0 n
smndex1mgm.b B = I n 0 ..^ N G n
smndex1mgm.s S = M 𝑠 B
Assertion smndex1sgrp Could not format assertion : No typesetting found for |- S e. Smgrp with typecode |-

Proof

Step Hyp Ref Expression
1 smndex1ibas.m Could not format M = ( EndoFMnd ` NN0 ) : No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
2 smndex1ibas.n N
3 smndex1ibas.i I = x 0 x mod N
4 smndex1ibas.g G = n 0 ..^ N x 0 n
5 smndex1mgm.b B = I n 0 ..^ N G n
6 smndex1mgm.s S = M 𝑠 B
7 1 2 3 4 5 6 smndex1mgm S Mgm
8 eqid Base S = Base S
9 eqid + S = + S
10 8 9 mgmcl S Mgm x Base S y Base S x + S y Base S
11 7 10 mp3an1 x Base S y Base S x + S y Base S
12 snex I V
13 ovex 0 ..^ N V
14 snex G n V
15 13 14 iunex n 0 ..^ N G n V
16 12 15 unex I n 0 ..^ N G n V
17 5 16 eqeltri B V
18 eqid + M = + M
19 6 18 ressplusg B V + M = + S
20 17 19 ax-mp + M = + S
21 20 eqcomi + S = + M
22 21 oveqi x + S y = x + M y
23 1 2 3 4 5 6 smndex1bas Base S = B
24 1 2 3 4 5 smndex1basss B Base M
25 23 24 eqsstri Base S Base M
26 ssel Base S Base M x Base S x Base M
27 ssel Base S Base M y Base S y Base M
28 26 27 anim12d Base S Base M x Base S y Base S x Base M y Base M
29 25 28 ax-mp x Base S y Base S x Base M y Base M
30 eqid Base M = Base M
31 1 30 18 efmndov x Base M y Base M x + M y = x y
32 29 31 syl x Base S y Base S x + M y = x y
33 22 32 syl5eq x Base S y Base S x + S y = x y
34 11 33 symggrplem a Base S b Base S c Base S a + S b + S c = a + S b + S c
35 34 rgen3 a Base S b Base S c Base S a + S b + S c = a + S b + S c
36 8 9 issgrp Could not format ( 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 ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) with typecode |-
37 7 35 36 mpbir2an Could not format S e. Smgrp : No typesetting found for |- S e. Smgrp with typecode |-