P. 135 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13401-13500   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-sgrp 13401*	A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 13355), 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 13402*	The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ Smgrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))
Theorem	issgrpv 13403*	The predicate "is a semigroup" for a structure which is a set. (Contributed by AV, 1-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Smgrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))))
Theorem	issgrpn0 13404*	The predicate "is a semigroup" for a structure with a nonempty base set. (Contributed by AV, 1-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ (𝐴 ∈ 𝐵 → (𝑀 ∈ Smgrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))))
Theorem	isnsgrp 13405	A condition for a structure not to be a semigroup. (Contributed by AV, 30-Jan-2020.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (((𝑋 ⚬ 𝑌) ⚬ 𝑍) ≠ (𝑋 ⚬ (𝑌 ⚬ 𝑍)) → 𝑀 ∉ Smgrp))
Theorem	sgrpmgm 13406	A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.)
⊢ (𝑀 ∈ Smgrp → 𝑀 ∈ Mgm)
Theorem	sgrpass 13407	A semigroup operation is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 30-Jan-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⚬ = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ⚬ 𝑌) ⚬ 𝑍) = (𝑋 ⚬ (𝑌 ⚬ 𝑍)))
Theorem	sgrpcl 13408	Closure of the operation of a semigroup. (Contributed by AV, 15-Feb-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ⚬ = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⚬ 𝑌) ∈ 𝐵)
Theorem	sgrp0 13409	Any set with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021.)
⊢ ((𝑀 ∈ 𝑉 ∧ (Base‘𝑀) = ∅) → 𝑀 ∈ Smgrp)
Theorem	sgrp1 13410	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 13411*	Deduce a semigroup from its properties. (Contributed by AV, 13-Feb-2025.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Smgrp)
Theorem	sgrppropd 13412*	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 13413	Structure product pointwise sums are closed when the factors are semigroups. (Contributed by AV, 21-Feb-2025.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Smgrp)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝐹 + 𝐺) ∈ 𝐵)
Theorem	prdssgrpd 13414	The product of a family of semigroups is a semigroup. (Contributed by AV, 21-Feb-2025.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Smgrp)    ⇒   ⊢ (𝜑 → 𝑌 ∈ Smgrp)
7.1.5  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 13416, 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 13418. 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 13415	Extend class notation with class of all monoids.
class Mnd
Definition	df-mnd 13416*	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 13422), whose operation is associative (see mndass 13423) and has a two-sided neutral element (see mndid 13424), see also ismnd 13418. (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.)
⊢ Mnd = {𝑔 ∈ Smgrp ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)}
Theorem	ismnddef 13417*	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 13418*	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 13422), whose operation is associative (so, a semigroup, see also mndass 13423) and has a two-sided neutral element (see mndid 13424). (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd ↔ (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 + 𝑏) ∈ 𝐵 ∧ ∀𝑐 ∈ 𝐵 ((𝑎 + 𝑏) + 𝑐) = (𝑎 + (𝑏 + 𝑐))) ∧ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎)))
Theorem	sgrpidmndm 13419*	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 13420	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 13421	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 13422	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 13423	A monoid operation is associative. (Contributed by NM, 14-Aug-2011.) (Proof shortened by AV, 8-Feb-2020.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	mndid 13424*	A monoid has a two-sided identity element. (Contributed by NM, 16-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → ∃𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥))
Theorem	mndideu 13425*	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 13426	Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑌 + 𝑍) = (𝑍 + 𝑌))    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌))
Theorem	mnd12g 13427	Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))    ⇒   ⊢ (𝜑 → (𝑋 + (𝑌 + 𝑍)) = (𝑌 + (𝑋 + 𝑍)))
Theorem	mnd4g 13428	Commutative/associative law for commutative monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑊 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑌 + 𝑍) = (𝑍 + 𝑌))    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊)))
Theorem	mndidcl 13429	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 13430	The base set of a monoid is not empty. (It is also inhabited, as seen at mndidcl 13429). Statement in [Lang] p. 3. (Contributed by AV, 29-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → 𝐵 ≠ ∅)
Theorem	hashfinmndnn 13431	A finite monoid has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ)
Theorem	mndplusf 13432	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 13433	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 13434	The identity element of a monoid is a left identity. (Contributed by NM, 18-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
Theorem	mndrid 13435	The identity element of a monoid is a right identity. (Contributed by NM, 18-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)
Theorem	ismndd 13436*	Deduce a monoid from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 0 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Mnd)
Theorem	mndpfo 13437	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 13438	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 13439*	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 13440	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 13441*	Characterize a submonoid by closure properties. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) → (𝐻 ∈ Mnd ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆))
Theorem	ress0g 13442	0g is unaffected by restriction. This is a bit more generic than submnd0 13443. (Contributed by Thierry Arnoux, 23-Oct-2017.)
⊢ 𝑆 = (𝑅 ↾s 𝐴)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 0 = (0g‘𝑆))
Theorem	submnd0 13443	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. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆)) → 0 = (0g‘𝐻))
Theorem	mndinvmod 13444*	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	prdsplusgcl 13445	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 13446*	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 13447	The product of a family of monoids is a monoid. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Mnd)    ⇒   ⊢ (𝜑 → 𝑌 ∈ Mnd)
Theorem	prds0g 13448	The identity in a product of monoids. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Mnd)    ⇒   ⊢ (𝜑 → (0g ∘ 𝑅) = (0g‘𝑌))
Theorem	pwsmnd 13449	The structure power of a monoid is a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Mnd)
Theorem	pws0g 13450	The identity in a structure power of a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) → (𝐼 × { 0 }) = (0g‘𝑌))
Theorem	imasmnd2 13451*	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 13452*	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 13453	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	mnd1 13454	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 13455	The singleton element of a trivial monoid is its identity element. (Contributed by AV, 23-Jan-2020.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (0g‘𝑀) = 𝐼)
7.1.6  Monoid homomorphisms and submonoids
Syntax	cmhm 13456	Hom-set generator class for monoids.
class MndHom
Syntax	csubmnd 13457	Class function taking a monoid to its lattice of submonoids.
class SubMnd
Definition	df-mhm 13458*	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 13459*	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 13460*	Property of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    &   ⊢ 0 = (0g‘𝑆)    &   ⊢ 𝑌 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌)))
Theorem	mhmex 13461	The set of monoid homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.)
⊢ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) → (𝑆 MndHom 𝑇) ∈ V)
Theorem	mhmrcl1 13462	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑆 ∈ Mnd)
Theorem	mhmrcl2 13463	Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑇 ∈ Mnd)
Theorem	mhmf 13464	A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐶 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:𝐵⟶𝐶)
Theorem	mhmpropd 13465*	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 13466	A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)))
Theorem	mhm0 13467	A monoid homomorphism preserves zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 0 = (0g‘𝑆)    &   ⊢ 𝑌 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹‘ 0 ) = 𝑌)
Theorem	idmhm 13468	The identity homomorphism on a monoid. (Contributed by AV, 14-Feb-2020.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mnd → ( I ↾ 𝐵) ∈ (𝑀 MndHom 𝑀))
Theorem	mhmf1o 13469	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 13470	Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑀 ∈ Mnd)
Theorem	issubm 13471*	Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 0 = (0g‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)))
Theorem	issubm2 13472	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	issubmd 13473*	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 13474	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 13475	Submonoids are subsets of the base set. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 ⊆ 𝐵)
Theorem	submid 13476	Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (𝑀 ∈ Mnd → 𝐵 ∈ (SubMnd‘𝑀))
Theorem	subm0cl 13477	Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 0 = (0g‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 ∈ 𝑆)
Theorem	submcl 13478	Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑆 ∈ (SubMnd‘𝑀) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆)
Theorem	submmnd 13479	Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝐻 ∈ Mnd)
Theorem	submbas 13480	The base set of a submonoid. (Contributed by Stefan O'Rear, 15-Jun-2015.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 = (Base‘𝐻))
Theorem	subm0 13481	Submonoids have the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐻 = (𝑀 ↾s 𝑆)    &   ⊢ 0 = (0g‘𝑀)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 = (0g‘𝐻))
Theorem	subsubm 13482	A submonoid of a submonoid is a submonoid. (Contributed by Mario Carneiro, 21-Jun-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubMnd‘𝐺) → (𝐴 ∈ (SubMnd‘𝐻) ↔ (𝐴 ∈ (SubMnd‘𝐺) ∧ 𝐴 ⊆ 𝑆)))
Theorem	0subm 13483	The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Mnd → { 0 } ∈ (SubMnd‘𝐺))
Theorem	insubm 13484	The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024.)
⊢ ((𝐴 ∈ (SubMnd‘𝑀) ∧ 𝐵 ∈ (SubMnd‘𝑀)) → (𝐴 ∩ 𝐵) ∈ (SubMnd‘𝑀))
Theorem	0mhm 13485	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 13486	Restriction of a monoid homomorphism to a submonoid is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MndHom 𝑇))
Theorem	resmhm2 13487	One direction of resmhm2b 13488. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → 𝐹 ∈ (𝑆 MndHom 𝑇))
Theorem	resmhm2b 13488	Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ (𝑆 MndHom 𝑈)))
Theorem	mhmco 13489	The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐹 ∈ (𝑇 MndHom 𝑈) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 MndHom 𝑈))
Theorem	mhmima 13490	The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015.)
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (SubMnd‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubMnd‘𝑁))
Theorem	mhmeql 13491	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‘𝑆))
7.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-igsum 13258. If order is not significant, it is simpler to use families instead.
Theorem	gsumvallem2 13492*	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 13493	Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014.)
⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → 𝐹:𝐴⟶𝑆)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹))
Theorem	gsumfzz 13494*	Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by Jim Kingdon, 15-Aug-2025.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐺 Σg (𝑘 ∈ (𝑀...𝑁) ↦ 0 )) = 0 )
Theorem	gsumwsubmcl 13495	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	gsumwcl 13496	Closure of the composite of a word in a structure 𝐺. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵)
Theorem	gsumwmhm 13497	Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊)))
Theorem	gsumfzcl 13498	Closure of a finite group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 16-Aug-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵)
7.2  Groups
7.2.1  Definition and basic properties
Syntax	cgrp 13499	Extend class notation with class of all groups.
class Grp
Syntax	cminusg 13500	Extend class notation with inverse of group element.
class invg