Theorem smndex1igid

Description: The composition of the modulo function I and a constant function ( GK ) 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	smndex1igid	⊢ ( 𝐾 ∈ ( 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		fconstmpt	⊢ ( ℕ0 × { 𝐾 } ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 )
6	5	eqcomi	⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) = ( ℕ0 × { 𝐾 } )
7	6	a1i	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) = ( ℕ0 × { 𝐾 } ) )
8	7	coeq2d	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∘ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ) = ( 𝐼 ∘ ( ℕ0 × { 𝐾 } ) ) )
9		id	⊢ ( 𝑛 = 𝐾 → 𝑛 = 𝐾 )
10	9	mpteq2dv	⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
11		nn0ex	⊢ ℕ0 ∈ V
12		snex	⊢ { 𝐾 } ∈ V
13	11 12	xpex	⊢ ( ℕ0 × { 𝐾 } ) ∈ V
14	5 13	eqeltrri	⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V
15	10 4 14	fvmpt	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
16	15	coeq2d	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∘ ( 𝐺 ‘ 𝐾 ) ) = ( 𝐼 ∘ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ) )
17		oveq1	⊢ ( 𝑥 = 𝐾 → ( 𝑥 mod 𝑁 ) = ( 𝐾 mod 𝑁 ) )
18		zmodidfzoimp	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 mod 𝑁 ) = 𝐾 )
19	17 18	sylan9eqr	⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 = 𝐾 ) → ( 𝑥 mod 𝑁 ) = 𝐾 )
20		elfzonn0	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ∈ ℕ0 )
21	3 19 20 20	fvmptd2	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ‘ 𝐾 ) = 𝐾 )
22	21	eqcomd	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 = ( 𝐼 ‘ 𝐾 ) )
23	22	sneqd	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → { 𝐾 } = { ( 𝐼 ‘ 𝐾 ) } )
24	23	xpeq2d	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( ℕ0 × { 𝐾 } ) = ( ℕ0 × { ( 𝐼 ‘ 𝐾 ) } ) )
25	15 5	eqtr4di	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( ℕ0 × { 𝐾 } ) )
26		ovex	⊢ ( 𝑥 mod 𝑁 ) ∈ V
27	26 3	fnmpti	⊢ 𝐼 Fn ℕ0
28		fcoconst	⊢ ( ( 𝐼 Fn ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐼 ∘ ( ℕ0 × { 𝐾 } ) ) = ( ℕ0 × { ( 𝐼 ‘ 𝐾 ) } ) )
29	27 20 28	sylancr	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∘ ( ℕ0 × { 𝐾 } ) ) = ( ℕ0 × { ( 𝐼 ‘ 𝐾 ) } ) )
30	24 25 29	3eqtr4d	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝐼 ∘ ( ℕ0 × { 𝐾 } ) ) )
31	8 16 30	3eqtr4d	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∘ ( 𝐺 ‘ 𝐾 ) ) = ( 𝐺 ‘ 𝐾 ) )