HomeTheorem List (p. 132 of 149)
GIF version.
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Intuitionistic Logic Explorer Theorem List (p. 132 of 149) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | iscmnd 13101* | Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ (π β π΅ = (BaseβπΊ)) & β’ (π β + = (+gβπΊ)) & β’ (π β πΊ β Mnd) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) = (π¦ + π₯)) β β’ (π β πΊ β CMnd) | ||
| Theorem | isabld 13102* | Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.) |
| β’ (π β π΅ = (BaseβπΊ)) & β’ (π β + = (+gβπΊ)) & β’ (π β πΊ β Grp) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) = (π¦ + π₯)) β β’ (π β πΊ β Abel) | ||
| Theorem | isabli 13103* | Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.) |
| β’ πΊ β Grp & β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) = (π¦ + π₯)) β β’ πΊ β Abel | ||
| Theorem | cmnmnd 13104 | A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| β’ (πΊ β CMnd β πΊ β Mnd) | ||
| Theorem | cmncom 13105 | A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β CMnd β§ π β π΅ β§ π β π΅) β (π + π) = (π + π)) | ||
| Theorem | ablcom 13106 | An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Abel β§ π β π΅ β§ π β π΅) β (π + π) = (π + π)) | ||
| Theorem | cmn32 13107 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β CMnd β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) + π) = ((π + π) + π)) | ||
| Theorem | cmn4 13108 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β CMnd β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π + π) + (π + π)) = ((π + π) + (π + π))) | ||
| Theorem | cmn12 13109 | Commutative/associative law for commutative monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β CMnd β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π + (π + π)) = (π + (π + π))) | ||
| Theorem | abl32 13110 | Commutative/associative law for Abelian groups. (Contributed by Stefan O'Rear, 10-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π + π) + π) = ((π + π) + π)) | ||
| Theorem | cmnmndd 13111 | A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.) |
| β’ (π β πΊ β CMnd) β β’ (π β πΊ β Mnd) | ||
| Theorem | rinvmod 13112* | Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovimo 6068. (Contributed by AV, 31-Dec-2023.) |
| β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β π΄ β π΅) β β’ (π β β*π€ β π΅ (π΄ + π€) = 0 ) | ||
| Theorem | ablinvadd 13113 | The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π = (invgβπΊ) β β’ ((πΊ β Abel β§ π β π΅ β§ π β π΅) β (πβ(π + π)) = ((πβπ) + (πβπ))) | ||
| Theorem | ablsub2inv 13114 | Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015.) |
| β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ π = (invgβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πβπ) β (πβπ)) = (π β π)) | ||
| Theorem | ablsubadd 13115 | Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Abel β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β π) = π β (π + π) = π)) | ||
| Theorem | ablsub4 13116 | Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Abel β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π + π) β (π + π)) = ((π β π) + (π β π))) | ||
| Theorem | abladdsub4 13117 | Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Abel β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π + π) = (π + π) β (π β π) = (π β π))) | ||
| Theorem | abladdsub 13118 | Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Abel β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) β π) = ((π β π) + π)) | ||
| Theorem | ablpncan2 13119 | Cancellation law for subtraction in an Abelian group. (Contributed by NM, 2-Oct-2014.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Abel β§ π β π΅ β§ π β π΅) β ((π + π) β π) = π) | ||
| Theorem | ablpncan3 13120 | A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Abel β§ (π β π΅ β§ π β π΅)) β (π + (π β π)) = π) | ||
| Theorem | ablsubsub 13121 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β (π β π)) = ((π β π) + π)) | ||
| Theorem | ablsubsub4 13122 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π β π) β π) = (π β (π + π))) | ||
| Theorem | ablpnpcan 13123 | Cancellation law for mixed addition and subtraction. (pnpcan 8196 analog.) (Contributed by NM, 29-May-2015.) |
| β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΊ β Abel) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π + π) β (π + π)) = (π β π)) | ||
| Theorem | ablnncan 13124 | Cancellation law for group subtraction. (nncan 8186 analog.) (Contributed by NM, 7-Apr-2015.) |
| β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β (π β π)) = π) | ||
| Theorem | ablsub32 13125 | Swap the second and third terms in a double group subtraction. (Contributed by NM, 7-Apr-2015.) |
| β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π β π) β π) = ((π β π) β π)) | ||
| Theorem | ablnnncan 13126 | Cancellation law for group subtraction. (nnncan 8192 analog.) (Contributed by NM, 29-Feb-2008.) (Revised by AV, 27-Aug-2021.) |
| β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π β (π β π)) β π) = (π β π)) | ||
| Theorem | ablnnncan1 13127 | Cancellation law for group subtraction. (nnncan1 8193 analog.) (Contributed by NM, 7-Apr-2015.) |
| β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ (π β πΊ β Abel) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π β π) β (π β π)) = (π β π)) | ||
| Theorem | ablsubsub23 13128 | Swap subtrahend and result of group subtraction. (Contributed by NM, 14-Dec-2007.) (Revised by AV, 7-Oct-2021.) |
| β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Abel β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ β π΅) = πΆ β (π΄ β πΆ) = π΅)) | ||
| Theorem | subcmnd 13129 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.) |
| β’ (π β π» = (πΊ βΎs π)) & β’ (π β πΊ β CMnd) & β’ (π β π» β Mnd) & β’ (π β π β π) β β’ (π β π» β CMnd) | ||
| Syntax | cmgp 13130 | Multiplicative group. |
| class mulGrp | ||
| Definition | df-mgp 13131 | Define a structure that puts the multiplication operation of a ring in the addition slot. Note that this will not actually be a group for the average ring, or even for a field, but it will be a monoid, and we get a group if we restrict to the elements that have inverses. This allows us to formalize such notions as "the multiplication operation of a ring is a monoid" or "the multiplicative identity" in terms of the identity of a monoid (df-ur 13143). (Contributed by Mario Carneiro, 21-Dec-2014.) |
| β’ mulGrp = (π€ β V β¦ (π€ sSet β¨(+gβndx), (.rβπ€)β©)) | ||
| Theorem | fnmgp 13132 | The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.) |
| β’ mulGrp Fn V | ||
| Theorem | mgpvalg 13133 | Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014.) |
| β’ π = (mulGrpβπ ) & β’ Β· = (.rβπ ) β β’ (π β π β π = (π sSet β¨(+gβndx), Β· β©)) | ||
| Theorem | mgpplusgg 13134 | Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) |
| β’ π = (mulGrpβπ ) & β’ Β· = (.rβπ ) β β’ (π β π β Β· = (+gβπ)) | ||
| Theorem | mgpex 13135 | Existence of the multiplication group. If π is known to be a semiring, see srgmgp 13151. (Contributed by Jim Kingdon, 10-Jan-2025.) |
| β’ π = (mulGrpβπ ) β β’ (π β π β π β V) | ||
| Theorem | mgpbasg 13136 | Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.) |
| β’ π = (mulGrpβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β π β π΅ = (Baseβπ)) | ||
| Theorem | mgpscag 13137 | The multiplication monoid has the same (if any) scalars as the original ring. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
| β’ π = (mulGrpβπ ) & β’ π = (Scalarβπ ) β β’ (π β π β π = (Scalarβπ)) | ||
| Theorem | mgptsetg 13138 | Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ π = (mulGrpβπ ) β β’ (π β π β (TopSetβπ ) = (TopSetβπ)) | ||
| Theorem | mgptopng 13139 | Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ π = (mulGrpβπ ) & β’ π½ = (TopOpenβπ ) β β’ (π β π β π½ = (TopOpenβπ)) | ||
| Theorem | mgpdsg 13140 | Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| β’ π = (mulGrpβπ ) & β’ π΅ = (distβπ ) β β’ (π β π β π΅ = (distβπ)) | ||
| Theorem | mgpress 13141 | Subgroup commutes with the multiplicative group operator. (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof shortened by AV, 18-Oct-2024.) |
| β’ π = (π βΎs π΄) & β’ π = (mulGrpβπ ) β β’ ((π β π β§ π΄ β π) β (π βΎs π΄) = (mulGrpβπ)) | ||
In Wikipedia "Identity element", see https://en.wikipedia.org/wiki/Identity_element (18-Jan-2025): "... an identity with respect to multiplication is called a multiplicative identity (often denoted as 1). ... The distinction between additive and multiplicative identity is used most often for sets that support both binary operations, such as rings, integral domains, and fields. The multiplicative identity is often called unity in the latter context (a ring with unity). This should not be confused with a unit in ring theory, which is any element having a multiplicative inverse. By its own definition, unity itself is necessarily a unit." Calling the multiplicative identity of a ring a unity is taken from the definition of a ring with unity in section 17.3 of [BeauregardFraleigh] p. 135, "A ring ( R , + , . ) is a ring with unity if R is not the zero ring and ( R , . ) is a monoid. In this case, the identity element of ( R , . ) is denoted by 1 and is called the unity of R." This definition of a "ring with unity" corresponds to our definition of a unital ring (see df-ring 13181). Some authors call the multiplicative identity "unit" or "unit element" (for example in section I, 2.2 of [BourbakiAlg1] p. 14, definition in section 1.3 of [Hall] p. 4, or in section I, 1 of [Lang] p. 3), whereas other authors use the term "unit" for an element having a multiplicative inverse (for example in section 17.3 of [BeauregardFraleigh] p. 135, in definition in [Roman] p. 26, or even in section II, 1 of [Lang] p. 84). Sometimes, the multiplicative identity is simply called "one" (see, for example, chapter 8 in [Schechter] p. 180). To avoid this ambiguity of the term "unit", also mentioned in Wikipedia, we call the multiplicative identity of a structure with a multiplication (usually a ring) a "ring unity", or straightly "multiplicative identity". The term "unit" will be used for an element having a multiplicative inverse (see https://us.metamath.org/mpeuni/df-unit.html 13181 in set.mm), and we have "the ring unity is a unit", see https://us.metamath.org/mpeuni/1unit.html 13181. | ||
| Syntax | cur 13142 | Extend class notation with ring unity. |
| class 1r | ||
| Definition | df-ur 13143 |
Define the multiplicative identity, i.e., the monoid identity (df-0g 12707)
of the multiplicative monoid (df-mgp 13131) of a ring-like structure. This
multiplicative identity is also called "ring unity" or
"unity element".
This definition works by transferring the multiplicative operation from the .r slot to the +g slot and then looking at the element which is then the 0g element, that is an identity with respect to the operation which started out in the .r slot. See also dfur2g 13145, which derives the "traditional" definition as the unique element of a ring which is left- and right-neutral under multiplication. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
| β’ 1r = (0g β mulGrp) | ||
| Theorem | ringidvalg 13144 | The value of the unity element of a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
| β’ πΊ = (mulGrpβπ ) & β’ 1 = (1rβπ ) β β’ (π β π β 1 = (0gβπΊ)) | ||
| Theorem | dfur2g 13145* | The multiplicative identity is the unique element of the ring that is left- and right-neutral on all elements under multiplication. (Contributed by Mario Carneiro, 10-Jan-2015.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ (π β π β 1 = (β©π(π β π΅ β§ βπ₯ β π΅ ((π Β· π₯) = π₯ β§ (π₯ Β· π) = π₯)))) | ||
| Syntax | csrg 13146 | Extend class notation with the class of all semirings. |
| class SRing | ||
| Definition | df-srg 13147* | Define class of all semirings. A semiring is a set equipped with two everywhere-defined internal operations, whose first one is an additive commutative monoid structure and the second one is a multiplicative monoid structure, and where multiplication is (left- and right-) distributive over addition. Like with rings, the additive identity is an absorbing element of the multiplicative law, but in the case of semirings, this has to be part of the definition, as it cannot be deduced from distributivity alone. Definition of [Golan] p. 1. Note that our semirings are unital. Such semirings are sometimes called "rigs", being "rings without negatives". (Contributed by Thierry Arnoux, 21-Mar-2018.) |
| β’ SRing = {π β CMnd β£ ((mulGrpβπ) β Mnd β§ [(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘][(0gβπ) / π]βπ₯ β π (βπ¦ β π βπ§ β π ((π₯π‘(π¦ππ§)) = ((π₯π‘π¦)π(π₯π‘π§)) β§ ((π₯ππ¦)π‘π§) = ((π₯π‘π§)π(π¦π‘π§))) β§ ((ππ‘π₯) = π β§ (π₯π‘π) = π)))} | ||
| Theorem | issrg 13148* | The predicate "is a semiring". (Contributed by Thierry Arnoux, 21-Mar-2018.) |
| β’ π΅ = (Baseβπ ) & β’ πΊ = (mulGrpβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ (π β SRing β (π β CMnd β§ πΊ β Mnd β§ βπ₯ β π΅ (βπ¦ β π΅ βπ§ β π΅ ((π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§)) β§ ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) β§ (( 0 Β· π₯) = 0 β§ (π₯ Β· 0 ) = 0 )))) | ||
| Theorem | srgcmn 13149 | A semiring is a commutative monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
| β’ (π β SRing β π β CMnd) | ||
| Theorem | srgmnd 13150 | A semiring is a monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
| β’ (π β SRing β π β Mnd) | ||
| Theorem | srgmgp 13151 | A semiring is a monoid under multiplication. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
| β’ πΊ = (mulGrpβπ ) β β’ (π β SRing β πΊ β Mnd) | ||
| Theorem | srgdilem 13152 | Lemma for srgdi 13157 and srgdir 13158. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β SRing β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π Β· (π + π)) = ((π Β· π) + (π Β· π)) β§ ((π + π) Β· π) = ((π Β· π) + (π Β· π)))) | ||
| Theorem | srgcl 13153 | Closure of the multiplication operation of a semiring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β SRing β§ π β π΅ β§ π β π΅) β (π Β· π) β π΅) | ||
| Theorem | srgass 13154 | Associative law for the multiplication operation of a semiring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β SRing β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π Β· π) Β· π) = (π Β· (π Β· π))) | ||
| Theorem | srgideu 13155* | The unity element of a semiring is unique. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β SRing β β!π’ β π΅ βπ₯ β π΅ ((π’ Β· π₯) = π₯ β§ (π₯ Β· π’) = π₯)) | ||
| Theorem | srgfcl 13156 | Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by AV, 24-Aug-2021.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β SRing β§ Β· Fn (π΅ Γ π΅)) β Β· :(π΅ Γ π΅)βΆπ΅) | ||
| Theorem | srgdi 13157 | Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β SRing β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π Β· (π + π)) = ((π Β· π) + (π Β· π))) | ||
| Theorem | srgdir 13158 | Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β SRing β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) Β· π) = ((π Β· π) + (π Β· π))) | ||
| Theorem | srgidcl 13159 | The unity element of a semiring belongs to the base set of the semiring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ (π β SRing β 1 β π΅) | ||
| Theorem | srg0cl 13160 | The zero element of a semiring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ (π β SRing β 0 β π΅) | ||
| Theorem | srgidmlem 13161 | Lemma for srglidm 13162 and srgridm 13163. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β SRing β§ π β π΅) β (( 1 Β· π) = π β§ (π Β· 1 ) = π)) | ||
| Theorem | srglidm 13162 | The unity element of a semiring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β SRing β§ π β π΅) β ( 1 Β· π) = π) | ||
| Theorem | srgridm 13163 | The unity element of a semiring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β SRing β§ π β π΅) β (π Β· 1 ) = π) | ||
| Theorem | issrgid 13164* | Properties showing that an element πΌ is the unity element of a semiring. (Contributed by NM, 7-Aug-2013.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ (π β SRing β ((πΌ β π΅ β§ βπ₯ β π΅ ((πΌ Β· π₯) = π₯ β§ (π₯ Β· πΌ) = π₯)) β 1 = πΌ)) | ||
| Theorem | srgacl 13165 | Closure of the addition operation of a semiring. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((π β SRing β§ π β π΅ β§ π β π΅) β (π + π) β π΅) | ||
| Theorem | srgcom 13166 | Commutativity of the additive group of a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((π β SRing β§ π β π΅ β§ π β π΅) β (π + π) = (π + π)) | ||
| Theorem | srgrz 13167 | The zero of a semiring is a right-absorbing element. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β SRing β§ π β π΅) β (π Β· 0 ) = 0 ) | ||
| Theorem | srglz 13168 | The zero of a semiring is a left-absorbing element. (Contributed by AV, 23-Aug-2019.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β SRing β§ π β π΅) β ( 0 Β· π) = 0 ) | ||
| Theorem | srgisid 13169* | In a semiring, the only left-absorbing element is the additive identity. Remark in [Golan] p. 1. (Contributed by Thierry Arnoux, 1-May-2018.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β SRing) & β’ (π β π β π΅) & β’ ((π β§ π₯ β π΅) β (π Β· π₯) = π) β β’ (π β π = 0 ) | ||
| Theorem | srg1zr 13170 | The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
| β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ β = (.rβπ ) β β’ (((π β SRing β§ + Fn (π΅ Γ π΅) β§ β Fn (π΅ Γ π΅)) β§ π β π΅) β (π΅ = {π} β ( + = {β¨β¨π, πβ©, πβ©} β§ β = {β¨β¨π, πβ©, πβ©}))) | ||
| Theorem | srgen1zr 13171 | The only semiring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
| β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ β = (.rβπ ) & β’ π = (0gβπ ) β β’ ((π β SRing β§ + Fn (π΅ Γ π΅) β§ β Fn (π΅ Γ π΅)) β (π΅ β 1o β ( + = {β¨β¨π, πβ©, πβ©} β§ β = {β¨β¨π, πβ©, πβ©}))) | ||
| Theorem | srgmulgass 13172 | An associative property between group multiple and ring multiplication for semirings. (Contributed by AV, 23-Aug-2019.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.gβπ ) & β’ Γ = (.rβπ ) β β’ ((π β SRing β§ (π β β0 β§ π β π΅ β§ π β π΅)) β ((π Β· π) Γ π) = (π Β· (π Γ π))) | ||
| Theorem | srgpcomp 13173 | If two elements of a semiring commute, they also commute if one of the elements is raised to a higher power. (Contributed by AV, 23-Aug-2019.) |
| β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) & β’ (π β π β SRing) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΎ β β0) & β’ (π β (π΄ Γ π΅) = (π΅ Γ π΄)) β β’ (π β ((πΎ β π΅) Γ π΄) = (π΄ Γ (πΎ β π΅))) | ||
| Theorem | srgpcompp 13174 | If two elements of a semiring commute, they also commute if the elements are raised to a higher power. (Contributed by AV, 23-Aug-2019.) |
| β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) & β’ (π β π β SRing) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΎ β β0) & β’ (π β (π΄ Γ π΅) = (π΅ Γ π΄)) & β’ (π β π β β0) β β’ (π β (((π β π΄) Γ (πΎ β π΅)) Γ π΄) = (((π + 1) β π΄) Γ (πΎ β π΅))) | ||
| Theorem | srgpcomppsc 13175 | If two elements of a semiring commute, they also commute if the elements are raised to a higher power and a scalar multiplication is involved. (Contributed by AV, 23-Aug-2019.) |
| β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) & β’ (π β π β SRing) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΎ β β0) & β’ (π β (π΄ Γ π΅) = (π΅ Γ π΄)) & β’ (π β π β β0) & β’ Β· = (.gβπ ) & β’ (π β πΆ β β0) β β’ (π β ((πΆ Β· ((π β π΄) Γ (πΎ β π΅))) Γ π΄) = (πΆ Β· (((π + 1) β π΄) Γ (πΎ β π΅)))) | ||
| Theorem | srglmhm 13176* | Left-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism. (Contributed by AV, 23-Aug-2019.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β SRing β§ π β π΅) β (π₯ β π΅ β¦ (π Β· π₯)) β (π MndHom π )) | ||
| Theorem | srgrmhm 13177* | Right-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism. (Contributed by AV, 23-Aug-2019.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β SRing β§ π β π΅) β (π₯ β π΅ β¦ (π₯ Β· π)) β (π MndHom π )) | ||
| Theorem | srg1expzeq1 13178 | The exponentiation (by a nonnegative integer) of the multiplicative identity of a semiring, analogous to mulgnn0z 13010. (Contributed by AV, 25-Nov-2019.) |
| β’ πΊ = (mulGrpβπ ) & β’ Β· = (.gβπΊ) & β’ 1 = (1rβπ ) β β’ ((π β SRing β§ π β β0) β (π Β· 1 ) = 1 ) | ||
| Syntax | crg 13179 | Extend class notation with class of all (unital) rings. |
| class Ring | ||
| Syntax | ccrg 13180 | Extend class notation with class of all (unital) commutative rings. |
| class CRing | ||
| Definition | df-ring 13181* | Define class of all (unital) rings. A unital ring is a set equipped with two everywhere-defined internal operations, whose first one is an additive group structure and the second one is a multiplicative monoid structure, and where the addition is left- and right-distributive for the multiplication. Definition 1 in [BourbakiAlg1] p. 92 or definition of a ring with identity in part Preliminaries of [Roman] p. 19. So that the additive structure must be abelian (see ringcom 13214), care must be taken that in the case of a non-unital ring, the commutativity of addition must be postulated and cannot be proved from the other conditions. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 27-Dec-2014.) |
| β’ Ring = {π β Grp β£ ((mulGrpβπ) β Mnd β§ [(Baseβπ) / π][(+gβπ) / π][(.rβπ) / π‘]βπ₯ β π βπ¦ β π βπ§ β π ((π₯π‘(π¦ππ§)) = ((π₯π‘π¦)π(π₯π‘π§)) β§ ((π₯ππ¦)π‘π§) = ((π₯π‘π§)π(π¦π‘π§))))} | ||
| Definition | df-cring 13182 | Define class of all commutative rings. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ CRing = {π β Ring β£ (mulGrpβπ) β CMnd} | ||
| Theorem | isring 13183* | The predicate "is a (unital) ring". Definition of "ring with unit" in [Schechter] p. 187. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
| β’ π΅ = (Baseβπ ) & β’ πΊ = (mulGrpβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ (π β Ring β (π β Grp β§ πΊ β Mnd β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ ((π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§)) β§ ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))))) | ||
| Theorem | ringgrp 13184 | A ring is a group. (Contributed by NM, 15-Sep-2011.) |
| β’ (π β Ring β π β Grp) | ||
| Theorem | ringmgp 13185 | A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| β’ πΊ = (mulGrpβπ ) β β’ (π β Ring β πΊ β Mnd) | ||
| Theorem | iscrng 13186 | A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ πΊ = (mulGrpβπ ) β β’ (π β CRing β (π β Ring β§ πΊ β CMnd)) | ||
| Theorem | crngmgp 13187 | A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ πΊ = (mulGrpβπ ) β β’ (π β CRing β πΊ β CMnd) | ||
| Theorem | ringgrpd 13188 | A ring is a group. (Contributed by SN, 16-May-2024.) |
| β’ (π β π β Ring) β β’ (π β π β Grp) | ||
| Theorem | ringmnd 13189 | A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ (π β Ring β π β Mnd) | ||
| Theorem | ringmgm 13190 | A ring is a magma. (Contributed by AV, 31-Jan-2020.) |
| β’ (π β Ring β π β Mgm) | ||
| Theorem | crngring 13191 | A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ (π β CRing β π β Ring) | ||
| Theorem | crngringd 13192 | A commutative ring is a ring. (Contributed by SN, 16-May-2024.) |
| β’ (π β π β CRing) β β’ (π β π β Ring) | ||
| Theorem | crnggrpd 13193 | A commutative ring is a group. (Contributed by SN, 16-May-2024.) |
| β’ (π β π β CRing) β β’ (π β π β Grp) | ||
| Theorem | mgpf 13194 | Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015.) |
| β’ (mulGrp βΎ Ring):RingβΆMnd | ||
| Theorem | ringdilem 13195 | Properties of a unital ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
| β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π Β· (π + π)) = ((π Β· π) + (π Β· π)) β§ ((π + π) Β· π) = ((π Β· π) + (π Β· π)))) | ||
| Theorem | ringcl 13196 | Closure of the multiplication operation of a ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π΅) β (π Β· π) β π΅) | ||
| Theorem | crngcom 13197 | A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β CRing β§ π β π΅ β§ π β π΅) β (π Β· π) = (π Β· π)) | ||
| Theorem | iscrng2 13198* | A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β CRing β (π β Ring β§ βπ₯ β π΅ βπ¦ β π΅ (π₯ Β· π¦) = (π¦ Β· π₯))) | ||
| Theorem | ringass 13199 | Associative law for multiplication in a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π Β· π) Β· π) = (π Β· (π Β· π))) | ||
| Theorem | ringideu 13200* | The unity element of a ring is unique. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
| β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β Ring β β!π’ β π΅ βπ₯ β π΅ ((π’ Β· π₯) = π₯ β§ (π₯ Β· π’) = π₯)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |