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

Metamath Proof Explorer

Theorem smndex1id

Description: The modulo function I is the identity of the monoid of endofunctions on NN0 restricted to the modulo function I and the constant functions ( GK ) . (Contributed by AV, 16-Feb-2024)

Ref Expression
Hypotheses smndex1ibas.m ⊢ M = EndoFMnd ⁡ ℕ 0
smndex1ibas.n ⊢ N ∈ ℕ
smndex1ibas.i ⊢ I = x ∈ ℕ 0 ⟼ x mod N
smndex1ibas.g ⊢ G = n ∈ 0 ..^ N ⟼ x ∈ ℕ 0 ⟼ n
smndex1mgm.b ⊢ B = I ∪ ⋃ n ∈ 0 ..^ N G ⁡ n
smndex1mgm.s ⊢ S = M ↾ 𝑠 B
Assertion smndex1id ⊢ I = 0 S

Proof

Step Hyp Ref Expression
1 smndex1ibas.m ⊢ M = EndoFMnd ⁡ ℕ 0
2 smndex1ibas.n ⊢ N ∈ ℕ
3 smndex1ibas.i ⊢ I = x ∈ ℕ 0 ⟼ x mod N
4 smndex1ibas.g ⊢ G = n ∈ 0 ..^ N ⟼ x ∈ ℕ 0 ⟼ n
5 smndex1mgm.b ⊢ B = I ∪ ⋃ n ∈ 0 ..^ N G ⁡ n
6 smndex1mgm.s ⊢ S = M ↾ 𝑠 B
7 nn0ex ⊢ ℕ 0 ∈ V
8 7 mptex ⊢ x ∈ ℕ 0 ⟼ x mod N ∈ V
9 3 8 eqeltri ⊢ I ∈ V
10 9 snid ⊢ I ∈ I
11 elun1 ⊢ I ∈ I → I ∈ I ∪ ⋃ n ∈ 0 ..^ N G ⁡ n
12 10 11 ax-mp ⊢ I ∈ I ∪ ⋃ n ∈ 0 ..^ N G ⁡ n
13 12 5 eleqtrri ⊢ I ∈ B
14 1 2 3 4 5 6 smndex1bas ⊢ Base S = B
15 14 eqcomi ⊢ B = Base S
16 15 a1i ⊢ I ∈ B → B = Base S
17 snex ⊢ I ∈ V
18 ovex ⊢ 0 ..^ N ∈ V
19 snex ⊢ G ⁡ n ∈ V
20 18 19 iunex ⊢ ⋃ n ∈ 0 ..^ N G ⁡ n ∈ V
21 17 20 unex ⊢ I ∪ ⋃ n ∈ 0 ..^ N G ⁡ n ∈ V
22 5 21 eqeltri ⊢ B ∈ V
23 eqid ⊢ + M = + M
24 6 23 ressplusg ⊢ B ∈ V → + M = + S
25 22 24 mp1i ⊢ I ∈ B → + M = + S
26 id ⊢ I ∈ B → I ∈ B
27 1 2 3 smndex1ibas ⊢ I ∈ Base M
28 27 a1i ⊢ I ∈ B → I ∈ Base M
29 1 2 3 4 5 smndex1basss ⊢ B ⊆ Base M
30 29 sseli ⊢ a ∈ B → a ∈ Base M
31 eqid ⊢ Base M = Base M
32 1 31 23 efmndov ⊢ I ∈ Base M ∧ a ∈ Base M → I + M a = I ∘ a
33 28 30 32 syl2an ⊢ I ∈ B ∧ a ∈ B → I + M a = I ∘ a
34 1 2 3 4 5 6 smndex1mndlem ⊢ a ∈ B → I ∘ a = a ∧ a ∘ I = a
35 34 simpld ⊢ a ∈ B → I ∘ a = a
36 35 adantl ⊢ I ∈ B ∧ a ∈ B → I ∘ a = a
37 33 36 eqtrd ⊢ I ∈ B ∧ a ∈ B → I + M a = a
38 1 31 23 efmndov ⊢ a ∈ Base M ∧ I ∈ Base M → a + M I = a ∘ I
39 30 28 38 syl2anr ⊢ I ∈ B ∧ a ∈ B → a + M I = a ∘ I
40 34 simprd ⊢ a ∈ B → a ∘ I = a
41 40 adantl ⊢ I ∈ B ∧ a ∈ B → a ∘ I = a
42 39 41 eqtrd ⊢ I ∈ B ∧ a ∈ B → a + M I = a
43 16 25 26 37 42 grpidd ⊢ I ∈ B → I = 0 S
44 13 43 ax-mp ⊢ I = 0 S