Home | Metamath
Proof Explorer Theorem List (p. 186 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cur 18501 | Extend class notation with ring unit. |
Definition | df-ur 18502 | Define the multiplicative neutral element of a ring. This definition works by extracting the element, i.e. the neutral element in a group or monoid, and transferring it to the multiplicative monoid via the mulGrp function (df-mgp 18490). See also dfur2 18504, 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.) |
mulGrp | ||
Theorem | ringidval 18503 | The value of the unity element of a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
mulGrp | ||
Theorem | dfur2 18504* | 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.) |
Syntax | csrg 18505 | Extend class notation with the class of all semirings. |
SRing | ||
Definition | df-srg 18506* | 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. Compared to the definition of a ring, this definition also adds that the additive identity is an absorbing element of the multiplicative law, as this 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 | ||
Theorem | issrg 18507* | The predicate "is a semiring." (Contributed by Thierry Arnoux, 21-Mar-2018.) |
mulGrp SRing CMnd | ||
Theorem | srgcmn 18508 | A semiring is a commutative monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
SRing CMnd | ||
Theorem | srgmnd 18509 | A semiring is a monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
SRing | ||
Theorem | srgmgp 18510 | A semiring is a monoid under multiplication. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
mulGrp SRing | ||
Theorem | srgi 18511 | Properties of a semiring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
SRing | ||
Theorem | srgcl 18512 | 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.) |
SRing | ||
Theorem | srgass 18513 | 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.) |
SRing | ||
Theorem | srgideu 18514* | The unit 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.) |
SRing | ||
Theorem | srgfcl 18515 | Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by AV, 24-Aug-2021.) |
SRing | ||
Theorem | srgdi 18516 | Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
SRing | ||
Theorem | srgdir 18517 | Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
SRing | ||
Theorem | srgidcl 18518 | The unit 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.) |
SRing | ||
Theorem | srg0cl 18519 | 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.) |
SRing | ||
Theorem | srgidmlem 18520 | Lemma for srglidm 18521 and srgridm 18522. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
SRing | ||
Theorem | srglidm 18521 | The unit element of a semiring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
SRing | ||
Theorem | srgridm 18522 | The unit element of a semiring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
SRing | ||
Theorem | issrgid 18523* | 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.) |
SRing | ||
Theorem | srgacl 18524 | Closure of the addition operation of a semiring. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
SRing | ||
Theorem | srgcom 18525 | Commutativity of the additive group of a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
SRing | ||
Theorem | srgrz 18526 | The zero of a semiring is a right-absorbing element. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
SRing | ||
Theorem | srglz 18527 | The zero of a semiring is a left-absorbing element. (Contributed by AV, 23-Aug-2019.) |
SRing | ||
Theorem | srgisid 18528* | In a semiring, the only left-absorbing element is the additive identity. Remark in [Golan] p. 1. (Contributed by Thierry Arnoux, 1-May-2018.) |
SRing | ||
Theorem | srg1zr 18529 | 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.) |
SRing | ||
Theorem | srgen1zr 18530 | 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.) |
SRing | ||
Theorem | srgmulgass 18531 | An associative property between group multiple and ring multiplication for semirings. (Contributed by AV, 23-Aug-2019.) |
.g SRing | ||
Theorem | srgpcomp 18532 | 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.) |
mulGrp .g SRing | ||
Theorem | srgpcompp 18533 | 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.) |
mulGrp .g SRing | ||
Theorem | srgpcomppsc 18534 | 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.) |
mulGrp .g SRing .g | ||
Theorem | srglmhm 18535* | Left-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism, analogous to ringlghm 18604. (Contributed by AV, 23-Aug-2019.) |
SRing MndHom | ||
Theorem | srgrmhm 18536* | Right-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism, analogous to ringrghm 18605. (Contributed by AV, 23-Aug-2019.) |
SRing MndHom | ||
Theorem | srgsummulcr 18537* | A finite semiring sum multiplied by a constant, analogous to gsummulc1 18606. (Contributed by AV, 23-Aug-2019.) |
SRing finSupp g g | ||
Theorem | sgsummulcl 18538* | A finite semiring sum multiplied by a constant, analogous to gsummulc2 18607. (Contributed by AV, 23-Aug-2019.) |
SRing finSupp g g | ||
Theorem | srg1expzeq1 18539 | The exponentiation (by a nonnegative integer) of the unity element of a (semi)ring, analogous to mulgnn0z 17567. (Contributed by AV, 25-Nov-2019.) |
mulGrp .g SRing | ||
In this section, we prove the binomial theorem for semirings, srgbinom 18545, which is a generalization of the binomial theorem for complex numbers, binom 14562: is the sum from to of . Notice that the binomial theorem would also hold in the non-unital case (that is, in a "rg") and actually, the additive unit is not needed in its proof either. Therefore, it could be proven for even more general cases. An example would be the integrable nonnegative (resp. positive) bounded functions on . Special cases of the binomial theorem are csrgbinom 18546 (binomial theorem for commutative semirings) and crngbinom 18621 (binomial theorem for commutative rings). | ||
Theorem | srgbinomlem1 18540 | Lemma 1 for srgbinomlem 18544. (Contributed by AV, 23-Aug-2019.) |
.g mulGrp .g SRing | ||
Theorem | srgbinomlem2 18541 | Lemma 2 for srgbinomlem 18544. (Contributed by AV, 23-Aug-2019.) |
.g mulGrp .g SRing | ||
Theorem | srgbinomlem3 18542* | Lemma 3 for srgbinomlem 18544. (Contributed by AV, 23-Aug-2019.) (Proof shortened by AV, 27-Oct-2019.) |
.g mulGrp .g SRing g g | ||
Theorem | srgbinomlem4 18543* | Lemma 4 for srgbinomlem 18544. (Contributed by AV, 24-Aug-2019.) (Proof shortened by AV, 19-Nov-2019.) |
.g mulGrp .g SRing g g | ||
Theorem | srgbinomlem 18544* | Lemma for srgbinom 18545. Inductive step, analogous to binomlem 14561. (Contributed by AV, 24-Aug-2019.) |
.g mulGrp .g SRing g g | ||
Theorem | srgbinom 18545* | The binomial theorem for commuting elements of a semiring: is the sum from to of (generalization of binom 14562). (Contributed by AV, 24-Aug-2019.) |
.g mulGrp .g SRing g | ||
Theorem | csrgbinom 18546* | The binomial theorem for commutative semirings. (Contributed by AV, 24-Aug-2019.) |
.g mulGrp .g SRing CMnd g | ||
Syntax | crg 18547 | Extend class notation with class of all (unital) rings. |
Syntax | ccrg 18548 | Extend class notation with class of all (unital) commutative rings. |
Definition | df-ring 18549* | 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 18579), 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.) |
mulGrp | ||
Definition | df-cring 18550 | Define class of all commutative rings. (Contributed by Mario Carneiro, 7-Jan-2015.) |
mulGrp CMnd | ||
Theorem | isring 18551* | 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.) |
mulGrp | ||
Theorem | ringgrp 18552 | A ring is a group. (Contributed by NM, 15-Sep-2011.) |
Theorem | ringmgp 18553 | A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015.) |
mulGrp | ||
Theorem | iscrng 18554 | A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
mulGrp CMnd | ||
Theorem | crngmgp 18555 | A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) |
mulGrp CMnd | ||
Theorem | ringmnd 18556 | A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.) |
Theorem | ringmgm 18557 | A ring is a magma. (Contributed by AV, 31-Jan-2020.) |
Mgm | ||
Theorem | crngring 18558 | A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.) |
Theorem | mgpf 18559 | Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015.) |
mulGrp | ||
Theorem | ringi 18560 | Properties of a unital ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
Theorem | ringcl 18561 | Closure of the multiplication operation of a ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
Theorem | crngcom 18562 | A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) |
Theorem | iscrng2 18563* | A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.) |
Theorem | ringass 18564 | Associative law for the multiplication operation of a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
Theorem | ringideu 18565* | The unit element of a ring is unique. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
Theorem | ringdi 18566 | Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) |
Theorem | ringdir 18567 | Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) |
Theorem | ringidcl 18568 | The unit element of a ring belongs to the base set of the ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
Theorem | ring0cl 18569 | The zero element of a ring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.) |
Theorem | ringidmlem 18570 | Lemma for ringlidm 18571 and ringridm 18572. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
Theorem | ringlidm 18571 | The unit element of a ring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011.) |
Theorem | ringridm 18572 | The unit element of a ring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011.) |
Theorem | isringid 18573* | Properties showing that an element is the unity element of a ring. (Contributed by NM, 7-Aug-2013.) |
Theorem | ringid 18574* | The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (Revised by AV, 24-Aug-2021.) |
Theorem | ringadd2 18575* | A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (Revised by AV, 24-Aug-2021.) |
Theorem | rngo2times 18576 | A ring element plus itself is two times the element. "Two" in an arbitrary unital ring is the sum of the unit with itself. (Contributed by AV, 24-Aug-2021.) |
Theorem | ringidss 18577 | A subset of the multiplicative group has the multiplicative identity as its identity if the identity is in the subset. (Contributed by Mario Carneiro, 27-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
mulGrp ↾s | ||
Theorem | ringacl 18578 | Closure of the addition operation of a ring. (Contributed by Mario Carneiro, 14-Jan-2014.) |
Theorem | ringcom 18579 | Commutativity of the additive group of a ring. (See also lmodcom 18909.) (Contributed by Gérard Lang, 4-Dec-2014.) |
Theorem | ringabl 18580 | A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.) |
Theorem | ringcmn 18581 | A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
CMnd | ||
Theorem | ringpropd 18582* | If two structures have the same group components (properties), one is a ring iff the other one is. (Contributed by Mario Carneiro, 6-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.) |
Theorem | crngpropd 18583* | If two structures have the same group components (properties), one is a commutative ring iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015.) |
Theorem | ringprop 18584 | If two structures have the same ring components (properties), one is a ring iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.) |
Theorem | isringd 18585* | Properties that determine a ring. (Contributed by NM, 2-Aug-2013.) |
Theorem | iscrngd 18586* | Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.) |
Theorem | ringlz 18587 | The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) |
Theorem | ringrz 18588 | The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) |
Theorem | ringsrg 18589 | Any ring is also a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
SRing | ||
Theorem | ring1eq0 18590 | If one and zero are equal, then any two elements of a ring are equal. Alternately, every ring has one distinct from zero except the zero ring containing the single element . (Contributed by Mario Carneiro, 10-Sep-2014.) |
Theorem | ring1ne0 18591 | If a ring has at least two elements, its one and zero are different. (Contributed by AV, 13-Apr-2019.) |
Theorem | ringinvnz1ne0 18592* | In a unitary ring, a left invertible element is different from zero iff . (Contributed by FL, 18-Apr-2010.) (Revised by AV, 24-Aug-2021.) |
Theorem | ringinvnzdiv 18593* | In a unitary ring, a left invertible element is not a zero divisor. (Contributed by FL, 18-Apr-2010.) (Revised by Jeff Madsen, 18-Apr-2010.) (Revised by AV, 24-Aug-2021.) |
Theorem | ringnegl 18594 | Negation in a ring is the same as left multiplication by -1. (rngonegmn1l 33740 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
Theorem | rngnegr 18595 | Negation in a ring is the same as right multiplication by -1. (rngonegmn1r 33741 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
Theorem | ringmneg1 18596 | Negation of a product in a ring. (mulneg1 10466 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
Theorem | ringmneg2 18597 | Negation of a product in a ring. (mulneg2 10467 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
Theorem | ringm2neg 18598 | Double negation of a product in a ring. (mul2neg 10469 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) |
Theorem | ringsubdi 18599 | Ring multiplication distributes over subtraction. (subdi 10463 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
Theorem | rngsubdir 18600 | Ring multiplication distributes over subtraction. (subdir 10464 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |