Theorem smndex1gid

Description: The composition of a constant function ( GK ) with another endofunction on NN0 results in ( GK ) itself. (Contributed by AV, 14-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	smndex1gid	$$⊢\left(F\in {\mathrm{Base}}_M\wedge K\in \left(0..^N\right)\right)\to G\left(K\right)\circ F=G\left(K\right)$$

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	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)$$
6		id	$$⊢n=K\to n=K$$
7	6	mpteq2dv	$$⊢n=K\to \left(x\in {\mathbb{N}}_0⟼n\right)=\left(x\in {\mathbb{N}}_0⟼K\right)$$
8	7	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)$$
9		id	$$⊢K\in \left(0..^N\right)\to K\in \left(0..^N\right)$$
10		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
11	10	mptex	$$⊢\left(x\in {\mathbb{N}}_0⟼K\right)\in \mathrm{V}$$
12	11	a1i	$$⊢K\in \left(0..^N\right)\to \left(x\in {\mathbb{N}}_0⟼K\right)\in \mathrm{V}$$
13	5 8 9 12	fvmptd	$$⊢K\in \left(0..^N\right)\to G\left(K\right)=\left(x\in {\mathbb{N}}_0⟼K\right)$$
14	13	adantl	$$⊢\left(F\in {\mathrm{Base}}_M\wedge K\in \left(0..^N\right)\right)\to G\left(K\right)=\left(x\in {\mathbb{N}}_0⟼K\right)$$
15	14	adantr	$$⊢\left(\left(F\in {\mathrm{Base}}_M\wedge K\in \left(0..^N\right)\right)\wedge y\in {\mathbb{N}}_0\right)\to G\left(K\right)=\left(x\in {\mathbb{N}}_0⟼K\right)$$
16		eqidd	$$⊢\left(\left(\left(F\in {\mathrm{Base}}_M\wedge K\in \left(0..^N\right)\right)\wedge y\in {\mathbb{N}}_0\right)\wedge x=F\left(y\right)\right)\to K=K$$
17		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
18	1 17	efmndbasf	$$⊢F\in {\mathrm{Base}}_M\to F:{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
19		ffvelrn	$$⊢\left(F:{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge y\in {\mathbb{N}}_0\right)\to F\left(y\right)\in {\mathbb{N}}_0$$
20	19	ex	$$⊢F:{\mathbb{N}}_0⟶{\mathbb{N}}_0\to \left(y\in {\mathbb{N}}_0\to F\left(y\right)\in {\mathbb{N}}_0\right)$$
21	18 20	syl	$$⊢F\in {\mathrm{Base}}_M\to \left(y\in {\mathbb{N}}_0\to F\left(y\right)\in {\mathbb{N}}_0\right)$$
22	21	adantr	$$⊢\left(F\in {\mathrm{Base}}_M\wedge K\in \left(0..^N\right)\right)\to \left(y\in {\mathbb{N}}_0\to F\left(y\right)\in {\mathbb{N}}_0\right)$$
23	22	imp	$$⊢\left(\left(F\in {\mathrm{Base}}_M\wedge K\in \left(0..^N\right)\right)\wedge y\in {\mathbb{N}}_0\right)\to F\left(y\right)\in {\mathbb{N}}_0$$
24		simplr	$$⊢\left(\left(F\in {\mathrm{Base}}_M\wedge K\in \left(0..^N\right)\right)\wedge y\in {\mathbb{N}}_0\right)\to K\in \left(0..^N\right)$$
25	15 16 23 24	fvmptd	$$⊢\left(\left(F\in {\mathrm{Base}}_M\wedge K\in \left(0..^N\right)\right)\wedge y\in {\mathbb{N}}_0\right)\to G\left(K\right)\left(F\left(y\right)\right)=K$$
26	25	mpteq2dva	$$⊢\left(F\in {\mathrm{Base}}_M\wedge K\in \left(0..^N\right)\right)\to \left(y\in {\mathbb{N}}_0⟼G\left(K\right)\left(F\left(y\right)\right)\right)=\left(y\in {\mathbb{N}}_0⟼K\right)$$
27	1 2 3 4	smndex1gbas	$$⊢K\in \left(0..^N\right)\to G\left(K\right)\in {\mathrm{Base}}_M$$
28	1 17	efmndbasf	$$⊢G\left(K\right)\in {\mathrm{Base}}_M\to G\left(K\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
29	27 28	syl	$$⊢K\in \left(0..^N\right)\to G\left(K\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0$$
30		fcompt	$$⊢\left(G\left(K\right):{\mathbb{N}}_0⟶{\mathbb{N}}_0\wedge F:{\mathbb{N}}_0⟶{\mathbb{N}}_0\right)\to G\left(K\right)\circ F=\left(y\in {\mathbb{N}}_0⟼G\left(K\right)\left(F\left(y\right)\right)\right)$$
31	29 18 30	syl2anr	$$⊢\left(F\in {\mathrm{Base}}_M\wedge K\in \left(0..^N\right)\right)\to G\left(K\right)\circ F=\left(y\in {\mathbb{N}}_0⟼G\left(K\right)\left(F\left(y\right)\right)\right)$$
32		eqidd	$$⊢x=y\to K=K$$
33	32	cbvmptv	$$⊢\left(x\in {\mathbb{N}}_0⟼K\right)=\left(y\in {\mathbb{N}}_0⟼K\right)$$
34	7 33	syl6eq	$$⊢n=K\to \left(x\in {\mathbb{N}}_0⟼n\right)=\left(y\in {\mathbb{N}}_0⟼K\right)$$
35	34	adantl	$$⊢\left(K\in \left(0..^N\right)\wedge n=K\right)\to \left(x\in {\mathbb{N}}_0⟼n\right)=\left(y\in {\mathbb{N}}_0⟼K\right)$$
36	10	mptex	$$⊢\left(y\in {\mathbb{N}}_0⟼K\right)\in \mathrm{V}$$
37	36	a1i	$$⊢K\in \left(0..^N\right)\to \left(y\in {\mathbb{N}}_0⟼K\right)\in \mathrm{V}$$
38	5 35 9 37	fvmptd	$$⊢K\in \left(0..^N\right)\to G\left(K\right)=\left(y\in {\mathbb{N}}_0⟼K\right)$$
39	38	adantl	$$⊢\left(F\in {\mathrm{Base}}_M\wedge K\in \left(0..^N\right)\right)\to G\left(K\right)=\left(y\in {\mathbb{N}}_0⟼K\right)$$
40	26 31 39	3eqtr4d	$$⊢\left(F\in {\mathrm{Base}}_M\wedge K\in \left(0..^N\right)\right)\to G\left(K\right)\circ F=G\left(K\right)$$