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) Avoid ax-rep . (Revised by GG, 2-Apr-2026)

	Ref	Expression
Hypotheses	smndex1ibas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
	smndex1ibas.n	⊢ 𝑁 ∈ ℕ
	smndex1ibas.i	⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
	smndex1ibas.g	⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
Assertion	smndex1gid	⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝐾 ) ∘ 𝐹 ) = ( 𝐺 ‘ 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2		smndex1ibas.n	⊢ 𝑁 ∈ ℕ
3		smndex1ibas.i	⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4		smndex1ibas.g	⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
5		id	⊢ ( 𝑛 = 𝐾 → 𝑛 = 𝐾 )
6	5	mpteq2dv	⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
7		fconstmpt	⊢ ( ℕ0 × { 𝐾 } ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 )
8		nn0ex	⊢ ℕ0 ∈ V
9		snex	⊢ { 𝐾 } ∈ V
10	8 9	xpex	⊢ ( ℕ0 × { 𝐾 } ) ∈ V
11	7 10	eqeltrri	⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V
12	6 4 11	fvmpt	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
13	12	adantl	⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
14	13	adantr	⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
15		eqidd	⊢ ( ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → 𝐾 = 𝐾 )
16		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
17	1 16	efmndbasf	⊢ ( 𝐹 ∈ ( Base ‘ 𝑀 ) → 𝐹 : ℕ0 ⟶ ℕ0 )
18		ffvelcdm	⊢ ( ( 𝐹 : ℕ0 ⟶ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
19	18	ex	⊢ ( 𝐹 : ℕ0 ⟶ ℕ0 → ( 𝑦 ∈ ℕ0 → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 ) )
20	17 19	syl	⊢ ( 𝐹 ∈ ( Base ‘ 𝑀 ) → ( 𝑦 ∈ ℕ0 → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 ) )
21	20	adantr	⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ℕ0 → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 ) )
22	21	imp	⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
23		simplr	⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )
24	14 15 22 23	fvmptd	⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) = 𝐾 )
25	24	mpteq2dva	⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
26	1 2 3 4	smndex1gbas	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑀 ) )
27	1 16	efmndbasf	⊢ ( ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑀 ) → ( 𝐺 ‘ 𝐾 ) : ℕ0 ⟶ ℕ0 )
28	26 27	syl	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) : ℕ0 ⟶ ℕ0 )
29		fcompt	⊢ ( ( ( 𝐺 ‘ 𝐾 ) : ℕ0 ⟶ ℕ0 ∧ 𝐹 : ℕ0 ⟶ ℕ0 ) → ( ( 𝐺 ‘ 𝐾 ) ∘ 𝐹 ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
30	28 17 29	syl2anr	⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝐾 ) ∘ 𝐹 ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
31		eqidd	⊢ ( 𝑥 = 𝑦 → 𝐾 = 𝐾 )
32	31	cbvmptv	⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 )
33	6 32	eqtrdi	⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
34		fconstmpt	⊢ ( ℕ0 × { 𝐾 } ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 )
35	34 10	eqeltrri	⊢ ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) ∈ V
36	33 4 35	fvmpt	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
37	36	adantl	⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
38	25 30 37	3eqtr4d	⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝐾 ) ∘ 𝐹 ) = ( 𝐺 ‘ 𝐾 ) )