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	mnd1 18701	The (smallest) structure representing a trivial monoid consists of one element. (Contributed by AV, 28-Apr-2019.) (Proof shortened by AV, 11-Feb-2020.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩}    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd)
Theorem	mnd1id 18702	The singleton element of a trivial monoid is its identity element. (Contributed by AV, 23-Jan-2020.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (0g‘𝑀) = 𝐼)
10.1.7  Monoid homomorphisms and submonoids
Syntax	cmhm 18703	Hom-set generator class for monoids.
class MndHom
Syntax	csubmnd 18704	Class function taking a monoid to its lattice of submonoids.
class SubMnd
Definition	df-mhm 18705*	A monoid homomorphism is a function on the base sets which preserves the binary operation and the identity. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ MndHom = (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))})
Definition	df-submnd 18706*	A submonoid is a subset of a monoid which contains the identity and is closed under the operation. Such subsets are themselves monoids with the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ SubMnd = (𝑠 ∈ Mnd ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ((0g‘𝑠) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡)})
Theorem	ismhm 18707*	Property of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝑌 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)))
Theorem	ismhmd 18708*	Deduction version of ismhm 18707. (Contributed by SN, 27-Jul-2024.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝑍 = (0g‘𝑇)    &   ⊢ (𝜑 → 𝑆 ∈ Mnd)    &   ⊢ (𝜑 → 𝑇 ∈ Mnd)    &   ⊢ (𝜑 → 𝐹:𝐵⟶𝐶)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    &   ⊢ (𝜑 → (𝐹‘ 0 ) = 𝑍)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆 MndHom 𝑇))
Theorem	mhmrcl1 18709	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑆 ∈ Mnd)
Theorem	mhmrcl2 18710	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑇 ∈ Mnd)
Theorem	mhmf 18711	A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:𝐵⟶𝐶)
Theorem	ismhm0 18712	Property of a monoid homomorphism, expressed by a magma homomorphism. (Contributed by AV, 17-Apr-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝑌 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ (𝐹‘ 0 ) = 𝑌)))
Theorem	mhmismgmhm 18713	Each monoid homomorphism is a magma homomorphism. (Contributed by AV, 29-Feb-2020.)
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → 𝐹 ∈ (𝑅 MgmHom 𝑆))
Theorem	mhmpropd 18714*	Monoid homomorphism depends only on the monoidal attributes of structures. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 7-Nov-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐽))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝑀))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦))    ⇒   ⊢ (𝜑 → (𝐽 MndHom 𝐾) = (𝐿 MndHom 𝑀))
Theorem	mhmlin 18715	A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)))
Theorem	mhm0 18716	A monoid homomorphism preserves zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 0 = (0g‘𝑆)    &   ⊢ 𝑌 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹‘ 0 ) = 𝑌)
Theorem	idmhm 18717	The identity homomorphism on a monoid. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mnd → ( I ↾ 𝐵) ∈ (𝑀 MndHom 𝑀))
Theorem	mhmf1o 18718	A monoid homomorphism is bijective iff its converse is also a monoid homomorphism. (Contributed by AV, 22-Oct-2019.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → (𝐹:𝐵–1-1-onto→𝐶 ↔ ◡𝐹 ∈ (𝑆 MndHom 𝑅)))
Theorem	submrcl 18719	Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑀 ∈ Mnd)
Theorem	issubm 18720*	Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)))
Theorem	issubm2 18721	Submonoids are subsets that are also monoids with the same zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ 𝐻 ∈ Mnd)))
Theorem	issubmndb 18722	The submonoid predicate. Analogous to issubg 19042. (Contributed by AV, 1-Feb-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝐺) ↔ ((𝐺 ∈ Mnd ∧ (𝐺 ↾s 𝑆) ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆)))
Theorem	issubmd 18723*	Deduction for proving a submonoid. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ Mnd)    &   ⊢ (𝜑 → 𝜒)    &   ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝜃 ∧ 𝜏))) → 𝜂)    &   ⊢ (𝑧 = 0 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑧 = 𝑥 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑧 = (𝑥 + 𝑦) → (𝜓 ↔ 𝜂))    ⇒   ⊢ (𝜑 → {𝑧 ∈ 𝐵 ∣ 𝜓} ∈ (SubMnd‘𝑀))
Theorem	mndissubm 18724	If the base set of a monoid is contained in the base set of another monoid, and the group operation of the monoid is the restriction of the group operation of the other monoid to its base set, and the identity element of the other monoid is contained in the base set of the monoid, then the (base set of the) monoid is a submonoid of the other monoid. Analogous to grpissubg 19062. (Contributed by AV, 17-Feb-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = (Base‘𝐻)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) → ((𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → 𝑆 ∈ (SubMnd‘𝐺)))
Theorem	resmndismnd 18725	If the base set of a monoid is contained in the base set of another monoid, and the group operation of the monoid is the restriction of the group operation of the other monoid to its base set, and the identity element of the other monoid is contained in the base set of the monoid, then the other monoid restricted to the base set of the monoid is a monoid. Analogous to resgrpisgrp 19063. (Contributed by AV, 17-Feb-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = (Base‘𝐻)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) → ((𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → (𝐺 ↾s 𝑆) ∈ Mnd))
Theorem	submss 18726	Submonoids are subsets of the base set. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 ⊆ 𝐵)
Theorem	submid 18727	Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mnd → 𝐵 ∈ (SubMnd‘𝑀))
Theorem	subm0cl 18728	Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 0 = (0g‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 ∈ 𝑆)
Theorem	submcl 18729	Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑆 ∈ (SubMnd‘𝑀) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆)
Theorem	submmnd 18730	Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝐻 ∈ Mnd)
Theorem	submbas 18731	The base set of a submonoid. (Contributed by Stefan O'Rear, 15-Jun-2015.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 = (Base‘𝐻))
Theorem	subm0 18732	Submonoids have the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    &   ⊢ 0 = (0g‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 = (0g‘𝐻))
Theorem	subsubm 18733	A submonoid of a submonoid is a submonoid. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝐺) → (𝐴 ∈ (SubMnd‘𝐻) ↔ (𝐴 ∈ (SubMnd‘𝐺) ∧ 𝐴 ⊆ 𝑆)))
Theorem	0subm 18734	The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → { 0 } ∈ (SubMnd‘𝐺))
Theorem	insubm 18735	The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024.)
⊢ ((𝐴 ∈ (SubMnd‘𝑀) ∧ 𝐵 ∈ (SubMnd‘𝑀)) → (𝐴 ∩ 𝐵) ∈ (SubMnd‘𝑀))
Theorem	0mhm 18736	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 18737	Restriction of a monoid homomorphism to a submonoid is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MndHom 𝑇))
Theorem	resmhm2 18738	One direction of resmhm2b 18739. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → 𝐹 ∈ (𝑆 MndHom 𝑇))
Theorem	resmhm2b 18739	Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ (𝑆 MndHom 𝑈)))
Theorem	mhmco 18740	The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐹 ∈ (𝑇 MndHom 𝑈) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 MndHom 𝑈))
Theorem	mhmimalem 18741*	Lemma for mhmima 18742 and similar theorems, formerly part of proof for mhmima 18742. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 16-Feb-2025.)
⊢ (𝜑 → 𝐹 ∈ (𝑀 MndHom 𝑁))    &   ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝑀))    &   ⊢ (𝜑 → ⊕ = (+g‘𝑀))    &   ⊢ (𝜑 → + = (+g‘𝑁))    &   ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧 ⊕ 𝑥) ∈ 𝑋)    ⇒   ⊢ (𝜑 → ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥 + 𝑦) ∈ (𝐹 “ 𝑋))
Theorem	mhmima 18742	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 18743	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 18744	Submonoids are an algebraic closure system. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → (SubMnd‘𝐺) ∈ (ACS‘𝐵))
Theorem	mndind 18745*	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 18746*	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 18747*	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 18748*	Diagonal monoid homomorphism into a structure power. (Contributed by Stefan O'Rear, 12-Mar-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 MndHom 𝑌))
Theorem	pwsco1mhm 18749*	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 18750*	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 17392. If order is not significant, it is simpler to use families instead.
Theorem	gsumvallem2 18751*	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 18752	Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))
Theorem	gsumz 18753*	Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 )
Theorem	gsumwsubmcl 18754	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 18755	A singleton composite recovers the initial symbol. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑆 ∈ 𝐵 → (𝐺 Σg ⟨“𝑆”⟩) = 𝑆)
Theorem	gsumwcl 18756	Closure of the composite of a word in a structure 𝐺. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵)
Theorem	gsumsgrpccat 18757	Homomorphic property of not empty composites of a group sum over a semigroup. Formerly part of proof for gsumccat 18758. (Contributed by AV, 26-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋)))
Theorem	gsumccat 18758	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 18759	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 18760	Homomorphic property of composites with a singleton. (Contributed by AV, 20-Jan-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ ⟨“𝑍”⟩)) = ((𝐺 Σg 𝑊) + 𝑍))
Theorem	gsumspl 18761	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 18762	Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊)))
Theorem	gsumwspan 18763*	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 18764	Extend class definition with the free monoid construction.
class freeMnd
Syntax	cvrmd 18765	Extend class notation with free monoid injection.
class varFMnd
Definition	df-frmd 18766	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 18767*	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 18768	Value of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼)    &   ⊢ + = ( ++ ↾ (𝐵 × 𝐵))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩})
Theorem	frmdbas 18769	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 18770	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 18771	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 18772	Value of the monoid operation of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ++ 𝑌))
Theorem	vrmdfval 18773*	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 18774	The value of the generating elements of a free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = ⟨“𝐴”⟩)
Theorem	vrmdf 18775	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 18776	A free monoid is a monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd)
Theorem	frmd0 18777	The identity of the free monoid is the empty word. (Contributed by Mario Carneiro, 27-Sep-2015.)
⊢ 𝑀 = (freeMnd‘𝐼)    ⇒   ⊢ ∅ = (0g‘𝑀)
Theorem	frmdsssubm 18778	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 18779	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 18780	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 18781*	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 18782*	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 18783*	Lemma for frmdup3 18784. (Contributed by Mario Carneiro, 18-Jul-2016.)
⊢ 𝑀 = (freeMnd‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑈 = (varFMnd‘𝐼)    ⇒   ⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → 𝐹 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥))))
Theorem	frmdup3 18784*	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 18785	Extend class notation to include the class of monoids of endofunctions.
class EndoFMnd
Definition	df-efmnd 18786*	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 19276 and symgvalstruct 19305. (Contributed by AV, 25-Jan-2024.)
⊢ EndoFMnd = (𝑥 ∈ V ↦ ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
Theorem	efmnd 18787*	The monoid of endofunctions on set 𝐴. (Contributed by AV, 25-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (𝐴 ↑m 𝐴)    &   ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))    &   ⊢ 𝐽 = (∏t‘(𝐴 × {𝒫 𝐴}))    ⇒   ⊢ (𝐴 ∈ 𝑉 → 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩})
Theorem	efmndbas 18788	The base set of the monoid of endofunctions on class 𝐴. (Contributed by AV, 25-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝐵 = (𝐴 ↑m 𝐴)
Theorem	efmndbasabf 18789*	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 18790	Two ways of saying a function is a mapping of 𝐴 to itself. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐴))
Theorem	elefmndbas2 18791	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 18792	Elements in the monoid of endofunctions on 𝐴 are functions from 𝐴 into itself. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴⟶𝐴)
Theorem	efmndhash 18793	The monoid of endofunctions on 𝑛 objects has cardinality 𝑛↑𝑛. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → (♯‘𝐵) = ((♯‘𝐴)↑(♯‘𝐴)))
Theorem	efmndbasfi 18794	The monoid of endofunctions on a finite set 𝐴 is finite. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin)
Theorem	efmndfv 18795	The function value of an endofunction. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴)
Theorem	efmndtset 18796	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 18797*	The group operation of a monoid of endofunctions is the function composition. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔))
Theorem	efmndov 18798	The value of the group operation of the monoid of endofunctions on 𝐴. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌))
Theorem	efmndcl 18799	The group operation of the monoid of endofunctions on 𝐴 is closed. (Contributed by AV, 27-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	efmndtopn 18800	The topology of the monoid of endofunctions on 𝐴. (Contributed by AV, 31-Jan-2024.)
⊢ 𝐺 = (EndoFMnd‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺))