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)

	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		simpl	⊢ ( ( 𝑛 = 𝐾 ∧ 𝑥 ∈ ℕ0 ) → 𝑛 = 𝐾 )
10	9	mpteq2dva	⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
11		nn0ex	⊢ ℕ0 ∈ V
12	11	mptex	⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V
13	10 4 12	fvmpt	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
14	13	coeq2d	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∘ ( 𝐺 ‘ 𝐾 ) ) = ( 𝐼 ∘ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ) )
15		oveq1	⊢ ( 𝑥 = 𝐾 → ( 𝑥 mod 𝑁 ) = ( 𝐾 mod 𝑁 ) )
16		zmodidfzoimp	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 mod 𝑁 ) = 𝐾 )
17	15 16	sylan9eqr	⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 = 𝐾 ) → ( 𝑥 mod 𝑁 ) = 𝐾 )
18		elfzonn0	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ∈ ℕ0 )
19	3 17 18 18	fvmptd2	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ‘ 𝐾 ) = 𝐾 )
20	19	eqcomd	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 = ( 𝐼 ‘ 𝐾 ) )
21	20	sneqd	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → { 𝐾 } = { ( 𝐼 ‘ 𝐾 ) } )
22	21	xpeq2d	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( ℕ0 × { 𝐾 } ) = ( ℕ0 × { ( 𝐼 ‘ 𝐾 ) } ) )
23	13 6	eqtrdi	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( ℕ0 × { 𝐾 } ) )
24		ovex	⊢ ( 𝑥 mod 𝑁 ) ∈ V
25	24 3	fnmpti	⊢ 𝐼 Fn ℕ0
26		fcoconst	⊢ ( ( 𝐼 Fn ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐼 ∘ ( ℕ0 × { 𝐾 } ) ) = ( ℕ0 × { ( 𝐼 ‘ 𝐾 ) } ) )
27	25 18 26	sylancr	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∘ ( ℕ0 × { 𝐾 } ) ) = ( ℕ0 × { ( 𝐼 ‘ 𝐾 ) } ) )
28	22 23 27	3eqtr4d	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝐼 ∘ ( ℕ0 × { 𝐾 } ) ) )
29	8 14 28	3eqtr4d	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∘ ( 𝐺 ‘ 𝐾 ) ) = ( 𝐺 ‘ 𝐾 ) )