Theorem smndex1id

Description: The modulo function I is the identity of the monoid of endofunctions on NN0 restricted to the modulo function I and the constant functions ( GK ) . (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	smndex1id	$$⊢I=0_S$$

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		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
8	7	mptex	$$⊢\left(x\in {\mathbb{N}}_0⟼x\mathrm{mod}N\right)\in \mathrm{V}$$
9	3 8	eqeltri	$$⊢I\in \mathrm{V}$$
10	9	snid	$$⊢I\in \left\{I\right\}$$
11		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)$$
12	10 11	ax-mp	$$⊢I\in \left(\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\right)$$
13	12 5	eleqtrri	$$⊢I\in B$$
14	1 2 3 4 5 6	smndex1bas	$$⊢{\mathrm{Base}}_S=B$$
15	14	eqcomi	$$⊢B={\mathrm{Base}}_S$$
16	15	a1i	$$⊢I\in B\to B={\mathrm{Base}}_S$$
17		snex	$$⊢\left\{I\right\}\in \mathrm{V}$$
18		ovex	$$⊢\left(0..^N\right)\in \mathrm{V}$$
19		snex	$$⊢\left\{G\left(n\right)\right\}\in \mathrm{V}$$
20	18 19	iunex	$$⊢\bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\in \mathrm{V}$$
21	17 20	unex	$$⊢\left\{I\right\}\cup \bigcup _{n\in \left(0..^N\right)}\left\{G\left(n\right)\right\}\in \mathrm{V}$$
22	5 21	eqeltri	$$⊢B\in \mathrm{V}$$
23		eqid	$$⊢{+}_M={+}_M$$
24	6 23	ressplusg	$$⊢B\in \mathrm{V}\to {+}_M={+}_S$$
25	22 24	mp1i	$$⊢I\in B\to {+}_M={+}_S$$
26		id	$$⊢I\in B\to I\in B$$
27	1 2 3	smndex1ibas	$$⊢I\in {\mathrm{Base}}_M$$
28	27	a1i	$$⊢I\in B\to I\in {\mathrm{Base}}_M$$
29	1 2 3 4 5	smndex1basss	$$⊢B\subseteq {\mathrm{Base}}_M$$
30	29	sseli	$$⊢a\in B\to a\in {\mathrm{Base}}_M$$
31		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
32	1 31 23	efmndov	$$⊢\left(I\in {\mathrm{Base}}_M\wedge a\in {\mathrm{Base}}_M\right)\to I{+}_{M}a=I\circ a$$
33	28 30 32	syl2an	$$⊢\left(I\in B\wedge a\in B\right)\to I{+}_{M}a=I\circ a$$
34	1 2 3 4 5 6	smndex1mndlem	$$⊢a\in B\to \left(I\circ a=a\wedge a\circ I=a\right)$$
35	34	simpld	$$⊢a\in B\to I\circ a=a$$
36	35	adantl	$$⊢\left(I\in B\wedge a\in B\right)\to I\circ a=a$$
37	33 36	eqtrd	$$⊢\left(I\in B\wedge a\in B\right)\to I{+}_{M}a=a$$
38	1 31 23	efmndov	$$⊢\left(a\in {\mathrm{Base}}_M\wedge I\in {\mathrm{Base}}_M\right)\to a{+}_{M}I=a\circ I$$
39	30 28 38	syl2anr	$$⊢\left(I\in B\wedge a\in B\right)\to a{+}_{M}I=a\circ I$$
40	34	simprd	$$⊢a\in B\to a\circ I=a$$
41	40	adantl	$$⊢\left(I\in B\wedge a\in B\right)\to a\circ I=a$$
42	39 41	eqtrd	$$⊢\left(I\in B\wedge a\in B\right)\to a{+}_{M}I=a$$
43	16 25 26 37 42	grpidd	$$⊢I\in B\to I=0_S$$
44	13 43	ax-mp	$$⊢I=0_S$$