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	No typesetting found for |- M = ( EndoFMnd ` NN0 ) with typecode |-
	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	smndex1mnd	$$⊢S\in \mathrm{Mnd}$$

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\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	smndex1sgrp	Could not format S e. Smgrp : No typesetting found for |- S e. Smgrp with typecode |-
8		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
9	8	mptex	$$⊢\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)\in \mathrm{V}$$
10	3 9	eqeltri	$$⊢I\in \mathrm{V}$$
11	10	snid	$$⊢I\in \left\{I\right\}$$
12		elun1	$$⊢I\in \left\{I\right\}\to I\in \left(\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)$$
13	11 12	ax-mp	$$⊢I\in \left(\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)$$
14	13 5	eleqtrri	$$⊢I\in B$$
15		id	$$⊢I\in B\to I\in B$$
16		coeq1	$$⊢a=I\to a\circ b=I\circ b$$
17	16	eqeq1d	$$⊢a=I\to \left(a\circ b=b\leftrightarrow I\circ b=b\right)$$
18		coeq2	$$⊢a=I\to b\circ a=b\circ I$$
19	18	eqeq1d	$$⊢a=I\to \left(b\circ a=b\leftrightarrow b\circ I=b\right)$$
20	17 19	anbi12d	$$⊢a=I\to \left(\left(a\circ b=b\wedge b\circ a=b\right)\leftrightarrow \left(I\circ b=b\wedge b\circ I=b\right)\right)$$
21	20	ralbidv	$$⊢a=I\to \left(\forall b\in B\left(a\circ b=b\wedge b\circ a=b\right)\leftrightarrow \forall b\in B\left(I\circ b=b\wedge b\circ I=b\right)\right)$$
22	21	adantl	$$⊢\left(I\in B\wedge a=I\right)\to \left(\forall b\in B\left(a\circ b=b\wedge b\circ a=b\right)\leftrightarrow \forall b\in B\left(I\circ b=b\wedge b\circ I=b\right)\right)$$
23	1 2 3 4 5 6	smndex1mndlem	$$⊢b\in B\to \left(I\circ b=b\wedge b\circ I=b\right)$$
24	23	rgen	$$⊢\forall b\in B\left(I\circ b=b\wedge b\circ I=b\right)$$
25	24	a1i	$$⊢I\in B\to \forall b\in B\left(I\circ b=b\wedge b\circ I=b\right)$$
26	15 22 25	rspcedvd	$$⊢I\in B\to \exists a\in B\forall b\in B\left(a\circ b=b\wedge b\circ a=b\right)$$
27	14 26	ax-mp	$$⊢\exists a\in B\forall b\in B\left(a\circ b=b\wedge b\circ a=b\right)$$
28	1 2 3 4 5	smndex1basss	$$⊢B\subseteq {\mathrm{Base}}_M$$
29		ssel	$$⊢B\subseteq {\mathrm{Base}}_M\to \left(a\in B\to a\in {\mathrm{Base}}_M\right)$$
30		ssel	$$⊢B\subseteq {\mathrm{Base}}_M\to \left(b\in B\to b\in {\mathrm{Base}}_M\right)$$
31	29 30	anim12d	$$⊢B\subseteq {\mathrm{Base}}_M\to \left(\left(a\in B\wedge b\in B\right)\to \left(a\in {\mathrm{Base}}_M\wedge b\in {\mathrm{Base}}_M\right)\right)$$
32	28 31	ax-mp	$$⊢\left(a\in B\wedge b\in B\right)\to \left(a\in {\mathrm{Base}}_M\wedge b\in {\mathrm{Base}}_M\right)$$
33		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
34		snex	$$⊢\left\{I\right\}\in \mathrm{V}$$
35		ovex	$$⊢\left(0..^N\right)\in \mathrm{V}$$
36		snex	$$⊢\left\{G\left(n\right)\right\}\in \mathrm{V}$$
37	35 36	iunex	$$⊢\bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\in \mathrm{V}$$
38	34 37	unex	$$⊢\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\in \mathrm{V}$$
39	5 38	eqeltri	$$⊢B\in \mathrm{V}$$
40		eqid	$$⊢{+}_M={+}_M$$
41	6 40	ressplusg	$$⊢B\in \mathrm{V}\to {+}_M={+}_S$$
42	39 41	ax-mp	$$⊢{+}_M={+}_S$$
43	42	eqcomi	$$⊢{+}_S={+}_M$$
44	1 33 43	efmndov	$$⊢\left(a\in {\mathrm{Base}}_M\wedge b\in {\mathrm{Base}}_M\right)\to a{+}_{S}b=a\circ b$$
45	44	eqeq1d	$$⊢\left(a\in {\mathrm{Base}}_M\wedge b\in {\mathrm{Base}}_M\right)\to \left(a{+}_{S}b=b\leftrightarrow a\circ b=b\right)$$
46	43	oveqi	$$⊢b{+}_{S}a=b{+}_{M}a$$
47	1 33 40	efmndov	$$⊢\left(b\in {\mathrm{Base}}_M\wedge a\in {\mathrm{Base}}_M\right)\to b{+}_{M}a=b\circ a$$
48	47	ancoms	$$⊢\left(a\in {\mathrm{Base}}_M\wedge b\in {\mathrm{Base}}_M\right)\to b{+}_{M}a=b\circ a$$
49	46 48	eqtrid	$$⊢\left(a\in {\mathrm{Base}}_M\wedge b\in {\mathrm{Base}}_M\right)\to b{+}_{S}a=b\circ a$$
50	49	eqeq1d	$$⊢\left(a\in {\mathrm{Base}}_M\wedge b\in {\mathrm{Base}}_M\right)\to \left(b{+}_{S}a=b\leftrightarrow b\circ a=b\right)$$
51	45 50	anbi12d	$$⊢\left(a\in {\mathrm{Base}}_M\wedge b\in {\mathrm{Base}}_M\right)\to \left(\left(a{+}_{S}b=b\wedge b{+}_{S}a=b\right)\leftrightarrow \left(a\circ b=b\wedge b\circ a=b\right)\right)$$
52	32 51	syl	$$⊢\left(a\in B\wedge b\in B\right)\to \left(\left(a{+}_{S}b=b\wedge b{+}_{S}a=b\right)\leftrightarrow \left(a\circ b=b\wedge b\circ a=b\right)\right)$$
53	52	ralbidva	$$⊢a\in B\to \left(\forall b\in B\left(a{+}_{S}b=b\wedge b{+}_{S}a=b\right)\leftrightarrow \forall b\in B\left(a\circ b=b\wedge b\circ a=b\right)\right)$$
54	53	rexbiia	$$⊢\exists a\in B\forall b\in B\left(a{+}_{S}b=b\wedge b{+}_{S}a=b\right)\leftrightarrow \exists a\in B\forall b\in B\left(a\circ b=b\wedge b\circ a=b\right)$$
55	27 54	mpbir	$$⊢\exists a\in B\forall b\in B\left(a{+}_{S}b=b\wedge b{+}_{S}a=b\right)$$
56	1 2 3 4 5 6	smndex1bas	$$⊢{\mathrm{Base}}_S=B$$
57	56	eqcomi	$$⊢B={\mathrm{Base}}_S$$
58		eqid	$$⊢{+}_S={+}_S$$
59	57 58	ismnddef	Could not format ( S e. Mnd <-> ( S e. Smgrp /\ E. a e. B A. b e. B ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b ) ) ) : No typesetting found for |- ( S e. Mnd <-> ( S e. Smgrp /\ E. a e. B A. b e. B ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b ) ) ) with typecode |-
60	7 55 59	mpbir2an	$$⊢S\in \mathrm{Mnd}$$