Home | Metamath
Proof Explorer Theorem List (p. 459 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | issubmgm 45801* | Expand definition of a submagma. (Contributed by AV, 25-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) β β’ (π β Mgm β (π β (SubMgmβπ) β (π β π΅ β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π))) | ||
Theorem | issubmgm2 45802 | Submagmas are subsets that are also magmas. (Contributed by AV, 25-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ π» = (π βΎs π) β β’ (π β Mgm β (π β (SubMgmβπ) β (π β π΅ β§ π» β Mgm))) | ||
Theorem | rabsubmgmd 45803* | Deduction for proving that a restricted class abstraction is a submagma. (Contributed by AV, 26-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β Mgm) & β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π β§ π))) β π) & β’ (π§ = π₯ β (π β π)) & β’ (π§ = π¦ β (π β π)) & β’ (π§ = (π₯ + π¦) β (π β π)) β β’ (π β {π§ β π΅ β£ π} β (SubMgmβπ)) | ||
Theorem | submgmss 45804 | Submagmas are subsets of the base set. (Contributed by AV, 26-Feb-2020.) |
β’ π΅ = (Baseβπ) β β’ (π β (SubMgmβπ) β π β π΅) | ||
Theorem | submgmid 45805 | Every magma is trivially a submagma of itself. (Contributed by AV, 26-Feb-2020.) |
β’ π΅ = (Baseβπ) β β’ (π β Mgm β π΅ β (SubMgmβπ)) | ||
Theorem | submgmcl 45806 | Submagmas are closed under the monoid operation. (Contributed by AV, 26-Feb-2020.) |
β’ + = (+gβπ) β β’ ((π β (SubMgmβπ) β§ π β π β§ π β π) β (π + π) β π) | ||
Theorem | submgmmgm 45807 | Submagmas are themselves magmas under the given operation. (Contributed by AV, 26-Feb-2020.) |
β’ π» = (π βΎs π) β β’ (π β (SubMgmβπ) β π» β Mgm) | ||
Theorem | submgmbas 45808 | The base set of a submagma. (Contributed by AV, 26-Feb-2020.) |
β’ π» = (π βΎs π) β β’ (π β (SubMgmβπ) β π = (Baseβπ»)) | ||
Theorem | subsubmgm 45809 | A submagma of a submagma is a submagma. (Contributed by AV, 26-Feb-2020.) |
β’ π» = (πΊ βΎs π) β β’ (π β (SubMgmβπΊ) β (π΄ β (SubMgmβπ») β (π΄ β (SubMgmβπΊ) β§ π΄ β π))) | ||
Theorem | resmgmhm 45810 | Restriction of a magma homomorphism to a submagma is a homomorphism. (Contributed by AV, 26-Feb-2020.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π MgmHom π) β§ π β (SubMgmβπ)) β (πΉ βΎ π) β (π MgmHom π)) | ||
Theorem | resmgmhm2 45811 | One direction of resmgmhm2b 45812. (Contributed by AV, 26-Feb-2020.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π MgmHom π) β§ π β (SubMgmβπ)) β πΉ β (π MgmHom π)) | ||
Theorem | resmgmhm2b 45812 | Restriction of the codomain of a homomorphism. (Contributed by AV, 26-Feb-2020.) |
β’ π = (π βΎs π) β β’ ((π β (SubMgmβπ) β§ ran πΉ β π) β (πΉ β (π MgmHom π) β πΉ β (π MgmHom π))) | ||
Theorem | mgmhmco 45813 | The composition of magma homomorphisms is a homomorphism. (Contributed by AV, 27-Feb-2020.) |
β’ ((πΉ β (π MgmHom π) β§ πΊ β (π MgmHom π)) β (πΉ β πΊ) β (π MgmHom π)) | ||
Theorem | mgmhmima 45814 | The homomorphic image of a submagma is a submagma. (Contributed by AV, 27-Feb-2020.) |
β’ ((πΉ β (π MgmHom π) β§ π β (SubMgmβπ)) β (πΉ β π) β (SubMgmβπ)) | ||
Theorem | mgmhmeql 45815 | The equalizer of two magma homomorphisms is a submagma. (Contributed by AV, 27-Feb-2020.) |
β’ ((πΉ β (π MgmHom π) β§ πΊ β (π MgmHom π)) β dom (πΉ β© πΊ) β (SubMgmβπ)) | ||
Theorem | submgmacs 45816 | Submagmas are an algebraic closure system. (Contributed by AV, 27-Feb-2020.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Mgm β (SubMgmβπΊ) β (ACSβπ΅)) | ||
Theorem | ismhm0 45817 | Property of a monoid homomorphism, expressed by a magma homomorphism. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (0gβπ) β β’ (πΉ β (π MndHom π) β ((π β Mnd β§ π β Mnd) β§ (πΉ β (π MgmHom π) β§ (πΉβ 0 ) = π))) | ||
Theorem | mhmismgmhm 45818 | Each monoid homomorphism is a magma homomorphism. (Contributed by AV, 29-Feb-2020.) |
β’ (πΉ β (π MndHom π) β πΉ β (π MgmHom π)) | ||
Theorem | opmpoismgm 45819* | A structure with a group addition operation in maps-to notation is a magma if the operation value is contained in the base set. (Contributed by AV, 16-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ (+gβπ) = (π₯ β π΅, π¦ β π΅ β¦ πΆ) & β’ (π β π΅ β β ) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β πΆ β π΅) β β’ (π β π β Mgm) | ||
Theorem | copissgrp 45820* | A structure with a constant group addition operation is a semigroup if the constant is contained in the base set. (Contributed by AV, 16-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ (+gβπ) = (π₯ β π΅, π¦ β π΅ β¦ πΆ) & β’ (π β π΅ β β ) & β’ (π β πΆ β π΅) β β’ (π β π β Smgrp) | ||
Theorem | copisnmnd 45821* | A structure with a constant group addition operation and at least two elements is not a monoid. (Contributed by AV, 16-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ (+gβπ) = (π₯ β π΅, π¦ β π΅ β¦ πΆ) & β’ (π β πΆ β π΅) & β’ (π β 1 < (β―βπ΅)) β β’ (π β π β Mnd) | ||
Theorem | 0nodd 45822* | 0 is not an odd integer. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} β β’ 0 β π | ||
Theorem | 1odd 45823* | 1 is an odd integer. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} β β’ 1 β π | ||
Theorem | 2nodd 45824* | 2 is not an odd integer. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} β β’ 2 β π | ||
Theorem | oddibas 45825* | Lemma 1 for oddinmgm 45827: The base set of M is the set of all odd integers. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} & β’ π = (βfld βΎs π) β β’ π = (Baseβπ) | ||
Theorem | oddiadd 45826* | Lemma 2 for oddinmgm 45827: The group addition operation of M is the addition of complex numbers. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} & β’ π = (βfld βΎs π) β β’ + = (+gβπ) | ||
Theorem | oddinmgm 45827* | The structure of all odd integers together with the addition of complex numbers is not a magma. Remark: the structure of the complementary subset of the set of integers, the even integers, is a magma, actually an abelian group, see 2zrngaabl 45960, and even a non-unital ring, see 2zrng 45951. (Contributed by AV, 3-Feb-2020.) |
β’ π = {π§ β β€ β£ βπ₯ β β€ π§ = ((2 Β· π₯) + 1)} & β’ π = (βfld βΎs π) β β’ π β Mgm | ||
Theorem | nnsgrpmgm 45828 | The structure of positive integers together with the addition of complex numbers is a magma. (Contributed by AV, 4-Feb-2020.) |
β’ π = (βfld βΎs β) β β’ π β Mgm | ||
Theorem | nnsgrp 45829 | The structure of positive integers together with the addition of complex numbers is a semigroup. (Contributed by AV, 4-Feb-2020.) |
β’ π = (βfld βΎs β) β β’ π β Smgrp | ||
Theorem | nnsgrpnmnd 45830 | The structure of positive integers together with the addition of complex numbers is not a monoid. (Contributed by AV, 4-Feb-2020.) |
β’ π = (βfld βΎs β) β β’ π β Mnd | ||
Theorem | nn0mnd 45831 | The set of nonnegative integers under (complex) addition is a monoid. Example in [Lang] p. 6. Remark: π could have also been written as (βfld βΎs β0). (Contributed by AV, 27-Dec-2023.) |
β’ π = {β¨(Baseβndx), β0β©, β¨(+gβndx), + β©} β β’ π β Mnd | ||
Theorem | gsumsplit2f 45832* | Split a group sum into two parts. (Contributed by AV, 4-Sep-2019.) |
β’ β²ππ & β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β (π β π΄ β¦ π) finSupp 0 ) & β’ (π β (πΆ β© π·) = β ) & β’ (π β π΄ = (πΆ βͺ π·)) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ π)) = ((πΊ Ξ£g (π β πΆ β¦ π)) + (πΊ Ξ£g (π β π· β¦ π)))) | ||
Theorem | gsumdifsndf 45833* | Extract a summand from a finitely supported group sum. (Contributed by AV, 4-Sep-2019.) |
β’ β²ππ & β’ β²ππ & β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β (π β π΄ β¦ π) finSupp (0gβπΊ)) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β π β π΄) & β’ (π β π β π΅) & β’ ((π β§ π = π) β π = π) β β’ (π β (πΊ Ξ£g (π β π΄ β¦ π)) = ((πΊ Ξ£g (π β (π΄ β {π}) β¦ π)) + π)) | ||
Theorem | gsumfsupp 45834 | A group sum of a family can be restricted to the support of that family without changing its value, provided that that support is finite. This corresponds to the definition of an (infinite) product in [Lang] p. 5, last two formulas. (Contributed by AV, 27-Dec-2023.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ πΌ = (πΉ supp 0 ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β (πΊ Ξ£g (πΉ βΎ πΌ)) = (πΊ Ξ£g πΉ)) | ||
With df-mpo 7355, binary operations are defined by a rule, and with df-ov 7353, 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 (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, we call binary operations mapping the elements of the Cartesian product π Γ π internal binary operations, see df-intop 45851. If, in addition, the result is also contained in the set π, the operation is called closed internal binary operation, see df-clintop 45852. Therefore, a "binary operation on a set π " according to Wikipedia is a "closed internal binary operation" in our 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 45852 ). Taking a step back, we define "laws" applicable for "binary operations" (which even need not to be functions), according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7. These laws are used, on the one hand, to specialize internal binary operations (see df-clintop 45852 and df-assintop 45853), and on the other hand to define the common algebraic structures like magmas, groups, rings, etc. Internal binary operations, which obey these laws, are defined afterwards. Notice that in [BourbakiAlg1] p. 1, p. 4 and p. 7, these operations are called "laws" by themselves. In the following, an alternate definition df-cllaw 45838 for an internal binary operation is provided, which does not require function-ness, but only closure. Therefore, this definition could be used as binary operation (Slot 2) defined for a magma as extensible structure, see mgmplusgiopALT 45846, or for an alternate definition df-mgm2 45871 for a magma as extensible structure. Similar results are obtained for an associative operation (defining semigroups). | ||
In this subsection, the "laws" applicable for "binary operations" according to the definition in [Hall] p. 1 and [BourbakiAlg1] p. 1, p. 4 and p. 7 are defined. These laws are called "internal laws" in [BourbakiAlg1] p. xxi. | ||
Syntax | ccllaw 45835 | Extend class notation for the closure law. |
class clLaw | ||
Syntax | casslaw 45836 | Extend class notation for the associative law. |
class assLaw | ||
Syntax | ccomlaw 45837 | Extend class notation for the commutative law. |
class comLaw | ||
Definition | df-cllaw 45838* | The closure law for binary operations, see definitions of laws A0. and M0. in section 1.1 of [Hall] p. 1, or definition 1 in [BourbakiAlg1] p. 1: the value of a binary operation applied to two operands of a given sets is an element of this set. By this definition, the closure law is expressed as binary relation: a binary operation is related to a set by clLaw if the closure law holds for this binary operation regarding this set. Note that the binary operation needs not to be a function. (Contributed by AV, 7-Jan-2020.) |
β’ clLaw = {β¨π, πβ© β£ βπ₯ β π βπ¦ β π (π₯ππ¦) β π} | ||
Definition | df-comlaw 45839* | The commutative law for binary operations, see definitions of laws A2. and M2. in section 1.1 of [Hall] p. 1, or definition 8 in [BourbakiAlg1] p. 7: the value of a binary operation applied to two operands equals the value of a binary operation applied to the two operands in reversed order. By this definition, the commutative law is expressed as binary relation: a binary operation is related to a set by comLaw if the commutative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by AV, 7-Jan-2020.) |
β’ comLaw = {β¨π, πβ© β£ βπ₯ β π βπ¦ β π (π₯ππ¦) = (π¦ππ₯)} | ||
Definition | df-asslaw 45840* | The associative law for binary operations, see definitions of laws A1. and M1. in section 1.1 of [Hall] p. 1, or definition 5 in [BourbakiAlg1] p. 4: the value of a binary operation applied the value of the binary operation applied to two operands and a third operand equals the value of the binary operation applied to the first operand and the value of the binary operation applied to the second and third operand. By this definition, the associative law is expressed as binary relation: a binary operation is related to a set by assLaw if the associative law holds for this binary operation regarding this set. Note that the binary operation needs neither to be closed nor to be a function. (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.) |
β’ assLaw = {β¨π, πβ© β£ βπ₯ β π βπ¦ β π βπ§ β π ((π₯ππ¦)ππ§) = (π₯π(π¦ππ§))} | ||
Theorem | iscllaw 45841* | The predicate "is a closed operation". (Contributed by AV, 13-Jan-2020.) |
β’ (( β¬ β π β§ π β π) β ( β¬ clLaw π β βπ₯ β π βπ¦ β π (π₯ β¬ π¦) β π)) | ||
Theorem | iscomlaw 45842* | The predicate "is a commutative operation". (Contributed by AV, 20-Jan-2020.) |
β’ (( β¬ β π β§ π β π) β ( β¬ comLaw π β βπ₯ β π βπ¦ β π (π₯ β¬ π¦) = (π¦ β¬ π₯))) | ||
Theorem | clcllaw 45843 | Closure of a closed operation. (Contributed by FL, 14-Sep-2010.) (Revised by AV, 21-Jan-2020.) |
β’ (( β¬ clLaw π β§ π β π β§ π β π) β (π β¬ π) β π) | ||
Theorem | isasslaw 45844* | The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (Revised by AV, 13-Jan-2020.) |
β’ (( β¬ β π β§ π β π) β ( β¬ assLaw π β βπ₯ β π βπ¦ β π βπ§ β π ((π₯ β¬ π¦) β¬ π§) = (π₯ β¬ (π¦ β¬ π§)))) | ||
Theorem | asslawass 45845* | Associativity of an associative operation. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 21-Jan-2020.) |
β’ ( β¬ assLaw π β βπ₯ β π βπ¦ β π βπ§ β π ((π₯ β¬ π¦) β¬ π§) = (π₯ β¬ (π¦ β¬ π§))) | ||
Theorem | mgmplusgiopALT 45846 | Slot 2 (group operation) of a magma as extensible structure is a closed operation on the base set. (Contributed by AV, 13-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π β Mgm β (+gβπ) clLaw (Baseβπ)) | ||
Theorem | sgrpplusgaopALT 45847 | Slot 2 (group operation) of a semigroup as extensible structure is an associative operation on the base set. (Contributed by AV, 13-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (πΊ β Smgrp β (+gβπΊ) assLaw (BaseβπΊ)) | ||
In this subsection, "internal binary operations" obeying different laws are defined. | ||
Syntax | cintop 45848 | Extend class notation with class of internal (binary) operations for a set. |
class intOp | ||
Syntax | cclintop 45849 | Extend class notation with class of closed operations for a set. |
class clIntOp | ||
Syntax | cassintop 45850 | Extend class notation with class of associative operations for a set. |
class assIntOp | ||
Definition | df-intop 45851* | Function mapping a set to the class of all internal (binary) operations for this set. (Contributed by AV, 20-Jan-2020.) |
β’ intOp = (π β V, π β V β¦ (π βm (π Γ π))) | ||
Definition | df-clintop 45852 | Function mapping a set to the class of all closed (internal binary) operations for this set, see definition in section 1.2 of [Hall] p. 2, definition in section I.1 of [Bruck] p. 1, or definition 1 in [BourbakiAlg1] p. 1, where it is called "a law of composition". (Contributed by AV, 20-Jan-2020.) |
β’ clIntOp = (π β V β¦ (π intOp π)) | ||
Definition | df-assintop 45853* | Function mapping a set to the class of all associative (closed internal binary) operations for this set, see definition 5 in [BourbakiAlg1] p. 4, where it is called "an associative law of composition". (Contributed by AV, 20-Jan-2020.) |
β’ assIntOp = (π β V β¦ {π β ( clIntOp βπ) β£ π assLaw π}) | ||
Theorem | intopval 45854 | The internal (binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
β’ ((π β π β§ π β π) β (π intOp π) = (π βm (π Γ π))) | ||
Theorem | intop 45855 | An internal (binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
β’ ( β¬ β (π intOp π) β β¬ :(π Γ π)βΆπ) | ||
Theorem | clintopval 45856 | The closed (internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
β’ (π β π β ( clIntOp βπ) = (π βm (π Γ π))) | ||
Theorem | assintopval 45857* | The associative (closed internal binary) operations for a set. (Contributed by AV, 20-Jan-2020.) |
β’ (π β π β ( assIntOp βπ) = {π β ( clIntOp βπ) β£ π assLaw π}) | ||
Theorem | assintopmap 45858* | The associative (closed internal binary) operations for a set, expressed with set exponentiation. (Contributed by AV, 20-Jan-2020.) |
β’ (π β π β ( assIntOp βπ) = {π β (π βm (π Γ π)) β£ π assLaw π}) | ||
Theorem | isclintop 45859 | The predicate "is a closed (internal binary) operations for a set". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
β’ (π β π β ( β¬ β ( clIntOp βπ) β β¬ :(π Γ π)βΆπ)) | ||
Theorem | clintop 45860 | A closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
β’ ( β¬ β ( clIntOp βπ) β β¬ :(π Γ π)βΆπ) | ||
Theorem | assintop 45861 | An associative (closed internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
β’ ( β¬ β ( assIntOp βπ) β ( β¬ :(π Γ π)βΆπ β§ β¬ assLaw π)) | ||
Theorem | isassintop 45862* | The predicate "is an associative (closed internal binary) operations for a set". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
β’ (π β π β ( β¬ β ( assIntOp βπ) β ( β¬ :(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯ β¬ π¦) β¬ π§) = (π₯ β¬ (π¦ β¬ π§))))) | ||
Theorem | clintopcllaw 45863 | The closure law holds for a closed (internal binary) operation for a set. (Contributed by AV, 20-Jan-2020.) |
β’ ( β¬ β ( clIntOp βπ) β β¬ clLaw π) | ||
Theorem | assintopcllaw 45864 | The closure low holds for an associative (closed internal binary) operation for a set. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
β’ ( β¬ β ( assIntOp βπ) β β¬ clLaw π) | ||
Theorem | assintopasslaw 45865 | The associative low holds for a associative (closed internal binary) operation for a set. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
β’ ( β¬ β ( assIntOp βπ) β β¬ assLaw π) | ||
Theorem | assintopass 45866* | An associative (closed internal binary) operation for a set is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 20-Jan-2020.) |
β’ ( β¬ β ( assIntOp βπ) β βπ₯ β π βπ¦ β π βπ§ β π ((π₯ β¬ π¦) β¬ π§) = (π₯ β¬ (π¦ β¬ π§))) | ||
Syntax | cmgm2 45867 | Extend class notation with class of all magmas. |
class MgmALT | ||
Syntax | ccmgm2 45868 | Extend class notation with class of all commutative magmas. |
class CMgmALT | ||
Syntax | csgrp2 45869 | Extend class notation with class of all semigroups. |
class SGrpALT | ||
Syntax | ccsgrp2 45870 | Extend class notation with class of all commutative semigroups. |
class CSGrpALT | ||
Definition | df-mgm2 45871 | A magma is a set equipped with a closed operation. Definition 1 of [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 AV, 6-Jan-2020.) |
β’ MgmALT = {π β£ (+gβπ) clLaw (Baseβπ)} | ||
Definition | df-cmgm2 45872 | A commutative magma is a magma with a commutative operation. Definition 8 of [BourbakiAlg1] p. 7. (Contributed by AV, 20-Jan-2020.) |
β’ CMgmALT = {π β MgmALT β£ (+gβπ) comLaw (Baseβπ)} | ||
Definition | df-sgrp2 45873 | A semigroup is a magma with an associative operation. Definition in section II.1 of [Bruck] p. 23, or of an "associative magma" in definition 5 of [BourbakiAlg1] p. 4, or of a semigroup in section 1.3 of [Hall] p. 7. (Contributed by AV, 6-Jan-2020.) |
β’ SGrpALT = {π β MgmALT β£ (+gβπ) assLaw (Baseβπ)} | ||
Definition | df-csgrp2 45874 | A commutative semigroup is a semigroup with a commutative operation. (Contributed by AV, 20-Jan-2020.) |
β’ CSGrpALT = {π β SGrpALT β£ (+gβπ) comLaw (Baseβπ)} | ||
Theorem | ismgmALT 45875 | The predicate "is a magma". (Contributed by AV, 16-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π β π β (π β MgmALT β β¬ clLaw π΅)) | ||
Theorem | iscmgmALT 45876 | The predicate "is a commutative magma". (Contributed by AV, 20-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π β CMgmALT β (π β MgmALT β§ β¬ comLaw π΅)) | ||
Theorem | issgrpALT 45877 | The predicate "is a semigroup". (Contributed by AV, 16-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π β SGrpALT β (π β MgmALT β§ β¬ assLaw π΅)) | ||
Theorem | iscsgrpALT 45878 | The predicate "is a commutative semigroup". (Contributed by AV, 20-Jan-2020.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π β CSGrpALT β (π β SGrpALT β§ β¬ comLaw π΅)) | ||
Theorem | mgm2mgm 45879 | Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020.) |
β’ (π β MgmALT β π β Mgm) | ||
Theorem | sgrp2sgrp 45880 | Equivalence of the two definitions of a semigroup. (Contributed by AV, 16-Jan-2020.) |
β’ (π β SGrpALT β π β Smgrp) | ||
Theorem | idfusubc0 45881* | The identity functor for a subcategory is an "inclusion functor" from the subcategory into its supercategory. (Contributed by AV, 29-Mar-2020.) |
β’ π = (πΆ βΎcat π½) & β’ πΌ = (idfuncβπ) & β’ π΅ = (Baseβπ) β β’ (π½ β (SubcatβπΆ) β πΌ = β¨( I βΎ π΅), (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯(Hom βπ)π¦)))β©) | ||
Theorem | idfusubc 45882* | The identity functor for a subcategory is an "inclusion functor" from the subcategory into its supercategory. (Contributed by AV, 29-Mar-2020.) |
β’ π = (πΆ βΎcat π½) & β’ πΌ = (idfuncβπ) & β’ π΅ = (Baseβπ) β β’ (π½ β (SubcatβπΆ) β πΌ = β¨( I βΎ π΅), (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯π½π¦)))β©) | ||
Theorem | inclfusubc 45883* | The "inclusion functor" from a subcategory of a category into the category itself. (Contributed by AV, 30-Mar-2020.) |
β’ (π β π½ β (SubcatβπΆ)) & β’ π = (πΆ βΎcat π½) & β’ π΅ = (Baseβπ) & β’ (π β πΉ = ( I βΎ π΅)) & β’ (π β πΊ = (π₯ β π΅, π¦ β π΅ β¦ ( I βΎ (π₯π½π¦)))) β β’ (π β πΉ(π Func πΆ)πΊ) | ||
Theorem | lmod0rng 45884 | If the scalar ring of a module is the zero ring, the module is the zero module, i.e. the base set of the module is the singleton consisting of the identity element only. (Contributed by AV, 17-Apr-2019.) |
β’ ((π β LMod β§ Β¬ (Scalarβπ) β NzRing) β (Baseβπ) = {(0gβπ)}) | ||
Theorem | nzrneg1ne0 45885 | The additive inverse of the 1 in a nonzero ring is not zero ( -1 =/= 0 ). (Contributed by AV, 29-Apr-2019.) |
β’ (π β NzRing β ((invgβπ )β(1rβπ )) β (0gβπ )) | ||
Theorem | 0ringdif 45886 | A zero ring is a ring which is not a nonzero ring. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ (π β (Ring β NzRing) β (π β Ring β§ π΅ = { 0 })) | ||
Theorem | 0ringbas 45887 | The base set of a zero ring, a ring which is not a nonzero ring, is the singleton of the zero element. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ (π β (Ring β NzRing) β π΅ = { 0 }) | ||
Theorem | 0ring1eq0 45888 | In a zero ring, a ring which is not a nonzero ring, the ring unity equals the zero element. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) β β’ (π β (Ring β NzRing) β 1 = 0 ) | ||
Theorem | nrhmzr 45889 | There is no ring homomorphism from the zero ring into a nonzero ring. (Contributed by AV, 18-Apr-2020.) |
β’ ((π β (Ring β NzRing) β§ π β NzRing) β (π RingHom π ) = β ) | ||
According to Wikipedia, "... in abstract algebra, a rng (or pseudo-ring or non-unital ring) is an algebraic structure satisfying the same properties as a [unital] ring, without assuming the existence of a multiplicative identity. The term "rng" (pronounced rung) is meant to suggest that it is a "ring" without "i", i.e. without the requirement for an "identity element"." (see https://en.wikipedia.org/wiki/Rng_(algebra), 6-Jan-2020). | ||
Syntax | crng 45890 | Extend class notation with class of all non-unital rings. |
class Rng | ||
Definition | df-rng0 45891* | Define class of all (non-unital) rings. A non-unital ring (or rng, or pseudoring) is a set equipped with two everywhere-defined internal operations, whose first one is an additive abelian group operation and the second one is a multiplicative semigroup operation, and where the addition is left- and right-distributive for the multiplication. Definition of a pseudo-ring in section I.8.1 of [BourbakiAlg1] p. 93 or the definition of a ring in part Preliminaries of [Roman] p. 18. As almost always in mathematics, "non-unital" means "not necessarily unital". Therefore, by talking about a ring (in general) or a non-unital ring the "unital" case is always included. In contrast to a unital ring, the commutativity of addition must be postulated and cannot be proven from the other conditions. (Contributed by AV, 6-Jan-2020.) |
β’ Rng = {π β Abel β£ ((mulGrpβπ) β Smgrp β§ [(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘]βπ₯ β π βπ¦ β π βπ§ β π ((π₯π‘(π¦ππ§)) = ((π₯π‘π¦)π(π₯π‘π§)) β§ ((π₯ππ¦)π‘π§) = ((π₯π‘π§)π(π¦π‘π§))))} | ||
Theorem | isrng 45892* | The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020.) |
β’ π΅ = (Baseβπ ) & β’ πΊ = (mulGrpβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ (π β Rng β (π β Abel β§ πΊ β Smgrp β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ ((π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§)) β§ ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))))) | ||
Theorem | rngabl 45893 | A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.) |
β’ (π β Rng β π β Abel) | ||
Theorem | rngmgp 45894 | A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020.) |
β’ πΊ = (mulGrpβπ ) β β’ (π β Rng β πΊ β Smgrp) | ||
Theorem | ringrng 45895 | A unital ring is a (non-unital) ring. (Contributed by AV, 6-Jan-2020.) |
β’ (π β Ring β π β Rng) | ||
Theorem | ringssrng 45896 | The unital rings are (non-unital) rings. (Contributed by AV, 20-Mar-2020.) |
β’ Ring β Rng | ||
Theorem | isringrng 45897* | The predicate "is a unital ring" as extension of the predicate "is a non-unital ring". (Contributed by AV, 17-Feb-2020.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β Ring β (π β Rng β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = π¦ β§ (π¦ Β· π₯) = π¦))) | ||
Theorem | rngdir 45898 | Distributive law for the multiplication operation of a non-unital ring (right-distributivity). (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Rng β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) Β· π) = ((π Β· π) + (π Β· π))) | ||
Theorem | rngcl 45899 | Closure of the multiplication operation of a non-unital ring. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Rng β§ π β π΅ β§ π β π΅) β (π Β· π) β π΅) | ||
Theorem | rnglz 45900 | The zero of a non-unital ring is a left-absorbing element. (Contributed by AV, 17-Apr-2020.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Rng β§ π β π΅) β ( 0 Β· π) = 0 ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |