![]() |
Metamath
Proof Explorer Theorem List (p. 375 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | grpomndo 37401 | 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 37402 | Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ π = ran πΊ β β’ ((πΊ β (Magma β© ExId ) β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) β π) | ||
Theorem | exidreslem 37403* | Lemma for exidres 37404 and exidresid 37405. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π» = (πΊ βΎ (π Γ π)) β β’ ((πΊ β (Magma β© ExId ) β§ π β π β§ π β π) β (π β dom dom π» β§ βπ₯ β dom dom π»((ππ»π₯) = π₯ β§ (π₯π»π) = π₯))) | ||
Theorem | exidres 37404 | 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 37405 | 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 37406 | A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((πΊ β AbelOp β§ ((π΄ β π β§ π΅ β π) β§ (πΆ β π β§ πΉ β π))) β ((π΄πΊπ΅)π·(πΆπΊπΉ)) = ((π΄π·πΆ)πΊ(π΅π·πΉ))) | ||
Theorem | grpoeqdivid 37407 | Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π· = ( /π βπΊ) β β’ ((πΊ β GrpOp β§ π΄ β π β§ π΅ β π) β (π΄ = π΅ β (π΄π·π΅) = π)) | ||
Theorem | grposnOLD 37408 | The group operation for the singleton group. Obsolete, use grp1 19002. instead. (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ β V β β’ {β¨β¨π΄, π΄β©, π΄β©} β GrpOp | ||
Syntax | cghomOLD 37409 | Obsolete version of cghm 19166 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.) |
class GrpOpHom | ||
Definition | df-ghomOLD 37410* | Obsolete version of df-ghm 19167 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 37411* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 37413. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = {π β£ (π:ran πΊβΆran π» β§ βπ₯ β ran πΊβπ¦ β ran πΊ((πβπ₯)π»(πβπ¦)) = (πβ(π₯πΊπ¦)))} β β’ ((πΊ β GrpOp β§ π» β GrpOp) β (πΊ GrpOpHom π») = π) | ||
Theorem | elghomlem2OLD 37412* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 37413. (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 37413* | Obsolete version of isghm 19169 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 37414 | Obsolete version of ghmlin 19174 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 37415 | Obsolete version of ghmid 19175 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 37416 | Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) |
β’ π = ran πΊ & β’ π = ran π» β β’ ((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β πΉ:πβΆπ) | ||
Theorem | ghomco 37417 | 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 37418 | Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ π = ran πΊ & β’ π· = ( /π βπΊ) & β’ πΆ = ( /π βπ») β β’ (((πΊ β GrpOp β§ π» β GrpOp β§ πΉ β (πΊ GrpOpHom π»)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄π·π΅)) = ((πΉβπ΄)πΆ(πΉβπ΅))) | ||
Theorem | grpokerinj 37419 | 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 37420 | Extend class notation with the class of all unital rings. |
class RingOps | ||
Definition | df-rngo 37421* | 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 37422 | 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 37423* | 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 37424* | Conditions that determine a ring. (Changed label from isringd 20226 to isrngod 37424-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 37425* | 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 37426 | 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 37427 | 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 37428* | 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 37429* | 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 37430 | 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 37431 | 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 37432 | 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 37433* | 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 37434 | 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 37435 | In a unital ring the addition is an abelian group. (Contributed by FL, 31-Aug-2009.) (New usage is discouraged.) |
β’ (β¨πΊ, π»β© β RingOps β πΊ β AbelOp) | ||
Theorem | rngogrpo 37436 | 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 37437 | The base set of a ring is not empty. (Contributed by FL, 24-Jan-2010.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (π β RingOps β π β β ) | ||
Theorem | rngogcl 37438 | 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 37439 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) = (π΅πΊπ΄)) | ||
Theorem | rngoaass 37440 | The addition operation of a ring is associative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = (π΄πΊ(π΅πΊπΆ))) | ||
Theorem | rngoa32 37441 | The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = ((π΄πΊπΆ)πΊπ΅)) | ||
Theorem | rngoa4 37442 | 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 37443 | 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 37444 | 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 37445 | A ring has an additive identity element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β RingOps β π β π) | ||
Theorem | rngo0rid 37446 | 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 37447 | 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 37448 | 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 37449 | 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 37450 | Obsolete as of 25-Jan-2020. Use ring1zr 20663 or srg1zr 20154 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 37451 | Obsolete as of 25-Jan-2020. Use rngen1zr 20664 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 37452 | Obsolete as of 25-Jan-2020. Use ringen1zr 20665 or srgen1zr 20155 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 37453 | A ring is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) β β’ ((π β RingOps β§ π΄ β π) β (πβπ΄) β π) | ||
Theorem | rngoaddneg1 37454 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π΄ β π) β (π΄πΊ(πβπ΄)) = π) | ||
Theorem | rngoaddneg2 37455 | Adding the negative in a ring gives zero. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π΄ β π) β ((πβπ΄)πΊπ΄) = π) | ||
Theorem | rngosub 37456 | Subtraction in a ring, in terms of addition and negation. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) & β’ π· = ( /π βπΊ) β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (π΄πΊ(πβπ΅))) | ||
Theorem | rngmgmbs4 37457* | 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 37458 | 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 37459 | 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 37460 | 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 37461 | 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 37462 | 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 37463 | 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 37464 | 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 37465 | 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 37466 | Obsolete as of 23-Jan-2020. Use 0ring01eqbi 20468 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 37467 | 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 37468 | 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 37469 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (πβ(π΄π»π΅)) = ((πβπ΄)π»π΅)) | ||
Theorem | rngonegrmul 37470 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (πβ(π΄π»π΅)) = (π΄π»(πβπ΅))) | ||
Theorem | rngosubdi 37471 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π»(π΅π·πΆ)) = ((π΄π»π΅)π·(π΄π»πΆ))) | ||
Theorem | rngosubdir 37472 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π»πΆ) = ((π΄π»πΆ)π·(π΅π»πΆ))) | ||
Theorem | zerdivemp1x 37473* | In a unital ring a left invertible element is not a zero divisor. See also ringinvnzdiv 20236. (Contributed by Jeff Madsen, 18-Apr-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = (GIdβπΊ) & β’ π = ran πΊ & β’ π = (GIdβπ») β β’ ((π β RingOps β§ π΄ β π β§ βπ β π (ππ»π΄) = π) β (π΅ β π β ((π΄π»π΅) = π β π΅ = π))) | ||
Syntax | cdrng 37474 | Extend class notation with the class of all division rings. |
class DivRingOps | ||
Definition | df-drngo 37475* | 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 37476 | 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 37477 | 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 37478 | Obsolete as of 23-Jan-2020. Use mnd1id 18731 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 37479 | 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 37480 | 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 37481* | Properties that determine a group operation. (Contributed by Jeff Madsen, 1-Dec-2009.) (New usage is discouraged.) |
β’ (π β π β V) & β’ (π β πΊ:(π Γ π)βΆπ) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§))) & β’ (π β π β π) & β’ ((π β§ π₯ β π) β (ππΊπ₯) = π₯) & β’ ((π β§ π₯ β π) β βπ β π (ππΊπ₯) = π) β β’ (π β πΊ β GrpOp) | ||
Theorem | isdrngo1 37482 | The predicate "is a division ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = (GIdβπΊ) & β’ π = ran πΊ β β’ (π β DivRingOps β (π β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp)) | ||
Theorem | divrngcl 37483 | The product of two nonzero elements of a division ring is nonzero. (Contributed by Jeff Madsen, 9-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = (GIdβπΊ) & β’ π = ran πΊ β β’ ((π β DivRingOps β§ π΄ β (π β {π}) β§ π΅ β (π β {π})) β (π΄π»π΅) β (π β {π})) | ||
Theorem | isdrngo2 37484* | A division ring is a ring in which 1 β 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = (GIdβπΊ) & β’ π = ran πΊ & β’ π = (GIdβπ») β β’ (π β DivRingOps β (π β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β (π β {π})(π¦π»π₯) = π))) | ||
Theorem | isdrngo3 37485* | A division ring is a ring in which 1 β 0 and every nonzero element is invertible. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = (GIdβπΊ) & β’ π = ran πΊ & β’ π = (GIdβπ») β β’ (π β DivRingOps β (π β RingOps β§ (π β π β§ βπ₯ β (π β {π})βπ¦ β π (π¦π»π₯) = π))) | ||
Syntax | crngohom 37486 | Extend class notation with the class of ring homomorphisms. |
class RingOpsHom | ||
Syntax | crngoiso 37487 | Extend class notation with the class of ring isomorphisms. |
class RingOpsIso | ||
Syntax | crisc 37488 | Extend class notation with the ring isomorphism relation. |
class βπ | ||
Definition | df-rngohom 37489* | Define the function which gives the set of ring homomorphisms between two given rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ RingOpsHom = (π β RingOps, π β RingOps β¦ {π β (ran (1st βπ ) βm ran (1st βπ)) β£ ((πβ(GIdβ(2nd βπ))) = (GIdβ(2nd βπ )) β§ βπ₯ β ran (1st βπ)βπ¦ β ran (1st βπ)((πβ(π₯(1st βπ)π¦)) = ((πβπ₯)(1st βπ )(πβπ¦)) β§ (πβ(π₯(2nd βπ)π¦)) = ((πβπ₯)(2nd βπ )(πβπ¦))))}) | ||
Theorem | rngohomval 37490* | The set of ring homomorphisms. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 22-Sep-2015.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπ») & β’ π½ = (1st βπ) & β’ πΎ = (2nd βπ) & β’ π = ran π½ & β’ π = (GIdβπΎ) β β’ ((π β RingOps β§ π β RingOps) β (π RingOpsHom π) = {π β (π βm π) β£ ((πβπ) = π β§ βπ₯ β π βπ¦ β π ((πβ(π₯πΊπ¦)) = ((πβπ₯)π½(πβπ¦)) β§ (πβ(π₯π»π¦)) = ((πβπ₯)πΎ(πβπ¦))))}) | ||
Theorem | isrngohom 37491* | The predicate "is a ring homomorphism from π to π". (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπ») & β’ π½ = (1st βπ) & β’ πΎ = (2nd βπ) & β’ π = ran π½ & β’ π = (GIdβπΎ) β β’ ((π β RingOps β§ π β RingOps) β (πΉ β (π RingOpsHom π) β (πΉ:πβΆπ β§ (πΉβπ) = π β§ βπ₯ β π βπ¦ β π ((πΉβ(π₯πΊπ¦)) = ((πΉβπ₯)π½(πΉβπ¦)) β§ (πΉβ(π₯π»π¦)) = ((πΉβπ₯)πΎ(πΉβπ¦)))))) | ||
Theorem | rngohomf 37492 | A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) & β’ π = ran π½ β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RingOpsHom π)) β πΉ:πβΆπ) | ||
Theorem | rngohomcl 37493 | Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) & β’ π = ran π½ β β’ (((π β RingOps β§ π β RingOps β§ πΉ β (π RingOpsHom π)) β§ π΄ β π) β (πΉβπ΄) β π) | ||
Theorem | rngohom1 37494 | A ring homomorphism preserves 1. (Contributed by Jeff Madsen, 24-Jun-2011.) |
β’ π» = (2nd βπ ) & β’ π = (GIdβπ») & β’ πΎ = (2nd βπ) & β’ π = (GIdβπΎ) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RingOpsHom π)) β (πΉβπ) = π) | ||
Theorem | rngohomadd 37495 | Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) β β’ (((π β RingOps β§ π β RingOps β§ πΉ β (π RingOpsHom π)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄πΊπ΅)) = ((πΉβπ΄)π½(πΉβπ΅))) | ||
Theorem | rngohommul 37496 | Ring homomorphisms preserve multiplication. (Contributed by Jeff Madsen, 3-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π» = (2nd βπ ) & β’ πΎ = (2nd βπ) β β’ (((π β RingOps β§ π β RingOps β§ πΉ β (π RingOpsHom π)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄π»π΅)) = ((πΉβπ΄)πΎ(πΉβπ΅))) | ||
Theorem | rngogrphom 37497 | A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π½ = (1st βπ) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RingOpsHom π)) β πΉ β (πΊ GrpOpHom π½)) | ||
Theorem | rngohom0 37498 | A ring homomorphism preserves 0. (Contributed by Jeff Madsen, 2-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = (GIdβπΊ) & β’ π½ = (1st βπ) & β’ π = (GIdβπ½) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RingOpsHom π)) β (πΉβπ) = π) | ||
Theorem | rngohomsub 37499 | Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π» = ( /π βπΊ) & β’ π½ = (1st βπ) & β’ πΎ = ( /π βπ½) β β’ (((π β RingOps β§ π β RingOps β§ πΉ β (π RingOpsHom π)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄π»π΅)) = ((πΉβπ΄)πΎ(πΉβπ΅))) | ||
Theorem | rngohomco 37500 | The composition of two ring homomorphisms is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ (((π β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π RingOpsHom π) β§ πΊ β (π RingOpsHom π))) β (πΊ β πΉ) β (π RingOpsHom π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |