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	\|- M = ( EndoFMnd ` NN0 )
	smndex1ibas.n	\|- N e. NN
	smndex1ibas.i	\|- I = ( x e. NN0 \|-> ( x mod N ) )
	smndex1ibas.g	\|- G = ( n e. ( 0 ..^ N ) \|-> ( x e. NN0 \|-> n ) )
	smndex1mgm.b	\|- B = ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
	smndex1mgm.s	\|- S = ( M \|`s B )
Assertion	smndex1mnd	\|- S e. Mnd

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	\|- M = ( EndoFMnd ` NN0 )
2		smndex1ibas.n	\|- N e. NN
3		smndex1ibas.i	\|- I = ( x e. NN0 \|-> ( x mod N ) )
4		smndex1ibas.g	\|- G = ( n e. ( 0 ..^ N ) \|-> ( x e. NN0 \|-> n ) )
5		smndex1mgm.b	\|- B = ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
6		smndex1mgm.s	\|- S = ( M \|`s B )
7	1 2 3 4 5 6	smndex1sgrp	\|- S e. Smgrp
8		nn0ex	\|- NN0 e. _V
9	8	mptex	\|- ( x e. NN0 \|-> ( x mod N ) ) e. _V
10	3 9	eqeltri	\|- I e. _V
11	10	snid	\|- I e. { I }
12		elun1	\|- ( I e. { I } -> I e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) )
13	11 12	ax-mp	\|- I e. ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } )
14	13 5	eleqtrri	\|- I e. B
15		id	\|- ( I e. B -> I e. B )
16		coeq1	\|- ( a = I -> ( a o. b ) = ( I o. b ) )
17	16	eqeq1d	\|- ( a = I -> ( ( a o. b ) = b <-> ( I o. b ) = b ) )
18		coeq2	\|- ( a = I -> ( b o. a ) = ( b o. I ) )
19	18	eqeq1d	\|- ( a = I -> ( ( b o. a ) = b <-> ( b o. I ) = b ) )
20	17 19	anbi12d	\|- ( a = I -> ( ( ( a o. b ) = b /\ ( b o. a ) = b ) <-> ( ( I o. b ) = b /\ ( b o. I ) = b ) ) )
21	20	ralbidv	\|- ( a = I -> ( A. b e. B ( ( a o. b ) = b /\ ( b o. a ) = b ) <-> A. b e. B ( ( I o. b ) = b /\ ( b o. I ) = b ) ) )
22	21	adantl	\|- ( ( I e. B /\ a = I ) -> ( A. b e. B ( ( a o. b ) = b /\ ( b o. a ) = b ) <-> A. b e. B ( ( I o. b ) = b /\ ( b o. I ) = b ) ) )
23	1 2 3 4 5 6	smndex1mndlem	\|- ( b e. B -> ( ( I o. b ) = b /\ ( b o. I ) = b ) )
24	23	rgen	\|- A. b e. B ( ( I o. b ) = b /\ ( b o. I ) = b )
25	24	a1i	\|- ( I e. B -> A. b e. B ( ( I o. b ) = b /\ ( b o. I ) = b ) )
26	15 22 25	rspcedvd	\|- ( I e. B -> E. a e. B A. b e. B ( ( a o. b ) = b /\ ( b o. a ) = b ) )
27	14 26	ax-mp	\|- E. a e. B A. b e. B ( ( a o. b ) = b /\ ( b o. a ) = b )
28	1 2 3 4 5	smndex1basss	\|- B C_ ( Base ` M )
29		ssel	\|- ( B C_ ( Base ` M ) -> ( a e. B -> a e. ( Base ` M ) ) )
30		ssel	\|- ( B C_ ( Base ` M ) -> ( b e. B -> b e. ( Base ` M ) ) )
31	29 30	anim12d	\|- ( B C_ ( Base ` M ) -> ( ( a e. B /\ b e. B ) -> ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) ) )
32	28 31	ax-mp	\|- ( ( a e. B /\ b e. B ) -> ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) )
33		eqid	\|- ( Base ` M ) = ( Base ` M )
34		snex	\|- { I } e. _V
35		ovex	\|- ( 0 ..^ N ) e. _V
36		snex	\|- { ( G ` n ) } e. _V
37	35 36	iunex	\|- U_ n e. ( 0 ..^ N ) { ( G ` n ) } e. _V
38	34 37	unex	\|- ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) e. _V
39	5 38	eqeltri	\|- B e. _V
40		eqid	\|- ( +g ` M ) = ( +g ` M )
41	6 40	ressplusg	\|- ( B e. _V -> ( +g ` M ) = ( +g ` S ) )
42	39 41	ax-mp	\|- ( +g ` M ) = ( +g ` S )
43	42	eqcomi	\|- ( +g ` S ) = ( +g ` M )
44	1 33 43	efmndov	\|- ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( a ( +g ` S ) b ) = ( a o. b ) )
45	44	eqeq1d	\|- ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( ( a ( +g ` S ) b ) = b <-> ( a o. b ) = b ) )
46	43	oveqi	\|- ( b ( +g ` S ) a ) = ( b ( +g ` M ) a )
47	1 33 40	efmndov	\|- ( ( b e. ( Base ` M ) /\ a e. ( Base ` M ) ) -> ( b ( +g ` M ) a ) = ( b o. a ) )
48	47	ancoms	\|- ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( b ( +g ` M ) a ) = ( b o. a ) )
49	46 48	eqtrid	\|- ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( b ( +g ` S ) a ) = ( b o. a ) )
50	49	eqeq1d	\|- ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( ( b ( +g ` S ) a ) = b <-> ( b o. a ) = b ) )
51	45 50	anbi12d	\|- ( ( a e. ( Base ` M ) /\ b e. ( Base ` M ) ) -> ( ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b ) <-> ( ( a o. b ) = b /\ ( b o. a ) = b ) ) )
52	32 51	syl	\|- ( ( a e. B /\ b e. B ) -> ( ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b ) <-> ( ( a o. b ) = b /\ ( b o. a ) = b ) ) )
53	52	ralbidva	\|- ( a e. B -> ( A. b e. B ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b ) <-> A. b e. B ( ( a o. b ) = b /\ ( b o. a ) = b ) ) )
54	53	rexbiia	\|- ( E. a e. B A. b e. B ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b ) <-> E. a e. B A. b e. B ( ( a o. b ) = b /\ ( b o. a ) = b ) )
55	27 54	mpbir	\|- E. a e. B A. b e. B ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b )
56	1 2 3 4 5 6	smndex1bas	\|- ( Base ` S ) = B
57	56	eqcomi	\|- B = ( Base ` S )
58		eqid	\|- ( +g ` S ) = ( +g ` S )
59	57 58	ismnddef	\|- ( S e. Mnd <-> ( S e. Smgrp /\ E. a e. B A. b e. B ( ( a ( +g ` S ) b ) = b /\ ( b ( +g ` S ) a ) = b ) ) )
60	7 55 59	mpbir2an	\|- S e. Mnd

Metamath Proof Explorer

Theorem smndex1mnd

Proof