smndex1mgm

Description: The monoid of endofunctions on NN0 restricted to the modulo function I and the constant functions ( GK ) is a magma. (Contributed by AV, 14-Feb-2024)

	Ref	Expression
Hypotheses	smndex1ibas.m	No typesetting found for \|- M = ( EndoFMnd ` NN0 ) with typecode \|-
	smndex1ibas.n	$⊢ N \in ℕ$
	smndex1ibas.i	$⊢ I = (x \in ℕ_{0} ⟼ x \mod N)$
	smndex1ibas.g	$⊢ G = (n \in (0 ..^N) ⟼ (x \in ℕ_{0} ⟼ n))$
	smndex1mgm.b	$⊢ B = \{I\} \cup ⋃_{n \in (0 ..^N)} \{G (n)\}$
	smndex1mgm.s	$⊢ S = M ↾_{𝑠} B$
Assertion	smndex1mgm	$⊢ S \in Mgm$

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	Could not format M = ( EndoFMnd ` NN0 ) : No typesetting found for \|- M = ( EndoFMnd ` NN0 ) with typecode \|-
2		smndex1ibas.n	$⊢ N \in ℕ$
3		smndex1ibas.i	$⊢ I = (x \in ℕ_{0} ⟼ x \mod N)$
4		smndex1ibas.g	$⊢ G = (n \in (0 ..^N) ⟼ (x \in ℕ_{0} ⟼ n))$
5		smndex1mgm.b	$⊢ B = \{I\} \cup ⋃_{n \in (0 ..^N)} \{G (n)\}$
6		smndex1mgm.s	$⊢ S = M ↾_{𝑠} B$
7	1 2 3 4 5	smndex1basss	$⊢ B \subseteq {Base}_{M}$
8		ssel	$⊢ B \subseteq {Base}_{M} \to (a \in B \to a \in {Base}_{M})$
9		ssel	$⊢ B \subseteq {Base}_{M} \to (b \in B \to b \in {Base}_{M})$
10	8 9	anim12d	$⊢ B \subseteq {Base}_{M} \to ((a \in B \land b \in B) \to (a \in {Base}_{M} \land b \in {Base}_{M}))$
11	7 10	ax-mp	$⊢ (a \in B \land b \in B) \to (a \in {Base}_{M} \land b \in {Base}_{M})$
12		eqid	$⊢ {Base}_{M} = {Base}_{M}$
13		eqid	$⊢ +_{M} = +_{M}$
14	1 12 13	efmndov	$⊢ (a \in {Base}_{M} \land b \in {Base}_{M}) \to a +_{M} b = a \circ b$
15	11 14	syl	$⊢ (a \in B \land b \in B) \to a +_{M} b = a \circ b$
16		simpl	$⊢ (a = I \land b = I) \to a = I$
17		simpr	$⊢ (a = I \land b = I) \to b = I$
18	16 17	coeq12d	$⊢ (a = I \land b = I) \to a \circ b = I \circ I$
19	1 2 3	smndex1iidm	$⊢ I \circ I = I$
20	18 19	eqtrdi	$⊢ (a = I \land b = I) \to a \circ b = I$
21	20	orcd	$⊢ (a = I \land b = I) \to (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k))$
22	21	ex	$⊢ a = I \to (b = I \to (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k)))$
23		simpll	$⊢ ((a = I \land k \in (0 ..^N)) \land b = G (k)) \to a = I$
24		simpr	$⊢ ((a = I \land k \in (0 ..^N)) \land b = G (k)) \to b = G (k)$
25	23 24	coeq12d	$⊢ ((a = I \land k \in (0 ..^N)) \land b = G (k)) \to a \circ b = I \circ G (k)$
26	1 2 3 4	smndex1igid	$⊢ k \in (0 ..^N) \to I \circ G (k) = G (k)$
27	26	ad2antlr	$⊢ ((a = I \land k \in (0 ..^N)) \land b = G (k)) \to I \circ G (k) = G (k)$
28	25 27	eqtrd	$⊢ ((a = I \land k \in (0 ..^N)) \land b = G (k)) \to a \circ b = G (k)$
29	28	ex	$⊢ (a = I \land k \in (0 ..^N)) \to (b = G (k) \to a \circ b = G (k))$
30	29	reximdva	$⊢ a = I \to (\exists k \in (0 ..^N) b = G (k) \to \exists k \in (0 ..^N) a \circ b = G (k))$
31	30	imp	$⊢ (a = I \land \exists k \in (0 ..^N) b = G (k)) \to \exists k \in (0 ..^N) a \circ b = G (k)$
32	31	olcd	$⊢ (a = I \land \exists k \in (0 ..^N) b = G (k)) \to (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k))$
33	32	ex	$⊢ a = I \to (\exists k \in (0 ..^N) b = G (k) \to (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k)))$
34	22 33	jaod	$⊢ a = I \to ((b = I \lor \exists k \in (0 ..^N) b = G (k)) \to (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k)))$
35		simpr	$⊢ ((b = I \land k \in (0 ..^N)) \land a = G (k)) \to a = G (k)$
36		simpll	$⊢ ((b = I \land k \in (0 ..^N)) \land a = G (k)) \to b = I$
37	35 36	coeq12d	$⊢ ((b = I \land k \in (0 ..^N)) \land a = G (k)) \to a \circ b = G (k) \circ I$
38	1 2 3	smndex1ibas	$⊢ I \in {Base}_{M}$
39	1 2 3 4	smndex1gid	$⊢ (I \in {Base}_{M} \land k \in (0 ..^N)) \to G (k) \circ I = G (k)$
40	38 39	mpan	$⊢ k \in (0 ..^N) \to G (k) \circ I = G (k)$
41	40	ad2antlr	$⊢ ((b = I \land k \in (0 ..^N)) \land a = G (k)) \to G (k) \circ I = G (k)$
42	37 41	eqtrd	$⊢ ((b = I \land k \in (0 ..^N)) \land a = G (k)) \to a \circ b = G (k)$
43	42	ex	$⊢ (b = I \land k \in (0 ..^N)) \to (a = G (k) \to a \circ b = G (k))$
44	43	reximdva	$⊢ b = I \to (\exists k \in (0 ..^N) a = G (k) \to \exists k \in (0 ..^N) a \circ b = G (k))$
45	44	imp	$⊢ (b = I \land \exists k \in (0 ..^N) a = G (k)) \to \exists k \in (0 ..^N) a \circ b = G (k)$
46	45	olcd	$⊢ (b = I \land \exists k \in (0 ..^N) a = G (k)) \to (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k))$
47	46	expcom	$⊢ \exists k \in (0 ..^N) a = G (k) \to (b = I \to (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k)))$
48		fveq2	$⊢ k = m \to G (k) = G (m)$
49	48	eqeq2d	$⊢ k = m \to (b = G (k) \leftrightarrow b = G (m))$
50	49	cbvrexvw	$⊢ \exists k \in (0 ..^N) b = G (k) \leftrightarrow \exists m \in (0 ..^N) b = G (m)$
51		simpr	$⊢ (((m \in (0 ..^N) \land b = G (m)) \land k \in (0 ..^N)) \land a = G (k)) \to a = G (k)$
52		simpllr	$⊢ (((m \in (0 ..^N) \land b = G (m)) \land k \in (0 ..^N)) \land a = G (k)) \to b = G (m)$
53	51 52	coeq12d	$⊢ (((m \in (0 ..^N) \land b = G (m)) \land k \in (0 ..^N)) \land a = G (k)) \to a \circ b = G (k) \circ G (m)$
54	1 2 3 4	smndex1gbas	$⊢ m \in (0 ..^N) \to G (m) \in {Base}_{M}$
55	1 2 3 4	smndex1gid	$⊢ (G (m) \in {Base}_{M} \land k \in (0 ..^N)) \to G (k) \circ G (m) = G (k)$
56	54 55	sylan	$⊢ (m \in (0 ..^N) \land k \in (0 ..^N)) \to G (k) \circ G (m) = G (k)$
57	56	ad4ant13	$⊢ (((m \in (0 ..^N) \land b = G (m)) \land k \in (0 ..^N)) \land a = G (k)) \to G (k) \circ G (m) = G (k)$
58	53 57	eqtrd	$⊢ (((m \in (0 ..^N) \land b = G (m)) \land k \in (0 ..^N)) \land a = G (k)) \to a \circ b = G (k)$
59	58	ex	$⊢ ((m \in (0 ..^N) \land b = G (m)) \land k \in (0 ..^N)) \to (a = G (k) \to a \circ b = G (k))$
60	59	reximdva	$⊢ (m \in (0 ..^N) \land b = G (m)) \to (\exists k \in (0 ..^N) a = G (k) \to \exists k \in (0 ..^N) a \circ b = G (k))$
61	60	rexlimiva	$⊢ \exists m \in (0 ..^N) b = G (m) \to (\exists k \in (0 ..^N) a = G (k) \to \exists k \in (0 ..^N) a \circ b = G (k))$
62	61	imp	$⊢ (\exists m \in (0 ..^N) b = G (m) \land \exists k \in (0 ..^N) a = G (k)) \to \exists k \in (0 ..^N) a \circ b = G (k)$
63	62	olcd	$⊢ (\exists m \in (0 ..^N) b = G (m) \land \exists k \in (0 ..^N) a = G (k)) \to (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k))$
64	63	expcom	$⊢ \exists k \in (0 ..^N) a = G (k) \to (\exists m \in (0 ..^N) b = G (m) \to (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k)))$
65	50 64	biimtrid	$⊢ \exists k \in (0 ..^N) a = G (k) \to (\exists k \in (0 ..^N) b = G (k) \to (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k)))$
66	47 65	jaod	$⊢ \exists k \in (0 ..^N) a = G (k) \to ((b = I \lor \exists k \in (0 ..^N) b = G (k)) \to (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k)))$
67	34 66	jaoi	$⊢ (a = I \lor \exists k \in (0 ..^N) a = G (k)) \to ((b = I \lor \exists k \in (0 ..^N) b = G (k)) \to (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k)))$
68	67	imp	$⊢ ((a = I \lor \exists k \in (0 ..^N) a = G (k)) \land (b = I \lor \exists k \in (0 ..^N) b = G (k))) \to (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k))$
69	5	eleq2i	$⊢ a \in B \leftrightarrow a \in (\{I\} \cup ⋃_{n \in (0 ..^N)} \{G (n)\})$
70		fveq2	$⊢ n = k \to G (n) = G (k)$
71	70	sneqd	$⊢ n = k \to \{G (n)\} = \{G (k)\}$
72	71	cbviunv	$⊢ ⋃_{n \in (0 ..^N)} \{G (n)\} = ⋃_{k \in (0 ..^N)} \{G (k)\}$
73	72	uneq2i	$⊢ \{I\} \cup ⋃_{n \in (0 ..^N)} \{G (n)\} = \{I\} \cup ⋃_{k \in (0 ..^N)} \{G (k)\}$
74	73	eleq2i	$⊢ a \in (\{I\} \cup ⋃_{n \in (0 ..^N)} \{G (n)\}) \leftrightarrow a \in (\{I\} \cup ⋃_{k \in (0 ..^N)} \{G (k)\})$
75	69 74	bitri	$⊢ a \in B \leftrightarrow a \in (\{I\} \cup ⋃_{k \in (0 ..^N)} \{G (k)\})$
76		elun	$⊢ a \in (\{I\} \cup ⋃_{k \in (0 ..^N)} \{G (k)\}) \leftrightarrow (a \in \{I\} \lor a \in ⋃_{k \in (0 ..^N)} \{G (k)\})$
77		velsn	$⊢ a \in \{I\} \leftrightarrow a = I$
78		eliun	$⊢ a \in ⋃_{k \in (0 ..^N)} \{G (k)\} \leftrightarrow \exists k \in (0 ..^N) a \in \{G (k)\}$
79		velsn	$⊢ a \in \{G (k)\} \leftrightarrow a = G (k)$
80	79	rexbii	$⊢ \exists k \in (0 ..^N) a \in \{G (k)\} \leftrightarrow \exists k \in (0 ..^N) a = G (k)$
81	78 80	bitri	$⊢ a \in ⋃_{k \in (0 ..^N)} \{G (k)\} \leftrightarrow \exists k \in (0 ..^N) a = G (k)$
82	77 81	orbi12i	$⊢ (a \in \{I\} \lor a \in ⋃_{k \in (0 ..^N)} \{G (k)\}) \leftrightarrow (a = I \lor \exists k \in (0 ..^N) a = G (k))$
83	75 76 82	3bitri	$⊢ a \in B \leftrightarrow (a = I \lor \exists k \in (0 ..^N) a = G (k))$
84	5	eleq2i	$⊢ b \in B \leftrightarrow b \in (\{I\} \cup ⋃_{n \in (0 ..^N)} \{G (n)\})$
85	73	eleq2i	$⊢ b \in (\{I\} \cup ⋃_{n \in (0 ..^N)} \{G (n)\}) \leftrightarrow b \in (\{I\} \cup ⋃_{k \in (0 ..^N)} \{G (k)\})$
86	84 85	bitri	$⊢ b \in B \leftrightarrow b \in (\{I\} \cup ⋃_{k \in (0 ..^N)} \{G (k)\})$
87		elun	$⊢ b \in (\{I\} \cup ⋃_{k \in (0 ..^N)} \{G (k)\}) \leftrightarrow (b \in \{I\} \lor b \in ⋃_{k \in (0 ..^N)} \{G (k)\})$
88		velsn	$⊢ b \in \{I\} \leftrightarrow b = I$
89		eliun	$⊢ b \in ⋃_{k \in (0 ..^N)} \{G (k)\} \leftrightarrow \exists k \in (0 ..^N) b \in \{G (k)\}$
90		velsn	$⊢ b \in \{G (k)\} \leftrightarrow b = G (k)$
91	90	rexbii	$⊢ \exists k \in (0 ..^N) b \in \{G (k)\} \leftrightarrow \exists k \in (0 ..^N) b = G (k)$
92	89 91	bitri	$⊢ b \in ⋃_{k \in (0 ..^N)} \{G (k)\} \leftrightarrow \exists k \in (0 ..^N) b = G (k)$
93	88 92	orbi12i	$⊢ (b \in \{I\} \lor b \in ⋃_{k \in (0 ..^N)} \{G (k)\}) \leftrightarrow (b = I \lor \exists k \in (0 ..^N) b = G (k))$
94	86 87 93	3bitri	$⊢ b \in B \leftrightarrow (b = I \lor \exists k \in (0 ..^N) b = G (k))$
95	83 94	anbi12i	$⊢ (a \in B \land b \in B) \leftrightarrow ((a = I \lor \exists k \in (0 ..^N) a = G (k)) \land (b = I \lor \exists k \in (0 ..^N) b = G (k)))$
96	5	eleq2i	$⊢ a \circ b \in B \leftrightarrow a \circ b \in (\{I\} \cup ⋃_{n \in (0 ..^N)} \{G (n)\})$
97	73	eleq2i	$⊢ a \circ b \in (\{I\} \cup ⋃_{n \in (0 ..^N)} \{G (n)\}) \leftrightarrow a \circ b \in (\{I\} \cup ⋃_{k \in (0 ..^N)} \{G (k)\})$
98	96 97	bitri	$⊢ a \circ b \in B \leftrightarrow a \circ b \in (\{I\} \cup ⋃_{k \in (0 ..^N)} \{G (k)\})$
99		elun	$⊢ a \circ b \in (\{I\} \cup ⋃_{k \in (0 ..^N)} \{G (k)\}) \leftrightarrow (a \circ b \in \{I\} \lor a \circ b \in ⋃_{k \in (0 ..^N)} \{G (k)\})$
100		vex	$⊢ a \in V$
101		vex	$⊢ b \in V$
102	100 101	coex	$⊢ a \circ b \in V$
103	102	elsn	$⊢ a \circ b \in \{I\} \leftrightarrow a \circ b = I$
104		eliun	$⊢ a \circ b \in ⋃_{k \in (0 ..^N)} \{G (k)\} \leftrightarrow \exists k \in (0 ..^N) a \circ b \in \{G (k)\}$
105	102	elsn	$⊢ a \circ b \in \{G (k)\} \leftrightarrow a \circ b = G (k)$
106	105	rexbii	$⊢ \exists k \in (0 ..^N) a \circ b \in \{G (k)\} \leftrightarrow \exists k \in (0 ..^N) a \circ b = G (k)$
107	104 106	bitri	$⊢ a \circ b \in ⋃_{k \in (0 ..^N)} \{G (k)\} \leftrightarrow \exists k \in (0 ..^N) a \circ b = G (k)$
108	103 107	orbi12i	$⊢ (a \circ b \in \{I\} \lor a \circ b \in ⋃_{k \in (0 ..^N)} \{G (k)\}) \leftrightarrow (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k))$
109	98 99 108	3bitri	$⊢ a \circ b \in B \leftrightarrow (a \circ b = I \lor \exists k \in (0 ..^N) a \circ b = G (k))$
110	68 95 109	3imtr4i	$⊢ (a \in B \land b \in B) \to a \circ b \in B$
111	15 110	eqeltrd	$⊢ (a \in B \land b \in B) \to a +_{M} b \in B$
112	111	rgen2	$⊢ \forall a \in B \forall b \in B a +_{M} b \in B$
113	6	ovexi	$⊢ S \in V$
114	1 2 3 4 5 6	smndex1bas	$⊢ {Base}_{S} = B$
115	114	eqcomi	$⊢ B = {Base}_{S}$
116	115	fvexi	$⊢ B \in V$
117	6 13	ressplusg	$⊢ B \in V \to +_{M} = +_{S}$
118	116 117	ax-mp	$⊢ +_{M} = +_{S}$
119	115 118	ismgm	$⊢ S \in V \to (S \in Mgm \leftrightarrow \forall a \in B \forall b \in B a +_{M} b \in B)$
120	113 119	ax-mp	$⊢ S \in Mgm \leftrightarrow \forall a \in B \forall b \in B a +_{M} b \in B$
121	112 120	mpbir	$⊢ S \in Mgm$

Metamath Proof Explorer

Theorem smndex1mgm

Proof