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