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=\mathrm{EndoFMnd}\left({\mathbb{N}}_0\right)$$
	smndex1ibas.n	$$⊢N\in \mathbb{N}$$
	smndex1ibas.i	$$⊢I=\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)$$
	smndex1ibas.g	$$⊢G=\left(n\in \left(0..^N\right)⟼\left(x\in {\mathbb{N}}_0⟼n\right)\right)$$
	smndex1mgm.b	$$⊢B=\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}$$
	smndex1mgm.s	$$⊢S=M{\upharpoonright }_{𝑠}B$$
Assertion	smndex1sgrp	$$⊢S\in \mathrm{Smgrp}$$

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	$$⊢M=\mathrm{EndoFMnd}\left({\mathbb{N}}_0\right)$$
2		smndex1ibas.n	$$⊢N\in \mathbb{N}$$
3		smndex1ibas.i	$$⊢I=\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)$$
4		smndex1ibas.g	$$⊢G=\left(n\in \left(0..^N\right)⟼\left(x\in {\mathbb{N}}_0⟼n\right)\right)$$
5		smndex1mgm.b	$$⊢B=\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}$$
6		smndex1mgm.s	$$⊢S=M{\upharpoonright }_{𝑠}B$$
7	1 2 3 4 5 6	smndex1mgm	$$⊢S\in \mathrm{Mgm}$$
8		eqid	$$⊢{\mathrm{Base}}_S={\mathrm{Base}}_S$$
9		eqid	$$⊢{+}_S={+}_S$$
10	8 9	mgmcl	$$⊢\left(S\in \mathrm{Mgm}\wedge x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to x{+}_{S}y\in {\mathrm{Base}}_S$$
11	7 10	mp3an1	$$⊢\left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to x{+}_{S}y\in {\mathrm{Base}}_S$$
12		snex	$$⊢\left\{I\right\}\in \mathrm{V}$$
13		ovex	$$⊢\left(0..^N\right)\in \mathrm{V}$$
14		snex	$$⊢\left\{G\left(n\right)\right\}\in \mathrm{V}$$
15	13 14	iunex	$$⊢\bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\in \mathrm{V}$$
16	12 15	unex	$$⊢\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\in \mathrm{V}$$
17	5 16	eqeltri	$$⊢B\in \mathrm{V}$$
18		eqid	$$⊢{+}_M={+}_M$$
19	6 18	ressplusg	$$⊢B\in \mathrm{V}\to {+}_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	$$⊢{\mathrm{Base}}_S=B$$
24	1 2 3 4 5	smndex1basss	$$⊢B\subseteq {\mathrm{Base}}_M$$
25	23 24	eqsstri	$$⊢{\mathrm{Base}}_S\subseteq {\mathrm{Base}}_M$$
26		ssel	$$⊢{\mathrm{Base}}_S\subseteq {\mathrm{Base}}_M\to \left(x\in {\mathrm{Base}}_S\to x\in {\mathrm{Base}}_M\right)$$
27		ssel	$$⊢{\mathrm{Base}}_S\subseteq {\mathrm{Base}}_M\to \left(y\in {\mathrm{Base}}_S\to y\in {\mathrm{Base}}_M\right)$$
28	26 27	anim12d	$$⊢{\mathrm{Base}}_S\subseteq {\mathrm{Base}}_M\to \left(\left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to \left(x\in {\mathrm{Base}}_M\wedge y\in {\mathrm{Base}}_M\right)\right)$$
29	25 28	ax-mp	$$⊢\left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to \left(x\in {\mathrm{Base}}_M\wedge y\in {\mathrm{Base}}_M\right)$$
30		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
31	1 30 18	efmndov	$$⊢\left(x\in {\mathrm{Base}}_M\wedge y\in {\mathrm{Base}}_M\right)\to x{+}_{M}y=x\circ y$$
32	29 31	syl	$$⊢\left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to x{+}_{M}y=x\circ y$$
33	22 32	eqtrid	$$⊢\left(x\in {\mathrm{Base}}_S\wedge y\in {\mathrm{Base}}_S\right)\to x{+}_{S}y=x\circ y$$
34	11 33	symggrplem	$$⊢\left(a\in {\mathrm{Base}}_S\wedge b\in {\mathrm{Base}}_S\wedge c\in {\mathrm{Base}}_S\right)\to \left(a{+}_{S}b\right){+}_{S}c=a{+}_S\left(b{+}_{S}c\right)$$
35	34	rgen3	$$⊢\forall a\in {\mathrm{Base}}_S\forall b\in {\mathrm{Base}}_S\forall c\in {\mathrm{Base}}_S\left(a{+}_{S}b\right){+}_{S}c=a{+}_S\left(b{+}_{S}c\right)$$
36	8 9	issgrp	$$⊢S\in \mathrm{Smgrp}\leftrightarrow \left(S\in \mathrm{Mgm}\wedge \forall a\in {\mathrm{Base}}_S\forall b\in {\mathrm{Base}}_S\forall c\in {\mathrm{Base}}_S\left(a{+}_{S}b\right){+}_{S}c=a{+}_S\left(b{+}_{S}c\right)\right)$$
37	7 35 36	mpbir2an	$$⊢S\in \mathrm{Smgrp}$$