This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝐼 ∘ 𝐼 ) = 𝐼