![]() |
Metamath
Proof Explorer Theorem List (p. 368 of 479) | < 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: | ![]() (1-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ismrer1 36701* | An isometry between β and ββ1. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.) |
β’ π = ((abs β β ) βΎ (β Γ β)) & β’ πΉ = (π₯ β β β¦ ({π΄} Γ {π₯})) β β’ (π΄ β π β πΉ β (π Ismty (βnβ{π΄}))) | ||
Theorem | reheibor 36702 | Heine-Borel theorem for real numbers. A subset of β is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.) |
β’ π = ((abs β β ) βΎ (π Γ π)) & β’ π = (MetOpenβπ) & β’ π = (topGenβran (,)) β β’ (π β β β (π β Comp β (π β (Clsdβπ) β§ π β (Bndβπ)))) | ||
Theorem | iccbnd 36703 | A closed interval in β is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Sep-2015.) |
β’ π½ = (π΄[,]π΅) & β’ π = ((abs β β ) βΎ (π½ Γ π½)) β β’ ((π΄ β β β§ π΅ β β) β π β (Bndβπ½)) | ||
Theorem | icccmpALT 36704 | A closed interval in β is compact. Alternate proof of icccmp 24340 using the Heine-Borel theorem heibor 36684. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Aug-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π½ = (π΄[,]π΅) & β’ π = ((abs β β ) βΎ (π½ Γ π½)) & β’ π = (MetOpenβπ) β β’ ((π΄ β β β§ π΅ β β) β π β Comp) | ||
Syntax | cass 36705 | Extend class notation with a device to add associativity to internal operations. |
class Ass | ||
Definition | df-ass 36706* | A device to add associativity to various sorts of internal operations. The definition is meaningful when π is a magma at least. (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.) |
β’ Ass = {π β£ βπ₯ β dom dom πβπ¦ β dom dom πβπ§ β dom dom π((π₯ππ¦)ππ§) = (π₯π(π¦ππ§))} | ||
Syntax | cexid 36707 | Extend class notation with the class of all the internal operations with an identity element. |
class ExId | ||
Definition | df-exid 36708* | A device to add an identity element to various sorts of internal operations. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ ExId = {π β£ βπ₯ β dom dom πβπ¦ β dom dom π((π₯ππ¦) = π¦ β§ (π¦ππ₯) = π¦)} | ||
Theorem | isass 36709* | The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β π΄ β (πΊ β Ass β βπ₯ β π βπ¦ β π βπ§ β π ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§)))) | ||
Theorem | isexid 36710* | The predicate πΊ has a left and right identity element. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β π΄ β (πΊ β ExId β βπ₯ β π βπ¦ β π ((π₯πΊπ¦) = π¦ β§ (π¦πΊπ₯) = π¦))) | ||
Syntax | cmagm 36711 | Extend class notation with the class of all magmas. |
class Magma | ||
Definition | df-mgmOLD 36712* | Obsolete version of df-mgm 18560 as of 3-Feb-2020. A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ Magma = {π β£ βπ‘ π:(π‘ Γ π‘)βΆπ‘} | ||
Theorem | ismgmOLD 36713 | Obsolete version of ismgm 18561 as of 3-Feb-2020. The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β π΄ β (πΊ β Magma β πΊ:(π Γ π)βΆπ)) | ||
Theorem | clmgmOLD 36714 | Obsolete version of mgmcl 18563 as of 3-Feb-2020. Closure of a magma. (Contributed by FL, 14-Sep-2010.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = dom dom πΊ β β’ ((πΊ β Magma β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) | ||
Theorem | opidonOLD 36715 | Obsolete version of mndpfo 18647 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β (Magma β© ExId ) β πΊ:(π Γ π)βontoβπ) | ||
Theorem | rngopidOLD 36716 | Obsolete version of mndpfo 18647 as of 23-Jan-2020. Range of an operation with a left and right identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (πΊ β (Magma β© ExId ) β ran πΊ = dom dom πΊ) | ||
Theorem | opidon2OLD 36717 | Obsolete version of mndpfo 18647 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = ran πΊ β β’ (πΊ β (Magma β© ExId ) β πΊ:(π Γ π)βontoβπ) | ||
Theorem | isexid2 36718* | If πΊ β (Magma β© ExId ), then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ (πΊ β (Magma β© ExId ) β βπ’ β π βπ₯ β π ((π’πΊπ₯) = π₯ β§ (π₯πΊπ’) = π₯)) | ||
Theorem | exidu1 36719* | 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 36720* | 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 36721 | 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 36722 | 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 36723 | Extend class notation with the class of all semigroups. |
class SemiGrp | ||
Definition | df-sgrOLD 36724 | Obsolete version of df-sgrp 18609 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 36725 | Obsolete version of sgrpmgm 18614 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 36726* | Obsolete version of issgrp 18610 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 36727 | A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ π = dom dom πΊ β β’ (πΊ β SemiGrp β πΊ:(π Γ π)βΆπ) | ||
Theorem | smgrpassOLD 36728* | Obsolete version of sgrpass 18615 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 36729 | Extend class notation with the class of all monoids. |
class MndOp | ||
Definition | df-mndo 36730 | A monoid is a semigroup with an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ MndOp = (SemiGrp β© ExId ) | ||
Theorem | mndoissmgrpOLD 36731 | Obsolete version of mndsgrp 18630 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 36732 | A monoid has an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
β’ (πΊ β MndOp β πΊ β ExId ) | ||
Theorem | mndoismgmOLD 36733 | Obsolete version of mndmgm 18631 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 36734 | A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.) |
β’ (πΊ β MndOp β πΊ β (Magma β© ExId )) | ||
Theorem | ismndo 36735* | 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 36736* | 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 36737* | 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 36738 | 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 36739 | Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ π = ran πΊ β β’ ((πΊ β (Magma β© ExId ) β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) | ||
Theorem | exidreslem 36740* | Lemma for exidres 36741 and exidresid 36742. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π» = (πΊ βΎ (π Γ π)) β β’ ((πΊ β (Magma β© ExId ) β§ π β π β§ π β π) β (π β dom dom π» β§ βπ₯ β dom dom π»((ππ»π₯) = π₯ β§ (π₯π»π) = π₯))) | ||
Theorem | exidres 36741 | 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 36742 | 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 36743 | A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ πΉ β π))) β ((π΄πΊπ΅)π·(πΆπΊπΉ)) = ((π΄π·πΆ)πΊ(π΅π·πΉ))) | ||
Theorem | grpoeqdivid 36744 | Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄ = π΅ β (π΄π·π΅) = π)) | ||
Theorem | grposnOLD 36745 | The group operation for the singleton group. Obsolete, use grp1 18929. instead. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ β V β β’ {β¨β¨π΄, π΄β©, π΄β©} β GrpOp | ||
Syntax | cghomOLD 36746 | Obsolete version of cghm 19088 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.) |
class GrpOpHom | ||
Definition | df-ghomOLD 36747* | Obsolete version of df-ghm 19089 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 36748* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 36750. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = {π β£ (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))} β β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΊ GrpOpHom π») = π) | ||
Theorem | elghomlem2OLD 36749* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 36750. (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 36750* | Obsolete version of isghm 19091 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 36751 | Obsolete version of ghmlin 19096 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 36752 | Obsolete version of ghmid 19097 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 36753 | Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) |
β’ π = ran πΊ & β’ π = ran π» β β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β πΉ:πβΆπ) | ||
Theorem | ghomco 36754 | 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 36755 | Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) & β’ πΆ = ( /π βπ») β β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄π·π΅)) = ((πΉβπ΄)πΆ(πΉβπ΅))) | ||
Theorem | grpokerinj 36756 | 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 36757 | Extend class notation with the class of all unital rings. |
class RingOps | ||
Definition | df-rngo 36758* | 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 36759 | 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 36760* | 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 36761* | Conditions that determine a ring. (Changed label from isringd 20104 to isrngod 36761-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 36762* | 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 36763 | 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 36764 | 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 36765* | 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 36766* | 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 36767 | 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 36768 | 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 36769 | 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 36770* | 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 36771 | 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 36772 | In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
β’ (β¨πΊ, π»β© β RingOps β πΊ β AbelOp) | ||
Theorem | rngogrpo 36773 | 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 36774 | The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (π β RingOps β π β β ) | ||
Theorem | rngogcl 36775 | 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 36776 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) = (π΅πΊπ΄)) | ||
Theorem | rngoaass 36777 | The addition operation of a ring is associative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = (π΄πΊ(π΅πΊπΆ))) | ||
Theorem | rngoa32 36778 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = ((π΄πΊπΆ)πΊπ΅)) | ||
Theorem | rngoa4 36779 | 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 36780 | 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 36781 | 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 36782 | A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β RingOps β π β π) | ||
Theorem | rngo0rid 36783 | 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 36784 | 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 36785 | 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 36786 | 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 36787 | Obsolete as of 25-Jan-2020. Use ring1zr 20396 or srg1zr 20037 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 36788 | Obsolete as of 25-Jan-2020. Use rngen1zr 20397 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 36789 | Obsolete as of 25-Jan-2020. Use ringen1zr 20398 or srgen1zr 20038 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 36790 | A ring is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) β β’ ((π β RingOps β§ π΄ β π) β (πβπ΄) β π) | ||
Theorem | rngoaddneg1 36791 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π΄ β π) β (π΄πΊ(πβπ΄)) = π) | ||
Theorem | rngoaddneg2 36792 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π΄ β π) β ((πβπ΄)πΊπ΄) = π) | ||
Theorem | rngosub 36793 | Subtraction in a ring, in terms of addition and negation. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π· = ( /π βπΊ) β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (π΄πΊ(πβπ΅))) | ||
Theorem | rngmgmbs4 36794* | 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 36795 | 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 36796 | 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 36797 | 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 36798 | 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 36799 | 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 36800 | 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 β§ π΄ β π) β (ππ»π΄) = π΄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |