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

Metamath Proof Explorer

Theorem smndex1sgrp

Description: The monoid of endofunctions on NN0 restricted to the modulo function I and the constant functions ( GK ) is a semigroup. (Contributed by AV, 14-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 smndex1sgrp 𝑆 ∈ Smgrp

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 smndex1mgm ⊢ 𝑆 ∈ Mgm
8 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
9 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
10 8 9 mgmcl ⊢ ( ( 𝑆 ∈ Mgm ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
11 7 10 mp3an1 ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
12 snex ⊢ { 𝐼 } ∈ V
13 ovex ⊢ ( 0 ..^ 𝑁 ) ∈ V
14 snex ⊢ { ( 𝐺 ‘ 𝑛 ) } ∈ V
15 13 14 iunex ⊢ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ∈ V
16 12 15 unex ⊢ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ∈ V
17 5 16 eqeltri ⊢ 𝐵 ∈ V
18 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
19 6 18 ressplusg ⊢ ( 𝐵 ∈ V → ( +g ‘ 𝑀 ) = ( +g ‘ 𝑆 ) )
20 17 19 ax-mp ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑆 )
21 20 eqcomi ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑀 )
22 21 oveqi ⊢ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 )
23 1 2 3 4 5 6 smndex1bas ⊢ ( Base ‘ 𝑆 ) = 𝐵
24 1 2 3 4 5 smndex1basss ⊢ 𝐵 ⊆ ( Base ‘ 𝑀 )
25 23 24 eqsstri ⊢ ( Base ‘ 𝑆 ) ⊆ ( Base ‘ 𝑀 )
26 ssel ⊢ ( ( Base ‘ 𝑆 ) ⊆ ( Base ‘ 𝑀 ) → ( 𝑥 ∈ ( Base ‘ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝑀 ) ) )
27 ssel ⊢ ( ( Base ‘ 𝑆 ) ⊆ ( Base ‘ 𝑀 ) → ( 𝑦 ∈ ( Base ‘ 𝑆 ) → 𝑦 ∈ ( Base ‘ 𝑀 ) ) )
28 26 27 anim12d ⊢ ( ( Base ‘ 𝑆 ) ⊆ ( Base ‘ 𝑀 ) → ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) ) )
29 25 28 ax-mp ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) )
30 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
31 1 30 18 efmndov ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ 𝑦 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ∘ 𝑦 ) )
32 29 31 syl ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑥 ∘ 𝑦 ) )
33 22 32 eqtrid ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ∘ 𝑦 ) )
34 11 33 symggrplem ⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑆 ) ∧ 𝑏 ∈ ( Base ‘ 𝑆 ) ∧ 𝑐 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( +g ‘ 𝑆 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑆 ) ( 𝑏 ( +g ‘ 𝑆 ) 𝑐 ) ) )
35 34 rgen3 ⊢ ∀ 𝑎 ∈ ( Base ‘ 𝑆 ) ∀ 𝑏 ∈ ( Base ‘ 𝑆 ) ∀ 𝑐 ∈ ( Base ‘ 𝑆 ) ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( +g ‘ 𝑆 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑆 ) ( 𝑏 ( +g ‘ 𝑆 ) 𝑐 ) )
36 8 9 issgrp ⊢ ( 𝑆 ∈ Smgrp ↔ ( 𝑆 ∈ Mgm ∧ ∀ 𝑎 ∈ ( Base ‘ 𝑆 ) ∀ 𝑏 ∈ ( Base ‘ 𝑆 ) ∀ 𝑐 ∈ ( Base ‘ 𝑆 ) ( ( 𝑎 ( +g ‘ 𝑆 ) 𝑏 ) ( +g ‘ 𝑆 ) 𝑐 ) = ( 𝑎 ( +g ‘ 𝑆 ) ( 𝑏 ( +g ‘ 𝑆 ) 𝑐 ) ) ) )
37 7 35 36 mpbir2an ⊢ 𝑆 ∈ Smgrp