Home | Metamath
Proof Explorer Theorem List (p. 179 of 449) | < 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: | Metamath Proof Explorer
(1-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-tsr 17801 | Define the class of all totally ordered sets. (Contributed by FL, 1-Nov-2009.) |
⊢ TosetRel = {𝑟 ∈ PosetRel ∣ (dom 𝑟 × dom 𝑟) ⊆ (𝑟 ∪ ◡𝑟)} | ||
Theorem | isps 17802 | The predicate "is a poset" i.e. a transitive, reflexive, antisymmetric relation. (Contributed by NM, 11-May-2008.) |
⊢ (𝑅 ∈ 𝐴 → (𝑅 ∈ PosetRel ↔ (Rel 𝑅 ∧ (𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅)))) | ||
Theorem | psrel 17803 | A poset is a relation. (Contributed by NM, 12-May-2008.) |
⊢ (𝐴 ∈ PosetRel → Rel 𝐴) | ||
Theorem | psref2 17804 | A poset is antisymmetric and reflexive. (Contributed by FL, 3-Aug-2009.) |
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ ◡𝑅) = ( I ↾ ∪ ∪ 𝑅)) | ||
Theorem | pstr2 17805 | A poset is transitive. (Contributed by FL, 3-Aug-2009.) |
⊢ (𝑅 ∈ PosetRel → (𝑅 ∘ 𝑅) ⊆ 𝑅) | ||
Theorem | pslem 17806 | Lemma for psref 17808 and others. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ (𝑅 ∈ PosetRel → (((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) ∧ (𝐴 ∈ ∪ ∪ 𝑅 → 𝐴𝑅𝐴) ∧ ((𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵))) | ||
Theorem | psdmrn 17807 | The domain and range of a poset equal its field. (Contributed by NM, 13-May-2008.) |
⊢ (𝑅 ∈ PosetRel → (dom 𝑅 = ∪ ∪ 𝑅 ∧ ran 𝑅 = ∪ ∪ 𝑅)) | ||
Theorem | psref 17808 | A poset is reflexive. (Contributed by NM, 13-May-2008.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ∈ 𝑋) → 𝐴𝑅𝐴) | ||
Theorem | psrn 17809 | The range of a poset equals it domain. (Contributed by NM, 7-Jul-2008.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ (𝑅 ∈ PosetRel → 𝑋 = ran 𝑅) | ||
Theorem | psasym 17810 | A poset is antisymmetric. (Contributed by NM, 12-May-2008.) |
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵 ∧ 𝐵𝑅𝐴) → 𝐴 = 𝐵) | ||
Theorem | pstr 17811 | A poset is transitive. (Contributed by NM, 12-May-2008.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ ((𝑅 ∈ PosetRel ∧ 𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶) → 𝐴𝑅𝐶) | ||
Theorem | cnvps 17812 | The converse of a poset is a poset. In the general case (◡𝑅 ∈ PosetRel → 𝑅 ∈ PosetRel) is not true. See cnvpsb 17813 for a special case where the property holds. (Contributed by FL, 5-Jan-2009.) (Proof shortened by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝑅 ∈ PosetRel → ◡𝑅 ∈ PosetRel) | ||
Theorem | cnvpsb 17813 | The converse of a poset is a poset. (Contributed by FL, 5-Jan-2009.) |
⊢ (Rel 𝑅 → (𝑅 ∈ PosetRel ↔ ◡𝑅 ∈ PosetRel)) | ||
Theorem | psss 17814 | Any subset of a partially ordered set is partially ordered. (Contributed by FL, 24-Jan-2010.) |
⊢ (𝑅 ∈ PosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ PosetRel) | ||
Theorem | psssdm2 17815 | Field of a subposet. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ (𝑅 ∈ PosetRel → dom (𝑅 ∩ (𝐴 × 𝐴)) = (𝑋 ∩ 𝐴)) | ||
Theorem | psssdm 17816 | Field of a subposet. (Contributed by FL, 19-Sep-2011.) (Revised by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋) → dom (𝑅 ∩ (𝐴 × 𝐴)) = 𝐴) | ||
Theorem | istsr 17817 | The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ (𝑅 ∈ TosetRel ↔ (𝑅 ∈ PosetRel ∧ (𝑋 × 𝑋) ⊆ (𝑅 ∪ ◡𝑅))) | ||
Theorem | istsr2 17818* | The predicate is a toset. (Contributed by FL, 1-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ (𝑅 ∈ TosetRel ↔ (𝑅 ∈ PosetRel ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝑅𝑦 ∨ 𝑦𝑅𝑥))) | ||
Theorem | tsrlin 17819 | A toset is a linear order. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ TosetRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑅𝐵 ∨ 𝐵𝑅𝐴)) | ||
Theorem | tsrlemax 17820 | Two ways of saying a number is less than or equal to the maximum of two others. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ TosetRel ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑅if(𝐵𝑅𝐶, 𝐶, 𝐵) ↔ (𝐴𝑅𝐵 ∨ 𝐴𝑅𝐶))) | ||
Theorem | tsrps 17821 | A toset is a poset. (Contributed by Mario Carneiro, 9-Sep-2015.) |
⊢ (𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel) | ||
Theorem | cnvtsr 17822 | The converse of a toset is a toset. (Contributed by Mario Carneiro, 3-Sep-2015.) |
⊢ (𝑅 ∈ TosetRel → ◡𝑅 ∈ TosetRel ) | ||
Theorem | tsrss 17823 | Any subset of a totally ordered set is totally ordered. (Contributed by FL, 24-Jan-2010.) (Proof shortened by Mario Carneiro, 21-Nov-2013.) |
⊢ (𝑅 ∈ TosetRel → (𝑅 ∩ (𝐴 × 𝐴)) ∈ TosetRel ) | ||
Theorem | ledm 17824 | The domain of ≤ is ℝ*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.) |
⊢ ℝ* = dom ≤ | ||
Theorem | lern 17825 | The range of ≤ is ℝ*. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
⊢ ℝ* = ran ≤ | ||
Theorem | lefld 17826 | The field of the 'less or equal to' relationship on the extended real. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 4-May-2015.) |
⊢ ℝ* = ∪ ∪ ≤ | ||
Theorem | letsr 17827 | The "less than or equal to" relationship on the extended reals is a toset. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
⊢ ≤ ∈ TosetRel | ||
Syntax | cdir 17828 | Extend class notation with the class of directed sets. |
class DirRel | ||
Syntax | ctail 17829 | Extend class notation with the tail function for directed sets. |
class tail | ||
Definition | df-dir 17830 | Define the class of directed sets (the order relation itself is sometimes called a direction, and a directed set is a set equipped with a direction). (Contributed by Jeff Hankins, 25-Nov-2009.) |
⊢ DirRel = {𝑟 ∣ ((Rel 𝑟 ∧ ( I ↾ ∪ ∪ 𝑟) ⊆ 𝑟) ∧ ((𝑟 ∘ 𝑟) ⊆ 𝑟 ∧ (∪ ∪ 𝑟 × ∪ ∪ 𝑟) ⊆ (◡𝑟 ∘ 𝑟)))} | ||
Definition | df-tail 17831* | Define the tail function for directed sets. (Contributed by Jeff Hankins, 25-Nov-2009.) |
⊢ tail = (𝑟 ∈ DirRel ↦ (𝑥 ∈ ∪ ∪ 𝑟 ↦ (𝑟 “ {𝑥}))) | ||
Theorem | isdir 17832 | A condition for a relation to be a direction. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
⊢ 𝐴 = ∪ ∪ 𝑅 ⇒ ⊢ (𝑅 ∈ 𝑉 → (𝑅 ∈ DirRel ↔ ((Rel 𝑅 ∧ ( I ↾ 𝐴) ⊆ 𝑅) ∧ ((𝑅 ∘ 𝑅) ⊆ 𝑅 ∧ (𝐴 × 𝐴) ⊆ (◡𝑅 ∘ 𝑅))))) | ||
Theorem | reldir 17833 | A direction is a relation. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
⊢ (𝑅 ∈ DirRel → Rel 𝑅) | ||
Theorem | dirdm 17834 | A direction's domain is equal to its field. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
⊢ (𝑅 ∈ DirRel → dom 𝑅 = ∪ ∪ 𝑅) | ||
Theorem | dirref 17835 | A direction is reflexive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ DirRel ∧ 𝐴 ∈ 𝑋) → 𝐴𝑅𝐴) | ||
Theorem | dirtr 17836 | A direction is transitive. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
⊢ (((𝑅 ∈ DirRel ∧ 𝐶 ∈ 𝑉) ∧ (𝐴𝑅𝐵 ∧ 𝐵𝑅𝐶)) → 𝐴𝑅𝐶) | ||
Theorem | dirge 17837* | For any two elements of a directed set, there exists a third element greater than or equal to both. Note that this does not say that the two elements have a least upper bound. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
⊢ 𝑋 = dom 𝑅 ⇒ ⊢ ((𝑅 ∈ DirRel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ∃𝑥 ∈ 𝑋 (𝐴𝑅𝑥 ∧ 𝐵𝑅𝑥)) | ||
Theorem | tsrdir 17838 | A totally ordered set is a directed set. (Contributed by Jeff Hankins, 25-Nov-2009.) (Revised by Mario Carneiro, 22-Nov-2013.) |
⊢ (𝐴 ∈ TosetRel → 𝐴 ∈ DirRel) | ||
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 7150, binary operations are defined by a rule, and with df-ov 7148, 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 7148 (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 7148). The definition of magmas (Mgm, see df-mgm 17842) 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 17839 | Extend class notation with group addition as a function. |
class +𝑓 | ||
Syntax | cmgm 17840 | Extend class notation with class of all magmas. |
class Mgm | ||
Definition | df-plusf 17841* | 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 17852), while +g only has closure (mgmcl 17845). (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ +𝑓 = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)𝑦))) | ||
Definition | df-mgm 17842* | 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 17843* | The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵)) | ||
Theorem | ismgmn0 17844* | The predicate "is a magma" for a structure with a nonempty base set. (Contributed by AV, 29-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝑀 ∈ Mgm ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ⚬ 𝑦) ∈ 𝐵)) | ||
Theorem | mgmcl 17845 | Closure of the operation of a magma. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 13-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mgm ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⚬ 𝑌) ∈ 𝐵) | ||
Theorem | isnmgm 17846 | 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 17847 | 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. Formerly part of proof of grpissubg 18239. (Contributed by AV, 17-Feb-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = (Base‘𝐻) ⇒ ⊢ (((𝐺 ∈ Mgm ∧ 𝐻 ∈ Mgm) ∧ (𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆)) → (𝑋(+g‘𝐺)𝑌) ∈ 𝑆) | ||
Theorem | plusffval 17848* | The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 2-Mar-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+𝑓‘𝐺) ⇒ ⊢ ⨣ = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + 𝑦)) | ||
Theorem | plusfval 17849 | The group addition operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+𝑓‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ⨣ 𝑌) = (𝑋 + 𝑌)) | ||
Theorem | plusfeq 17850 | 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 | plusffn 17851 | The group addition operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ ⨣ = (+𝑓‘𝐺) ⇒ ⊢ ⨣ Fn (𝐵 × 𝐵) | ||
Theorem | mgmplusf 17852 | 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 | issstrmgm 17853* | Characterize a substructure as submagma by closure properties. (Contributed by AV, 30-Aug-2021.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐻 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐵) → (𝐻 ∈ Mgm ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)) | ||
Theorem | intopsn 17854 | The internal operation for a set is the trivial operation iff the set is a singleton. Formerly part of proof of ring1zr 19978. (Contributed by FL, 13-Feb-2010.) (Revised by AV, 23-Jan-2020.) |
⊢ (( ⚬ :(𝐵 × 𝐵)⟶𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ⚬ = {〈〈𝑍, 𝑍〉, 𝑍〉})) | ||
Theorem | mgmb1mgm1 17855 | 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 17856 | Any set with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021.) |
⊢ ((𝑀 ∈ 𝑉 ∧ (Base‘𝑀) = ∅) → 𝑀 ∈ Mgm) | ||
Theorem | mgm0b 17857 | The structure with an empty base set and any group operation is a magma. (Contributed by AV, 28-Aug-2021.) |
⊢ {〈(Base‘ndx), ∅〉, 〈(+g‘ndx), 𝑂〉} ∈ Mgm | ||
Theorem | mgm1 17858 | 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 | opifismgm 17859* | 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(𝜓, 𝐶, 𝐷)) & ⊢ (𝜑 → 𝐵 ≠ ∅) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → 𝐷 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑀 ∈ Mgm) | ||
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 17860) is an important property of monoids (see mndid 17911), and therefore also for groups (see grpid 18079), 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 16705. Related theorems which are already valid for magmas are provided in the following. | ||
Theorem | mgmidmo 17860* | 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 | grpidval 17861* | 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 | grpidpropd 17862* | 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 17863 | The group zero extractor is a function. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 0g Fn V | ||
Theorem | 0g0 17864 | The identity element function evaluates to the empty set on an empty structure. (Contributed by Stefan O'Rear, 2-Oct-2015.) |
⊢ ∅ = (0g‘∅) | ||
Theorem | ismgmid 17865* | 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 17866* | 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 17867* | 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 17868* | 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 17869* | 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 17870* | 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 17869) is equal to the two-sided identity element. (Contributed by AV, 26-Dec-2023.) |
⊢ (𝜑 → 𝐿 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝐵) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝐿 + 𝑥) = 𝑥) & ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑥 + 𝑅) = 𝑥) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝜑 → 𝐿 = 0 ) | ||
Theorem | grpidd 17871* | 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 17872* | 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 17873* | Lemma for grprinvd 17874. (Contributed by NM, 9-Aug-2013.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ (𝜑 → 𝑂 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂 + 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂) & ⊢ ((𝜑 ∧ 𝜓) → 𝑋 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝜓) → (𝑋 + 𝑋) = 𝑋) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝑋 = 𝑂) | ||
Theorem | grprinvd 17874* | 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 17875* | 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.) |
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ (𝜑 → 𝑂 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑂 + 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 𝑂) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 𝑂) = 𝑥) | ||
The symbol Σg is mostly used in the context of abelian groups. Therefore, it is usually called "group sum". It can be defined, however, in arbitrary magmas (then it should be called "iterated sum"). If the magma is not required to be commutative or associative, then the order of the summands and the order in which summations are done become important. If the magma is not unital, then one cannot define a meaningful empty sum. See Remark 2. in the comment for df-gsum 16706. | ||
Theorem | gsumvalx 17876* | Expand out the substitutions in df-gsum 16706. (Contributed by Mario Carneiro, 18-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑂 = {𝑠 ∈ 𝐵 ∣ ∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)} & ⊢ (𝜑 → 𝑊 = (◡𝐹 “ (V ∖ 𝑂))) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) & ⊢ (𝜑 → dom 𝐹 = 𝐴) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))))) | ||
Theorem | gsumval 17877* | Expand out the substitutions in df-gsum 16706. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑂 = {𝑠 ∈ 𝐵 ∣ ∀𝑡 ∈ 𝐵 ((𝑠 + 𝑡) = 𝑡 ∧ (𝑡 + 𝑠) = 𝑡)} & ⊢ (𝜑 → 𝑊 = (◡𝐹 “ (V ∖ 𝑂))) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = if(ran 𝐹 ⊆ 𝑂, 0 , if(𝐴 ∈ ran ..., (℩𝑥∃𝑚∃𝑛 ∈ (ℤ≥‘𝑚)(𝐴 = (𝑚...𝑛) ∧ 𝑥 = (seq𝑚( + , 𝐹)‘𝑛))), (℩𝑥∃𝑓(𝑓:(1...(♯‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(♯‘𝑊))))))) | ||
Theorem | gsumpropd 17878 | The group sum depends only on the base set and additive operation. Note that for entirely unrestricted functions, there can be dependency on out-of-domain values of the operation, so this is somewhat weaker than mndpropd 17926 etc. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Proof shortened by Mario Carneiro, 18-Sep-2015.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻)) & ⊢ (𝜑 → (+g‘𝐺) = (+g‘𝐻)) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹)) | ||
Theorem | gsumpropd2lem 17879* | Lemma for gsumpropd2 17880. (Contributed by Thierry Arnoux, 28-Jun-2017.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻)) & ⊢ ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g‘𝐺)𝑡) ∈ (Base‘𝐺)) & ⊢ ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g‘𝐺)𝑡) = (𝑠(+g‘𝐻)𝑡)) & ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → ran 𝐹 ⊆ (Base‘𝐺)) & ⊢ 𝐴 = (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐺) ∣ ∀𝑡 ∈ (Base‘𝐺)((𝑠(+g‘𝐺)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐺)𝑠) = 𝑡)})) & ⊢ 𝐵 = (◡𝐹 “ (V ∖ {𝑠 ∈ (Base‘𝐻) ∣ ∀𝑡 ∈ (Base‘𝐻)((𝑠(+g‘𝐻)𝑡) = 𝑡 ∧ (𝑡(+g‘𝐻)𝑠) = 𝑡)})) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹)) | ||
Theorem | gsumpropd2 17880* | A stronger version of gsumpropd 17878, working for magma, where only the closure of the addition operation on a common base is required, see gsummgmpropd 17881. (Contributed by Thierry Arnoux, 28-Jun-2017.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻)) & ⊢ ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g‘𝐺)𝑡) ∈ (Base‘𝐺)) & ⊢ ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g‘𝐺)𝑡) = (𝑠(+g‘𝐻)𝑡)) & ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → ran 𝐹 ⊆ (Base‘𝐺)) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹)) | ||
Theorem | gsummgmpropd 17881* | A stronger version of gsumpropd 17878 if at least one of the involved structures is a magma, see gsumpropd2 17880. (Contributed by AV, 31-Jan-2020.) |
⊢ (𝜑 → 𝐹 ∈ 𝑉) & ⊢ (𝜑 → 𝐺 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 ∈ 𝑋) & ⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻)) & ⊢ (𝜑 → 𝐺 ∈ Mgm) & ⊢ ((𝜑 ∧ (𝑠 ∈ (Base‘𝐺) ∧ 𝑡 ∈ (Base‘𝐺))) → (𝑠(+g‘𝐺)𝑡) = (𝑠(+g‘𝐻)𝑡)) & ⊢ (𝜑 → Fun 𝐹) & ⊢ (𝜑 → ran 𝐹 ⊆ (Base‘𝐺)) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹)) | ||
Theorem | gsumress 17882* | The group sum in a substructure is the same as the group sum in the original structure. The only requirement on the substructure is that it contain the identity element; neither 𝐺 nor 𝐻 need be groups. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 0 ∈ 𝑆) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (( 0 + 𝑥) = 𝑥 ∧ (𝑥 + 0 ) = 𝑥)) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹)) | ||
Theorem | gsumval1 17883* | Value of the group sum operation when every element being summed is an identity of 𝐺. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑂 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑂) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = 0 ) | ||
Theorem | gsum0 17884 | Value of the empty group sum. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 Σg ∅) = 0 | ||
Theorem | gsumval2a 17885* | 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 17886 | 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 17887 | 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 17888 | Value of the group sum operation over a pair of sequential integers. (Contributed by AV, 14-Dec-2018.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 = (𝑀 + 1)) & ⊢ (𝜑 → 𝐹:{𝑀, 𝑁}⟶𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐹‘𝑀) + (𝐹‘𝑁))) | ||
Theorem | gsumpr12val 17889 | Value of the group sum operation over the pair {1, 2}. (Contributed by AV, 14-Dec-2018.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:{1, 2}⟶𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐹‘1) + (𝐹‘2))) | ||
A semigroup (Smgrp, see df-sgrp 17891) is a set together with an associative binary operation (see Wikipedia, Semigroup, 8-Jan-2020, https://en.wikipedia.org/wiki/Semigroup 17891). 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 17890 | Extend class notation with class of all semigroups. |
class Smgrp | ||
Definition | df-sgrp 17891* | A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 17842), 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 17892* | The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ Smgrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) | ||
Theorem | issgrpv 17893* | The predicate "is a semigroup" for a structure which is a set. (Contributed by AV, 1-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ Smgrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))) | ||
Theorem | issgrpn0 17894* | The predicate "is a semigroup" for a structure with a nonempty base set. (Contributed by AV, 1-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝑀 ∈ Smgrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))) | ||
Theorem | isnsgrp 17895 | A condition for a structure not to be a semigroup. (Contributed by AV, 30-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (((𝑋 ⚬ 𝑌) ⚬ 𝑍) ≠ (𝑋 ⚬ (𝑌 ⚬ 𝑍)) → 𝑀 ∉ Smgrp)) | ||
Theorem | sgrpmgm 17896 | A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
⊢ (𝑀 ∈ Smgrp → 𝑀 ∈ Mgm) | ||
Theorem | sgrpass 17897 | A semigroup operation is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 30-Jan-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ ⚬ = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Smgrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ⚬ 𝑌) ⚬ 𝑍) = (𝑋 ⚬ (𝑌 ⚬ 𝑍))) | ||
Theorem | sgrp0 17898 | Any set with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021.) |
⊢ ((𝑀 ∈ 𝑉 ∧ (Base‘𝑀) = ∅) → 𝑀 ∈ Smgrp) | ||
Theorem | sgrp0b 17899 | 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 17900 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |