P. 188 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18701-18800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	submss 18701	Submonoids are subsets of the base set. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 ⊆ 𝐵)
Theorem	submid 18702	Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mnd → 𝐵 ∈ (SubMnd‘𝑀))
Theorem	subm0cl 18703	Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 0 = (0g‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 ∈ 𝑆)
Theorem	submcl 18704	Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑆 ∈ (SubMnd‘𝑀) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆)
Theorem	submmnd 18705	Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝐻 ∈ Mnd)
Theorem	submbas 18706	The base set of a submonoid. (Contributed by Stefan O'Rear, 15-Jun-2015.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 = (Base‘𝐻))
Theorem	subm0 18707	Submonoids have the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    &   ⊢ 0 = (0g‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 = (0g‘𝐻))
Theorem	subsubm 18708	A submonoid of a submonoid is a submonoid. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝐺) → (𝐴 ∈ (SubMnd‘𝐻) ↔ (𝐴 ∈ (SubMnd‘𝐺) ∧ 𝐴 ⊆ 𝑆)))
Theorem	0subm 18709	The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → { 0 } ∈ (SubMnd‘𝐺))
Theorem	insubm 18710	The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024.)
⊢ ((𝐴 ∈ (SubMnd‘𝑀) ∧ 𝐵 ∈ (SubMnd‘𝑀)) → (𝐴 ∩ 𝐵) ∈ (SubMnd‘𝑀))
Theorem	0mhm 18711	The constant zero linear function between two monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 0 = (0g‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) → (𝐵 × { 0 }) ∈ (𝑀 MndHom 𝑁))
Theorem	resmhm 18712	Restriction of a monoid homomorphism to a submonoid is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MndHom 𝑇))
Theorem	resmhm2 18713	One direction of resmhm2b 18714. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → 𝐹 ∈ (𝑆 MndHom 𝑇))
Theorem	resmhm2b 18714	Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ (𝑆 MndHom 𝑈)))
Theorem	mhmco 18715	The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐹 ∈ (𝑇 MndHom 𝑈) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 MndHom 𝑈))
Theorem	mhmimalem 18716*	Lemma for mhmima 18717 and similar theorems, formerly part of proof for mhmima 18717. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 16-Feb-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑀 MndHom 𝑁))    &   ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝑀))    &   ⊢ (𝜑 → ⊕ = (+g‘𝑀))    &   ⊢ (𝜑 → + = (+g‘𝑁))    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧 ⊕ 𝑥) ∈ 𝑋)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥 + 𝑦) ∈ (𝐹 “ 𝑋))
Theorem	mhmima 18717	The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015.) (Proof shortened by AV, 8-Mar-2025.)
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (SubMnd‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubMnd‘𝑁))
Theorem	mhmeql 18718	The equalizer of two monoid homomorphisms is a submonoid. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubMnd‘𝑆))
Theorem	submacs 18719	Submonoids are an algebraic closure system. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → (SubMnd‘𝐺) ∈ (ACS‘𝐵))
Theorem	mndind 18720*	Induction in a monoid. In this theorem, 𝜓(𝑥) is the "generic" proposition to be be proved (the first four hypotheses tell its values at y, y+z, 0, A respectively). The two induction hypotheses mndind.i1 and mndind.i2 tell that it is true at 0, that if it is true at y then it is true at y+z (provided z is in 𝐺). The hypothesis mndind.k tells that 𝐺 is generating. (Contributed by SO, 14-Jul-2018.)
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑥 = (𝑦 + 𝑧) → (𝜓 ↔ 𝜃))    &   ⊢ (𝑥 = 0 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂))    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝐺 ⊆ 𝐵)    &   ⊢ (𝜑 → 𝐵 = ((mrCls‘(SubMnd‘𝑀))‘𝐺))    &   ⊢ (𝜑 → 𝜏)    &   ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐺) ∧ 𝜒) → 𝜃)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝜂)
Theorem	prdspjmhm 18721*	A projection from a product of monoids to one of the factors is a monoid homomorphism. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑌 MndHom (𝑅‘𝐴)))
Theorem	pwspjmhm 18722*	A projection from a structure power of a monoid to the monoid itself is a monoid homomorphism. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑌 MndHom 𝑅))
Theorem	pwsdiagmhm 18723*	Diagonal monoid homomorphism into a structure power. (Contributed by Stefan O'Rear, 12-Mar-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 MndHom 𝑌))
Theorem	pwsco1mhm 18724*	Right composition with a function on the index sets yields a monoid homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐴)    &   ⊢ 𝑍 = (𝑅 ↑s 𝐵)    &   ⊢ 𝐶 = (Base‘𝑍)    &   ⊢ (𝜑 → 𝑅 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)    ⇒   ⊢ (𝜑 → (𝑔 ∈ 𝐶 ↦ (𝑔 ∘ 𝐹)) ∈ (𝑍 MndHom 𝑌))
Theorem	pwsco2mhm 18725*	Left composition with a monoid homomorphism yields a monoid homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐴)    &   ⊢ 𝑍 = (𝑆 ↑s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ (𝑅 MndHom 𝑆))    ⇒   ⊢ (𝜑 → (𝑔 ∈ 𝐵 ↦ (𝐹 ∘ 𝑔)) ∈ (𝑌 MndHom 𝑍))
10.1.8  Iterated sums in a monoid One important use of words is as formal composites in cases where order is significant, using the general sum operator df-gsum 17364. If order is not significant, it is simpler to use families instead.
Theorem	gsumvallem2 18726*	Lemma for properties of the set of identities of 𝐺. The set of identities of a monoid is exactly the unique identity element. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑂 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}    ⇒   ⊢ (𝐺 ∈ Mnd → 𝑂 = { 0 })
Theorem	gsumsubm 18727	Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))
Theorem	gsumz 18728*	Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 )
Theorem	gsumwsubmcl 18729	Closure of the composite in any submonoid. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.)
⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑊 ∈ Word 𝑆) → (𝐺 Σg 𝑊) ∈ 𝑆)
Theorem	gsumws1 18730	A singleton composite recovers the initial symbol. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑆 ∈ 𝐵 → (𝐺 Σg ⟨“𝑆”⟩) = 𝑆)
Theorem	gsumwcl 18731	Closure of the composite of a word in a structure 𝐺. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵)
Theorem	gsumsgrpccat 18732	Homomorphic property of not empty composites of a group sum over a semigroup. Formerly part of proof for gsumccat 18733. (Contributed by AV, 26-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
Theorem	gsumccat 18733	Homomorphic property of composites. Second formula in [Lang] p. 4. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 26-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
Theorem	gsumws2 18734	Valuation of a pair in a monoid. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ∈ 𝐵 ∧ 𝑇 ∈ 𝐵) → (𝐺 Σg ⟨“𝑆𝑇”⟩) = (𝑆 + 𝑇))
Theorem	gsumccatsn 18735	Homomorphic property of composites with a singleton. (Contributed by AV, 20-Jan-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ ⟨“𝑍”⟩)) = ((𝐺 Σg 𝑊) + 𝑍))
Theorem	gsumspl 18736	The primary purpose of the splice construction is to enable local rewrites. Thus, in any monoidal valuation, if a splice does not cause a local change it does not cause a global change. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝑆 ∈ Word 𝐵)    &   ⊢ (𝜑 → 𝐹 ∈ (0...𝑇))    &   ⊢ (𝜑 → 𝑇 ∈ (0...(♯‘𝑆)))    &   ⊢ (𝜑 → 𝑋 ∈ Word 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ Word 𝐵)    &   ⊢ (𝜑 → (𝑀 Σg 𝑋) = (𝑀 Σg 𝑌))    ⇒   ⊢ (𝜑 → (𝑀 Σg (𝑆 splice ⟨𝐹, 𝑇, 𝑋⟩)) = (𝑀 Σg (𝑆 splice ⟨𝐹, 𝑇, 𝑌⟩)))
Theorem	gsumwmhm 18737	Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊)))
Theorem	gsumwspan 18738*	The submonoid generated by a set of elements is precisely the set of elements which can be expressed as finite products of the generator. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝐾 = (mrCls‘(SubMnd‘𝑀))    ⇒   ⊢ ((𝑀 ∈ Mnd ∧ 𝐺 ⊆ 𝐵) → (𝐾‘𝐺) = ran (𝑤 ∈ Word 𝐺 ↦ (𝑀 Σg 𝑤)))
10.1.9  Free monoids
Syntax	cfrmd 18739	Extend class definition with the free monoid construction.
class freeMnd
Syntax	cvrmd 18740	Extend class notation with free monoid injection.
class varFMnd
Definition	df-frmd 18741	Define a free monoid over a set 𝑖 of generators, defined as the set of finite strings on 𝐼 with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ freeMnd = (𝑖 ∈ V ↦ {⟨(Base‘ndx), Word 𝑖⟩, ⟨(+g‘ndx), ( ++ ↾ (Word 𝑖 × Word 𝑖))⟩})
Definition	df-vrmd 18742*	Define a free monoid over a set 𝑖 of generators, defined as the set of finite strings on 𝐼 with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ varFMnd = (𝑖 ∈ V ↦ (𝑗 ∈ 𝑖 ↦ ⟨“𝑗”⟩))
Theorem	frmdval 18743	Value of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼)    &   ⊢ + = ( ++ ↾ (𝐵 × 𝐵))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩})
Theorem	frmdbas 18744	The base set of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼)
Theorem	frmdelbas 18745	An element of the base set of a free monoid is a string on the generators. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑋 ∈ 𝐵 → 𝑋 ∈ Word 𝐼)
Theorem	frmdplusg 18746	The monoid operation of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) (Proof shortened by AV, 6-Nov-2024.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ + = ( ++ ↾ (𝐵 × 𝐵))
Theorem	frmdadd 18747	Value of the monoid operation of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ++ 𝑌))
Theorem	vrmdfval 18748*	The canonical injection from the generating set 𝐼 to the base set of the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑈 = (𝑗 ∈ 𝐼 ↦ ⟨“𝑗”⟩))
Theorem	vrmdval 18749	The value of the generating elements of a free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = ⟨“𝐴”⟩)
Theorem	vrmdf 18750	The mapping from the index set to the generators is a function into the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑈:𝐼⟶Word 𝐼)
Theorem	frmdmnd 18751	A free monoid is a monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd)
Theorem	frmd0 18752	The identity of the free monoid is the empty word. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    ⇒   ⊢ ∅ = (0g‘𝑀)
Theorem	frmdsssubm 18753	The set of words taking values in a subset is a (free) submonoid of the free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼) → Word 𝐽 ∈ (SubMnd‘𝑀))
Theorem	frmdgsum 18754	Any word in a free monoid can be expressed as the sum of the singletons composing it. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐼) → (𝑀 Σg (𝑈 ∘ 𝑊)) = 𝑊)
Theorem	frmdss2 18755	A subset of generators is contained in a submonoid iff the set of words on the generators is in the submonoid. This can be viewed as an elementary way of saying "the monoidal closure of 𝐽 is Word 𝐽". (Contributed by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ⊆ 𝐼 ∧ 𝐴 ∈ (SubMnd‘𝑀)) → ((𝑈 “ 𝐽) ⊆ 𝐴 ↔ Word 𝐽 ⊆ 𝐴))
Theorem	frmdup1 18756*	Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐸 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥)))    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴:𝐼⟶𝐵)    ⇒   ⊢ (𝜑 → 𝐸 ∈ (𝑀 MndHom 𝐺))
Theorem	frmdup2 18757*	The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐸 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥)))    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴:𝐼⟶𝐵)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐼)    ⇒   ⊢ (𝜑 → (𝐸‘(𝑈‘𝑌)) = (𝐴‘𝑌))
Theorem	frmdup3lem 18758*	Lemma for frmdup3 18759. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → 𝐹 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥))))
Theorem	frmdup3 18759*	Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) → ∃!𝑚 ∈ (𝑀 MndHom 𝐺)(𝑚 ∘ 𝑈) = 𝐴)
10.1.9.1  Monoid of endofunctions According to Wikipedia ("Endomorphism", 25-Jan-2024, https://en.wikipedia.org/wiki/Endomorphism) "An endofunction is a function whose domain is equal to its codomain.". An endofunction is sometimes also called "self-mapping" (see https://www.wikidata.org/wiki/Q1691962) or "self-map" (see https://mathworld.wolfram.com/Self-Map.html), in German "Selbstabbildung" (see https://de.wikipedia.org/wiki/Selbstabbildung).
Syntax	cefmnd 18760	Extend class notation to include the class of monoids of endofunctions.
class EndoFMnd
Definition	df-efmnd 18761*	Define the monoid of endofunctions on set 𝑥. We represent the monoid as the set of functions from 𝑥 to itself ((𝑥 ↑m 𝑥)) under function composition, and topologize it as a function space assuming the set is discrete. Analogous to the former definition of SymGrp, see df-symg 19267 and symgvalstruct 19294. (Contributed by AV, 25-Jan-2024.)
⊢ EndoFMnd = (𝑥 ∈ V ↦ ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
Theorem	efmnd 18762*	The monoid of endofunctions on set 𝐴. (Contributed by AV, 25-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (𝐴 ↑m 𝐴)    &   ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))    &   ⊢ 𝐽 = (∏t‘(𝐴 × {𝒫 𝐴}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
Theorem	efmndbas 18763	The base set of the monoid of endofunctions on class 𝐴. (Contributed by AV, 25-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝐵 = (𝐴 ↑m 𝐴)
Theorem	efmndbasabf 18764*	The base set of the monoid of endofunctions on class 𝐴 is the set of functions from 𝐴 into itself. (Contributed by AV, 29-Mar-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝐵 = {𝑓 ∣ 𝑓:𝐴⟶𝐴}
Theorem	elefmndbas 18765	Two ways of saying a function is a mapping of 𝐴 to itself. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐴))
Theorem	elefmndbas2 18766	Two ways of saying a function is a mapping of 𝐴 to itself. (Contributed by AV, 27-Jan-2024.) (Proof shortened by AV, 29-Mar-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐴))
Theorem	efmndbasf 18767	Elements in the monoid of endofunctions on 𝐴 are functions from 𝐴 into itself. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴⟶𝐴)
Theorem	efmndhash 18768	The monoid of endofunctions on 𝑛 objects has cardinality 𝑛↑𝑛. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → (♯‘𝐵) = ((♯‘𝐴)↑(♯‘𝐴)))
Theorem	efmndbasfi 18769	The monoid of endofunctions on a finite set 𝐴 is finite. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin)
Theorem	efmndfv 18770	The function value of an endofunction. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴)
Theorem	efmndtset 18771	The topology of the monoid of endofunctions on 𝐴. This component is defined on a larger set than the true base - the product topology is defined on the set of all functions, not just endofunctions - but the definition of TopOpen ensures that it is trimmed down before it gets use. (Contributed by AV, 25-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (∏t‘(𝐴 × {𝒫 𝐴})) = (TopSet‘𝐺))
Theorem	efmndplusg 18772*	The group operation of a monoid of endofunctions is the function composition. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))
Theorem	efmndov 18773	The value of the group operation of the monoid of endofunctions on 𝐴. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
Theorem	efmndcl 18774	The group operation of the monoid of endofunctions on 𝐴 is closed. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	efmndtopn 18775	The topology of the monoid of endofunctions on 𝐴. (Contributed by AV, 31-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺))
Theorem	symggrplem 18776*	Lemma for symggrp 19297 and efmndsgrp 18778. Conditions for an operation to be associative. Formerly part of proof for symggrp 19297. (Contributed by AV, 28-Jan-2024.)
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑥 ∘ 𝑦))    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	efmndmgm 18777	The monoid of endofunctions on a class 𝐴 is a magma. (Contributed by AV, 28-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ 𝐺 ∈ Mgm
Theorem	efmndsgrp 18778	The monoid of endofunctions on a class 𝐴 is a semigroup. (Contributed by AV, 28-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ 𝐺 ∈ Smgrp
Theorem	ielefmnd 18779	The identity function restricted to a set 𝐴 is an element of the base set of the monoid of endofunctions on 𝐴. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ (Base‘𝐺))
Theorem	efmndid 18780	The identity function restricted to a set 𝐴 is the identity element of the monoid of endofunctions on 𝐴. (Contributed by AV, 25-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) = (0g‘𝐺))
Theorem	efmndmnd 18781	The monoid of endofunctions on a set 𝐴 is actually a monoid. (Contributed by AV, 31-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd)
Theorem	efmnd0nmnd 18782	Even the monoid of endofunctions on the empty set is actually a monoid. (Contributed by AV, 31-Jan-2024.)
⊢ (EndoFMnd‘∅) ∈ Mnd
Theorem	efmndbas0 18783	The base set of the monoid of endofunctions on the empty set is the singleton containing the empty set. (Contributed by AV, 27-Jan-2024.) (Proof shortened by AV, 31-Mar-2024.)
⊢ (Base‘(EndoFMnd‘∅)) = {∅}
Theorem	efmnd1hash 18784	The monoid of endofunctions on a singleton has cardinality 1. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (♯‘𝐵) = 1)
Theorem	efmnd1bas 18785	The monoid of endofunctions on a singleton consists of the identity only. (Contributed by AV, 31-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼}    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = {{⟨𝐼, 𝐼⟩}})
Theorem	efmnd2hash 18786	The monoid of endofunctions on a (proper) pair has cardinality 4. (Contributed by AV, 18-Feb-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼, 𝐽}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 4)
Theorem	submefmnd 18787*	If the base set of a monoid is contained in the base set of the monoid of endofunctions on a set 𝐴, contains the identity function and has the function composition as group operation, then its base set is a submonoid of the monoid of endofunctions on set 𝐴. Analogous to pgrpsubgsymg 19306. (Contributed by AV, 17-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ 𝐹 = (Base‘𝑆)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (((𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹) ∧ (+g‘𝑆) = (𝑓 ∈ 𝐹, 𝑔 ∈ 𝐹 ↦ (𝑓 ∘ 𝑔))) → 𝐹 ∈ (SubMnd‘𝑀)))
Theorem	sursubmefmnd 18788*	The set of surjective endofunctions on a set 𝐴 is a submonoid of the monoid of endofunctions on 𝐴. (Contributed by AV, 25-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → {ℎ ∣ ℎ:𝐴–onto→𝐴} ∈ (SubMnd‘𝑀))
Theorem	injsubmefmnd 18789*	The set of injective endofunctions on a set 𝐴 is a submonoid of the monoid of endofunctions on 𝐴. (Contributed by AV, 25-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → {ℎ ∣ ℎ:𝐴–1-1→𝐴} ∈ (SubMnd‘𝑀))
Theorem	idressubmefmnd 18790	The singleton containing only the identity function restricted to a set is a submonoid of the monoid of endofunctions on this set. (Contributed by AV, 17-Feb-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → {( I ↾ 𝐴)} ∈ (SubMnd‘𝐺))
Theorem	idresefmnd 18791	The structure with the singleton containing only the identity function restricted to a set 𝐴 as base set and the function composition as group operation, constructed by (structure) restricting the monoid of endofunctions on 𝐴 to that singleton, is a monoid whose base set is a subset of the base set of the monoid of endofunctions on 𝐴. (Contributed by AV, 17-Feb-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐸 = (𝐺 ↾s {( I ↾ 𝐴)})    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐸 ∈ Mnd ∧ (Base‘𝐸) ⊆ (Base‘𝐺)))
Theorem	smndex1ibas 18792	The modulo function 𝐼 is an endofunction on ℕ0. (Contributed by AV, 12-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    ⇒   ⊢ 𝐼 ∈ (Base‘𝑀)
Theorem	smndex1iidm 18793*	The modulo function 𝐼 is idempotent. (Contributed by AV, 12-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    ⇒   ⊢ (𝐼 ∘ 𝐼) = 𝐼
Theorem	smndex1gbas 18794*	The constant functions (𝐺‘𝐾) are endofunctions on ℕ0. (Contributed by AV, 12-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    ⇒   ⊢ (𝐾 ∈ (0..^𝑁) → (𝐺‘𝐾) ∈ (Base‘𝑀))
Theorem	smndex1gid 18795*	The composition of a constant function (𝐺‘𝐾) with another endofunction on ℕ0 results in (𝐺‘𝐾) itself. (Contributed by AV, 14-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    ⇒   ⊢ ((𝐹 ∈ (Base‘𝑀) ∧ 𝐾 ∈ (0..^𝑁)) → ((𝐺‘𝐾) ∘ 𝐹) = (𝐺‘𝐾))
Theorem	smndex1igid 18796*	The composition of the modulo function 𝐼 and a constant function (𝐺‘𝐾) results in (𝐺‘𝐾) itself. (Contributed by AV, 14-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    ⇒   ⊢ (𝐾 ∈ (0..^𝑁) → (𝐼 ∘ (𝐺‘𝐾)) = (𝐺‘𝐾))
Theorem	smndex1basss 18797*	The modulo function 𝐼 and the constant functions (𝐺‘𝐾) are endofunctions on ℕ0. (Contributed by AV, 12-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    ⇒   ⊢ 𝐵 ⊆ (Base‘𝑀)
Theorem	smndex1bas 18798*	The base set of the monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾). (Contributed by AV, 12-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ (Base‘𝑆) = 𝐵
Theorem	smndex1mgm 18799*	The monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾) is a magma. (Contributed by AV, 14-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ 𝑆 ∈ Mgm
Theorem	smndex1sgrp 18800*	The monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾) is a semigroup. (Contributed by AV, 14-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ 𝑆 ∈ Smgrp