Home | Metamath
Proof Explorer Theorem List (p. 364 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-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isdrngo1 36301 | The predicate "is a division ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = (GIdβπΊ) & β’ π = ran πΊ β β’ (π β DivRingOps β (π β RingOps β§ (π» βΎ ((π β {π}) Γ (π β {π}))) β GrpOp)) | ||
Theorem | divrngcl 36302 | 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 36303* | 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 36304* | 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 36305 | Extend class notation with the class of ring homomorphisms. |
class RngHom | ||
Syntax | crngiso 36306 | Extend class notation with the class of ring isomorphisms. |
class RngIso | ||
Syntax | crisc 36307 | Extend class notation with the ring isomorphism relation. |
class βπ | ||
Definition | df-rngohom 36308* | 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 36309* | 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 36310* | 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 36311 | A ring homomorphism is a function. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) & β’ π = ran π½ β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β πΉ:πβΆπ) | ||
Theorem | rngohomcl 36312 | Closure law for a ring homomorphism. (Contributed by Jeff Madsen, 3-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) & β’ π = ran π½ β β’ (((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β§ π΄ β π) β (πΉβπ΄) β π) | ||
Theorem | rngohom1 36313 | A ring homomorphism preserves 1. (Contributed by Jeff Madsen, 24-Jun-2011.) |
β’ π» = (2nd βπ ) & β’ π = (GIdβπ») & β’ πΎ = (2nd βπ) & β’ π = (GIdβπΎ) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β (πΉβπ) = π) | ||
Theorem | rngohomadd 36314 | Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) β β’ (((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄πΊπ΅)) = ((πΉβπ΄)π½(πΉβπ΅))) | ||
Theorem | rngohommul 36315 | Ring homomorphisms preserve multiplication. (Contributed by Jeff Madsen, 3-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π» = (2nd βπ ) & β’ πΎ = (2nd βπ) β β’ (((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄π»π΅)) = ((πΉβπ΄)πΎ(πΉβπ΅))) | ||
Theorem | rngogrphom 36316 | A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π½ = (1st βπ) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β πΉ β (πΊ GrpOpHom π½)) | ||
Theorem | rngohom0 36317 | A ring homomorphism preserves 0. (Contributed by Jeff Madsen, 2-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = (GIdβπΊ) & β’ π½ = (1st βπ) & β’ π = (GIdβπ½) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β (πΉβπ) = π) | ||
Theorem | rngohomsub 36318 | Ring homomorphisms preserve subtraction. (Contributed by Jeff Madsen, 15-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π» = ( /π βπΊ) & β’ π½ = (1st βπ) & β’ πΎ = ( /π βπ½) β β’ (((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β§ (π΄ β π β§ π΅ β π)) β (πΉβ(π΄π»π΅)) = ((πΉβπ΄)πΎ(πΉβπ΅))) | ||
Theorem | rngohomco 36319 | 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 36320 | 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 36321* | 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 36322* | 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 36323 | 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 36324 | 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 36325 | A ring isomorphism is a ring homomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngIso π)) β πΉ β (π RngHom π)) | ||
Theorem | rngoisocnv 36326 | The inverse of a ring isomorphism is a ring isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngIso π)) β β‘πΉ β (π RngIso π )) | ||
Theorem | rngoisoco 36327 | 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 36328* | Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ βπ = {β¨π, π β© β£ ((π β RingOps β§ π β RingOps) β§ βπ π β (π RngIso π ))} | ||
Theorem | isriscg 36329* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β π΄ β§ π β π΅) β (π βπ π β ((π β RingOps β§ π β RingOps) β§ βπ π β (π RngIso π)))) | ||
Theorem | isrisc 36330* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ π β V & β’ π β V β β’ (π βπ π β ((π β RingOps β§ π β RingOps) β§ βπ π β (π RngIso π))) | ||
Theorem | risc 36331* | The ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β RingOps β§ π β RingOps) β (π βπ π β βπ π β (π RngIso π))) | ||
Theorem | risci 36332 | Determine that two rings are isomorphic. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngIso π)) β π βπ π) | ||
Theorem | riscer 36333 | Ring isomorphism is an equivalence relation. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Mario Carneiro, 12-Aug-2015.) |
β’ βπ Er dom βπ | ||
Syntax | ccm2 36334 | Extend class notation with a class that adds commutativity to various flavors of rings. |
class Com2 | ||
Definition | df-com2 36335* | 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 36336 | Extend class notation with the class of all fields. |
class Fld | ||
Definition | df-fld 36337 | 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 36338 | Extend class notation with the class of commutative rings. |
class CRingOps | ||
Definition | df-crngo 36339 | Define the class of commutative rings. (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ CRingOps = (RingOps β© Com2) | ||
Theorem | iscom2 36340* | 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 36341 | The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ (π β CRingOps β (π β RingOps β§ π β Com2)) | ||
Theorem | iscrngo2 36342* | The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β CRingOps β (π β RingOps β§ βπ₯ β π βπ¦ β π (π₯π»π¦) = (π¦π»π₯))) | ||
Theorem | iscringd 36343* | 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 36344 | 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 36345 | A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (π β CRingOps β π β RingOps) | ||
Theorem | crngocom 36346 | The multiplication operation of a commutative ring is commutative. (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β CRingOps β§ π΄ β π β§ π΅ β π) β (π΄π»π΅) = (π΅π»π΄)) | ||
Theorem | crngm23 36347 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β CRingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π»π΅)π»πΆ) = ((π΄π»πΆ)π»π΅)) | ||
Theorem | crngm4 36348 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β CRingOps β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄π»π΅)π»(πΆπ»π·)) = ((π΄π»πΆ)π»(π΅π»π·))) | ||
Theorem | fldcrngo 36349 | A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ (πΎ β Fld β πΎ β CRingOps) | ||
Theorem | isfld2 36350 | The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (πΎ β Fld β (πΎ β DivRingOps β§ πΎ β CRingOps)) | ||
Theorem | crngohomfo 36351 | 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 36352 | Extend class notation with the class of ideals. |
class Idl | ||
Syntax | cpridl 36353 | Extend class notation with the class of prime ideals. |
class PrIdl | ||
Syntax | cmaxidl 36354 | Extend class notation with the class of maximal ideals. |
class MaxIdl | ||
Definition | df-idl 36355* | 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 36356* | 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 36383 and ispridlc 36415. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ PrIdl = (π β RingOps β¦ {π β (Idlβπ) β£ (π β ran (1st βπ) β§ βπ β (Idlβπ)βπ β (Idlβπ)(βπ₯ β π βπ¦ β π (π₯(2nd βπ)π¦) β π β (π β π β¨ π β π)))}) | ||
Definition | df-maxidl 36357* | 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 36358* | The class of ideals of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β RingOps β (Idlβπ ) = {π β π« π β£ (π β π β§ βπ₯ β π (βπ¦ β π (π₯πΊπ¦) β π β§ βπ§ β π ((π§π»π₯) β π β§ (π₯π»π§) β π)))}) | ||
Theorem | isidl 36359* | The predicate "is an ideal of the ring π ". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β RingOps β (πΌ β (Idlβπ ) β (πΌ β π β§ π β πΌ β§ βπ₯ β πΌ (βπ¦ β πΌ (π₯πΊπ¦) β πΌ β§ βπ§ β π ((π§π»π₯) β πΌ β§ (π₯π»π§) β πΌ))))) | ||
Theorem | isidlc 36360* | The predicate "is an ideal of the commutative ring π ". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β CRingOps β (πΌ β (Idlβπ ) β (πΌ β π β§ π β πΌ β§ βπ₯ β πΌ (βπ¦ β πΌ (π₯πΊπ¦) β πΌ β§ βπ§ β π (π§π»π₯) β πΌ)))) | ||
Theorem | idlss 36361 | An ideal of π is a subset of π . (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ πΌ β (Idlβπ )) β πΌ β π) | ||
Theorem | idlcl 36362 | An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ π΄ β πΌ) β π΄ β π) | ||
Theorem | idl0cl 36363 | An ideal contains 0. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ πΌ β (Idlβπ )) β π β πΌ) | ||
Theorem | idladdcl 36364 | An ideal is closed under addition. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ (π΄ β πΌ β§ π΅ β πΌ)) β (π΄πΊπ΅) β πΌ) | ||
Theorem | idllmulcl 36365 | An ideal is closed under multiplication on the left. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ (π΄ β πΌ β§ π΅ β π)) β (π΅π»π΄) β πΌ) | ||
Theorem | idlrmulcl 36366 | An ideal is closed under multiplication on the right. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ (π΄ β πΌ β§ π΅ β π)) β (π΄π»π΅) β πΌ) | ||
Theorem | idlnegcl 36367 | An ideal is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = (invβπΊ) β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ π΄ β πΌ) β (πβπ΄) β πΌ) | ||
Theorem | idlsubcl 36368 | An ideal is closed under subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π· = ( /π βπΊ) β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ (π΄ β πΌ β§ π΅ β πΌ)) β (π΄π·π΅) β πΌ) | ||
Theorem | rngoidl 36369 | A ring π is an π ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (π β RingOps β π β (Idlβπ )) | ||
Theorem | 0idl 36370 | The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = (GIdβπΊ) β β’ (π β RingOps β {π} β (Idlβπ )) | ||
Theorem | 1idl 36371 | Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπ») β β’ ((π β RingOps β§ πΌ β (Idlβπ )) β (π β πΌ β πΌ = π)) | ||
Theorem | 0rngo 36372 | 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 36373 | 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 36374 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ ((π β RingOps β§ πΆ β β β§ πΆ β (Idlβπ )) β β© πΆ β (Idlβπ )) | ||
Theorem | inidl 36375 | The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β RingOps β§ πΌ β (Idlβπ ) β§ π½ β (Idlβπ )) β (πΌ β© π½) β (Idlβπ )) | ||
Theorem | unichnidl 36376* | The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ ((π β RingOps β§ (πΆ β β β§ πΆ β (Idlβπ ) β§ βπ β πΆ βπ β πΆ (π β π β¨ π β π))) β βͺ πΆ β (Idlβπ )) | ||
Theorem | keridl 36377 | The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.) |
β’ πΊ = (1st βπ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RngHom π)) β (β‘πΉ β {π}) β (Idlβπ )) | ||
Theorem | pridlval 36378* | The class of prime ideals of a ring π . (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β RingOps β (PrIdlβπ ) = {π β (Idlβπ ) β£ (π β π β§ βπ β (Idlβπ )βπ β (Idlβπ )(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π)))}) | ||
Theorem | ispridl 36379* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β RingOps β (π β (PrIdlβπ ) β (π β (Idlβπ ) β§ π β π β§ βπ β (Idlβπ )βπ β (Idlβπ )(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π))))) | ||
Theorem | pridlidl 36380 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ ((π β RingOps β§ π β (PrIdlβπ )) β π β (Idlβπ )) | ||
Theorem | pridlnr 36381 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π β (PrIdlβπ )) β π β π) | ||
Theorem | pridl 36382* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ π» = (2nd βπ ) β β’ (((π β RingOps β§ π β (PrIdlβπ )) β§ (π΄ β (Idlβπ ) β§ π΅ β (Idlβπ ) β§ βπ₯ β π΄ βπ¦ β π΅ (π₯π»π¦) β π)) β (π΄ β π β¨ π΅ β π)) | ||
Theorem | ispridl2 36383* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 36415 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π β (Idlβπ ) β§ π β π β§ βπ β π βπ β π ((ππ»π) β π β (π β π β¨ π β π)))) β π β (PrIdlβπ )) | ||
Theorem | maxidlval 36384* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (π β RingOps β (MaxIdlβπ ) = {π β (Idlβπ ) β£ (π β π β§ βπ β (Idlβπ )(π β π β (π = π β¨ π = π)))}) | ||
Theorem | ismaxidl 36385* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (π β RingOps β (π β (MaxIdlβπ ) β (π β (Idlβπ ) β§ π β π β§ βπ β (Idlβπ )(π β π β (π = π β¨ π = π))))) | ||
Theorem | maxidlidl 36386 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ ((π β RingOps β§ π β (MaxIdlβπ )) β π β (Idlβπ )) | ||
Theorem | maxidlnr 36387 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π β (MaxIdlβπ )) β π β π) | ||
Theorem | maxidlmax 36388 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (((π β RingOps β§ π β (MaxIdlβπ )) β§ (πΌ β (Idlβπ ) β§ π β πΌ)) β (πΌ = π β¨ πΌ = π)) | ||
Theorem | maxidln1 36389 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) |
β’ π» = (2nd βπ ) & β’ π = (GIdβπ») β β’ ((π β RingOps β§ π β (MaxIdlβπ )) β Β¬ π β π) | ||
Theorem | maxidln0 36390 | A ring with a maximal ideal is not the zero ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = (GIdβπΊ) & β’ π = (GIdβπ») β β’ ((π β RingOps β§ π β (MaxIdlβπ )) β π β π) | ||
Syntax | cprrng 36391 | Extend class notation with the class of prime rings. |
class PrRing | ||
Syntax | cdmn 36392 | Extend class notation with the class of domains. |
class Dmn | ||
Definition | df-prrngo 36393 | Define the class of prime rings. A ring is prime if the zero ideal is a prime ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ PrRing = {π β RingOps β£ {(GIdβ(1st βπ))} β (PrIdlβπ)} | ||
Definition | df-dmn 36394 | Define the class of (integral) domains. A domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ Dmn = (PrRing β© Com2) | ||
Theorem | isprrngo 36395 | The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = (GIdβπΊ) β β’ (π β PrRing β (π β RingOps β§ {π} β (PrIdlβπ ))) | ||
Theorem | prrngorngo 36396 | A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (π β PrRing β π β RingOps) | ||
Theorem | smprngopr 36397 | A simple ring (one whose only ideals are 0 and π ) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π = (GIdβπ») β β’ ((π β RingOps β§ π β π β§ (Idlβπ ) = {{π}, π}) β π β PrRing) | ||
Theorem | divrngpr 36398 | A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ (π β DivRingOps β π β PrRing) | ||
Theorem | isdmn 36399 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (π β Dmn β (π β PrRing β§ π β Com2)) | ||
Theorem | isdmn2 36400 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (π β Dmn β (π β PrRing β§ π β CRingOps)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |