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	syl5eq	⊢ ( ( 𝑥 ∈ ( 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