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 ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
smndex1ibas.n ⊢ 𝑁 ∈ ℕ
smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
smndex1ibas.g ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
smndex1mgm.b ⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
smndex1mgm.s ⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
Assertion smndex1id 𝐼 = ( 0g ‘ 𝑆 )

Proof

Step Hyp Ref Expression
1 smndex1ibas.m ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2 smndex1ibas.n ⊢ 𝑁 ∈ ℕ
3 smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4 smndex1ibas.g ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
5 smndex1mgm.b ⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
6 smndex1mgm.s ⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
7 nn0ex ⊢ ℕ0 ∈ V
8 7 mptex ⊢ ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) ∈ V
9 3 8 eqeltri ⊢ 𝐼 ∈ V
10 9 snid ⊢ 𝐼 ∈ { 𝐼 }
11 elun1 ⊢ ( 𝐼 ∈ { 𝐼 } → 𝐼 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) )
12 10 11 ax-mp ⊢ 𝐼 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
13 12 5 eleqtrri ⊢ 𝐼 ∈ 𝐵
14 1 2 3 4 5 6 smndex1bas ⊢ ( Base ‘ 𝑆 ) = 𝐵
15 14 eqcomi ⊢ 𝐵 = ( Base ‘ 𝑆 )
16 15 a1i ⊢ ( 𝐼 ∈ 𝐵 → 𝐵 = ( Base ‘ 𝑆 ) )
17 snex ⊢ { 𝐼 } ∈ V
18 ovex ⊢ ( 0 ..^ 𝑁 ) ∈ V
19 snex ⊢ { ( 𝐺 ‘ 𝑛 ) } ∈ V
20 18 19 iunex ⊢ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ∈ V
21 17 20 unex ⊢ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ∈ V
22 5 21 eqeltri ⊢ 𝐵 ∈ V
23 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
24 6 23 ressplusg ⊢ ( 𝐵 ∈ V → ( +g ‘ 𝑀 ) = ( +g ‘ 𝑆 ) )
25 22 24 mp1i ⊢ ( 𝐼 ∈ 𝐵 → ( +g ‘ 𝑀 ) = ( +g ‘ 𝑆 ) )
26 id ⊢ ( 𝐼 ∈ 𝐵 → 𝐼 ∈ 𝐵 )
27 1 2 3 smndex1ibas ⊢ 𝐼 ∈ ( Base ‘ 𝑀 )
28 27 a1i ⊢ ( 𝐼 ∈ 𝐵 → 𝐼 ∈ ( Base ‘ 𝑀 ) )
29 1 2 3 4 5 smndex1basss ⊢ 𝐵 ⊆ ( Base ‘ 𝑀 )
30 29 sseli ⊢ ( 𝑎 ∈ 𝐵 → 𝑎 ∈ ( Base ‘ 𝑀 ) )
31 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
32 1 31 23 efmndov ⊢ ( ( 𝐼 ∈ ( Base ‘ 𝑀 ) ∧ 𝑎 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐼 ( +g ‘ 𝑀 ) 𝑎 ) = ( 𝐼 ∘ 𝑎 ) )
33 28 30 32 syl2an ⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐼 ( +g ‘ 𝑀 ) 𝑎 ) = ( 𝐼 ∘ 𝑎 ) )
34 1 2 3 4 5 6 smndex1mndlem ⊢ ( 𝑎 ∈ 𝐵 → ( ( 𝐼 ∘ 𝑎 ) = 𝑎 ∧ ( 𝑎 ∘ 𝐼 ) = 𝑎 ) )
35 34 simpld ⊢ ( 𝑎 ∈ 𝐵 → ( 𝐼 ∘ 𝑎 ) = 𝑎 )
36 35 adantl ⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐼 ∘ 𝑎 ) = 𝑎 )
37 33 36 eqtrd ⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐼 ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 )
38 1 31 23 efmndov ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝐼 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝐼 ) = ( 𝑎 ∘ 𝐼 ) )
39 30 28 38 syl2anr ⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝐼 ) = ( 𝑎 ∘ 𝐼 ) )
40 34 simprd ⊢ ( 𝑎 ∈ 𝐵 → ( 𝑎 ∘ 𝐼 ) = 𝑎 )
41 40 adantl ⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 ∘ 𝐼 ) = 𝑎 )
42 39 41 eqtrd ⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝐼 ) = 𝑎 )
43 16 25 26 37 42 grpidd ⊢ ( 𝐼 ∈ 𝐵 → 𝐼 = ( 0g ‘ 𝑆 ) )
44 13 43 ax-mp ⊢ 𝐼 = ( 0g ‘ 𝑆 )