Theorem smndex1gbas

Description: The constant functions ( GK ) are endofunctions on NN0 . (Contributed by AV, 12-Feb-2024) Avoid ax-rep and shorten proof. (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	smndex1gbas	$$⊢K\in \left(0..^N\right)\to G\left(K\right)\in {\mathrm{Base}}_M$$

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		elfzonn0	$$⊢K\in \left(0..^N\right)\to K\in {\mathbb{N}}_0$$
6	5	adantr	$$⊢\left(K\in \left(0..^N\right)\wedge x\in {\mathbb{N}}_0\right)\to K\in {\mathbb{N}}_0$$
7	6	fmpttd	$$⊢K\in \left(0..^N\right)\to \left(x\in {\mathbb{N}}_0⟼K\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
8		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
9	8 8	elmap	$$⊢\left(x\in {\mathbb{N}}_0⟼K\right)\in \left({{\mathbb{N}}_0}^{{\mathbb{N}}_0}\right)\leftrightarrow \left(x\in {\mathbb{N}}_0⟼K\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
10	7 9	sylibr	$$⊢K\in \left(0..^N\right)\to \left(x\in {\mathbb{N}}_0⟼K\right)\in \left({{\mathbb{N}}_0}^{{\mathbb{N}}_0}\right)$$
11		id	$$⊢n=K\to n=K$$
12	11	mpteq2dv	$$⊢n=K\to \left(x\in {\mathbb{N}}_0⟼n\right)=\left(x\in {\mathbb{N}}_0⟼K\right)$$
13		fconstmpt	$$⊢{\mathbb{N}}_0\times \left\{K\right\}=\left(x\in {\mathbb{N}}_0⟼K\right)$$
14		snex	$$⊢\left\{K\right\}\in \mathrm{V}$$
15	8 14	xpex	$$⊢{\mathbb{N}}_0\times \left\{K\right\}\in \mathrm{V}$$
16	13 15	eqeltrri	$$⊢\left(x\in {\mathbb{N}}_0⟼K\right)\in \mathrm{V}$$
17	12 4 16	fvmpt	$$⊢K\in \left(0..^N\right)\to G\left(K\right)=\left(x\in {\mathbb{N}}_0⟼K\right)$$
18		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
19	1 18	efmndbas	$$⊢{\mathrm{Base}}_M={{\mathbb{N}}_0}^{{\mathbb{N}}_0}$$
20	19	a1i	$$⊢K\in \left(0..^N\right)\to {\mathrm{Base}}_M={{\mathbb{N}}_0}^{{\mathbb{N}}_0}$$
21	10 17 20	3eltr4d	$$⊢K\in \left(0..^N\right)\to G\left(K\right)\in {\mathrm{Base}}_M$$