Theorem smndex1iidm

Description: The modulo function I is idempotent. (Contributed by AV, 12-Feb-2024)

	Ref	Expression
Hypotheses	smndex1ibas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
	smndex1ibas.n	⊢ 𝑁 ∈ ℕ
	smndex1ibas.i	⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
Assertion	smndex1iidm	⊢ ( 𝐼 ∘ 𝐼 ) = 𝐼

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2		smndex1ibas.n	⊢ 𝑁 ∈ ℕ
3		smndex1ibas.i	⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4		nn0re	⊢ ( 𝑦 ∈ ℕ0 → 𝑦 ∈ ℝ )
5		nnrp	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ+ )
6	2 5	ax-mp	⊢ 𝑁 ∈ ℝ+
7		modabs2	⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) → ( ( 𝑦 mod 𝑁 ) mod 𝑁 ) = ( 𝑦 mod 𝑁 ) )
8	4 6 7	sylancl	⊢ ( 𝑦 ∈ ℕ0 → ( ( 𝑦 mod 𝑁 ) mod 𝑁 ) = ( 𝑦 mod 𝑁 ) )
9	8	eqcomd	⊢ ( 𝑦 ∈ ℕ0 → ( 𝑦 mod 𝑁 ) = ( ( 𝑦 mod 𝑁 ) mod 𝑁 ) )
10	9	mpteq2ia	⊢ ( 𝑦 ∈ ℕ0 ↦ ( 𝑦 mod 𝑁 ) ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝑦 mod 𝑁 ) mod 𝑁 ) )
11		oveq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 mod 𝑁 ) = ( 𝑦 mod 𝑁 ) )
12	11	cbvmptv	⊢ ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) = ( 𝑦 ∈ ℕ0 ↦ ( 𝑦 mod 𝑁 ) )
13	3 12	eqtri	⊢ 𝐼 = ( 𝑦 ∈ ℕ0 ↦ ( 𝑦 mod 𝑁 ) )
14		nn0z	⊢ ( 𝑦 ∈ ℕ0 → 𝑦 ∈ ℤ )
15	14	anim2i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℕ0 ) → ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℤ ) )
16	15	ancomd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℕ0 ) → ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℕ ) )
17		zmodcl	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑁 ∈ ℕ ) → ( 𝑦 mod 𝑁 ) ∈ ℕ0 )
18	16 17	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑦 ∈ ℕ0 ) → ( 𝑦 mod 𝑁 ) ∈ ℕ0 )
19	13	a1i	⊢ ( 𝑁 ∈ ℕ → 𝐼 = ( 𝑦 ∈ ℕ0 ↦ ( 𝑦 mod 𝑁 ) ) )
20	3	a1i	⊢ ( 𝑁 ∈ ℕ → 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) )
21		oveq1	⊢ ( 𝑥 = ( 𝑦 mod 𝑁 ) → ( 𝑥 mod 𝑁 ) = ( ( 𝑦 mod 𝑁 ) mod 𝑁 ) )
22	18 19 20 21	fmptco	⊢ ( 𝑁 ∈ ℕ → ( 𝐼 ∘ 𝐼 ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝑦 mod 𝑁 ) mod 𝑁 ) ) )
23	2 22	ax-mp	⊢ ( 𝐼 ∘ 𝐼 ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝑦 mod 𝑁 ) mod 𝑁 ) )
24	10 13 23	3eqtr4ri	⊢ ( 𝐼 ∘ 𝐼 ) = 𝐼