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	gsum0 18701	Value of the empty group sum. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 Σg ∅) = 0
Theorem	gsumval2a 18702*	Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    &   ⊢ 𝑂 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}    &   ⊢ (𝜑 → ¬ ran 𝐹 ⊆ 𝑂)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq𝑀( + , 𝐹)‘𝑁))
Theorem	gsumval2 18703	Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq𝑀( + , 𝐹)‘𝑁))
Theorem	gsumsplit1r 18704	Splitting off the rightmost summand of a group sum. This corresponds to the (inductive) definition of a (finite) product in [Lang] p. 4, first formula. (Contributed by AV, 26-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀))    &   ⊢ (𝜑 → 𝐹:(𝑀...(𝑁 + 1))⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹 ↾ (𝑀...𝑁))) + (𝐹‘(𝑁 + 1))))
Theorem	gsumprval 18705	Value of the group sum operation over a pair of sequential integers. (Contributed by AV, 14-Dec-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 = (𝑀 + 1))    &   ⊢ (𝜑 → 𝐹:{𝑀, 𝑁}⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐹‘𝑀) + (𝐹‘𝑁)))
Theorem	gsumpr12val 18706	Value of the group sum operation over the pair {1, 2}. (Contributed by AV, 14-Dec-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹:{1, 2}⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐹‘1) + (𝐹‘2)))
10.1.4  Magma homomorphisms and submagmas
Syntax	cmgmhm 18707	Hom-set generator class for magmas.
class MgmHom
Syntax	csubmgm 18708	Class function taking a magma to its lattice of submagmas.
class SubMgm
Definition	df-mgmhm 18709*	A magma homomorphism is a function on the base sets which preserves the binary operation. (Contributed by AV, 24-Feb-2020.)
⊢ MgmHom = (𝑠 ∈ Mgm, 𝑡 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))})
Definition	df-submgm 18710*	A submagma is a subset of a magma which is closed under the operation. Such subsets are themselves magmas. (Contributed by AV, 24-Feb-2020.)
⊢ SubMgm = (𝑠 ∈ Mgm ↦ {𝑡 ∈ 𝒫 (Base‘𝑠) ∣ ∀𝑥 ∈ 𝑡 ∀𝑦 ∈ 𝑡 (𝑥(+g‘𝑠)𝑦) ∈ 𝑡})
Theorem	mgmhmrcl 18711	Reverse closure of a magma homomorphism. (Contributed by AV, 24-Feb-2020.)
⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → (𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm))
Theorem	submgmrcl 18712	Reverse closure for submagmas. (Contributed by AV, 24-Feb-2020.)
⊢ (𝑆 ∈ (SubMgm‘𝑀) → 𝑀 ∈ Mgm)
Theorem	ismgmhm 18713*	Property of a magma homomorphism. (Contributed by AV, 25-Feb-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))))
Theorem	mgmhmf 18714	A magma homomorphism is a function. (Contributed by AV, 25-Feb-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → 𝐹:𝐵⟶𝐶)
Theorem	mgmhmpropd 18715*	Magma homomorphism depends only on the operation of structures. (Contributed by AV, 25-Feb-2020.)
⊢ (𝜑 → 𝐵 = (Base‘𝐽))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝑀))    &   ⊢ (𝜑 → 𝐵 ≠ ∅)    &   ⊢ (𝜑 → 𝐶 ≠ ∅)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦))    ⇒   ⊢ (𝜑 → (𝐽 MgmHom 𝐾) = (𝐿 MgmHom 𝑀))
Theorem	mgmhmlin 18716	A magma homomorphism preserves the binary operation. (Contributed by AV, 25-Feb-2020.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)))
Theorem	mgmhmf1o 18717	A magma homomorphism is bijective iff its converse is also a magma homomorphism. (Contributed by AV, 25-Feb-2020.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 MgmHom 𝑆) → (𝐹:𝐵–1-1-onto→𝐶 ↔ ◡𝐹 ∈ (𝑆 MgmHom 𝑅)))
Theorem	idmgmhm 18718	The identity homomorphism on a magma. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mgm → ( I ↾ 𝐵) ∈ (𝑀 MgmHom 𝑀))
Theorem	issubmgm 18719*	Expand definition of a submagma. (Contributed by AV, 25-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mgm → (𝑆 ∈ (SubMgm‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)))
Theorem	issubmgm2 18720	Submagmas are subsets that are also magmas. (Contributed by AV, 25-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑀 ∈ Mgm → (𝑆 ∈ (SubMgm‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 𝐻 ∈ Mgm)))
Theorem	rabsubmgmd 18721*	Deduction for proving that a restricted class abstraction is a submagma. (Contributed by AV, 26-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ Mgm)    &   ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝜃 ∧ 𝜏))) → 𝜂)    &   ⊢ (𝑧 = 𝑥 → (𝜓 ↔ 𝜃))    &   ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜏))    &   ⊢ (𝑧 = (𝑥 + 𝑦) → (𝜓 ↔ 𝜂))    ⇒   ⊢ (𝜑 → {𝑧 ∈ 𝐵 ∣ 𝜓} ∈ (SubMgm‘𝑀))
Theorem	submgmss 18722	Submagmas are subsets of the base set. (Contributed by AV, 26-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMgm‘𝑀) → 𝑆 ⊆ 𝐵)
Theorem	submgmid 18723	Every magma is trivially a submagma of itself. (Contributed by AV, 26-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mgm → 𝐵 ∈ (SubMgm‘𝑀))
Theorem	submgmcl 18724	Submagmas are closed under the magma operation. (Contributed by AV, 26-Feb-2020.)
⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑆 ∈ (SubMgm‘𝑀) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆)
Theorem	submgmmgm 18725	Submagmas are themselves magmas under the given operation. (Contributed by AV, 26-Feb-2020.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMgm‘𝑀) → 𝐻 ∈ Mgm)
Theorem	submgmbas 18726	The base set of a submagma. (Contributed by AV, 26-Feb-2020.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMgm‘𝑀) → 𝑆 = (Base‘𝐻))
Theorem	subsubmgm 18727	A submagma of a submagma is a submagma. (Contributed by AV, 26-Feb-2020.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMgm‘𝐺) → (𝐴 ∈ (SubMgm‘𝐻) ↔ (𝐴 ∈ (SubMgm‘𝐺) ∧ 𝐴 ⊆ 𝑆)))
Theorem	resmgmhm 18728	Restriction of a magma homomorphism to a submagma is a homomorphism. (Contributed by AV, 26-Feb-2020.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ 𝑋 ∈ (SubMgm‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MgmHom 𝑇))
Theorem	resmgmhm2 18729	One direction of resmgmhm2b 18730. (Contributed by AV, 26-Feb-2020.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑈) ∧ 𝑋 ∈ (SubMgm‘𝑇)) → 𝐹 ∈ (𝑆 MgmHom 𝑇))
Theorem	resmgmhm2b 18730	Restriction of the codomain of a homomorphism. (Contributed by AV, 26-Feb-2020.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ 𝐹 ∈ (𝑆 MgmHom 𝑈)))
Theorem	mgmhmco 18731	The composition of magma homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.)
⊢ ((𝐹 ∈ (𝑇 MgmHom 𝑈) ∧ 𝐺 ∈ (𝑆 MgmHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 MgmHom 𝑈))
Theorem	mgmhmima 18732	The homomorphic image of a submagma is a submagma. (Contributed by AV, 27-Feb-2020.)
⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubMgm‘𝑁))
Theorem	mgmhmeql 18733	The equalizer of two magma homomorphisms is a submagma. (Contributed by AV, 27-Feb-2020.)
⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ 𝐺 ∈ (𝑆 MgmHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubMgm‘𝑆))
Theorem	submgmacs 18734	Submagmas are an algebraic closure system. (Contributed by AV, 27-Feb-2020.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mgm → (SubMgm‘𝐺) ∈ (ACS‘𝐵))
10.1.5  Semigroups A semigroup (Smgrp, see df-sgrp 18736) is a set together with an associative binary operation (see Wikipedia, Semigroup, 8-Jan-2020, https://en.wikipedia.org/wiki/Semigroup 18736). In other words, a semigroup is an associative magma. The notion of semigroup is a generalization of that of group where the existence of an identity or inverses is not required.
Syntax	csgrp 18735	Extend class notation with class of all semigroups.
class Smgrp
Definition	df-sgrp 18736*	A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 18657), whose operation is associative. Definition in section II.1 of [Bruck] p. 23, or of an "associative magma" in definition 5 of [BourbakiAlg1] p. 4 . (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ Smgrp = {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))}
Theorem	issgrp 18737*	The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ Smgrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
Theorem	issgrpv 18738*	The predicate "is a semigroup" for a structure which is a set. (Contributed by AV, 1-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Smgrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))))
Theorem	issgrpn0 18739*	The predicate "is a semigroup" for a structure with a nonempty base set. (Contributed by AV, 1-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝐴 ∈ 𝐵 → (𝑀 ∈ Smgrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))))
Theorem	isnsgrp 18740	A condition for a structure not to be a semigroup. (Contributed by AV, 30-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (((𝑋 ⚬ 𝑌) ⚬ 𝑍) ≠ (𝑋 ⚬ (𝑌 ⚬ 𝑍)) → 𝑀 ∉ Smgrp))
Theorem	sgrpmgm 18741	A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ (𝑀 ∈ Smgrp → 𝑀 ∈ Mgm)
Theorem	sgrpass 18742	A semigroup operation is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 30-Jan-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⚬ = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ⚬ 𝑌) ⚬ 𝑍) = (𝑋 ⚬ (𝑌 ⚬ 𝑍)))
Theorem	sgrpcl 18743	Closure of the operation of a semigroup. (Contributed by AV, 15-Feb-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⚬ = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⚬ 𝑌) ∈ 𝐵)
Theorem	sgrp0 18744	Any set with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021.)
⊢ ((𝑀 ∈ 𝑉 ∧ (Base‘𝑀) = ∅) → 𝑀 ∈ Smgrp)
Theorem	sgrp0b 18745	The structure with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021.)
⊢ {⟨(Base‘ndx), ∅⟩, ⟨(+g‘ndx), 𝑂⟩} ∈ Smgrp
Theorem	sgrp1 18746	The structure with one element and the only closed internal operation for a singleton is a semigroup. (Contributed by AV, 10-Feb-2020.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩}    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Smgrp)
Theorem	issgrpd 18747*	Deduce a semigroup from its properties. (Contributed by AV, 13-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Smgrp)
Theorem	sgrppropd 18748*	If two structures are sets, have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a semigroup iff the other one is. (Contributed by AV, 15-Feb-2025.)
⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑊)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Smgrp ↔ 𝐿 ∈ Smgrp))
Theorem	prdsplusgsgrpcl 18749	Structure product pointwise sums are closed when the factors are semigroups. (Contributed by AV, 21-Feb-2025.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Smgrp)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 + 𝐺) ∈ 𝐵)
Theorem	prdssgrpd 18750	The product of a family of semigroups is a semigroup. (Contributed by AV, 21-Feb-2025.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Smgrp)    ⇒   ⊢ (𝜑 → 𝑌 ∈ Smgrp)
10.1.6  Definition and basic properties of monoids According to Wikipedia ("Monoid", https://en.wikipedia.org/wiki/Monoid, 6-Feb-2020,) "In abstract algebra [...] a monoid is an algebraic structure with a single associative binary operation and an identity element. Monoids are semigroups with identity.". In the following, monoids are defined in the second way (as semigroups with identity), see df-mnd 18752, whereas many authors define magmas in the first way (as algebraic structure with a single associative binary operation and an identity element, i.e. without the need of a definition for/knowledge about semigroups), see ismnd 18754. See, for example, the definition in [Lang] p. 3: "A monoid is a set G, with a law of composition which is associative, and having a unit element".
Syntax	cmnd 18751	Extend class notation with class of all monoids.
class Mnd
Definition	df-mnd 18752*	A monoid is a semigroup, which has a two-sided neutral element. Definition 2 in [BourbakiAlg1] p. 12. In other words (according to the definition in [Lang] p. 3), a monoid is a set equipped with an everywhere defined internal operation (see mndcl 18759), whose operation is associative (see mndass 18760) and has a two-sided neutral element (see mndid 18761), see also ismnd 18754. (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.)
⊢ Mnd = {𝑔 ∈ Smgrp ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)}
Theorem	ismnddef 18753*	The predicate "is a monoid", corresponding 1-to-1 to the definition. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 1-Feb-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd ↔ (𝐺 ∈ Smgrp ∧ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎)))
Theorem	ismnd 18754*	The predicate "is a monoid". This is the defining theorem of a monoid by showing that a set is a monoid if and only if it is a set equipped with a closed, everywhere defined internal operation (so, a magma, see mndcl 18759), whose operation is associative (so, a semigroup, see also mndass 18760) and has a two-sided neutral element (see mndid 18761). (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd ↔ (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 + 𝑏) ∈ 𝐵 ∧ ∀𝑐 ∈ 𝐵 ((𝑎 + 𝑏) + 𝑐) = (𝑎 + (𝑏 + 𝑐))) ∧ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎)))
Theorem	isnmnd 18755*	A condition for a structure not to be a monoid: every element of the base set is not a left identity for at least one element of the base set. (Contributed by AV, 4-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (∀𝑧 ∈ 𝐵 ∃𝑥 ∈ 𝐵 (𝑧 ⚬ 𝑥) ≠ 𝑥 → 𝑀 ∉ Mnd)
Theorem	sgrpidmnd 18756*	A semigroup with an identity element which is not the empty set is a monoid. Of course there could be monoids with the empty set as identity element (see, for example, the monoid of the power set of a class under union, pwmnd 18957 and pwmndid 18956), but these cannot be proven to be monoids with this theorem. (Contributed by AV, 29-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ ∃𝑒 ∈ 𝐵 (𝑒 ≠ ∅ ∧ 𝑒 = 0 )) → 𝐺 ∈ Mnd)
Theorem	mndsgrp 18757	A monoid is a semigroup. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) (Proof shortened by AV, 6-Feb-2020.)
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ Smgrp)
Theorem	mndmgm 18758	A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) (Proof shortened by AV, 6-Feb-2020.)
⊢ (𝑀 ∈ Mnd → 𝑀 ∈ Mgm)
Theorem	mndcl 18759	Closure of the operation of a monoid. (Contributed by NM, 14-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Proof shortened by AV, 8-Feb-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	mndass 18760	A monoid operation is associative. (Contributed by NM, 14-Aug-2011.) (Proof shortened by AV, 8-Feb-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	mndid 18761*	A monoid has a two-sided identity element. (Contributed by NM, 16-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → ∃𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥))
Theorem	mndideu 18762*	The two-sided identity element of a monoid is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by Mario Carneiro, 8-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → ∃!𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥))
Theorem	mnd32g 18763	Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑌 + 𝑍) = (𝑍 + 𝑌))    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌))
Theorem	mnd12g 18764	Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))    ⇒   ⊢ (𝜑 → (𝑋 + (𝑌 + 𝑍)) = (𝑌 + (𝑋 + 𝑍)))
Theorem	mnd4g 18765	Commutative/associative law for commutative monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑌 + 𝑍) = (𝑍 + 𝑌))    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊)))
Theorem	mndidcl 18766	The identity element of a monoid belongs to the monoid. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → 0 ∈ 𝐵)
Theorem	mndbn0 18767	The base set of a monoid is not empty. Statement in [Lang] p. 3. (Contributed by AV, 29-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → 𝐵 ≠ ∅)
Theorem	hashfinmndnn 18768	A finite monoid has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ)
Theorem	mndplusf 18769	The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 3-Feb-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → ⨣ :(𝐵 × 𝐵)⟶𝐵)
Theorem	mndlrid 18770	A monoid's identity element is a two-sided identity. (Contributed by NM, 18-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋))
Theorem	mndlid 18771	The identity element of a monoid is a left identity. (Contributed by NM, 18-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
Theorem	mndrid 18772	The identity element of a monoid is a right identity. (Contributed by NM, 18-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)
Theorem	ismndd 18773*	Deduce a monoid from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 0 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Mnd)
Theorem	mndpfo 18774	The addition operation of a monoid as a function is an onto function. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 11-Oct-2013.) (Revised by AV, 23-Jan-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → ⨣ :(𝐵 × 𝐵)–onto→𝐵)
Theorem	mndfo 18775	The addition operation of a monoid is an onto function (assuming it is a function). (Contributed by Mario Carneiro, 11-Oct-2013.) (Proof shortened by AV, 23-Jan-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ + Fn (𝐵 × 𝐵)) → + :(𝐵 × 𝐵)–onto→𝐵)
Theorem	mndpropd 18776*	If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Mnd ↔ 𝐿 ∈ Mnd))
Theorem	mndprop 18777	If two structures have the same group components (properties), one is a monoid iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.)
⊢ (Base‘𝐾) = (Base‘𝐿)    &   ⊢ (+g‘𝐾) = (+g‘𝐿)    ⇒   ⊢ (𝐾 ∈ Mnd ↔ 𝐿 ∈ Mnd)
Theorem	issubmnd 18778*	Characterize a submonoid by closure properties. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) → (𝐻 ∈ Mnd ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆))
Theorem	ress0g 18779	0g is unaffected by restriction. This is a bit more generic than submnd0 18780. (Contributed by Thierry Arnoux, 23-Oct-2017.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 0 = (0g‘𝑆))
Theorem	submnd0 18780	The zero of a submonoid is the same as the zero in the parent monoid. (Note that we must add the condition that the zero of the parent monoid is actually contained in the submonoid, because it is possible to have "subsets that are monoids" which are not submonoids because they have a different identity element. See, for example, smndex1mnd 18930 and smndex1n0mnd 18932). (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆)) → 0 = (0g‘𝐻))
Theorem	mndinvmod 18781*	Uniqueness of an inverse element in a monoid, if it exists. (Contributed by AV, 20-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ∃*𝑤 ∈ 𝐵 ((𝑤 + 𝐴) = 0 ∧ (𝐴 + 𝑤) = 0 ))
Theorem	mndpsuppss 18782	The support of a mapping of a scalar multiplication with a function of scalars is a subset of the support of the function of scalars. (Contributed by AV, 5-Apr-2019.)
⊢ 𝑅 = (Base‘𝑀)    ⇒   ⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉))) → ((𝐴 ∘f (+g‘𝑀)𝐵) supp (0g‘𝑀)) ⊆ ((𝐴 supp (0g‘𝑀)) ∪ (𝐵 supp (0g‘𝑀))))
Theorem	mndpsuppfi 18783	The support of a mapping of a scalar multiplication with a function of scalars is finite if the support of the function of scalars is finite. (Contributed by AV, 5-Apr-2019.)
⊢ 𝑅 = (Base‘𝑀)    ⇒   ⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ ((𝐴 supp (0g‘𝑀)) ∈ Fin ∧ (𝐵 supp (0g‘𝑀)) ∈ Fin)) → ((𝐴 ∘f (+g‘𝑀)𝐵) supp (0g‘𝑀)) ∈ Fin)
Theorem	mndpfsupp 18784	A mapping of a scalar multiplication with a function of scalars is finitely supported if the function of scalars is finitely supported. (Contributed by AV, 9-Jun-2019.)
⊢ 𝑅 = (Base‘𝑀)    ⇒   ⊢ (((𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝑋) ∧ (𝐴 ∈ (𝑅 ↑m 𝑉) ∧ 𝐵 ∈ (𝑅 ↑m 𝑉)) ∧ (𝐴 finSupp (0g‘𝑀) ∧ 𝐵 finSupp (0g‘𝑀))) → (𝐴 ∘f (+g‘𝑀)𝐵) finSupp (0g‘𝑀))
Theorem	prdsplusgcl 18785	Structure product pointwise sums are closed when the factors are monoids. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Mnd)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 + 𝐺) ∈ 𝐵)
Theorem	prdsidlem 18786*	Characterization of identity in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Mnd)    &   ⊢ 0 = (0g ∘ 𝑅)    ⇒   ⊢ (𝜑 → ( 0 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)))
Theorem	prdsmndd 18787	The product of a family of monoids is a monoid. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Mnd)    ⇒   ⊢ (𝜑 → 𝑌 ∈ Mnd)
Theorem	prds0g 18788	The identity in a product of monoids. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Mnd)    ⇒   ⊢ (𝜑 → (0g ∘ 𝑅) = (0g‘𝑌))
Theorem	pwsmnd 18789	The structure power of a monoid is a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Mnd)
Theorem	pws0g 18790	The identity in a structure power of a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) → (𝐼 × { 0 }) = (0g‘𝑌))
Theorem	imasmnd2 18791*	The image structure of a monoid is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ + = (+g‘𝑅)    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘(𝑥 + (𝑦 + 𝑧))))    &   ⊢ (𝜑 → 0 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑥 + 0 )) = (𝐹‘𝑥))    ⇒   ⊢ (𝜑 → (𝑈 ∈ Mnd ∧ (𝐹‘ 0 ) = (0g‘𝑈)))
Theorem	imasmnd 18792*	The image structure of a monoid is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ + = (+g‘𝑅)    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ (𝜑 → 𝑅 ∈ Mnd)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝜑 → (𝑈 ∈ Mnd ∧ (𝐹‘ 0 ) = (0g‘𝑈)))
Theorem	imasmndf1 18793	The image of a monoid under an injection is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015.)
⊢ 𝑈 = (𝐹 “s 𝑅)    &   ⊢ 𝑉 = (Base‘𝑅)    ⇒   ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ 𝑅 ∈ Mnd) → 𝑈 ∈ Mnd)
Theorem	xpsmnd 18794	The binary product of monoids is a monoid. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑇 ∈ Mnd)
Theorem	xpsmnd0 18795	The identity element of a binary product of monoids. (Contributed by AV, 25-Feb-2025.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (0g‘𝑇) = ⟨(0g‘𝑅), (0g‘𝑆)⟩)
Theorem	mnd1 18796	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 18797	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 18798	Hom-set generator class for monoids.
class MndHom
Syntax	csubmnd 18799	Class function taking a monoid to its lattice of submonoids.
class SubMnd
Definition	df-mhm 18800*	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‘𝑡))})