Theorem smndex1igid

Description: The composition of the modulo function I and a constant function ( GK ) results in ( GK ) itself. (Contributed by AV, 14-Feb-2024) Avoid ax-rep . (Revised by GG, 2-Apr-2026)

	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)$$
Assertion	smndex1igid	$$⊢K\in \left(0..^N\right)\to I\circ G\left(K\right)=G\left(K\right)$$

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		fconstmpt	$$⊢{\mathbb{N}}_0\times \left\{K\right\}=\left(x\in {\mathbb{N}}_0⟼K\right)$$
6	5	eqcomi	$$⊢\left(x\in {\mathbb{N}}_0⟼K\right)={\mathbb{N}}_0\times \left\{K\right\}$$
7	6	a1i	$$⊢K\in \left(0..^N\right)\to \left(x\in {\mathbb{N}}_0⟼K\right)={\mathbb{N}}_0\times \left\{K\right\}$$
8	7	coeq2d	$$⊢K\in \left(0..^N\right)\to I\circ \left(x\in {\mathbb{N}}_0⟼K\right)=I\circ \left({\mathbb{N}}_0\times \left\{K\right\}\right)$$
9		id	$$⊢n=K\to n=K$$
10	9	mpteq2dv	$$⊢n=K\to \left(x\in {\mathbb{N}}_0⟼n\right)=\left(x\in {\mathbb{N}}_0⟼K\right)$$
11		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
12		snex	$$⊢\left\{K\right\}\in \mathrm{V}$$
13	11 12	xpex	$$⊢{\mathbb{N}}_0\times \left\{K\right\}\in \mathrm{V}$$
14	5 13	eqeltrri	$$⊢\left(x\in {\mathbb{N}}_0⟼K\right)\in \mathrm{V}$$
15	10 4 14	fvmpt	$$⊢K\in \left(0..^N\right)\to G\left(K\right)=\left(x\in {\mathbb{N}}_0⟼K\right)$$
16	15	coeq2d	$$⊢K\in \left(0..^N\right)\to I\circ G\left(K\right)=I\circ \left(x\in {\mathbb{N}}_0⟼K\right)$$
17		oveq1	$$⊢x=K\to x\mathrm{mod}N=K\mathrm{mod}N$$
18		zmodidfzoimp	$$⊢K\in \left(0..^N\right)\to K\mathrm{mod}N=K$$
19	17 18	sylan9eqr	$$⊢\left(K\in \left(0..^N\right)\wedge x=K\right)\to x\mathrm{mod}N=K$$
20		elfzonn0	$$⊢K\in \left(0..^N\right)\to K\in {\mathbb{N}}_0$$
21	3 19 20 20	fvmptd2	$$⊢K\in \left(0..^N\right)\to I\left(K\right)=K$$
22	21	eqcomd	$$⊢K\in \left(0..^N\right)\to K=I\left(K\right)$$
23	22	sneqd	$$⊢K\in \left(0..^N\right)\to \left\{K\right\}=\left\{I\left(K\right)\right\}$$
24	23	xpeq2d	$$⊢K\in \left(0..^N\right)\to {\mathbb{N}}_0\times \left\{K\right\}={\mathbb{N}}_0\times \left\{I\left(K\right)\right\}$$
25	15 5	eqtr4di	$$⊢K\in \left(0..^N\right)\to G\left(K\right)={\mathbb{N}}_0\times \left\{K\right\}$$
26		ovex	$$⊢x\mathrm{mod}N\in \mathrm{V}$$
27	26 3	fnmpti	$$⊢IFn{\mathbb{N}}_0$$
28		fcoconst	$$⊢\left(IFn{\mathbb{N}}_0\wedge K\in {\mathbb{N}}_0\right)\to I\circ \left({\mathbb{N}}_0\times \left\{K\right\}\right)={\mathbb{N}}_0\times \left\{I\left(K\right)\right\}$$
29	27 20 28	sylancr	$$⊢K\in \left(0..^N\right)\to I\circ \left({\mathbb{N}}_0\times \left\{K\right\}\right)={\mathbb{N}}_0\times \left\{I\left(K\right)\right\}$$
30	24 25 29	3eqtr4d	$$⊢K\in \left(0..^N\right)\to G\left(K\right)=I\circ \left({\mathbb{N}}_0\times \left\{K\right\}\right)$$
31	8 16 30	3eqtr4d	$$⊢K\in \left(0..^N\right)\to I\circ G\left(K\right)=G\left(K\right)$$