Theorem smndex1gbas

Description: The constant functions ( GK ) are endofunctions on NN0 . (Contributed by AV, 12-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)$$
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	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		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	ralrimiva	$$⊢K\in \left(0..^N\right)\to \forall x\in {\mathbb{N}}_{0}K\in {\mathbb{N}}_0$$
8		eqid	$$⊢\left(x\in {\mathbb{N}}_0⟼K\right)=\left(x\in {\mathbb{N}}_0⟼K\right)$$
9	8	fmpt	$$⊢\forall x\in {\mathbb{N}}_{0}K\in {\mathbb{N}}_0\leftrightarrow \left(x\in {\mathbb{N}}_0⟼K\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
10	7 9	sylib	$$⊢K\in \left(0..^N\right)\to \left(x\in {\mathbb{N}}_0⟼K\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
11		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
12	11 11	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$$
13	10 12	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)$$
14	4	a1i	$$⊢K\in \left(0..^N\right)\to G=\left(n\in \left(0..^N\right)⟼\left(x\in {\mathbb{N}}_0⟼n\right)\right)$$
15		id	$$⊢n=K\to n=K$$
16	15	mpteq2dv	$$⊢n=K\to \left(x\in {\mathbb{N}}_0⟼n\right)=\left(x\in {\mathbb{N}}_0⟼K\right)$$
17	16	adantl	$$⊢\left(K\in \left(0..^N\right)\wedge n=K\right)\to \left(x\in {\mathbb{N}}_0⟼n\right)=\left(x\in {\mathbb{N}}_0⟼K\right)$$
18		id	$$⊢K\in \left(0..^N\right)\to K\in \left(0..^N\right)$$
19	11	mptex	$$⊢\left(x\in {\mathbb{N}}_0⟼K\right)\in \mathrm{V}$$
20	19	a1i	$$⊢K\in \left(0..^N\right)\to \left(x\in {\mathbb{N}}_0⟼K\right)\in \mathrm{V}$$
21	14 17 18 20	fvmptd	$$⊢K\in \left(0..^N\right)\to G\left(K\right)=\left(x\in {\mathbb{N}}_0⟼K\right)$$
22		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
23	1 22	efmndbas	$$⊢{\mathrm{Base}}_M={{\mathbb{N}}_0}^{{\mathbb{N}}_0}$$
24	23	a1i	$$⊢K\in \left(0..^N\right)\to {\mathrm{Base}}_M={{\mathbb{N}}_0}^{{\mathbb{N}}_0}$$
25	13 21 24	3eltr4d	$$⊢K\in \left(0..^N\right)\to G\left(K\right)\in {\mathrm{Base}}_M$$