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	⊢ 𝑀 = ( 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	4	a1i	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) ) )
6		id	⊢ ( 𝑛 = 𝐾 → 𝑛 = 𝐾 )
7	6	mpteq2dv	⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
8	7	adantl	⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑛 = 𝐾 ) → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
9		id	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )
10		nn0ex	⊢ ℕ0 ∈ V
11	10	mptex	⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V
12	11	a1i	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V )
13	5 8 9 12	fvmptd	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
14	13	adantl	⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
15	14	adantr	⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
16		eqidd	⊢ ( ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → 𝐾 = 𝐾 )
17		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
18	1 17	efmndbasf	⊢ ( 𝐹 ∈ ( Base ‘ 𝑀 ) → 𝐹 : ℕ0 ⟶ ℕ0 )
19		ffvelrn	⊢ ( ( 𝐹 : ℕ0 ⟶ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
20	19	ex	⊢ ( 𝐹 : ℕ0 ⟶ ℕ0 → ( 𝑦 ∈ ℕ0 → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 ) )
21	18 20	syl	⊢ ( 𝐹 ∈ ( Base ‘ 𝑀 ) → ( 𝑦 ∈ ℕ0 → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 ) )
22	21	adantr	⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ℕ0 → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 ) )
23	22	imp	⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
24		simplr	⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )
25	15 16 23 24	fvmptd	⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) = 𝐾 )
26	25	mpteq2dva	⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
27	1 2 3 4	smndex1gbas	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑀 ) )
28	1 17	efmndbasf	⊢ ( ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑀 ) → ( 𝐺 ‘ 𝐾 ) : ℕ0 ⟶ ℕ0 )
29	27 28	syl	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) : ℕ0 ⟶ ℕ0 )
30		fcompt	⊢ ( ( ( 𝐺 ‘ 𝐾 ) : ℕ0 ⟶ ℕ0 ∧ 𝐹 : ℕ0 ⟶ ℕ0 ) → ( ( 𝐺 ‘ 𝐾 ) ∘ 𝐹 ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
31	29 18 30	syl2anr	⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝐾 ) ∘ 𝐹 ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
32		eqidd	⊢ ( 𝑥 = 𝑦 → 𝐾 = 𝐾 )
33	32	cbvmptv	⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 )
34	7 33	eqtrdi	⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
35	34	adantl	⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑛 = 𝐾 ) → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
36	10	mptex	⊢ ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) ∈ V
37	36	a1i	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) ∈ V )
38	5 35 9 37	fvmptd	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
39	38	adantl	⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
40	26 31 39	3eqtr4d	⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝐾 ) ∘ 𝐹 ) = ( 𝐺 ‘ 𝐾 ) )