| Metamath
Proof Explorer Theorem List (p. 188 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | gsumprval 18701 | Value of the group sum operation over a pair of sequential integers. (Contributed by AV, 14-Dec-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 = (𝑀 + 1)) & ⊢ (𝜑 → 𝐹:{𝑀, 𝑁}⟶𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐹‘𝑀) + (𝐹‘𝑁))) | ||
| Theorem | gsumpr12val 18702 | Value of the group sum operation over the pair {1, 2}. (Contributed by AV, 14-Dec-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:{1, 2}⟶𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐹‘1) + (𝐹‘2))) | ||
| Syntax | cmgmhm 18703 | Hom-set generator class for magmas. |
| class MgmHom | ||
| Syntax | csubmgm 18704 | Class function taking a magma to its lattice of submagmas. |
| class SubMgm | ||
| Definition | df-mgmhm 18705* | 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 18706* | 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 18707 | Reverse closure of a magma homomorphism. (Contributed by AV, 24-Feb-2020.) |
| ⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → (𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm)) | ||
| Theorem | submgmrcl 18708 | Reverse closure for submagmas. (Contributed by AV, 24-Feb-2020.) |
| ⊢ (𝑆 ∈ (SubMgm‘𝑀) → 𝑀 ∈ Mgm) | ||
| Theorem | ismgmhm 18709* | Property of a magma homomorphism. (Contributed by AV, 25-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ ((𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))))) | ||
| Theorem | mgmhmf 18710 | A magma homomorphism is a function. (Contributed by AV, 25-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 MgmHom 𝑇) → 𝐹:𝐵⟶𝐶) | ||
| Theorem | mgmhmpropd 18711* | 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 18712 | A magma homomorphism preserves the binary operation. (Contributed by AV, 25-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌))) | ||
| Theorem | mgmhmf1o 18713 | 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 18714 | The identity homomorphism on a magma. (Contributed by AV, 27-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑀 ∈ Mgm → ( I ↾ 𝐵) ∈ (𝑀 MgmHom 𝑀)) | ||
| Theorem | issubmgm 18715* | Expand definition of a submagma. (Contributed by AV, 25-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ Mgm → (𝑆 ∈ (SubMgm‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆))) | ||
| Theorem | issubmgm2 18716 | Submagmas are subsets that are also magmas. (Contributed by AV, 25-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝐻 = (𝑀 ↾s 𝑆) ⇒ ⊢ (𝑀 ∈ Mgm → (𝑆 ∈ (SubMgm‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 𝐻 ∈ Mgm))) | ||
| Theorem | rabsubmgmd 18717* | Deduction for proving that a restricted class abstraction is a submagma. (Contributed by AV, 26-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Mgm) & ⊢ ((𝜑 ∧ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ (𝜃 ∧ 𝜏))) → 𝜂) & ⊢ (𝑧 = 𝑥 → (𝜓 ↔ 𝜃)) & ⊢ (𝑧 = 𝑦 → (𝜓 ↔ 𝜏)) & ⊢ (𝑧 = (𝑥 + 𝑦) → (𝜓 ↔ 𝜂)) ⇒ ⊢ (𝜑 → {𝑧 ∈ 𝐵 ∣ 𝜓} ∈ (SubMgm‘𝑀)) | ||
| Theorem | submgmss 18718 | Submagmas are subsets of the base set. (Contributed by AV, 26-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑆 ∈ (SubMgm‘𝑀) → 𝑆 ⊆ 𝐵) | ||
| Theorem | submgmid 18719 | Every magma is trivially a submagma of itself. (Contributed by AV, 26-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑀 ∈ Mgm → 𝐵 ∈ (SubMgm‘𝑀)) | ||
| Theorem | submgmcl 18720 | Submagmas are closed under the magma operation. (Contributed by AV, 26-Feb-2020.) |
| ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑆 ∈ (SubMgm‘𝑀) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆) | ||
| Theorem | submgmmgm 18721 | Submagmas are themselves magmas under the given operation. (Contributed by AV, 26-Feb-2020.) |
| ⊢ 𝐻 = (𝑀 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMgm‘𝑀) → 𝐻 ∈ Mgm) | ||
| Theorem | submgmbas 18722 | The base set of a submagma. (Contributed by AV, 26-Feb-2020.) |
| ⊢ 𝐻 = (𝑀 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMgm‘𝑀) → 𝑆 = (Base‘𝐻)) | ||
| Theorem | subsubmgm 18723 | A submagma of a submagma is a submagma. (Contributed by AV, 26-Feb-2020.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMgm‘𝐺) → (𝐴 ∈ (SubMgm‘𝐻) ↔ (𝐴 ∈ (SubMgm‘𝐺) ∧ 𝐴 ⊆ 𝑆))) | ||
| Theorem | resmgmhm 18724 | Restriction of a magma homomorphism to a submagma is a homomorphism. (Contributed by AV, 26-Feb-2020.) |
| ⊢ 𝑈 = (𝑆 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ 𝑋 ∈ (SubMgm‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MgmHom 𝑇)) | ||
| Theorem | resmgmhm2 18725 | One direction of resmgmhm2b 18726. (Contributed by AV, 26-Feb-2020.) |
| ⊢ 𝑈 = (𝑇 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑈) ∧ 𝑋 ∈ (SubMgm‘𝑇)) → 𝐹 ∈ (𝑆 MgmHom 𝑇)) | ||
| Theorem | resmgmhm2b 18726 | Restriction of the codomain of a homomorphism. (Contributed by AV, 26-Feb-2020.) |
| ⊢ 𝑈 = (𝑇 ↾s 𝑋) ⇒ ⊢ ((𝑋 ∈ (SubMgm‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MgmHom 𝑇) ↔ 𝐹 ∈ (𝑆 MgmHom 𝑈))) | ||
| Theorem | mgmhmco 18727 | The composition of magma homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.) |
| ⊢ ((𝐹 ∈ (𝑇 MgmHom 𝑈) ∧ 𝐺 ∈ (𝑆 MgmHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 MgmHom 𝑈)) | ||
| Theorem | mgmhmima 18728 | The homomorphic image of a submagma is a submagma. (Contributed by AV, 27-Feb-2020.) |
| ⊢ ((𝐹 ∈ (𝑀 MgmHom 𝑁) ∧ 𝑋 ∈ (SubMgm‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubMgm‘𝑁)) | ||
| Theorem | mgmhmeql 18729 | The equalizer of two magma homomorphisms is a submagma. (Contributed by AV, 27-Feb-2020.) |
| ⊢ ((𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ 𝐺 ∈ (𝑆 MgmHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubMgm‘𝑆)) | ||
| Theorem | submgmacs 18730 | Submagmas are an algebraic closure system. (Contributed by AV, 27-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Mgm → (SubMgm‘𝐺) ∈ (ACS‘𝐵)) | ||
A semigroup (Smgrp, see df-sgrp 18732) is a set together with an associative binary operation (see Wikipedia, Semigroup, 8-Jan-2020, https://en.wikipedia.org/wiki/Semigroup 18732). 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 18731 | Extend class notation with class of all semigroups. |
| class Smgrp | ||
| Definition | df-sgrp 18732* | A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 18653), 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 18733* | The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ Smgrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) | ||
| Theorem | issgrpv 18734* | The predicate "is a semigroup" for a structure which is a set. (Contributed by AV, 1-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Smgrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))) | ||
| Theorem | issgrpn0 18735* | The predicate "is a semigroup" for a structure with a nonempty base set. (Contributed by AV, 1-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝑀 ∈ Smgrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))) | ||
| Theorem | isnsgrp 18736 | A condition for a structure not to be a semigroup. (Contributed by AV, 30-Jan-2020.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (((𝑋 ⚬ 𝑌) ⚬ 𝑍) ≠ (𝑋 ⚬ (𝑌 ⚬ 𝑍)) → 𝑀 ∉ Smgrp)) | ||
| Theorem | sgrpmgm 18737 | A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
| ⊢ (𝑀 ∈ Smgrp → 𝑀 ∈ Mgm) | ||
| Theorem | sgrpass 18738 | A semigroup operation is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 30-Jan-2020.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⚬ = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Smgrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ⚬ 𝑌) ⚬ 𝑍) = (𝑋 ⚬ (𝑌 ⚬ 𝑍))) | ||
| Theorem | sgrpcl 18739 | Closure of the operation of a semigroup. (Contributed by AV, 15-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⚬ = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Smgrp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⚬ 𝑌) ∈ 𝐵) | ||
| Theorem | sgrp0 18740 | Any set with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021.) |
| ⊢ ((𝑀 ∈ 𝑉 ∧ (Base‘𝑀) = ∅) → 𝑀 ∈ Smgrp) | ||
| Theorem | sgrp0b 18741 | 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 18742 | 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 18743* | Deduce a semigroup from its properties. (Contributed by AV, 13-Feb-2025.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) ⇒ ⊢ (𝜑 → 𝐺 ∈ Smgrp) | ||
| Theorem | sgrppropd 18744* | 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 18745 | Structure product pointwise sums are closed when the factors are semigroups. (Contributed by AV, 21-Feb-2025.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅:𝐼⟶Smgrp) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 + 𝐺) ∈ 𝐵) | ||
| Theorem | prdssgrpd 18746 | The product of a family of semigroups is a semigroup. (Contributed by AV, 21-Feb-2025.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Smgrp) ⇒ ⊢ (𝜑 → 𝑌 ∈ Smgrp) | ||
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 18748, 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 18750. 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 18747 | Extend class notation with class of all monoids. |
| class Mnd | ||
| Definition | df-mnd 18748* | 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 18755), whose operation is associative (see mndass 18756) and has a two-sided neutral element (see mndid 18757), see also ismnd 18750. (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.) |
| ⊢ Mnd = {𝑔 ∈ Smgrp ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)} | ||
| Theorem | ismnddef 18749* | 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 18750* | 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 18755), whose operation is associative (so, a semigroup, see also mndass 18756) and has a two-sided neutral element (see mndid 18757). (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd ↔ (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 + 𝑏) ∈ 𝐵 ∧ ∀𝑐 ∈ 𝐵 ((𝑎 + 𝑏) + 𝑐) = (𝑎 + (𝑏 + 𝑐))) ∧ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎))) | ||
| Theorem | isnmnd 18751* | 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 18752* | 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 18950 and pwmndid 18949), 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 18753 | 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 18754 | 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 18755 | 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 18756 | A monoid operation is associative. (Contributed by NM, 14-Aug-2011.) (Proof shortened by AV, 8-Feb-2020.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
| Theorem | mndid 18757* | A monoid has a two-sided identity element. (Contributed by NM, 16-Aug-2011.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → ∃𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥)) | ||
| Theorem | mndideu 18758* | 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 18759 | Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → (𝑌 + 𝑍) = (𝑍 + 𝑌)) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌)) | ||
| Theorem | mnd12g 18760 | Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) ⇒ ⊢ (𝜑 → (𝑋 + (𝑌 + 𝑍)) = (𝑌 + (𝑋 + 𝑍))) | ||
| Theorem | mnd4g 18761 | Commutative/associative law for commutative monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → (𝑌 + 𝑍) = (𝑍 + 𝑌)) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) | ||
| Theorem | mndidcl 18762 | 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 18763 | The base set of a monoid is not empty. Statement in [Lang] p. 3. (Contributed by AV, 29-Dec-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → 𝐵 ≠ ∅) | ||
| Theorem | hashfinmndnn 18764 | A finite monoid has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ) | ||
| Theorem | mndplusf 18765 | 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 18766 | 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 18767 | The identity element of a monoid is a left identity. (Contributed by NM, 18-Aug-2011.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) | ||
| Theorem | mndrid 18768 | The identity element of a monoid is a right identity. (Contributed by NM, 18-Aug-2011.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋) | ||
| Theorem | ismndd 18769* | Deduce a monoid from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 0 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) ⇒ ⊢ (𝜑 → 𝐺 ∈ Mnd) | ||
| Theorem | mndpfo 18770 | 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 18771 | 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 18772* | 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 18773 | 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 18774* | Characterize a submonoid by closure properties. (Contributed by Mario Carneiro, 10-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) → (𝐻 ∈ Mnd ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)) | ||
| Theorem | ress0g 18775 | 0g is unaffected by restriction. This is a bit more generic than submnd0 18776. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 0 = (0g‘𝑆)) | ||
| Theorem | submnd0 18776 | 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 18923 and smndex1n0mnd 18925). (Contributed by Mario Carneiro, 10-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆)) → 0 = (0g‘𝐻)) | ||
| Theorem | mndinvmod 18777* | 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 18778 | 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 18779 | 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 18780 | 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 18781 | 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 18782* | 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 18783 | The product of a family of monoids is a monoid. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Mnd) ⇒ ⊢ (𝜑 → 𝑌 ∈ Mnd) | ||
| Theorem | prds0g 18784 | Zero in a product of monoids. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Mnd) ⇒ ⊢ (𝜑 → (0g ∘ 𝑅) = (0g‘𝑌)) | ||
| Theorem | pwsmnd 18785 | The structure power of a monoid is a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Mnd) | ||
| Theorem | pws0g 18786 | Zero in a structure power of a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) → (𝐼 × { 0 }) = (0g‘𝑌)) | ||
| Theorem | imasmnd2 18787* | 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 18788* | 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 18789 | 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 18790 | The binary product of monoids is a monoid. (Contributed by Mario Carneiro, 20-Aug-2015.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑇 ∈ Mnd) | ||
| Theorem | xpsmnd0 18791 | The identity element of a binary product of monoids. (Contributed by AV, 25-Feb-2025.) |
| ⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (0g‘𝑇) = 〈(0g‘𝑅), (0g‘𝑆)〉) | ||
| Theorem | mnd1 18792 | 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 18793 | The singleton element of a trivial monoid is its identity element. (Contributed by AV, 23-Jan-2020.) |
| ⊢ 𝑀 = {〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉} ⇒ ⊢ (𝐼 ∈ 𝑉 → (0g‘𝑀) = 𝐼) | ||
| Syntax | cmhm 18794 | Hom-set generator class for monoids. |
| class MndHom | ||
| Syntax | csubmnd 18795 | Class function taking a monoid to its lattice of submonoids. |
| class SubMnd | ||
| Definition | df-mhm 18796* | 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 18797* | 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 18798* | 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 18799* | Deduction version of ismhm 18798. (Contributed by SN, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝑍 = (0g‘𝑇) & ⊢ (𝜑 → 𝑆 ∈ Mnd) & ⊢ (𝜑 → 𝑇 ∈ Mnd) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ (𝜑 → (𝐹‘ 0 ) = 𝑍) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆 MndHom 𝑇)) | ||
| Theorem | mhmrcl1 18800 | Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.) |
| ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑆 ∈ Mnd) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |