P. 127 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 12601-12700   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-pt 12601*	Define the product topology on a collection of topologies. For convenience, it is defined on arbitrary collections of sets, expressed as a function from some index set to the subbases of each factor space. (Contributed by Mario Carneiro, 3-Feb-2015.)
⊢ ∏t = (𝑓 ∈ V ↦ (topGen‘{𝑥 ∣ ∃𝑔((𝑔 Fn dom 𝑓 ∧ ∀𝑦 ∈ dom 𝑓(𝑔‘𝑦) ∈ (𝑓‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (dom 𝑓 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝑓‘𝑦)) ∧ 𝑥 = X𝑦 ∈ dom 𝑓(𝑔‘𝑦))}))
Syntax	cprds 12602	The function constructing structure products.
class Xs
Syntax	cpws 12603	The function constructing structure powers.
class ↑s
Definition	df-prds 12604*	Define a structure product. This can be a product of groups, rings, modules, or ordered topological fields; any unused components will have garbage in them but this is usually not relevant for the purpose of inheriting the structures present in the factors. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.)
⊢ Xs = (𝑠 ∈ V, 𝑟 ∈ V ↦ ⦋X𝑥 ∈ dom 𝑟(Base‘(𝑟‘𝑥)) / 𝑣⦌⦋(𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ X𝑥 ∈ dom 𝑟((𝑓‘𝑥)(Hom ‘(𝑟‘𝑥))(𝑔‘𝑥))) / ℎ⦌(({⟨(Base‘ndx), 𝑣⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(+g‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(.r‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(.r‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩} ∪ {⟨(Scalar‘ndx), 𝑠⟩, ⟨( ·𝑠 ‘ndx), (𝑓 ∈ (Base‘𝑠), 𝑔 ∈ 𝑣 ↦ (𝑥 ∈ dom 𝑟 ↦ (𝑓( ·𝑠 ‘(𝑟‘𝑥))(𝑔‘𝑥))))⟩, ⟨(·𝑖‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ (𝑠 Σg (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(·𝑖‘(𝑟‘𝑥))(𝑔‘𝑥)))))⟩}) ∪ ({⟨(TopSet‘ndx), (∏t‘(TopOpen ∘ 𝑟))⟩, ⟨(le‘ndx), {⟨𝑓, 𝑔⟩ ∣ ({𝑓, 𝑔} ⊆ 𝑣 ∧ ∀𝑥 ∈ dom 𝑟(𝑓‘𝑥)(le‘(𝑟‘𝑥))(𝑔‘𝑥))}⟩, ⟨(dist‘ndx), (𝑓 ∈ 𝑣, 𝑔 ∈ 𝑣 ↦ sup((ran (𝑥 ∈ dom 𝑟 ↦ ((𝑓‘𝑥)(dist‘(𝑟‘𝑥))(𝑔‘𝑥))) ∪ {0}), ℝ*, < ))⟩} ∪ {⟨(Hom ‘ndx), ℎ⟩, ⟨(comp‘ndx), (𝑎 ∈ (𝑣 × 𝑣), 𝑐 ∈ 𝑣 ↦ (𝑑 ∈ (𝑐ℎ(2nd ‘𝑎)), 𝑒 ∈ (ℎ‘𝑎) ↦ (𝑥 ∈ dom 𝑟 ↦ ((𝑑‘𝑥)(⟨((1st ‘𝑎)‘𝑥), ((2nd ‘𝑎)‘𝑥)⟩(comp‘(𝑟‘𝑥))(𝑐‘𝑥))(𝑒‘𝑥)))))⟩})))
Theorem	reldmprds 12605	The structure product is a well-behaved binary operator. (Contributed by Stefan O'Rear, 7-Jan-2015.) (Revised by Thierry Arnoux, 15-Jun-2019.)
⊢ Rel dom Xs
Definition	df-pws 12606*	Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ ↑s = (𝑟 ∈ V, 𝑖 ∈ V ↦ ((Scalar‘𝑟)Xs(𝑖 × {𝑟})))
PART 7  BASIC ALGEBRAIC STRUCTURES
7.1  Monoids
7.1.1  Magmas According to Wikipedia ("Magma (algebra)", 08-Jan-2020, https://en.wikipedia.org/wiki/magma_(algebra)) "In abstract algebra, a magma [...] is a basic kind of algebraic structure. Specifically, a magma consists of a set equipped with a single binary operation. The binary operation must be closed by definition but no other properties are imposed.". Since the concept of a "binary operation" is used in different variants, these differences are explained in more detail in the following: With df-mpo 5858, binary operations are defined by a rule, and with df-ov 5856, the value of a binary operation applied to two operands can be expressed. In both cases, the two operands can belong to different sets, and the result can be an element of a third set. However, according to Wikipedia "Binary operation", see https://en.wikipedia.org/wiki/Binary_operation 5856 (19-Jan-2020), "... a binary operation on a set 𝑆 is a mapping of the elements of the Cartesian product 𝑆 × 𝑆 to S: 𝑓:𝑆 × 𝑆⟶𝑆. Because the result of performing the operation on a pair of elements of S is again an element of S, the operation is called a closed binary operation on S (or sometimes expressed as having the property of closure).". To distinguish this more restrictive definition (in Wikipedia and most of the literature) from the general case, binary operations mapping the elements of the Cartesian product 𝑆 × 𝑆 are more precisely called internal binary operations. If, in addition, the result is also contained in the set 𝑆, the operation should be called closed internal binary operation. Therefore, a "binary operation on a set 𝑆" according to Wikipedia is a "closed internal binary operation" in a more precise terminology. If the sets are different, the operation is explicitly called external binary operation (see Wikipedia https://en.wikipedia.org/wiki/Binary_operation#External_binary_operations 5856). The definition of magmas (Mgm, see df-mgm 12610) concentrates on the closure property of the associated operation, and poses no additional restrictions on it. In this way, it is most general and flexible.
Syntax	cplusf 12607	Extend class notation with group addition as a function.
class +𝑓
Syntax	cmgm 12608	Extend class notation with class of all magmas.
class Mgm
Definition	df-plusf 12609*	Define group addition function. Usually we will use +g directly instead of +𝑓, and they have the same behavior in most cases. The main advantage of +𝑓 for any magma is that it is a guaranteed function (mgmplusf 12620), while +g only has closure (mgmcl 12613). (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ +𝑓 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)𝑦)))
Definition	df-mgm 12610*	A magma is a set equipped with an everywhere defined internal operation. Definition 1 in [BourbakiAlg1] p. 1, or definition of a groupoid in section I.1 of [Bruck] p. 1. Note: The term "groupoid" is now widely used to refer to other objects: (small) categories all of whose morphisms are invertible, or groups with a partial function replacing the binary operation. Therefore, we will only use the term "magma" for the present notion in set.mm. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ Mgm = {𝑔 ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 (𝑥𝑜𝑦) ∈ 𝑏}
Theorem	ismgm 12611*	The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))
Theorem	ismgmn0 12612*	The predicate "is a magma" for a structure with a nonempty base set. (Contributed by AV, 29-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝐴 ∈ 𝐵 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵))
Theorem	mgmcl 12613	Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 13-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⚬ 𝑌) ∈ 𝐵)
Theorem	isnmgm 12614	A condition for a structure not to be a magma. (Contributed by AV, 30-Jan-2020.) (Proof shortened by NM, 5-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ (𝑋 ⚬ 𝑌) ∉ 𝐵) → 𝑀 ∉ Mgm)
Theorem	mgmsscl 12615	If the base set of a magma is contained in the base set of another magma, and the group operation of the magma is the restriction of the group operation of the other magma to its base set, then the base set of the magma is closed under the group operation of the other magma. (Contributed by AV, 17-Feb-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = (Base‘𝐻)    ⇒   ⊢ (((𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑋(+g‘𝐺)𝑌) ∈ 𝑆)
Theorem	plusffvalg 12616*	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 2-Mar-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → ⨣ = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)))
Theorem	plusfvalg 12617	The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⨣ 𝑌) = (𝑋 + 𝑌))
Theorem	plusfeqg 12618	If the addition operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ + Fn (𝐵 × 𝐵)) → ⨣ = + )
Theorem	plusffng 12619	The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⨣ = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → ⨣ Fn (𝐵 × 𝐵))
Theorem	mgmplusf 12620	The group addition function of a magma is a function into its base set. (Contributed by Mario Carneiro, 14-Aug-2015.) (Revisd by AV, 28-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⨣ = (+𝑓‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mgm → ⨣ :(𝐵 × 𝐵)⟶𝐵)
Theorem	intopsn 12621	The internal operation for a set is the trivial operation iff the set is a singleton. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 23-Jan-2020.)
⊢ (( ⚬ :(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ⚬ = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}))
Theorem	mgmb1mgm1 12622	The only magma with a base set consisting of one element is the trivial magma (at least if its operation is an internal binary operation). (Contributed by AV, 23-Jan-2020.) (Revised by AV, 7-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Mgm ∧ 𝑍 ∈ 𝐵 ∧ + Fn (𝐵 × 𝐵)) → (𝐵 = {𝑍} ↔ + = {⟨⟨𝑍, 𝑍⟩, 𝑍⟩}))
Theorem	mgm0 12623	Any set with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021.)
⊢ ((𝑀 ∈ 𝑉 ∧ (Base‘𝑀) = ∅) → 𝑀 ∈ Mgm)
Theorem	mgm1 12624	The structure with one element and the only closed internal operation for a singleton is a magma. (Contributed by AV, 10-Feb-2020.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩}    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mgm)
Theorem	opifismgmdc 12625*	A structure with a group addition operation expressed by a conditional operator is a magma if both values of the conditional operator are contained in the base set. (Contributed by AV, 9-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ if(𝜓, 𝐶, 𝐷))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → DECID 𝜓)    &   ⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐷 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝑀 ∈ Mgm)
7.1.2  Identity elements According to Wikipedia ("Identity element", 7-Feb-2020, https://en.wikipedia.org/wiki/Identity_element): "In mathematics, an identity element, or neutral element, is a special type of element of a set with respect to a binary operation on that set, which leaves any element of the set unchanged when combined with it.". Or in more detail "... an element e of S is called a left identity if e * a = a for all a in S, and a right identity if a * e = a for all a in S. If e is both a left identity and a right identity, then it is called a two-sided identity, or simply an identity." We concentrate on two-sided identities in the following. The existence of an identity (an identity is unique if it exists, see mgmidmo 12626) is an important property of monoids, and therefore also for groups, but also for magmas not required to be associative. Magmas with an identity element are called "unital magmas" (see Definition 2 in [BourbakiAlg1] p. 12) or, if the magmas are cancellative, "loops" (see definition in [Bruck] p. 15). In the context of extensible structures, the identity element (of any magma 𝑀) is defined as "group identity element" (0g‘𝑀), see df-0g 12598. Related theorems which are already valid for magmas are provided in the following.
Theorem	mgmidmo 12626*	A two-sided identity element is unique (if it exists) in any magma. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by NM, 17-Jun-2017.)
⊢ ∃*𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥)
Theorem	grpidvalg 12627*	The value of the identity element of a group. (Contributed by NM, 20-Aug-2011.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 0 = (℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))))
Theorem	grpidpropdg 12628*	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, they have the same identity element. (Contributed by Mario Carneiro, 27-Nov-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (0g‘𝐾) = (0g‘𝐿))
Theorem	fn0g 12629	The group zero extractor is a function. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 0g Fn V
Theorem	0g0 12630	The identity element function evaluates to the empty set on an empty structure. (Contributed by Stefan O'Rear, 2-Oct-2015.)
⊢ ∅ = (0g‘∅)
Theorem	ismgmid 12631*	The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → ∃𝑒 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))    ⇒   ⊢ (𝜑 → ((𝑈 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑈 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑈) = 𝑥)) ↔ 0 = 𝑈))
Theorem	mgmidcl 12632*	The identity element of a magma, if it exists, belongs to the base set. (Contributed by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → ∃𝑒 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))    ⇒   ⊢ (𝜑 → 0 ∈ 𝐵)
Theorem	mgmlrid 12633*	The identity element of a magma, if it exists, is a left and right identity. (Contributed by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → ∃𝑒 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐵) → (( 0 + 𝑋) = 𝑋 ∧ (𝑋 + 0 ) = 𝑋))
Theorem	ismgmid2 12634*	Show that a given element is the identity element of a magma. (Contributed by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑈 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 𝑈) = 𝑥)    ⇒   ⊢ (𝜑 → 𝑈 = 0 )
Theorem	lidrideqd 12635*	If there is a left and right identity element for any binary operation (group operation) +, both identity elements are equal. Generalization of statement in [Lang] p. 3: it is sufficient that "e" is a left identity element and "e`" is a right identity element instead of both being (two-sided) identity elements. (Contributed by AV, 26-Dec-2023.)
⊢ (𝜑 → 𝐿 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝐿 + 𝑥) = 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑥 + 𝑅) = 𝑥)    ⇒   ⊢ (𝜑 → 𝐿 = 𝑅)
Theorem	lidrididd 12636*	If there is a left and right identity element for any binary operation (group operation) +, the left identity element (and therefore also the right identity element according to lidrideqd 12635) is equal to the two-sided identity element. (Contributed by AV, 26-Dec-2023.)
⊢ (𝜑 → 𝐿 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑅 ∈ 𝐵)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝐿 + 𝑥) = 𝑥)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑥 + 𝑅) = 𝑥)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝜑 → 𝐿 = 0 )
Theorem	grpidd 12637*	Deduce the identity element of a magma from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 0 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)    ⇒   ⊢ (𝜑 → 0 = (0g‘𝐺))
Theorem	mgmidsssn0 12638*	Property of the set of identities of 𝐺. Either 𝐺 has no identities, and 𝑂 = ∅, or it has one and this identity is unique and identified by the 0g function. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑂 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)}    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝑂 ⊆ { 0 })
Theorem	grprinvlem 12639*	Lemma for grprinvd 12640. (Contributed by NM, 9-Aug-2013.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ (𝜑 → 𝑂 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝑋 + 𝑋) = 𝑋)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → 𝑋 = 𝑂)
Theorem	grprinvd 12640*	Deduce right inverse from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ (𝜑 → 𝑂 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝜓) → 𝑁 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝜓) → (𝑁 + 𝑋) = 𝑂)    ⇒   ⊢ ((𝜑 ∧ 𝜓) → (𝑋 + 𝑁) = 𝑂)
Theorem	grpridd 12641*	Deduce right identity from left inverse and left identity in an associative structure (such as a group). (Contributed by NM, 10-Aug-2013.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ (𝜑 → 𝑂 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 𝑂) = 𝑥)
7.1.3  Semigroups A semigroup (Smgrp, see df-sgrp 12643) is a set together with an associative binary operation (see Wikipedia, Semigroup, 8-Jan-2020, https://en.wikipedia.org/wiki/Semigroup 12643). 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 12642	Extend class notation with class of all semigroups.
class Smgrp
Definition	df-sgrp 12643*	A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 12610), 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 12644*	The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ Smgrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
Theorem	issgrpv 12645*	The predicate "is a semigroup" for a structure which is a set. (Contributed by AV, 1-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Smgrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))))
Theorem	issgrpn0 12646*	The predicate "is a semigroup" for a structure with a nonempty base set. (Contributed by AV, 1-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝐴 ∈ 𝐵 → (𝑀 ∈ Smgrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))))
Theorem	isnsgrp 12647	A condition for a structure not to be a semigroup. (Contributed by AV, 30-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (((𝑋 ⚬ 𝑌) ⚬ 𝑍) ≠ (𝑋 ⚬ (𝑌 ⚬ 𝑍)) → 𝑀 ∉ Smgrp))
Theorem	sgrpmgm 12648	A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ (𝑀 ∈ Smgrp → 𝑀 ∈ Mgm)
Theorem	sgrpass 12649	A semigroup operation is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 30-Jan-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⚬ = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ⚬ 𝑌) ⚬ 𝑍) = (𝑋 ⚬ (𝑌 ⚬ 𝑍)))
Theorem	sgrp0 12650	Any set with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021.)
⊢ ((𝑀 ∈ 𝑉 ∧ (Base‘𝑀) = ∅) → 𝑀 ∈ Smgrp)
Theorem	sgrp1 12651	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)
7.1.4  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 12653, 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 12655. 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 12652	Extend class notation with class of all monoids.
class Mnd
Definition	df-mnd 12653*	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 12659), whose operation is associative (see mndass 12660) and has a two-sided neutral element (see mndid 12661), see also ismnd 12655. (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.)
⊢ Mnd = {𝑔 ∈ Smgrp ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)}
Theorem	ismnddef 12654*	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 12655*	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 12659), whose operation is associative (so, a semigroup, see also mndass 12660) and has a two-sided neutral element (see mndid 12661). (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd ↔ (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 + 𝑏) ∈ 𝐵 ∧ ∀𝑐 ∈ 𝐵 ((𝑎 + 𝑏) + 𝑐) = (𝑎 + (𝑏 + 𝑐))) ∧ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎)))
Theorem	sgrpidmndm 12656*	A semigroup with an identity element which is inhabited is a monoid. Of course there could be monoids with the empty set as identity element, 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 12657	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 12658	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 12659	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 12660	A monoid operation is associative. (Contributed by NM, 14-Aug-2011.) (Proof shortened by AV, 8-Feb-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	mndid 12661*	A monoid has a two-sided identity element. (Contributed by NM, 16-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → ∃𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥))
Theorem	mndideu 12662*	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 12663	Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑌 + 𝑍) = (𝑍 + 𝑌))    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌))
Theorem	mnd12g 12664	Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))    ⇒   ⊢ (𝜑 → (𝑋 + (𝑌 + 𝑍)) = (𝑌 + (𝑋 + 𝑍)))
Theorem	mnd4g 12665	Commutative/associative law for commutative monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑌 + 𝑍) = (𝑍 + 𝑌))    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊)))
Theorem	mndidcl 12666	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 12667	The base set of a monoid is not empty. (It is also inhabited, as seen at mndidcl 12666). Statement in [Lang] p. 3. (Contributed by AV, 29-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → 𝐵 ≠ ∅)
Theorem	hashfinmndnn 12668	A finite monoid has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ)
Theorem	mndplusf 12669	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 12670	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 12671	The identity element of a monoid is a left identity. (Contributed by NM, 18-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
Theorem	mndrid 12672	The identity element of a monoid is a right identity. (Contributed by NM, 18-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)
Theorem	ismndd 12673*	Deduce a monoid from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 0 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Mnd)
Theorem	mndpfo 12674	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 12675	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 12676*	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 12677	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	mndinvmod 12678*	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	mnd1 12679	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 12680	The singleton element of a trivial monoid is its identity element. (Contributed by AV, 23-Jan-2020.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (0g‘𝑀) = 𝐼)
7.1.5  Monoid homomorphisms and submonoids
Syntax	cmhm 12681	Hom-set generator class for monoids.
class MndHom
Syntax	csubmnd 12682	Class function taking a monoid to its lattice of submonoids.
class SubMnd
Definition	df-mhm 12683*	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‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))})
Definition	df-submnd 12684*	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 12685*	Property of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝑌 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)))
Theorem	mhmrcl1 12686	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑆 ∈ Mnd)
Theorem	mhmrcl2 12687	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑇 ∈ Mnd)
Theorem	mhmf 12688	A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:𝐵⟶𝐶)
Theorem	mhmpropd 12689*	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 12690	A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)))
Theorem	mhm0 12691	A monoid homomorphism preserves zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 0 = (0g‘𝑆)    &   ⊢ 𝑌 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹‘ 0 ) = 𝑌)
Theorem	idmhm 12692	The identity homomorphism on a monoid. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mnd → ( I ↾ 𝐵) ∈ (𝑀 MndHom 𝑀))
Theorem	mhmf1o 12693	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 12694	Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑀 ∈ Mnd)
Theorem	issubm 12695*	Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)))
Theorem	issubmd 12696*	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 12697	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 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. (Contributed by AV, 17-Feb-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = (Base‘𝐻)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) → ((𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → 𝑆 ∈ (SubMnd‘𝐺)))
Theorem	submss 12698	Submonoids are subsets of the base set. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 ⊆ 𝐵)
Theorem	submid 12699	Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mnd → 𝐵 ∈ (SubMnd‘𝑀))
Theorem	subm0cl 12700	Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 0 = (0g‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 ∈ 𝑆)