Home | Metamath
Proof Explorer Theorem List (p. 200 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 | crngringd 19901 | A commutative ring is a ring. (Contributed by SN, 16-May-2024.) |
β’ (π β π β CRing) β β’ (π β π β Ring) | ||
Theorem | crnggrpd 19902 | A commutative ring is a group. (Contributed by SN, 16-May-2024.) |
β’ (π β π β CRing) β β’ (π β π β Grp) | ||
Theorem | mgpf 19903 | Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ (mulGrp βΎ Ring):RingβΆMnd | ||
Theorem | ringdilem 19904 | Properties of a unital ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π Β· (π + π)) = ((π Β· π) + (π Β· π)) β§ ((π + π) Β· π) = ((π Β· π) + (π Β· π)))) | ||
Theorem | ringcl 19905 | 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 19906 | A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β CRing β§ π β π΅ β§ π β π΅) β (π Β· π) = (π Β· π)) | ||
Theorem | iscrng2 19907* | 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 19908 | 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 19909* | The unity element of a ring is unique. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β Ring β β!π’ β π΅ βπ₯ β π΅ ((π’ Β· π₯) = π₯ β§ (π₯ Β· π’) = π₯)) | ||
Theorem | ringcld 19910 | Closure of the multiplication operation of a ring. (Contributed by SN, 29-Jul-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π Β· π) β π΅) | ||
Theorem | ringdi 19911 | Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π Β· (π + π)) = ((π Β· π) + (π Β· π))) | ||
Theorem | ringdir 19912 | Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) Β· π) = ((π Β· π) + (π Β· π))) | ||
Theorem | ringidcl 19913 | The unity 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.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ (π β Ring β 1 β π΅) | ||
Theorem | ring0cl 19914 | The zero element of a ring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β 0 β π΅) | ||
Theorem | ringidmlem 19915 | Lemma for ringlidm 19916 and ringridm 19917. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π΅) β (( 1 Β· π) = π β§ (π Β· 1 ) = π)) | ||
Theorem | ringlidm 19916 | The unity element of a ring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π΅) β ( 1 Β· π) = π) | ||
Theorem | ringridm 19917 | The unity element of a ring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β π΅) β (π Β· 1 ) = π) | ||
Theorem | isringid 19918* | Properties showing that an element πΌ is the unity element of a ring. (Contributed by NM, 7-Aug-2013.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ (π β Ring β ((πΌ β π΅ β§ βπ₯ β π΅ ((πΌ Β· π₯) = π₯ β§ (π₯ Β· πΌ) = π₯)) β 1 = πΌ)) | ||
Theorem | ringid 19919* | 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.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅) β βπ’ β π΅ ((π’ Β· π) = π β§ (π Β· π’) = π)) | ||
Theorem | ringadd2 19920* | 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.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅) β βπ₯ β π΅ (π + π) = ((π₯ + π₯) Β· π)) | ||
Theorem | rngo2times 19921 | A ring element plus itself is two times the element. "Two" in an arbitrary unital ring is the sum of the unity element with itself. (Contributed by AV, 24-Aug-2021.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π΄ β π΅) β (π΄ + π΄) = (( 1 + 1 ) Β· π΄)) | ||
Theorem | ringidss 19922 | 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 π΄) & β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π΄ β π΅ β§ 1 β π΄) β 1 = (0gβπ)) | ||
Theorem | ringacl 19923 | Closure of the addition operation of a ring. (Contributed by Mario Carneiro, 14-Jan-2014.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π΅) β (π + π) β π΅) | ||
Theorem | ringcom 19924 | Commutativity of the additive group of a ring. (See also lmodcom 20291.) (Contributed by GΓ©rard Lang, 4-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π΅) β (π + π) = (π + π)) | ||
Theorem | ringabl 19925 | A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.) |
β’ (π β Ring β π β Abel) | ||
Theorem | ringcmn 19926 | A ring is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ (π β Ring β π β CMnd) | ||
Theorem | ringabld 19927 | A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.) |
β’ (π β π β Ring) β β’ (π β π β Abel) | ||
Theorem | ringcmnd 19928 | A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
β’ (π β π β Ring) β β’ (π β π β CMnd) | ||
Theorem | ringpropd 19929* | 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.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) β β’ (π β (πΎ β Ring β πΏ β Ring)) | ||
Theorem | crngpropd 19930* | 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.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) β β’ (π β (πΎ β CRing β πΏ β CRing)) | ||
Theorem | ringprop 19931 | 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.) |
β’ (BaseβπΎ) = (BaseβπΏ) & β’ (+gβπΎ) = (+gβπΏ) & β’ (.rβπΎ) = (.rβπΏ) β β’ (πΎ β Ring β πΏ β Ring) | ||
Theorem | isringd 19932* | Properties that determine a ring. (Contributed by NM, 2-Aug-2013.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β + = (+gβπ )) & β’ (π β Β· = (.rβπ )) & β’ (π β π β Grp) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ Β· π¦) β π΅) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ Β· π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) & β’ (π β 1 β π΅) & β’ ((π β§ π₯ β π΅) β ( 1 Β· π₯) = π₯) & β’ ((π β§ π₯ β π΅) β (π₯ Β· 1 ) = π₯) β β’ (π β π β Ring) | ||
Theorem | iscrngd 19933* | Properties that determine a commutative ring. (Contributed by Mario Carneiro, 7-Jan-2015.) |
β’ (π β π΅ = (Baseβπ )) & β’ (π β + = (+gβπ )) & β’ (π β Β· = (.rβπ )) & β’ (π β π β Grp) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ Β· π¦) β π΅) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ Β· π¦) Β· π§) = (π₯ Β· (π¦ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β (π₯ Β· (π¦ + π§)) = ((π₯ Β· π¦) + (π₯ Β· π§))) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) Β· π§) = ((π₯ Β· π§) + (π¦ Β· π§))) & β’ (π β 1 β π΅) & β’ ((π β§ π₯ β π΅) β ( 1 Β· π₯) = π₯) & β’ ((π β§ π₯ β π΅) β (π₯ Β· 1 ) = π₯) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ Β· π¦) = (π¦ Β· π₯)) β β’ (π β π β CRing) | ||
Theorem | ringlz 19934 | The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β π΅) β ( 0 Β· π) = 0 ) | ||
Theorem | ringrz 19935 | The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β π΅) β (π Β· 0 ) = 0 ) | ||
Theorem | ringsrg 19936 | Any ring is also a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
β’ (π β Ring β π β SRing) | ||
Theorem | ring1eq0 19937 | 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 {0}. (Contributed by Mario Carneiro, 10-Sep-2014.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β π΅) β ( 1 = 0 β π = π)) | ||
Theorem | ring1ne0 19938 | If a ring has at least two elements, its one and zero are different. (Contributed by AV, 13-Apr-2019.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ 1 < (β―βπ΅)) β 1 β 0 ) | ||
Theorem | ringinvnz1ne0 19939* | In a unital ring, a left invertible element is different from zero iff 1 β 0. (Contributed by FL, 18-Apr-2010.) (Revised by AV, 24-Aug-2021.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β βπ β π΅ (π Β· π) = 1 ) β β’ (π β (π β 0 β 1 β 0 )) | ||
Theorem | ringinvnzdiv 19940* | In a unital 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.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β βπ β π΅ (π Β· π) = 1 ) & β’ (π β π β π΅) β β’ (π β ((π Β· π) = 0 β π = 0 )) | ||
Theorem | ringnegl 19941 | Negation in a ring is the same as left multiplication by -1. (rngonegmn1l 36286 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ π = (invgβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β ((πβ 1 ) Β· π) = (πβπ)) | ||
Theorem | rngnegr 19942 | Negation in a ring is the same as right multiplication by -1. (rngonegmn1r 36287 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ π = (invgβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β (π Β· (πβ 1 )) = (πβπ)) | ||
Theorem | ringmneg1 19943 | Negation of a product in a ring. (mulneg1 11525 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (invgβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πβπ) Β· π) = (πβ(π Β· π))) | ||
Theorem | ringmneg2 19944 | Negation of a product in a ring. (mulneg2 11526 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (invgβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π Β· (πβπ)) = (πβ(π Β· π))) | ||
Theorem | ringm2neg 19945 | Double negation of a product in a ring. (mul2neg 11528 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (invgβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πβπ) Β· (πβπ)) = (π Β· π)) | ||
Theorem | ringsubdi 19946 | Ring multiplication distributes over subtraction. (subdi 11522 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ β = (-gβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π Β· (π β π)) = ((π Β· π) β (π Β· π))) | ||
Theorem | rngsubdir 19947 | Ring multiplication distributes over subtraction. (subdir 11523 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ β = (-gβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π β π) Β· π) = ((π Β· π) β (π Β· π))) | ||
Theorem | mulgass2 19948 | An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.gβπ ) & β’ Γ = (.rβπ ) β β’ ((π β Ring β§ (π β β€ β§ π β π΅ β§ π β π΅)) β ((π Β· π) Γ π) = (π Β· (π Γ π))) | ||
Theorem | ring1 19949 | The (smallest) structure representing a zero ring. (Contributed by AV, 28-Apr-2019.) |
β’ π = {β¨(Baseβndx), {π}β©, β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©, β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} β β’ (π β π β π β Ring) | ||
Theorem | ringn0 19950 | Rings exist. (Contributed by AV, 29-Apr-2019.) |
β’ Ring β β | ||
Theorem | ringlghm 19951* | Left-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅) β (π₯ β π΅ β¦ (π Β· π₯)) β (π GrpHom π )) | ||
Theorem | ringrghm 19952* | Right-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β π΅) β (π₯ β π΅ β¦ (π₯ Β· π)) β (π GrpHom π )) | ||
Theorem | gsummulc1 19953* | A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β π΄ β π) & β’ (π β π β π΅) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β (π β π΄ β¦ π) finSupp 0 ) β β’ (π β (π Ξ£g (π β π΄ β¦ (π Β· π))) = ((π Ξ£g (π β π΄ β¦ π)) Β· π)) | ||
Theorem | gsummulc2 19954* | A finite ring sum multiplied by a constant. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 10-Jul-2019.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β π΄ β π) & β’ (π β π β π΅) & β’ ((π β§ π β π΄) β π β π΅) & β’ (π β (π β π΄ β¦ π) finSupp 0 ) β β’ (π β (π Ξ£g (π β π΄ β¦ (π Β· π))) = (π Β· (π Ξ£g (π β π΄ β¦ π)))) | ||
Theorem | gsummgp0 19955* | If one factor in a finite group sum of the multiplicative group of a commutative ring is 0, the whole "sum" (i.e. product) is 0. (Contributed by AV, 3-Jan-2019.) |
β’ πΊ = (mulGrpβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β CRing) & β’ (π β π β Fin) & β’ ((π β§ π β π) β π΄ β (Baseβπ )) & β’ ((π β§ π = π) β π΄ = π΅) & β’ (π β βπ β π π΅ = 0 ) β β’ (π β (πΊ Ξ£g (π β π β¦ π΄)) = 0 ) | ||
Theorem | gsumdixp 19956* | Distribute a binary product of sums to a sum of binary products in a ring. (Contributed by Mario Carneiro, 8-Mar-2015.) (Revised by AV, 10-Jul-2019.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β πΌ β π) & β’ (π β π½ β π) & β’ (π β π β Ring) & β’ ((π β§ π₯ β πΌ) β π β π΅) & β’ ((π β§ π¦ β π½) β π β π΅) & β’ (π β (π₯ β πΌ β¦ π) finSupp 0 ) & β’ (π β (π¦ β π½ β¦ π) finSupp 0 ) β β’ (π β ((π Ξ£g (π₯ β πΌ β¦ π)) Β· (π Ξ£g (π¦ β π½ β¦ π))) = (π Ξ£g (π₯ β πΌ, π¦ β π½ β¦ (π Β· π)))) | ||
Theorem | prdsmgp 19957 | The multiplicative monoid of a product is the product of the multiplicative monoids of the factors. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ π = (πXsπ ) & β’ π = (mulGrpβπ) & β’ π = (πXs(mulGrp β π )) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π Fn πΌ) β β’ (π β ((Baseβπ) = (Baseβπ) β§ (+gβπ) = (+gβπ))) | ||
Theorem | prdsmulrcl 19958 | A structure product of rings has closed binary operation. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ Β· = (.rβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π :πΌβΆRing) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (πΉ Β· πΊ) β π΅) | ||
Theorem | prdsringd 19959 | A product of rings is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆRing) β β’ (π β π β Ring) | ||
Theorem | prdscrngd 19960 | A product of commutative rings is a commutative ring. Since the resulting ring will have zero divisors in all nontrivial cases, this cannot be strengthened much further. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆCRing) β β’ (π β π β CRing) | ||
Theorem | prds1 19961 | Value of the ring unity in a structure family product. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆRing) β β’ (π β (1r β π ) = (1rβπ)) | ||
Theorem | pwsring 19962 | A structure power of a ring is a ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ π = (π βs πΌ) β β’ ((π β Ring β§ πΌ β π) β π β Ring) | ||
Theorem | pws1 19963 | Value of the ring unity in a structure power. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ π = (π βs πΌ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ πΌ β π) β (πΌ Γ { 1 }) = (1rβπ)) | ||
Theorem | pwscrng 19964 | A structure power of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 11-Mar-2015.) |
β’ π = (π βs πΌ) β β’ ((π β CRing β§ πΌ β π) β π β CRing) | ||
Theorem | pwsmgp 19965 | The multiplicative group of the power structure resembles the power of the multiplicative group. (Contributed by Mario Carneiro, 12-Mar-2015.) |
β’ π = (π βs πΌ) & β’ π = (mulGrpβπ ) & β’ π = (π βs πΌ) & β’ π = (mulGrpβπ) & β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ + = (+gβπ) & β’ β = (+gβπ) β β’ ((π β π β§ πΌ β π) β (π΅ = πΆ β§ + = β )) | ||
Theorem | pwspjmhmmgpd 19966* | The projection given by pwspjmhm 18575 is also a monoid homomorphism between the respective multiplicative groups. (Contributed by SN, 30-Jul-2024.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (mulGrpβπ) & β’ π = (mulGrpβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π΄ β πΌ) β β’ (π β (π₯ β π΅ β¦ (π₯βπ΄)) β (π MndHom π)) | ||
Theorem | pwsexpg 19967 | Value of a group exponentiation in a structure power. Compare pwsmulg 18854. (Contributed by SN, 30-Jul-2024.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (mulGrpβπ) & β’ π = (mulGrpβπ ) & β’ β = (.gβπ) & β’ Β· = (.gβπ) & β’ (π β π β Ring) & β’ (π β πΌ β π) & β’ (π β π β β0) & β’ (π β π β π΅) & β’ (π β π΄ β πΌ) β β’ (π β ((π β π)βπ΄) = (π Β· (πβπ΄))) | ||
Theorem | imasring 19968* | The image structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π β Ring) β β’ (π β (π β Ring β§ (πΉβ 1 ) = (1rβπ))) | ||
Theorem | qusring2 19969* | The quotient structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ ) & β’ (π β βΌ Er π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π + π) βΌ (π + π))) & β’ (π β ((π βΌ π β§ π βΌ π) β (π Β· π) βΌ (π Β· π))) & β’ (π β π β Ring) β β’ (π β (π β Ring β§ [ 1 ] βΌ = (1rβπ))) | ||
Theorem | crngbinom 19970* | The binomial theorem for commutative rings (special case of csrgbinom 19887): (π΄ + π΅)βπ is the sum from π = 0 to π of (πCπ) Β· ((π΄βπ) Β· (π΅β(π β π)). (Contributed by AV, 24-Aug-2019.) |
β’ π = (Baseβπ ) & β’ Γ = (.rβπ ) & β’ Β· = (.gβπ ) & β’ + = (+gβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (.gβπΊ) β β’ (((π β CRing β§ π β β0) β§ (π΄ β π β§ π΅ β π)) β (π β (π΄ + π΅)) = (π Ξ£g (π β (0...π) β¦ ((πCπ) Β· (((π β π) β π΄) Γ (π β π΅)))))) | ||
Syntax | coppr 19971 | The opposite ring operation. |
class oppr | ||
Definition | df-oppr 19972 | Define an opposite ring, which is the same as the original ring but with multiplication written the other way around. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ oppr = (π β V β¦ (π sSet β¨(.rβndx), tpos (.rβπ)β©)) | ||
Theorem | opprval 19973 | Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (opprβπ ) β β’ π = (π sSet β¨(.rβndx), tpos Β· β©) | ||
Theorem | opprmulfval 19974 | Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (opprβπ ) & β’ β = (.rβπ) β β’ β = tpos Β· | ||
Theorem | opprmul 19975 | Value of the multiplication operation of an opposite ring. Hypotheses eliminated by a suggestion of Stefan O'Rear, 30-Aug-2015. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (opprβπ ) & β’ β = (.rβπ) β β’ (π β π) = (π Β· π) | ||
Theorem | crngoppr 19976 | In a commutative ring, the opposite ring is equivalent to the original ring (for theorems like unitpropd 20049). (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ π = (opprβπ ) & β’ β = (.rβπ) β β’ ((π β CRing β§ π β π΅ β§ π β π΅) β (π Β· π) = (π β π)) | ||
Theorem | opprlem 19977 | Lemma for opprbas 19979 and oppradd 19981. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.) |
β’ π = (opprβπ ) & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β (.rβndx) β β’ (πΈβπ ) = (πΈβπ) | ||
Theorem | opprlemOLD 19978 | Obsolete version of opprlem 19977 as of 6-Nov-2024. Lemma for opprbas 19979 and oppradd 19981. (Contributed by Mario Carneiro, 1-Dec-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (opprβπ ) & β’ πΈ = Slot π & β’ π β β & β’ π < 3 β β’ (πΈβπ ) = (πΈβπ) | ||
Theorem | opprbas 19979 | Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
β’ π = (opprβπ ) & β’ π΅ = (Baseβπ ) β β’ π΅ = (Baseβπ) | ||
Theorem | opprbasOLD 19980 | Obsolete proof of opprbas 19979 as of 6-Nov-2024. Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (opprβπ ) & β’ π΅ = (Baseβπ ) β β’ π΅ = (Baseβπ) | ||
Theorem | oppradd 19981 | Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.) |
β’ π = (opprβπ ) & β’ + = (+gβπ ) β β’ + = (+gβπ) | ||
Theorem | oppraddOLD 19982 | Obsolete proof of opprbas 19979 as of 6-Nov-2024. Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (opprβπ ) & β’ + = (+gβπ ) β β’ + = (+gβπ) | ||
Theorem | opprring 19983 | An opposite ring is a ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.) |
β’ π = (opprβπ ) β β’ (π β Ring β π β Ring) | ||
Theorem | opprringb 19984 | Bidirectional form of opprring 19983. (Contributed by Mario Carneiro, 6-Dec-2014.) |
β’ π = (opprβπ ) β β’ (π β Ring β π β Ring) | ||
Theorem | oppr0 19985 | Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π = (opprβπ ) & β’ 0 = (0gβπ ) β β’ 0 = (0gβπ) | ||
Theorem | oppr1 19986 | Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π = (opprβπ ) & β’ 1 = (1rβπ ) β β’ 1 = (1rβπ) | ||
Theorem | opprneg 19987 | The negative function in an opposite ring. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ π = (opprβπ ) & β’ π = (invgβπ ) β β’ π = (invgβπ) | ||
Theorem | opprsubg 19988 | Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.) |
β’ π = (opprβπ ) β β’ (SubGrpβπ ) = (SubGrpβπ) | ||
Theorem | mulgass3 19989 | An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.gβπ ) & β’ Γ = (.rβπ ) β β’ ((π β Ring β§ (π β β€ β§ π β π΅ β§ π β π΅)) β (π Γ (π Β· π)) = (π Β· (π Γ π))) | ||
Syntax | cdsr 19990 | Ring divisibility relation. |
class β₯r | ||
Syntax | cui 19991 | Units in a ring. |
class Unit | ||
Syntax | cir 19992 | Ring irreducibles. |
class Irred | ||
Definition | df-dvdsr 19993* | Define the (right) divisibility relation in a ring. Access to the left divisibility relation is available through (β₯rβ(opprβπ )). (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ β₯r = (π€ β V β¦ {β¨π₯, π¦β© β£ (π₯ β (Baseβπ€) β§ βπ§ β (Baseβπ€)(π§(.rβπ€)π₯) = π¦)}) | ||
Definition | df-unit 19994 | Define the set of units in a ring, that is, all elements with a left and right multiplicative inverse. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ Unit = (π€ β V β¦ (β‘((β₯rβπ€) β© (β₯rβ(opprβπ€))) β {(1rβπ€)})) | ||
Definition | df-irred 19995* | Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.) |
β’ Irred = (π€ β V β¦ β¦((Baseβπ€) β (Unitβπ€)) / πβ¦{π§ β π β£ βπ₯ β π βπ¦ β π (π₯(.rβπ€)π¦) β π§}) | ||
Theorem | reldvdsr 19996 | The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ β₯ = (β₯rβπ ) β β’ Rel β₯ | ||
Theorem | dvdsrval 19997* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ Β· = (.rβπ ) β β’ β₯ = {β¨π₯, π¦β© β£ (π₯ β π΅ β§ βπ§ β π΅ (π§ Β· π₯) = π¦)} | ||
Theorem | dvdsr 19998* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ Β· = (.rβπ ) β β’ (π β₯ π β (π β π΅ β§ βπ§ β π΅ (π§ Β· π) = π)) | ||
Theorem | dvdsr2 19999* | Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ Β· = (.rβπ ) β β’ (π β π΅ β (π β₯ π β βπ§ β π΅ (π§ Β· π) = π)) | ||
Theorem | dvdsrmul 20000 | A left-multiple of π is divisible by π. (Contributed by Mario Carneiro, 1-Dec-2014.) |
β’ π΅ = (Baseβπ ) & β’ β₯ = (β₯rβπ ) & β’ Β· = (.rβπ ) β β’ ((π β π΅ β§ π β π΅) β π β₯ (π Β· π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |