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

Metamath Proof Explorer

Theorem smndex1mnd

Description: The monoid of endofunctions on NN0 restricted to the modulo function I and the constant functions ( GK ) is a monoid. (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 smndex1mnd 𝑆 ∈ Mnd

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 1 2 3 4 5 6 smndex1sgrp ⊢ 𝑆 ∈ Smgrp
8 nn0ex ⊢ ℕ0 ∈ V
9 8 mptex ⊢ ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) ∈ V
10 3 9 eqeltri ⊢ 𝐼 ∈ V
11 10 snid ⊢ 𝐼 ∈ { 𝐼 }
12 elun1 ⊢ ( 𝐼 ∈ { 𝐼 } → 𝐼 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) )
13 11 12 ax-mp ⊢ 𝐼 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
14 13 5 eleqtrri ⊢ 𝐼 ∈ 𝐵
15 id ⊢ ( 𝐼 ∈ 𝐵 → 𝐼 ∈ 𝐵 )
16 coeq1 ⊢ ( 𝑎 = 𝐼 → ( 𝑎 ∘ 𝑏 ) = ( 𝐼 ∘ 𝑏 ) )
17 16 eqeq1d ⊢ ( 𝑎 = 𝐼 → ( ( 𝑎 ∘ 𝑏 ) = 𝑏 ↔ ( 𝐼 ∘ 𝑏 ) = 𝑏 ) )
18 coeq2 ⊢ ( 𝑎 = 𝐼 → ( 𝑏 ∘ 𝑎 ) = ( 𝑏 ∘ 𝐼 ) )
19 18 eqeq1d ⊢ ( 𝑎 = 𝐼 → ( ( 𝑏 ∘ 𝑎 ) = 𝑏 ↔ ( 𝑏 ∘ 𝐼 ) = 𝑏 ) )
20 17 19 anbi12d ⊢ ( 𝑎 = 𝐼 → ( ( ( 𝑎 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝑎 ) = 𝑏 ) ↔ ( ( 𝐼 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝐼 ) = 𝑏 ) ) )
21 20 ralbidv ⊢ ( 𝑎 = 𝐼 → ( ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝑎 ) = 𝑏 ) ↔ ∀ 𝑏 ∈ 𝐵 ( ( 𝐼 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝐼 ) = 𝑏 ) ) )
22 21 adantl ⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑎 = 𝐼 ) → ( ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝑎 ) = 𝑏 ) ↔ ∀ 𝑏 ∈ 𝐵 ( ( 𝐼 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝐼 ) = 𝑏 ) ) )
23 1 2 3 4 5 6 smndex1mndlem ⊢ ( 𝑏 ∈ 𝐵 → ( ( 𝐼 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝐼 ) = 𝑏 ) )
24 23 rgen ⊢ ∀ 𝑏 ∈ 𝐵 ( ( 𝐼 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝐼 ) = 𝑏 )
25 24 a1i ⊢ ( 𝐼 ∈ 𝐵 → ∀ 𝑏 ∈ 𝐵 ( ( 𝐼 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝐼 ) = 𝑏 ) )
26 15 22 25 rspcedvd ⊢ ( 𝐼 ∈ 𝐵 → ∃ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝑎 ) = 𝑏 ) )
27 14 26 ax-mp ⊢ ∃ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝑎 ) = 𝑏 )
28 1 2 3 4 5 smndex1basss ⊢ 𝐵 ⊆ ( Base ‘ 𝑀 )
29 ssel ⊢ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) → ( 𝑎 ∈ 𝐵 → 𝑎 ∈ ( Base ‘ 𝑀 ) ) )
30 ssel ⊢ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) → ( 𝑏 ∈ 𝐵 → 𝑏 ∈ ( Base ‘ 𝑀 ) ) )
31 29 30 anim12d ⊢ ( 𝐵 ⊆ ( Base ‘ 𝑀 ) → ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) ) )
32 28 31 ax-mp ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) )
33 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
34 snex ⊢ { 𝐼 } ∈ V
35 ovex ⊢ ( 0 ..^ 𝑁 ) ∈ V
36 snex ⊢ { ( 𝐺 ‘ 𝑛 ) } ∈ V
37 35 36 iunex ⊢ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ∈ V
38 34 37 unex ⊢ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ∈ V
39 5 38 eqeltri ⊢ 𝐵 ∈ V
40 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
41 6 40 ressplusg ⊢ ( 𝐵 ∈ V → ( +g ‘ 𝑀 ) = ( +g ‘ 𝑆 ) )
42 39 41 ax-mp ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑆 )
43 42 eqcomi ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑀 )
44 1 33 43 efmndov ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) = ( 𝑎 ∘ 𝑏 ) )
45 44 eqeq1d ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) = 𝑏 ↔ ( 𝑎 ∘ 𝑏 ) = 𝑏 ) )
46 43 oveqi ⊢ ( 𝑏 ( +g ‘ 𝑆 ) 𝑎 ) = ( 𝑏 ( +g ‘ 𝑀 ) 𝑎 )
47 1 33 40 efmndov ⊢ ( ( 𝑏 ∈ ( Base ‘ 𝑀 ) ∧ 𝑎 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑏 ( +g ‘ 𝑀 ) 𝑎 ) = ( 𝑏 ∘ 𝑎 ) )
48 47 ancoms ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑏 ( +g ‘ 𝑀 ) 𝑎 ) = ( 𝑏 ∘ 𝑎 ) )
49 46 48 eqtrid ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑏 ( +g ‘ 𝑆 ) 𝑎 ) = ( 𝑏 ∘ 𝑎 ) )
50 49 eqeq1d ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) → ( ( 𝑏 ( +g ‘ 𝑆 ) 𝑎 ) = 𝑏 ↔ ( 𝑏 ∘ 𝑎 ) = 𝑏 ) )
51 45 50 anbi12d ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝑏 ∈ ( Base ‘ 𝑀 ) ) → ( ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑆 ) 𝑎 ) = 𝑏 ) ↔ ( ( 𝑎 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝑎 ) = 𝑏 ) ) )
52 32 51 syl ⊢ ( ( 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑆 ) 𝑎 ) = 𝑏 ) ↔ ( ( 𝑎 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝑎 ) = 𝑏 ) ) )
53 52 ralbidva ⊢ ( 𝑎 ∈ 𝐵 → ( ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑆 ) 𝑎 ) = 𝑏 ) ↔ ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝑎 ) = 𝑏 ) ) )
54 53 rexbiia ⊢ ( ∃ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑆 ) 𝑎 ) = 𝑏 ) ↔ ∃ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ∘ 𝑏 ) = 𝑏 ∧ ( 𝑏 ∘ 𝑎 ) = 𝑏 ) )
55 27 54 mpbir ⊢ ∃ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑆 ) 𝑎 ) = 𝑏 )
56 1 2 3 4 5 6 smndex1bas ⊢ ( Base ‘ 𝑆 ) = 𝐵
57 56 eqcomi ⊢ 𝐵 = ( Base ‘ 𝑆 )
58 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
59 57 58 ismnddef ⊢ ( 𝑆 ∈ Mnd ↔ ( 𝑆 ∈ Smgrp ∧ ∃ 𝑎 ∈ 𝐵 ∀ 𝑏 ∈ 𝐵 ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) = 𝑏 ∧ ( 𝑏 ( +g ‘ 𝑆 ) 𝑎 ) = 𝑏 ) ) )
60 7 55 59 mpbir2an ⊢ 𝑆 ∈ Mnd