P. 182 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18101-18200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	0subm 18101	The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → { 0 } ∈ (SubMnd‘𝐺))
Theorem	insubm 18102	The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024.)
⊢ ((𝐴 ∈ (SubMnd‘𝑀) ∧ 𝐵 ∈ (SubMnd‘𝑀)) → (𝐴 ∩ 𝐵) ∈ (SubMnd‘𝑀))
Theorem	0mhm 18103	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 18104	Restriction of a monoid homomorphism to a submonoid is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MndHom 𝑇))
Theorem	resmhm2 18105	One direction of resmhm2b 18106. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → 𝐹 ∈ (𝑆 MndHom 𝑇))
Theorem	resmhm2b 18106	Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ (𝑆 MndHom 𝑈)))
Theorem	mhmco 18107	The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐹 ∈ (𝑇 MndHom 𝑈) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 MndHom 𝑈))
Theorem	mhmima 18108	The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (SubMnd‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubMnd‘𝑁))
Theorem	mhmeql 18109	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 18110	Submonoids are an algebraic closure system. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → (SubMnd‘𝐺) ∈ (ACS‘𝐵))
Theorem	mndind 18111*	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 18112*	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 18113*	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 18114*	Diagonal monoid homomorphism into a structure power. (Contributed by Stefan O'Rear, 12-Mar-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 MndHom 𝑌))
Theorem	pwsco1mhm 18115*	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 18116*	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.7  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 16822. If order is not significant, it is simpler to use families instead.
Theorem	gsumvallem2 18117*	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 18118	Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))
Theorem	gsumz 18119*	Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 )
Theorem	gsumwsubmcl 18120	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 18121	A singleton composite recovers the initial symbol. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑆 ∈ 𝐵 → (𝐺 Σg ⟨“𝑆”⟩) = 𝑆)
Theorem	gsumwcl 18122	Closure of the composite of a word in a structure 𝐺. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵)
Theorem	gsumsgrpccat 18123	Homomorphic property of not empty composites of a group sum over a semigroup. Formerly part of proof for gsumccat 18125. (Contributed by AV, 26-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
Theorem	gsumccatOLD 18124	Obsolete version of gsumccat 18125 as of 13-Jan-2024. Homomorphic property of composites. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
Theorem	gsumccat 18125	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 18126	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 18127	Homomorphic property of composites with a singleton. (Contributed by AV, 20-Jan-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ ⟨“𝑍”⟩)) = ((𝐺 Σg 𝑊) + 𝑍))
Theorem	gsumspl 18128	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 18129	Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊)))
Theorem	gsumwspan 18130*	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.8  Free monoids
Syntax	cfrmd 18131	Extend class definition with the free monoid construction.
class freeMnd
Syntax	cvrmd 18132	Extend class notation with free monoid injection.
class varFMnd
Definition	df-frmd 18133	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 18134*	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 18135	Value of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼)    &   ⊢ + = ( ++ ↾ (𝐵 × 𝐵))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩})
Theorem	frmdbas 18136	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 18137	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 18138	The monoid operation of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ + = ( ++ ↾ (𝐵 × 𝐵))
Theorem	frmdadd 18139	Value of the monoid operation of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ++ 𝑌))
Theorem	vrmdfval 18140*	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 18141	The value of the generating elements of a free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = ⟨“𝐴”⟩)
Theorem	vrmdf 18142	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 18143	A free monoid is a monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd)
Theorem	frmd0 18144	The identity of the free monoid is the empty word. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    ⇒   ⊢ ∅ = (0g‘𝑀)
Theorem	frmdsssubm 18145	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 18146	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 18147	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 18148*	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 18149*	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 18150*	Lemma for frmdup3 18151. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → 𝐹 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥))))
Theorem	frmdup3 18151*	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.8.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 18152	Extend class notation to include the class of monoids of endofunctions.
class EndoFMnd
Definition	df-efmnd 18153*	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 18617 and symgvalstruct 18646. (Contributed by AV, 25-Jan-2024.)
⊢ EndoFMnd = (𝑥 ∈ V ↦ ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
Theorem	efmnd 18154*	The monoid of endofunctions on set 𝐴. (Contributed by AV, 25-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (𝐴 ↑m 𝐴)    &   ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))    &   ⊢ 𝐽 = (∏t‘(𝐴 × {𝒫 𝐴}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
Theorem	efmndbas 18155	The base set of the monoid of endofunctions on class 𝐴. (Contributed by AV, 25-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝐵 = (𝐴 ↑m 𝐴)
Theorem	efmndbasabf 18156*	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 18157	Two ways of saying a function is a mapping of 𝐴 to itself. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐴))
Theorem	elefmndbas2 18158	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 18159	Elements in the monoid of endofunctions on 𝐴 are functions from 𝐴 into itself. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴⟶𝐴)
Theorem	efmndhash 18160	The monoid of endofunctions on 𝑛 objects has cardinality 𝑛↑𝑛. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → (♯‘𝐵) = ((♯‘𝐴)↑(♯‘𝐴)))
Theorem	efmndbasfi 18161	The monoid of endofunctions on a finite set 𝐴 is finite. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin)
Theorem	efmndfv 18162	The function value of an endofunction. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴)
Theorem	efmndtset 18163	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 18164*	The group operation of a monoid of endofunctions is the function composition. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))
Theorem	efmndov 18165	The value of the group operation of the monoid of endofunctions on 𝐴. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
Theorem	efmndcl 18166	The group operation of the monoid of endofunctions on 𝐴 is closed. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	efmndtopn 18167	The topology of the monoid of endofunctions on 𝐴. (Contributed by AV, 31-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺))
Theorem	symggrplem 18168*	Lemma for symggrp 18649 and efmndsgrp 18170. Conditions for an operation to be associative. Formerly part of proof for symggrp 18649. (Contributed by AV, 28-Jan-2024.)
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑥 ∘ 𝑦))    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	efmndmgm 18169	The monoid of endofunctions on a class 𝐴 is a magma. (Contributed by AV, 28-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ 𝐺 ∈ Mgm
Theorem	efmndsgrp 18170	The monoid of endofunctions on a class 𝐴 is a semigroup. (Contributed by AV, 28-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ 𝐺 ∈ Smgrp
Theorem	ielefmnd 18171	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 18172	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 18173	The monoid of endofunctions on a set 𝐴 is actually a monoid. (Contributed by AV, 31-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd)
Theorem	efmnd0nmnd 18174	Even the monoid of endofunctions on the empty set is actually a monoid. (Contributed by AV, 31-Jan-2024.)
⊢ (EndoFMnd‘∅) ∈ Mnd
Theorem	efmndbas0 18175	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 18176	The monoid of endofunctions on a singleton has cardinality 1. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (♯‘𝐵) = 1)
Theorem	efmnd1bas 18177	The monoid of endofunctions on a singleton consists of the identity only. (Contributed by AV, 31-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼}    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = {{⟨𝐼, 𝐼⟩}})
Theorem	efmnd2hash 18178	The monoid of endofunctions on a (proper) pair has cardinality 4. (Contributed by AV, 18-Feb-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼, 𝐽}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 4)
Theorem	submefmnd 18179*	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 18658. (Contributed by AV, 17-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ 𝐹 = (Base‘𝑆)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (((𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹) ∧ (+g‘𝑆) = (𝑓 ∈ 𝐹, 𝑔 ∈ 𝐹 ↦ (𝑓 ∘ 𝑔))) → 𝐹 ∈ (SubMnd‘𝑀)))
Theorem	sursubmefmnd 18180*	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 18181*	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 18182	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 18183	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 18184	The modulo function 𝐼 is an endofunction on ℕ0. (Contributed by AV, 12-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    ⇒   ⊢ 𝐼 ∈ (Base‘𝑀)
Theorem	smndex1iidm 18185*	The modulo function 𝐼 is idempotent. (Contributed by AV, 12-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    ⇒   ⊢ (𝐼 ∘ 𝐼) = 𝐼
Theorem	smndex1gbas 18186*	The constant functions (𝐺‘𝐾) are endofunctions on ℕ0. (Contributed by AV, 12-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    ⇒   ⊢ (𝐾 ∈ (0..^𝑁) → (𝐺‘𝐾) ∈ (Base‘𝑀))
Theorem	smndex1gid 18187*	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 18188*	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 18189*	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 18190*	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 18191*	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 18192*	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
Theorem	smndex1mndlem 18193*	Lemma for smndex1mnd 18194 and smndex1id 18195. (Contributed by AV, 16-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ (𝑋 ∈ 𝐵 → ((𝐼 ∘ 𝑋) = 𝑋 ∧ (𝑋 ∘ 𝐼) = 𝑋))
Theorem	smndex1mnd 18194*	The monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾) is a monoid. (Contributed by AV, 16-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ 𝑆 ∈ Mnd
Theorem	smndex1id 18195*	The modulo function 𝐼 is the identity of the monoid of endofunctions on ℕ0 restricted to the modulo function 𝐼 and the constant functions (𝐺‘𝐾). (Contributed by AV, 16-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ 𝐼 = (0g‘𝑆)
Theorem	smndex1n0mnd 18196*	The identity of the monoid 𝑀 of endofunctions on set ℕ0 is not contained in the base set of the constructed monoid 𝑆. (Contributed by AV, 17-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ (0g‘𝑀) ∉ 𝐵
Theorem	nsmndex1 18197*	The base set 𝐵 of the constructed monoid 𝑆 is not a submonoid of the monoid 𝑀 of endofunctions on set ℕ0, although 𝑀 ∈ Mnd and 𝑆 ∈ Mnd and 𝐵 ⊆ (Base‘𝑀) hold. (Contributed by AV, 17-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝑁 ∈ ℕ    &   ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁))    &   ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛))    &   ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)})    &   ⊢ 𝑆 = (𝑀 ↾s 𝐵)    ⇒   ⊢ 𝐵 ∉ (SubMnd‘𝑀)
Theorem	smndex2dbas 18198	The doubling function 𝐷 is an endofunction on ℕ0. (Contributed by AV, 18-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2 · 𝑥))    ⇒   ⊢ 𝐷 ∈ 𝐵
Theorem	smndex2dnrinv 18199	The doubling function 𝐷 has no right inverse in the monoid of endofunctions on ℕ0. (Contributed by AV, 18-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2 · 𝑥))    ⇒   ⊢ ∀𝑓 ∈ 𝐵 (𝐷 ∘ 𝑓) ≠ 0
Theorem	smndex2hbas 18200	The halving functions 𝐻 are endofunctions on ℕ0. (Contributed by AV, 18-Feb-2024.)
⊢ 𝑀 = (EndoFMnd‘ℕ0)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2 · 𝑥))    &   ⊢ 𝑁 ∈ ℕ0    &   ⊢ 𝐻 = (𝑥 ∈ ℕ0 ↦ if(2 ∥ 𝑥, (𝑥 / 2), 𝑁))    ⇒   ⊢ 𝐻 ∈ 𝐵