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