![]() |
Metamath
Proof Explorer Theorem List (p. 369 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rngorn1 36801 | 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 36802 | 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 36803 | 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 36804 | 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 36805 | 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 36806 | 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 36807 | 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 36808 | Obsolete as of 23-Jan-2020. Use 0ring01eqbi 20307 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 36809 | 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 36810 | 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 36811 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (πβ(π΄π»π΅)) = ((πβπ΄)π»π΅)) | ||
Theorem | rngonegrmul 36812 | Negation of a product in a ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (invβπΊ) β β’ ((π β RingOps β§ π΄ β π β§ π΅ β π) β (πβ(π΄π»π΅)) = (π΄π»(πβπ΅))) | ||
Theorem | rngosubdi 36813 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π»(π΅π·πΆ)) = ((π΄π»π΅)π·(π΄π»πΆ))) | ||
Theorem | rngosubdir 36814 | Ring multiplication distributes over subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π· = ( /π βπΊ) β β’ ((π β RingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π·π΅)π»πΆ) = ((π΄π»πΆ)π·(π΅π»πΆ))) | ||
Theorem | zerdivemp1x 36815* | In a unital ring a left invertible element is not a zero divisor. See also ringinvnzdiv 20113. (Contributed by Jeff Madsen, 18-Apr-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = (GIdβπΊ) & β’ π = ran πΊ & β’ π = (GIdβπ») β β’ ((π β RingOps β§ π΄ β π β§ βπ β π (ππ»π΄) = π) β (π΅ β π β ((π΄π»π΅) = π β π΅ = π))) | ||
Syntax | cdrng 36816 | Extend class notation with the class of all division rings. |
class DivRingOps | ||
Definition | df-drngo 36817* | 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 36818 | 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 36819 | 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 36820 | Obsolete as of 23-Jan-2020. Use mnd1id 18668 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 36821 | 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 36822 | 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 36823* | Properties that determine a group operation. (Contributed by Jeff Madsen, 1-Dec-2009.) (New usage is discouraged.) |
β’ (π β π β V) & β’ (π β πΊ:(π Γ π)βΆπ) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯πΊπ¦)πΊπ§) = (π₯πΊ(π¦πΊπ§))) & β’ (π β π β π) & β’ ((π β§ π₯ β π) β (ππΊπ₯) = π₯) & β’ ((π β§ π₯ β π) β βπ β π (ππΊπ₯) = π) β β’ (π β πΊ β GrpOp) | ||
Theorem | isdrngo1 36824 | The predicate "is a division ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = (GIdβπΊ) & β’ π = ran πΊ β β’ (π β DivRingOps β (π β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp)) | ||
Theorem | divrngcl 36825 | 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 36826* | 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 36827* | 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 | crnghom 36828 | Extend class notation with the class of ring homomorphisms. |
class RngHom | ||
Syntax | crngiso 36829 | Extend class notation with the class of ring isomorphisms. |
class RngIso | ||
Syntax | crisc 36830 | Extend class notation with the ring isomorphism relation. |
class βπ | ||
Definition | df-rngohom 36831* | Define the function which gives the set of ring homomorphisms between two given rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ RngHom = (π β RingOps, π β RingOps β¦ {π β (ran (1st βπ ) βm ran (1st βπ)) β£ ((πβ(GIdβ(2nd βπ))) = (GIdβ(2nd βπ )) β§ βπ₯ β ran (1st βπ)βπ¦ β ran (1st βπ)((πβ(π₯(1st βπ)π¦)) = ((πβπ₯)(1st βπ )(πβπ¦)) β§ (πβ(π₯(2nd βπ)π¦)) = ((πβπ₯)(2nd βπ )(πβπ¦))))}) | ||
Theorem | rngohomval 36832* | 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) β (π RngHom π) = {π β (π βm π) β£ ((πβπ) = π β§ βπ₯ β π βπ¦ β π ((πβ(π₯πΊπ¦)) = ((πβπ₯)π½(πβπ¦)) β§ (πβ(π₯π»π¦)) = ((πβπ₯)πΎ(πβπ¦))))}) | ||
Theorem | isrngohom 36833* | 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) β (πΉ β (π RngHom π) β (πΉ:πβΆπ β§ (πΉβπ) = π β§ βπ₯ β π βπ¦ β π ((πΉβ(π₯πΊπ¦)) = ((πΉβπ₯)π½(πΉβπ¦)) β§ (πΉβ(π₯π»π¦)) = ((πΉβπ₯)πΎ(πΉβπ¦)))))) | ||
Theorem | rngohomf 36834 | A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) & β’ π = ran π½ β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β πΉ:πβΆπ) | ||
Theorem | rngohomcl 36835 | Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) & β’ π = ran π½ β β’ (((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β§ π΄ β π) β (πΉβπ΄) β π) | ||
Theorem | rngohom1 36836 | A ring homomorphism preserves 1. (Contributed by Jeff Madsen, 24-Jun-2011.) |
β’ π» = (2nd βπ ) & β’ π = (GIdβπ») & β’ πΎ = (2nd βπ) & β’ π = (GIdβπΎ) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β (πΉβπ) = π) | ||
Theorem | rngohomadd 36837 | Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) β β’ (((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄πΊπ΅)) = ((πΉβπ΄)π½(πΉβπ΅))) | ||
Theorem | rngohommul 36838 | Ring homomorphisms preserve multiplication. (Contributed by Jeff Madsen, 3-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π» = (2nd βπ ) & β’ πΎ = (2nd βπ) β β’ (((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄π»π΅)) = ((πΉβπ΄)πΎ(πΉβπ΅))) | ||
Theorem | rngogrphom 36839 | A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π½ = (1st βπ) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β πΉ β (πΊ GrpOpHom π½)) | ||
Theorem | rngohom0 36840 | A ring homomorphism preserves 0. (Contributed by Jeff Madsen, 2-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = (GIdβπΊ) & β’ π½ = (1st βπ) & β’ π = (GIdβπ½) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β (πΉβπ) = π) | ||
Theorem | rngohomsub 36841 | Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π» = ( /π βπΊ) & β’ π½ = (1st βπ) & β’ πΎ = ( /π βπ½) β β’ (((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄π»π΅)) = ((πΉβπ΄)πΎ(πΉβπ΅))) | ||
Theorem | rngohomco 36842 | The composition of two ring homomorphisms is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ (((π β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π RngHom π) β§ πΊ β (π RngHom π))) β (πΊ β πΉ) β (π RngHom π)) | ||
Theorem | rngokerinj 36843 | A ring homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π½ = (1st βπ) & β’ π = ran π½ & β’ π = (GIdβπ½) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β (πΉ:πβ1-1βπ β (β‘πΉ β {π}) = {π})) | ||
Definition | df-rngoiso 36844* | Define the function which gives the set of ring isomorphisms between two given rings. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ RngIso = (π β RingOps, π β RingOps β¦ {π β (π RngHom π ) β£ π:ran (1st βπ)β1-1-ontoβran (1st βπ )}) | ||
Theorem | rngoisoval 36845* | The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) & β’ π = ran π½ β β’ ((π β RingOps β§ π β RingOps) β (π RngIso π) = {π β (π RngHom π) β£ π:πβ1-1-ontoβπ}) | ||
Theorem | isrngoiso 36846 | The predicate "is a ring isomorphism between π and π". (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) & β’ π = ran π½ β β’ ((π β RingOps β§ π β RingOps) β (πΉ β (π RngIso π) β (πΉ β (π RngHom π) β§ πΉ:πβ1-1-ontoβπ))) | ||
Theorem | rngoiso1o 36847 | A ring isomorphism is a bijection. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) & β’ π = ran π½ β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngIso π)) β πΉ:πβ1-1-ontoβπ) | ||
Theorem | rngoisohom 36848 | A ring isomorphism is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngIso π)) β πΉ β (π RngHom π)) | ||
Theorem | rngoisocnv 36849 | The inverse of a ring isomorphism is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngIso π)) β β‘πΉ β (π RngIso π )) | ||
Theorem | rngoisoco 36850 | The composition of two ring isomorphisms is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ (((π β RingOps β§ π β RingOps β§ π β RingOps) β§ (πΉ β (π RngIso π) β§ πΊ β (π RngIso π))) β (πΊ β πΉ) β (π RngIso π)) | ||
Definition | df-risc 36851* | Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ βπ = {β¨π, π β© β£ ((π β RingOps β§ π β RingOps) β§ βπ π β (π RngIso π ))} | ||
Theorem | isriscg 36852* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β π΄ β§ π β π΅) β (π βπ π β ((π β RingOps β§ π β RingOps) β§ βπ π β (π RngIso π)))) | ||
Theorem | isrisc 36853* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ π β V & β’ π β V β β’ (π βπ π β ((π β RingOps β§ π β RingOps) β§ βπ π β (π RngIso π))) | ||
Theorem | risc 36854* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β RingOps β§ π β RingOps) β (π βπ π β βπ π β (π RngIso π))) | ||
Theorem | risci 36855 | Determine that two rings are isomorphic. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngIso π)) β π βπ π) | ||
Theorem | riscer 36856 | Ring isomorphism is an equivalence relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Mario Carneiro, 12-Aug-2015.) |
β’ βπ Er dom βπ | ||
Syntax | ccm2 36857 | Extend class notation with a class that adds commutativity to various flavors of rings. |
class Com2 | ||
Definition | df-com2 36858* | A device to add commutativity to various sorts of rings. I use ran π because I suppose π has a neutral element and therefore is onto. (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.) |
β’ Com2 = {β¨π, ββ© β£ βπ β ran πβπ β ran π(πβπ) = (πβπ)} | ||
Syntax | cfld 36859 | Extend class notation with the class of all fields. |
class Fld | ||
Definition | df-fld 36860 | Definition of a field. A field is a commutative division ring. (Contributed by FL, 6-Sep-2009.) (Revised by Jeff Madsen, 10-Jun-2010.) (New usage is discouraged.) |
β’ Fld = (DivRingOps β© Com2) | ||
Syntax | ccring 36861 | Extend class notation with the class of commutative rings. |
class CRingOps | ||
Definition | df-crngo 36862 | Define the class of commutative rings. (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ CRingOps = (RingOps β© Com2) | ||
Theorem | iscom2 36863* | A device to add commutativity to various sorts of rings. (Contributed by FL, 6-Sep-2009.) (New usage is discouraged.) |
β’ ((πΊ β π΄ β§ π» β π΅) β (β¨πΊ, π»β© β Com2 β βπ β ran πΊβπ β ran πΊ(ππ»π) = (ππ»π))) | ||
Theorem | iscrngo 36864 | The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ (π β CRingOps β (π β RingOps β§ π β Com2)) | ||
Theorem | iscrngo2 36865* | The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β CRingOps β (π β RingOps β§ βπ₯ β π βπ¦ β π (π₯π»π¦) = (π¦π»π₯))) | ||
Theorem | iscringd 36866* | Conditions that determine a commutative ring. (Contributed by Jeff Madsen, 20-Jun-2011.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ (π β πΊ β AbelOp) & β’ (π β π = ran πΊ) & β’ (π β π»:(π Γ π)βΆπ) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯π»π¦)π»π§) = (π₯π»(π¦π»π§))) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯π»(π¦πΊπ§)) = ((π₯π»π¦)πΊ(π₯π»π§))) & β’ (π β π β π) & β’ ((π β§ π¦ β π) β (π¦π»π) = π¦) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯π»π¦) = (π¦π»π₯)) β β’ (π β β¨πΊ, π»β© β CRingOps) | ||
Theorem | flddivrng 36867 | A field is a division ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
β’ (πΎ β Fld β πΎ β DivRingOps) | ||
Theorem | crngorngo 36868 | A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (π β CRingOps β π β RingOps) | ||
Theorem | crngocom 36869 | The multiplication operation of a commutative ring is commutative. (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β CRingOps β§ π΄ β π β§ π΅ β π) β (π΄π»π΅) = (π΅π»π΄)) | ||
Theorem | crngm23 36870 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β CRingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π»π΅)π»πΆ) = ((π΄π»πΆ)π»π΅)) | ||
Theorem | crngm4 36871 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β CRingOps β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄π»π΅)π»(πΆπ»π·)) = ((π΄π»πΆ)π»(π΅π»π·))) | ||
Theorem | fldcrngo 36872 | A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ (πΎ β Fld β πΎ β CRingOps) | ||
Theorem | isfld2 36873 | The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (πΎ β Fld β (πΎ β DivRingOps β§ πΎ β CRingOps)) | ||
Theorem | crngohomfo 36874 | The image of a homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) & β’ π = ran π½ β β’ (((π β CRingOps β§ π β RingOps) β§ (πΉ β (π RngHom π) β§ πΉ:πβontoβπ)) β π β CRingOps) | ||
Syntax | cidl 36875 | Extend class notation with the class of ideals. |
class Idl | ||
Syntax | cpridl 36876 | Extend class notation with the class of prime ideals. |
class PrIdl | ||
Syntax | cmaxidl 36877 | Extend class notation with the class of maximal ideals. |
class MaxIdl | ||
Definition | df-idl 36878* | Define the class of (two-sided) ideals of a ring π . A subset of π is an ideal if it contains 0, is closed under addition, and is closed under multiplication on either side by any element of π . (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ Idl = (π β RingOps β¦ {π β π« ran (1st βπ) β£ ((GIdβ(1st βπ)) β π β§ βπ₯ β π (βπ¦ β π (π₯(1st βπ)π¦) β π β§ βπ§ β ran (1st βπ)((π§(2nd βπ)π₯) β π β§ (π₯(2nd βπ)π§) β π)))}) | ||
Definition | df-pridl 36879* | Define the class of prime ideals of a ring π . A proper ideal πΌ of π is prime if whenever π΄π΅ β πΌ for ideals π΄ and π΅, either π΄ β πΌ or π΅ β πΌ. The more familiar definition using elements rather than ideals is equivalent provided π is commutative; see ispridl2 36906 and ispridlc 36938. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ PrIdl = (π β RingOps β¦ {π β (Idlβπ) β£ (π β ran (1st βπ) β§ βπ β (Idlβπ)βπ β (Idlβπ)(βπ₯ β π βπ¦ β π (π₯(2nd βπ)π¦) β π β (π β π β¨ π β π)))}) | ||
Definition | df-maxidl 36880* | Define the class of maximal ideals of a ring π . A proper ideal is called maximal if it is maximal with respect to inclusion among proper ideals. (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ MaxIdl = (π β RingOps β¦ {π β (Idlβπ) β£ (π β ran (1st βπ) β§ βπ β (Idlβπ)(π β π β (π = π β¨ π = ran (1st βπ))))}) | ||
Theorem | idlval 36881* | The class of ideals of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β RingOps β (Idlβπ ) = {π β π« π β£ (π β π β§ βπ₯ β π (βπ¦ β π (π₯πΊπ¦) β π β§ βπ§ β π ((π§π»π₯) β π β§ (π₯π»π§) β π)))}) | ||
Theorem | isidl 36882* | The predicate "is an ideal of the ring π ". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β RingOps β (πΌ β (Idlβπ ) β (πΌ β π β§ π β πΌ β§ βπ₯ β πΌ (βπ¦ β πΌ (π₯πΊπ¦) β πΌ β§ βπ§ β π ((π§π»π₯) β πΌ β§ (π₯π»π§) β πΌ))))) | ||
Theorem | isidlc 36883* | The predicate "is an ideal of the commutative ring π ". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β CRingOps β (πΌ β (Idlβπ ) β (πΌ β π β§ π β πΌ β§ βπ₯ β πΌ (βπ¦ β πΌ (π₯πΊπ¦) β πΌ β§ βπ§ β π (π§π»π₯) β πΌ)))) | ||
Theorem | idlss 36884 | An ideal of π is a subset of π . (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ πΌ β (Idlβπ )) β πΌ β π) | ||
Theorem | idlcl 36885 | An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ π΄ β πΌ) β π΄ β π) | ||
Theorem | idl0cl 36886 | An ideal contains 0. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ πΌ β (Idlβπ )) β π β πΌ) | ||
Theorem | idladdcl 36887 | An ideal is closed under addition. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ (π΄ β πΌ β§ π΅ β πΌ)) β (π΄πΊπ΅) β πΌ) | ||
Theorem | idllmulcl 36888 | An ideal is closed under multiplication on the left. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ (π΄ β πΌ β§ π΅ β π)) β (π΅π»π΄) β πΌ) | ||
Theorem | idlrmulcl 36889 | An ideal is closed under multiplication on the right. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ (π΄ β πΌ β§ π΅ β π)) β (π΄π»π΅) β πΌ) | ||
Theorem | idlnegcl 36890 | An ideal is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = (invβπΊ) β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ π΄ β πΌ) β (πβπ΄) β πΌ) | ||
Theorem | idlsubcl 36891 | An ideal is closed under subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π· = ( /π βπΊ) β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ (π΄ β πΌ β§ π΅ β πΌ)) β (π΄π·π΅) β πΌ) | ||
Theorem | rngoidl 36892 | A ring π is an π ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (π β RingOps β π β (Idlβπ )) | ||
Theorem | 0idl 36893 | The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = (GIdβπΊ) β β’ (π β RingOps β {π} β (Idlβπ )) | ||
Theorem | 1idl 36894 | Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπ») β β’ ((π β RingOps β§ πΌ β (Idlβπ )) β (π β πΌ β πΌ = π)) | ||
Theorem | 0rngo 36895 | In a ring, 0 = 1 iff the ring contains only 0. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π = (GIdβπ») β β’ (π β RingOps β (π = π β π = {π})) | ||
Theorem | divrngidl 36896 | The only ideals in a division ring are the zero ideal and the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β DivRingOps β (Idlβπ ) = {{π}, π}) | ||
Theorem | intidl 36897 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ ((π β RingOps β§ πΆ β β β§ πΆ β (Idlβπ )) β β© πΆ β (Idlβπ )) | ||
Theorem | inidl 36898 | The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β RingOps β§ πΌ β (Idlβπ ) β§ π½ β (Idlβπ )) β (πΌ β© π½) β (Idlβπ )) | ||
Theorem | unichnidl 36899* | The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ ((π β RingOps β§ (πΆ β β β§ πΆ β (Idlβπ ) β§ βπ β πΆ βπ β πΆ (π β π β¨ π β π))) β βͺ πΆ β (Idlβπ )) | ||
Theorem | keridl 36900 | The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.) |
β’ πΊ = (1st βπ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β (β‘πΉ β {π}) β (Idlβπ )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |