Home | Metamath
Proof Explorer Theorem List (p. 363 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 | exidu1 36201* | Uniqueness of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (πΊ β (Magma β© ExId ) β β!π’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ (π₯πΊπ’) = π₯)) | ||
Theorem | idrval 36202* | The value of the identity element. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (πΊ β π΄ β π = (β©π’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ (π₯πΊπ’) = π₯))) | ||
Theorem | iorlid 36203 | A magma right and left identity belongs to the underlying set of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (πΊ β (Magma β© ExId ) β π β π) | ||
Theorem | cmpidelt 36204 | A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ ((πΊ β (Magma β© ExId ) β§ π΄ β π) β ((ππΊπ΄) = π΄ β§ (π΄πΊπ) = π΄)) | ||
Syntax | csem 36205 | Extend class notation with the class of all semigroups. |
class SemiGrp | ||
Definition | df-sgrOLD 36206 | Obsolete version of df-sgrp 18481 as of 3-Feb-2020. A semigroup is an associative magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ SemiGrp = (Magma β© Ass) | ||
Theorem | smgrpismgmOLD 36207 | Obsolete version of sgrpmgm 18486 as of 3-Feb-2020. A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (πΊ β SemiGrp β πΊ β Magma) | ||
Theorem | issmgrpOLD 36208* | Obsolete version of issgrp 18482 as of 3-Feb-2020. The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β π΄ β (πΊ β SemiGrp β (πΊ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§))))) | ||
Theorem | smgrpmgm 36209 | A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β SemiGrp β πΊ:(π Γ π)βΆπ) | ||
Theorem | smgrpassOLD 36210* | Obsolete version of sgrpass 18487 as of 3-Feb-2020. A semigroup is associative. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β SemiGrp β βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§))) | ||
Syntax | cmndo 36211 | Extend class notation with the class of all monoids. |
class MndOp | ||
Definition | df-mndo 36212 | A monoid is a semigroup with an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ MndOp = (SemiGrp β© ExId ) | ||
Theorem | mndoissmgrpOLD 36213 | Obsolete version of mndsgrp 18497 as of 3-Feb-2020. A monoid is a semigroup. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (πΊ β MndOp β πΊ β SemiGrp) | ||
Theorem | mndoisexid 36214 | A monoid has an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ (πΊ β MndOp β πΊ β ExId ) | ||
Theorem | mndoismgmOLD 36215 | Obsolete version of mndmgm 18498 as of 3-Feb-2020. A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (πΊ β MndOp β πΊ β Magma) | ||
Theorem | mndomgmid 36216 | A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.) |
β’ (πΊ β MndOp β πΊ β (Magma β© ExId )) | ||
Theorem | ismndo 36217* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β π΄ β (πΊ β MndOp β (πΊ β SemiGrp β§ βπ₯ β π βπ¦ β π ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦)))) | ||
Theorem | ismndo1 36218* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β π΄ β (πΊ β MndOp β (πΊ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ₯ β π βπ¦ β π ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦)))) | ||
Theorem | ismndo2 36219* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (πΊ β π΄ β (πΊ β MndOp β (πΊ:(π Γ π)βΆπ β§ βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)) β§ βπ₯ β π βπ¦ β π ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦)))) | ||
Theorem | grpomndo 36220 | A group is a monoid. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ (πΊ β GrpOp β πΊ β MndOp) | ||
Theorem | exidcl 36221 | Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ π = ran πΊ β β’ ((πΊ β (Magma β© ExId ) β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) | ||
Theorem | exidreslem 36222* | Lemma for exidres 36223 and exidresid 36224. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π» = (πΊ βΎ (π Γ π)) β β’ ((πΊ β (Magma β© ExId ) β§ π β π β§ π β π) β (π β dom dom π» β§ βπ₯ β dom dom π»((ππ»π₯) = π₯ β§ (π₯π»π) = π₯))) | ||
Theorem | exidres 36223 | The restriction of a binary operation with identity to a subset containing the identity has an identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π» = (πΊ βΎ (π Γ π)) β β’ ((πΊ β (Magma β© ExId ) β§ π β π β§ π β π) β π» β ExId ) | ||
Theorem | exidresid 36224 | The restriction of a binary operation with identity to a subset containing the identity has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π» = (πΊ βΎ (π Γ π)) β β’ (((πΊ β (Magma β© ExId ) β§ π β π β§ π β π) β§ π» β Magma) β (GIdβπ») = π) | ||
Theorem | ablo4pnp 36225 | A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ πΉ β π))) β ((π΄πΊπ΅)π·(πΆπΊπΉ)) = ((π΄π·πΆ)πΊ(π΅π·πΉ))) | ||
Theorem | grpoeqdivid 36226 | Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄ = π΅ β (π΄π·π΅) = π)) | ||
Theorem | grposnOLD 36227 | The group operation for the singleton group. Obsolete, use grp1 18788. instead. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ β V β β’ {β¨β¨π΄, π΄β©, π΄β©} β GrpOp | ||
Syntax | cghomOLD 36228 | Obsolete version of cghm 18937 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.) |
class GrpOpHom | ||
Definition | df-ghomOLD 36229* | Obsolete version of df-ghm 18938 as of 15-Mar-2020. Define the set of group homomorphisms from π to β. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) |
β’ GrpOpHom = (π β GrpOp, β β GrpOp β¦ {π β£ (π:ran πβΆran β β§ βπ₯ β ran πβπ¦ β ran π((πβπ₯)β(πβπ¦)) = (πβ(π₯ππ¦)))}) | ||
Theorem | elghomlem1OLD 36230* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 36232. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = {π β£ (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))} β β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΊ GrpOpHom π») = π) | ||
Theorem | elghomlem2OLD 36231* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 36232. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = {π β£ (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))} β β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΉ β (πΊ GrpOpHom π») β (πΉ:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))))) | ||
Theorem | elghomOLD 36232* | Obsolete version of isghm 18940 as of 15-Mar-2020. Membership in the set of group homomorphisms from πΊ to π». (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = ran πΊ & β’ π = ran π» β β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΉ β (πΊ GrpOpHom π») β (πΉ:πβΆπ β§ βπ₯ β π βπ¦ β π ((πΉβπ₯)π»(πΉβπ¦)) = (πΉβ(π₯πΊπ¦))))) | ||
Theorem | ghomlinOLD 36233 | Obsolete version of ghmlin 18945 as of 15-Mar-2020. Linearity of a group homomorphism. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = ran πΊ β β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β ((πΉβπ΄)π»(πΉβπ΅)) = (πΉβ(π΄πΊπ΅))) | ||
Theorem | ghomidOLD 36234 | Obsolete version of ghmid 18946 as of 15-Mar-2020. A group homomorphism maps identity element to identity element. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (GIdβπΊ) & β’ π = (GIdβπ») β β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (πΉβπ) = π) | ||
Theorem | ghomf 36235 | Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) |
β’ π = ran πΊ & β’ π = ran π» β β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β πΉ:πβΆπ) | ||
Theorem | ghomco 36236 | The composition of two group homomorphisms is a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |
β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΎ β GrpOp) β§ (π β (πΊ GrpOpHom π») β§ π β (π» GrpOpHom πΎ))) β (π β π) β (πΊ GrpOpHom πΎ)) | ||
Theorem | ghomdiv 36237 | Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) & β’ πΆ = ( /π βπ») β β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄π·π΅)) = ((πΉβπ΄)πΆ(πΉβπ΅))) | ||
Theorem | grpokerinj 36238 | A group homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π = ran π» & β’ π = (GIdβπ») β β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β (πΉ:πβ1-1βπ β (β‘πΉ β {π}) = {π})) | ||
Syntax | crngo 36239 | Extend class notation with the class of all unital rings. |
class RingOps | ||
Definition | df-rngo 36240* | Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006.) (New usage is discouraged.) |
β’ RingOps = {β¨π, ββ© β£ ((π β AbelOp β§ β:(ran π Γ ran π)βΆran π) β§ (βπ₯ β ran πβπ¦ β ran πβπ§ β ran π(((π₯βπ¦)βπ§) = (π₯β(π¦βπ§)) β§ (π₯β(π¦ππ§)) = ((π₯βπ¦)π(π₯βπ§)) β§ ((π₯ππ¦)βπ§) = ((π₯βπ§)π(π¦βπ§))) β§ βπ₯ β ran πβπ¦ β ran π((π₯βπ¦) = π¦ β§ (π¦βπ₯) = π¦)))} | ||
Theorem | relrngo 36241 | The class of all unital rings is a relation. (Contributed by FL, 31-Aug-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ Rel RingOps | ||
Theorem | isrngo 36242* | The predicate "is a (unital) ring." Definition of "ring with unit" in [Schechter] p. 187. (Contributed by Jeff Hankins, 21-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (π» β π΄ β (β¨πΊ, π»β© β RingOps β ((πΊ β AbelOp β§ π»:(π Γ π)βΆπ) β§ (βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦))))) | ||
Theorem | isrngod 36243* | Conditions that determine a ring. (Changed label from isringd 19932 to isrngod 36243-NM 2-Aug-2013.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ (π β πΊ β AbelOp) & β’ (π β π = ran πΊ) & β’ (π β π»:(π Γ π)βΆπ) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§))) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§))) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) & β’ (π β π β π) & β’ ((π β§ π¦ β π) β (ππ»π¦) = π¦) & β’ ((π β§ π¦ β π) β (π¦π»π) = π¦) β β’ (π β β¨πΊ, π»β© β RingOps) | ||
Theorem | rngoi 36244* | The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007.) (Proof shortened by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β RingOps β ((πΊ β AbelOp β§ π»:(π Γ π)βΆπ) β§ (βπ₯ β π βπ¦ β π βπ§ β π (((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§)) β§ (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§)) β§ ((π₯πΊπ¦)π»π§) = ((π₯π»π§)πΊ(π¦π»π§))) β§ βπ₯ β π βπ¦ β π ((π₯π»π¦) = π¦ β§ (π¦π»π₯) = π¦)))) | ||
Theorem | rngosm 36245 | Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β RingOps β π»:(π Γ π)βΆπ) | ||
Theorem | rngocl 36246 | Closure of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (π΄π»π΅) β π) | ||
Theorem | rngoid 36247* | 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.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π) β βπ’ β π ((π’π»π΄) = π΄ β§ (π΄π»π’) = π΄)) | ||
Theorem | rngoideu 36248* | The unity element of a ring is unique. (Contributed by NM, 4-Apr-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β RingOps β β!π’ β π βπ₯ β π ((π’π»π₯) = π₯ β§ (π₯π»π’) = π₯)) | ||
Theorem | rngodi 36249 | Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π»(π΅πΊπΆ)) = ((π΄π»π΅)πΊ(π΄π»πΆ))) | ||
Theorem | rngodir 36250 | Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)π»πΆ) = ((π΄π»πΆ)πΊ(π΅π»πΆ))) | ||
Theorem | rngoass 36251 | Associative law for the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π»π΅)π»πΆ) = (π΄π»(π΅π»πΆ))) | ||
Theorem | rngo2 36252* | A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π) β βπ₯ β π (π΄πΊπ΄) = ((π₯πΊπ₯)π»π΄)) | ||
Theorem | rngoablo 36253 | A ring's addition operation is an Abelian group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) β β’ (π β RingOps β πΊ β AbelOp) | ||
Theorem | rngoablo2 36254 | In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
β’ (β¨πΊ, π»β© β RingOps β πΊ β AbelOp) | ||
Theorem | rngogrpo 36255 | A ring's addition operation is a group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) β β’ (π β RingOps β πΊ β GrpOp) | ||
Theorem | rngone0 36256 | The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (π β RingOps β π β β ) | ||
Theorem | rngogcl 36257 | Closure law for the addition (group) operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) | ||
Theorem | rngocom 36258 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) = (π΅πΊπ΄)) | ||
Theorem | rngoaass 36259 | The addition operation of a ring is associative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = (π΄πΊ(π΅πΊπΆ))) | ||
Theorem | rngoa32 36260 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = ((π΄πΊπΆ)πΊπ΅)) | ||
Theorem | rngoa4 36261 | Rearrangement of 4 terms in a sum of ring elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄πΊπ΅)πΊ(πΆπΊπ·)) = ((π΄πΊπΆ)πΊ(π΅πΊπ·))) | ||
Theorem | rngorcan 36262 | Right cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπΆ) = (π΅πΊπΆ) β π΄ = π΅)) | ||
Theorem | rngolcan 36263 | Left cancellation law for the addition operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((πΆπΊπ΄) = (πΆπΊπ΅) β π΄ = π΅)) | ||
Theorem | rngo0cl 36264 | A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β RingOps β π β π) | ||
Theorem | rngo0rid 36265 | The additive identity of a ring is a right identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π΄ β π) β (π΄πΊπ) = π΄) | ||
Theorem | rngo0lid 36266 | The additive identity of a ring is a left identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π΄ β π) β (ππΊπ΄) = π΄) | ||
Theorem | rngolz 36267 | The zero of a unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
β’ π = (GIdβπΊ) & β’ π = ran πΊ & β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) β β’ ((π β RingOps β§ π΄ β π) β (ππ»π΄) = π) | ||
Theorem | rngorz 36268 | The zero of a unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
β’ π = (GIdβπΊ) & β’ π = ran πΊ & β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) β β’ ((π β RingOps β§ π΄ β π) β (π΄π»π) = π) | ||
Theorem | rngosn3 36269 | Obsolete as of 25-Jan-2020. Use ring1zr 20668 or srg1zr 19870 instead. The only unital ring with a base set consisting in one element is the zero ring. (Contributed by FL, 13-Feb-2010.) (Proof shortened by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π΅) β (π = {π΄} β π = β¨{β¨β¨π΄, π΄β©, π΄β©}, {β¨β¨π΄, π΄β©, π΄β©}β©)) | ||
Theorem | rngosn4 36270 | Obsolete as of 25-Jan-2020. Use rngen1zr 20669 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 14-Feb-2010.) (Revised by Mario Carneiro, 30-Apr-2015.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π) β (π β 1o β π = β¨{β¨β¨π΄, π΄β©, π΄β©}, {β¨β¨π΄, π΄β©, π΄β©}β©)) | ||
Theorem | rngosn6 36271 | Obsolete as of 25-Jan-2020. Use ringen1zr 20670 or srgen1zr 19871 instead. The only unital ring with one element is the zero ring. (Contributed by FL, 15-Feb-2010.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β RingOps β (π β 1o β π = β¨{β¨β¨π, πβ©, πβ©}, {β¨β¨π, πβ©, πβ©}β©)) | ||
Theorem | rngonegcl 36272 | A ring is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) β β’ ((π β RingOps β§ π΄ β π) β (πβπ΄) β π) | ||
Theorem | rngoaddneg1 36273 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π΄ β π) β (π΄πΊ(πβπ΄)) = π) | ||
Theorem | rngoaddneg2 36274 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π΄ β π) β ((πβπ΄)πΊπ΄) = π) | ||
Theorem | rngosub 36275 | Subtraction in a ring, in terms of addition and negation. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π· = ( /π βπΊ) β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (π΄πΊ(πβπ΅))) | ||
Theorem | rngmgmbs4 36276* | The range of an internal operation with a left and right identity element equals its base set. (Contributed by FL, 24-Jan-2010.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ ((πΊ:(π Γ π)βΆπ β§ βπ’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ (π₯πΊπ’) = π₯)) β ran πΊ = π) | ||
Theorem | rngodm1dm2 36277 | In a unital ring the domain of the first variable of the addition equals the domain of the first variable of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
β’ π» = (2nd βπ ) & β’ πΊ = (1st βπ ) β β’ (π β RingOps β dom dom πΊ = dom dom π») | ||
Theorem | rngorn1 36278 | In a unital ring the range of the addition equals the domain of the first variable of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
β’ π» = (2nd βπ ) & β’ πΊ = (1st βπ ) β β’ (π β RingOps β ran πΊ = dom dom π») | ||
Theorem | rngorn1eq 36279 | In a unital ring the range of the addition equals the range of the multiplication. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
β’ π» = (2nd βπ ) & β’ πΊ = (1st βπ ) β β’ (π β RingOps β ran πΊ = ran π») | ||
Theorem | rngomndo 36280 | In a unital ring the multiplication is a monoid. (Contributed by FL, 24-Jan-2010.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π» = (2nd βπ ) β β’ (π β RingOps β π» β MndOp) | ||
Theorem | rngoidmlem 36281 | The unity element of a ring is an identity element for the multiplication. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.) |
β’ π» = (2nd βπ ) & β’ π = ran (1st βπ ) & β’ π = (GIdβπ») β β’ ((π β RingOps β§ π΄ β π) β ((ππ»π΄) = π΄ β§ (π΄π»π) = π΄)) | ||
Theorem | rngolidm 36282 | The unity element of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010.) (New usage is discouraged.) |
β’ π» = (2nd βπ ) & β’ π = ran (1st βπ ) & β’ π = (GIdβπ») β β’ ((π β RingOps β§ π΄ β π) β (ππ»π΄) = π΄) | ||
Theorem | rngoridm 36283 | The unity element of a ring is an identity element for the multiplication. (Contributed by FL, 18-Apr-2010.) (New usage is discouraged.) |
β’ π» = (2nd βπ ) & β’ π = ran (1st βπ ) & β’ π = (GIdβπ») β β’ ((π β RingOps β§ π΄ β π) β (π΄π»π) = π΄) | ||
Theorem | rngo1cl 36284 | The unity element of a ring belongs to the base set. (Contributed by FL, 12-Feb-2010.) (New usage is discouraged.) |
β’ π = ran (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = (GIdβπ») β β’ (π β RingOps β π β π) | ||
Theorem | rngoueqz 36285 | Obsolete as of 23-Jan-2020. Use 0ring01eqbi 20666 instead. In a unital ring the zero equals the ring unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = (GIdβπΊ) & β’ π = (GIdβπ») & β’ π = ran πΊ β β’ (π β RingOps β (π β 1o β π = π)) | ||
Theorem | rngonegmn1l 36286 | Negation in a ring is the same as left multiplication by -1. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π = (GIdβπ») β β’ ((π β RingOps β§ π΄ β π) β (πβπ΄) = ((πβπ)π»π΄)) | ||
Theorem | rngonegmn1r 36287 | Negation in a ring is the same as right multiplication by -1. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π = (GIdβπ») β β’ ((π β RingOps β§ π΄ β π) β (πβπ΄) = (π΄π»(πβπ))) | ||
Theorem | rngoneglmul 36288 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (πβ(π΄π»π΅)) = ((πβπ΄)π»π΅)) | ||
Theorem | rngonegrmul 36289 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (πβ(π΄π»π΅)) = (π΄π»(πβπ΅))) | ||
Theorem | rngosubdi 36290 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π»(π΅π·πΆ)) = ((π΄π»π΅)π·(π΄π»πΆ))) | ||
Theorem | rngosubdir 36291 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π»πΆ) = ((π΄π»πΆ)π·(π΅π»πΆ))) | ||
Theorem | zerdivemp1x 36292* | In a unital ring a left invertible element is not a zero divisor. See also ringinvnzdiv 19940. (Contributed by Jeff Madsen, 18-Apr-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = (GIdβπΊ) & β’ π = ran πΊ & β’ π = (GIdβπ») β β’ ((π β RingOps β§ π΄ β π β§ βπ β π (ππ»π΄) = π) β (π΅ β π β ((π΄π»π΅) = π β π΅ = π))) | ||
Syntax | cdrng 36293 | Extend class notation with the class of all division rings. |
class DivRingOps | ||
Definition | df-drngo 36294* | Define the class of all division rings (sometimes called skew fields). A division ring is a unital ring where every element except the additive identity has a multiplicative inverse. (Contributed by NM, 4-Apr-2009.) (New usage is discouraged.) |
β’ DivRingOps = {β¨π, ββ© β£ (β¨π, ββ© β RingOps β§ (β βΎ ((ran π β {(GIdβπ)}) Γ (ran π β {(GIdβπ)}))) β GrpOp)} | ||
Theorem | isdivrngo 36295 | The predicate "is a division ring". (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.) |
β’ (π» β π΄ β (β¨πΊ, π»β© β DivRingOps β (β¨πΊ, π»β© β RingOps β§ (π» βΎ ((ran πΊ β {(GIdβπΊ)}) Γ (ran πΊ β {(GIdβπΊ)}))) β GrpOp))) | ||
Theorem | drngoi 36296 | The properties of a division ring. (Contributed by NM, 4-Apr-2009.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β DivRingOps β (π β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp)) | ||
Theorem | gidsn 36297 | Obsolete as of 23-Jan-2020. Use mnd1id 18533 instead. The identity element of the trivial group. (Contributed by FL, 21-Jun-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
β’ π΄ β V β β’ (GIdβ{β¨β¨π΄, π΄β©, π΄β©}) = π΄ | ||
Theorem | zrdivrng 36298 | The zero ring is not a division ring. (Contributed by FL, 24-Jan-2010.) (Proof shortened by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
β’ π΄ β V β β’ Β¬ β¨{β¨β¨π΄, π΄β©, π΄β©}, {β¨β¨π΄, π΄β©, π΄β©}β© β DivRingOps | ||
Theorem | dvrunz 36299 | In a division ring the ring unit is different from the zero. (Contributed by FL, 14-Feb-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π = (GIdβπ») β β’ (π β DivRingOps β π β π) | ||
Theorem | isgrpda 36300* | Properties that determine a group operation. (Contributed by Jeff Madsen, 1-Dec-2009.) (New usage is discouraged.) |
β’ (π β π β V) & β’ (π β πΊ:(π Γ π)βΆπ) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§))) & β’ (π β π β π) & β’ ((π β§ π₯ β π) β (ππΊπ₯) = π₯) & β’ ((π β§ π₯ β π) β βπ β π (ππΊπ₯) = π) β β’ (π β πΊ β GrpOp) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |