![]() |
Metamath
Proof Explorer Theorem List (p. 375 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | ccring 37401 | Extend class notation with the class of commutative rings. |
class CRingOps | ||
Definition | df-crngo 37402 | Define the class of commutative rings. (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ CRingOps = (RingOps β© Com2) | ||
Theorem | iscom2 37403* | 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 37404 | The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ (π β CRingOps β (π β RingOps β§ π β Com2)) | ||
Theorem | iscrngo2 37405* | The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β CRingOps β (π β RingOps β§ βπ₯ β π βπ¦ β π (π₯π»π¦) = (π¦π»π₯))) | ||
Theorem | iscringd 37406* | 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 37407 | 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 37408 | A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (π β CRingOps β π β RingOps) | ||
Theorem | crngocom 37409 | The multiplication operation of a commutative ring is commutative. (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β CRingOps β§ π΄ β π β§ π΅ β π) β (π΄π»π΅) = (π΅π»π΄)) | ||
Theorem | crngm23 37410 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β CRingOps β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄π»π΅)π»πΆ) = ((π΄π»πΆ)π»π΅)) | ||
Theorem | crngm4 37411 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β CRingOps β§ (π΄ β π β§ π΅ β π) β§ (πΆ β π β§ π· β π)) β ((π΄π»π΅)π»(πΆπ»π·)) = ((π΄π»πΆ)π»(π΅π»π·))) | ||
Theorem | fldcrngo 37412 | A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010.) |
β’ (πΎ β Fld β πΎ β CRingOps) | ||
Theorem | isfld2 37413 | The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (πΎ β Fld β (πΎ β DivRingOps β§ πΎ β CRingOps)) | ||
Theorem | crngohomfo 37414 | The image of a homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ & β’ π½ = (1st βπ) & β’ π = ran π½ β β’ (((π β CRingOps β§ π β RingOps) β§ (πΉ β (π RingOpsHom π) β§ πΉ:πβontoβπ)) β π β CRingOps) | ||
Syntax | cidl 37415 | Extend class notation with the class of ideals. |
class Idl | ||
Syntax | cpridl 37416 | Extend class notation with the class of prime ideals. |
class PrIdl | ||
Syntax | cmaxidl 37417 | Extend class notation with the class of maximal ideals. |
class MaxIdl | ||
Definition | df-idl 37418* | 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 37419* | 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 37446 and ispridlc 37478. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ PrIdl = (π β RingOps β¦ {π β (Idlβπ) β£ (π β ran (1st βπ) β§ βπ β (Idlβπ)βπ β (Idlβπ)(βπ₯ β π βπ¦ β π (π₯(2nd βπ)π¦) β π β (π β π β¨ π β π)))}) | ||
Definition | df-maxidl 37420* | 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 37421* | The class of ideals of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β RingOps β (Idlβπ ) = {π β π« π β£ (π β π β§ βπ₯ β π (βπ¦ β π (π₯πΊπ¦) β π β§ βπ§ β π ((π§π»π₯) β π β§ (π₯π»π§) β π)))}) | ||
Theorem | isidl 37422* | The predicate "is an ideal of the ring π ". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β RingOps β (πΌ β (Idlβπ ) β (πΌ β π β§ π β πΌ β§ βπ₯ β πΌ (βπ¦ β πΌ (π₯πΊπ¦) β πΌ β§ βπ§ β π ((π§π»π₯) β πΌ β§ (π₯π»π§) β πΌ))))) | ||
Theorem | isidlc 37423* | The predicate "is an ideal of the commutative ring π ". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (π β CRingOps β (πΌ β (Idlβπ ) β (πΌ β π β§ π β πΌ β§ βπ₯ β πΌ (βπ¦ β πΌ (π₯πΊπ¦) β πΌ β§ βπ§ β π (π§π»π₯) β πΌ)))) | ||
Theorem | idlss 37424 | An ideal of π is a subset of π . (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ πΌ β (Idlβπ )) β πΌ β π) | ||
Theorem | idlcl 37425 | An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ π΄ β πΌ) β π΄ β π) | ||
Theorem | idl0cl 37426 | An ideal contains 0. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ πΌ β (Idlβπ )) β π β πΌ) | ||
Theorem | idladdcl 37427 | An ideal is closed under addition. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ (π΄ β πΌ β§ π΅ β πΌ)) β (π΄πΊπ΅) β πΌ) | ||
Theorem | idllmulcl 37428 | An ideal is closed under multiplication on the left. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ (π΄ β πΌ β§ π΅ β π)) β (π΅π»π΄) β πΌ) | ||
Theorem | idlrmulcl 37429 | An ideal is closed under multiplication on the right. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ (π΄ β πΌ β§ π΅ β π)) β (π΄π»π΅) β πΌ) | ||
Theorem | idlnegcl 37430 | An ideal is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = (invβπΊ) β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ π΄ β πΌ) β (πβπ΄) β πΌ) | ||
Theorem | idlsubcl 37431 | An ideal is closed under subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π· = ( /π βπΊ) β β’ (((π β RingOps β§ πΌ β (Idlβπ )) β§ (π΄ β πΌ β§ π΅ β πΌ)) β (π΄π·π΅) β πΌ) | ||
Theorem | rngoidl 37432 | A ring π is an π ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (π β RingOps β π β (Idlβπ )) | ||
Theorem | 0idl 37433 | The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = (GIdβπΊ) β β’ (π β RingOps β {π} β (Idlβπ )) | ||
Theorem | 1idl 37434 | Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπ») β β’ ((π β RingOps β§ πΌ β (Idlβπ )) β (π β πΌ β πΌ = π)) | ||
Theorem | 0rngo 37435 | 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 37436 | 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 37437 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ ((π β RingOps β§ πΆ β β β§ πΆ β (Idlβπ )) β β© πΆ β (Idlβπ )) | ||
Theorem | inidl 37438 | The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β RingOps β§ πΌ β (Idlβπ ) β§ π½ β (Idlβπ )) β (πΌ β© π½) β (Idlβπ )) | ||
Theorem | unichnidl 37439* | The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ ((π β RingOps β§ (πΆ β β β§ πΆ β (Idlβπ ) β§ βπ β πΆ βπ β πΆ (π β π β¨ π β π))) β βͺ πΆ β (Idlβπ )) | ||
Theorem | keridl 37440 | The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.) |
β’ πΊ = (1st βπ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RingOpsHom π)) β (β‘πΉ β {π}) β (Idlβπ )) | ||
Theorem | pridlval 37441* | 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 37442* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β RingOps β (π β (PrIdlβπ ) β (π β (Idlβπ ) β§ π β π β§ βπ β (Idlβπ )βπ β (Idlβπ )(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π))))) | ||
Theorem | pridlidl 37443 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ ((π β RingOps β§ π β (PrIdlβπ )) β π β (Idlβπ )) | ||
Theorem | pridlnr 37444 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π β (PrIdlβπ )) β π β π) | ||
Theorem | pridl 37445* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ π» = (2nd βπ ) β β’ (((π β RingOps β§ π β (PrIdlβπ )) β§ (π΄ β (Idlβπ ) β§ π΅ β (Idlβπ ) β§ βπ₯ β π΄ βπ¦ β π΅ (π₯π»π¦) β π)) β (π΄ β π β¨ π΅ β π)) | ||
Theorem | ispridl2 37446* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 37478 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π β (Idlβπ ) β§ π β π β§ βπ β π βπ β π ((ππ»π) β π β (π β π β¨ π β π)))) β π β (PrIdlβπ )) | ||
Theorem | maxidlval 37447* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (π β RingOps β (MaxIdlβπ ) = {π β (Idlβπ ) β£ (π β π β§ βπ β (Idlβπ )(π β π β (π = π β¨ π = π)))}) | ||
Theorem | ismaxidl 37448* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (π β RingOps β (π β (MaxIdlβπ ) β (π β (Idlβπ ) β§ π β π β§ βπ β (Idlβπ )(π β π β (π = π β¨ π = π))))) | ||
Theorem | maxidlidl 37449 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ ((π β RingOps β§ π β (MaxIdlβπ )) β π β (Idlβπ )) | ||
Theorem | maxidlnr 37450 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π β (MaxIdlβπ )) β π β π) | ||
Theorem | maxidlmax 37451 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (((π β RingOps β§ π β (MaxIdlβπ )) β§ (πΌ β (Idlβπ ) β§ π β πΌ)) β (πΌ = π β¨ πΌ = π)) | ||
Theorem | maxidln1 37452 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) |
β’ π» = (2nd βπ ) & β’ π = (GIdβπ») β β’ ((π β RingOps β§ π β (MaxIdlβπ )) β Β¬ π β π) | ||
Theorem | maxidln0 37453 | 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 37454 | Extend class notation with the class of prime rings. |
class PrRing | ||
Syntax | cdmn 37455 | Extend class notation with the class of domains. |
class Dmn | ||
Definition | df-prrngo 37456 | 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 37457 | 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 37458 | The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = (GIdβπΊ) β β’ (π β PrRing β (π β RingOps β§ {π} β (PrIdlβπ ))) | ||
Theorem | prrngorngo 37459 | A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (π β PrRing β π β RingOps) | ||
Theorem | smprngopr 37460 | 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 37461 | A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ (π β DivRingOps β π β PrRing) | ||
Theorem | isdmn 37462 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (π β Dmn β (π β PrRing β§ π β Com2)) | ||
Theorem | isdmn2 37463 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (π β Dmn β (π β PrRing β§ π β CRingOps)) | ||
Theorem | dmncrng 37464 | A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ (π β Dmn β π β CRingOps) | ||
Theorem | dmnrngo 37465 | A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ (π β Dmn β π β RingOps) | ||
Theorem | flddmn 37466 | A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (πΎ β Fld β πΎ β Dmn) | ||
Syntax | cigen 37467 | Extend class notation with the ideal generation function. |
class IdlGen | ||
Definition | df-igen 37468* | Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ IdlGen = (π β RingOps, π β π« ran (1st βπ) β¦ β© {π β (Idlβπ) β£ π β π}) | ||
Theorem | igenval 37469* | The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof shortened by Mario Carneiro, 20-Dec-2013.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π β π) β (π IdlGen π) = β© {π β (Idlβπ ) β£ π β π}) | ||
Theorem | igenss 37470 | A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π β π) β π β (π IdlGen π)) | ||
Theorem | igenidl 37471 | The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π β π) β (π IdlGen π) β (Idlβπ )) | ||
Theorem | igenmin 37472 | The ideal generated by a set is the minimal ideal containing that set. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ ((π β RingOps β§ πΌ β (Idlβπ ) β§ π β πΌ) β (π IdlGen π) β πΌ) | ||
Theorem | igenidl2 37473 | The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ ((π β RingOps β§ πΌ β (Idlβπ )) β (π IdlGen πΌ) = πΌ) | ||
Theorem | igenval2 37474* | The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π β π) β ((π IdlGen π) = πΌ β (πΌ β (Idlβπ ) β§ π β πΌ β§ βπ β (Idlβπ )(π β π β πΌ β π)))) | ||
Theorem | prnc 37475* | A principal ideal (an ideal generated by one element) in a commutative ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β CRingOps β§ π΄ β π) β (π IdlGen {π΄}) = {π₯ β π β£ βπ¦ β π π₯ = (π¦π»π΄)}) | ||
Theorem | isfldidl 37476 | Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπΎ) & β’ π» = (2nd βπΎ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π = (GIdβπ») β β’ (πΎ β Fld β (πΎ β CRingOps β§ π β π β§ (IdlβπΎ) = {{π}, π})) | ||
Theorem | isfldidl2 37477 | Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ πΊ = (1st βπΎ) & β’ π» = (2nd βπΎ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (πΎ β Fld β (πΎ β CRingOps β§ π β {π} β§ (IdlβπΎ) = {{π}, π})) | ||
Theorem | ispridlc 37478* | The predicate "is a prime ideal". Alternate definition for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β CRingOps β (π β (PrIdlβπ ) β (π β (Idlβπ ) β§ π β π β§ βπ β π βπ β π ((ππ»π) β π β (π β π β¨ π β π))))) | ||
Theorem | pridlc 37479 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (((π β CRingOps β§ π β (PrIdlβπ )) β§ (π΄ β π β§ π΅ β π β§ (π΄π»π΅) β π)) β (π΄ β π β¨ π΅ β π)) | ||
Theorem | pridlc2 37480 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (((π β CRingOps β§ π β (PrIdlβπ )) β§ (π΄ β (π β π) β§ π΅ β π β§ (π΄π»π΅) β π)) β π΅ β π) | ||
Theorem | pridlc3 37481 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (((π β CRingOps β§ π β (PrIdlβπ )) β§ (π΄ β (π β π) β§ π΅ β (π β π))) β (π΄π»π΅) β (π β π)) | ||
Theorem | isdmn3 37482* | The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π = (GIdβπ») β β’ (π β Dmn β (π β CRingOps β§ π β π β§ βπ β π βπ β π ((ππ»π) = π β (π = π β¨ π = π)))) | ||
Theorem | dmnnzd 37483 | A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ ((π β Dmn β§ (π΄ β π β§ π΅ β π β§ (π΄π»π΅) = π)) β (π΄ = π β¨ π΅ = π)) | ||
Theorem | dmncan1 37484 | Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (((π β Dmn β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β§ π΄ β π) β ((π΄π»π΅) = (π΄π»πΆ) β π΅ = πΆ)) | ||
Theorem | dmncan2 37485 | Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (((π β Dmn β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β§ πΆ β π) β ((π΄π»πΆ) = (π΅π»πΆ) β π΄ = π΅)) | ||
The results in this section are mostly meant for being used by automatic proof building programs. As a result, they might appear less useful or meaningful than others to human beings. | ||
Theorem | efald2 37486 | A proof by contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (Β¬ π β β₯) β β’ π | ||
Theorem | notbinot1 37487 | Simplification rule of negation across a biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (Β¬ (Β¬ π β π) β (π β π)) | ||
Theorem | bicontr 37488 | Biconditional of its own negation is a contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ ((Β¬ π β π) β β₯) | ||
Theorem | impor 37489 | An equivalent formula for implying a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ ((π β (π β¨ π)) β ((Β¬ π β¨ π) β¨ π)) | ||
Theorem | orfa 37490 | The falsum β₯ can be removed from a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ ((π β¨ β₯) β π) | ||
Theorem | notbinot2 37491 | Commutation rule between negation and biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (Β¬ (π β π) β (Β¬ π β π)) | ||
Theorem | biimpor 37492 | A rewriting rule for biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (((π β π) β π) β ((Β¬ π β π) β¨ π)) | ||
Theorem | orfa1 37493 | Add a contradicting disjunct to an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (π β π) β β’ ((π β¨ β₯) β π) | ||
Theorem | orfa2 37494 | Remove a contradicting disjunct from an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (π β β₯) β β’ ((π β¨ π) β π) | ||
Theorem | bifald 37495 | Infer the equivalence to a contradiction from a negation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (π β Β¬ π) β β’ (π β (π β β₯)) | ||
Theorem | orsild 37496 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (π β Β¬ (π β¨ π)) β β’ (π β Β¬ π) | ||
Theorem | orsird 37497 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (π β Β¬ (π β¨ π)) β β’ (π β Β¬ π) | ||
Theorem | cnf1dd 37498 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
β’ (π β (π β Β¬ π)) & β’ (π β (π β (π β¨ π))) β β’ (π β (π β π)) | ||
Theorem | cnf2dd 37499 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
β’ (π β (π β Β¬ π)) & β’ (π β (π β (π β¨ π))) β β’ (π β (π β π)) | ||
Theorem | cnfn1dd 37500 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
β’ (π β (π β π)) & β’ (π β (π β (Β¬ π β¨ π))) β β’ (π β (π β π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |