Home | Metamath
Proof Explorer Theorem List (p. 339 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | crngm23 33801 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
CRingOps | ||
Theorem | crngm4 33802 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
CRingOps | ||
Theorem | fldcrng 33803 | A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010.) |
CRingOps | ||
Theorem | isfld2 33804 | The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010.) |
CRingOps | ||
Theorem | crngohomfo 33805 | The image of a homomorphism from a commutative ring is commutative. (Contributed by Jeff Madsen, 4-Jan-2011.) |
CRingOps CRingOps | ||
Syntax | cidl 33806 | Extend class notation with the class of ideals. |
Syntax | cpridl 33807 | Extend class notation with the class of prime ideals. |
Syntax | cmaxidl 33808 | Extend class notation with the class of maximal ideals. |
Definition | df-idl 33809* | Define the class of (two-sided) ideals of a ring . A subset of is an ideal if it contains , is closed under addition, and is closed under multiplication on either side by any element of . (Contributed by Jeff Madsen, 10-Jun-2010.) |
GId | ||
Definition | df-pridl 33810* | 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 33837 and ispridlc 33869. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Definition | df-maxidl 33811* | 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.) |
Theorem | idlval 33812* | The class of ideals of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
GId | ||
Theorem | isidl 33813* | The predicate "is an ideal of the ring ." (Contributed by Jeff Madsen, 10-Jun-2010.) |
GId | ||
Theorem | isidlc 33814* | The predicate "is an ideal of the commutative ring ." (Contributed by Jeff Madsen, 10-Jun-2010.) |
GId CRingOps | ||
Theorem | idlss 33815 | An ideal of is a subset of . (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | idlcl 33816 | An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
Theorem | idl0cl 33817 | An ideal contains . (Contributed by Jeff Madsen, 10-Jun-2010.) |
GId | ||
Theorem | idladdcl 33818 | An ideal is closed under addition. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | idllmulcl 33819 | An ideal is closed under multiplication on the left. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | idlrmulcl 33820 | An ideal is closed under multiplication on the right. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | idlnegcl 33821 | An ideal is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | idlsubcl 33822 | An ideal is closed under subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
Theorem | rngoidl 33823 | A ring is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | 0idl 33824 | The set containing only is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
GId | ||
Theorem | 1idl 33825 | Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
GId | ||
Theorem | 0rngo 33826 | In a ring, iff the ring contains only . (Contributed by Jeff Madsen, 6-Jan-2011.) |
GId GId | ||
Theorem | divrngidl 33827 | The only ideals in a division ring are the zero ideal and the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
GId | ||
Theorem | intidl 33828 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | inidl 33829 | The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
Theorem | unichnidl 33830* | The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
Theorem | keridl 33831 | The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.) |
GId | ||
Theorem | pridlval 33832* | The class of prime ideals of a ring . (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | ispridl 33833* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | pridlidl 33834 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
Theorem | pridlnr 33835 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
Theorem | pridl 33836* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
Theorem | ispridl2 33837* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 33869 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) |
Theorem | maxidlval 33838* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) |
Theorem | ismaxidl 33839* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) |
Theorem | maxidlidl 33840 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
Theorem | maxidlnr 33841 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) |
Theorem | maxidlmax 33842 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
Theorem | maxidln1 33843 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) |
GId | ||
Theorem | maxidln0 33844 | A ring with a maximal ideal is not the zero ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
GId GId | ||
Syntax | cprrng 33845 | Extend class notation with the class of prime rings. |
Syntax | cdmn 33846 | Extend class notation with the class of domains. |
Definition | df-prrngo 33847 | 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.) |
GId | ||
Definition | df-dmn 33848 | Define the class of (integral) domains. A domain is a commutative prime ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | isprrngo 33849 | The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.) |
GId | ||
Theorem | prrngorngo 33850 | A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | smprngopr 33851 | A simple ring (one whose only ideals are and ) is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
GId GId | ||
Theorem | divrngpr 33852 | A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
Theorem | isdmn 33853 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | isdmn2 33854 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
CRingOps | ||
Theorem | dmncrng 33855 | A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
CRingOps | ||
Theorem | dmnrngo 33856 | A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
Theorem | flddmn 33857 | A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Syntax | cigen 33858 | Extend class notation with the ideal generation function. |
Definition | df-igen 33859* | Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | igenval 33860* | The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) (Proof shortened by Mario Carneiro, 20-Dec-2013.) |
Theorem | igenss 33861 | A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | igenidl 33862 | The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | igenmin 33863 | The ideal generated by a set is the minimal ideal containing that set. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | igenidl2 33864 | The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | igenval2 33865* | The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
Theorem | prnc 33866* | A principal ideal (an ideal generated by one element) in a commutative ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
CRingOps | ||
Theorem | isfldidl 33867 | Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 10-Jun-2010.) |
GId GId CRingOps | ||
Theorem | isfldidl2 33868 | Determine if a ring is a field based on its ideals. (Contributed by Jeff Madsen, 6-Jan-2011.) |
GId CRingOps | ||
Theorem | ispridlc 33869* | The predicate "is a prime ideal". Alternate definition for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
CRingOps | ||
Theorem | pridlc 33870 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
CRingOps | ||
Theorem | pridlc2 33871 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
CRingOps | ||
Theorem | pridlc3 33872 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
CRingOps | ||
Theorem | isdmn3 33873* | The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010.) |
GId GId CRingOps | ||
Theorem | dmnnzd 33874 | A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010.) |
GId | ||
Theorem | dmncan1 33875 | Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.) |
GId | ||
Theorem | dmncan2 33876 | Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.) |
GId | ||
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 33877 | A proof by contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | notbinot1 33878 | Simplification rule of negation across a biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | bicontr 33879 | Biimplication of its own negation is a contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | impor 33880 | An equivalent formula for implying a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | orfa 33881 | The falsum can be removed from a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | notbinot2 33882 | Commutation rule between negation and biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | biimpor 33883 | A rewriting rule for biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | unitresl 33884 | A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | unitresr 33885 | A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | orfa1 33886 | Add a contradicting disjunct to an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | orfa2 33887 | Remove a contradicting disjunct from an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | bifald 33888 | Infer the equivalence to a contradiction from a negation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | orsild 33889 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | orsird 33890 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
Theorem | orcomdd 33891 | Commutativity of logic disjunction, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
Theorem | cnf1dd 33892 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
Theorem | cnf2dd 33893 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
Theorem | cnfn1dd 33894 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
Theorem | cnfn2dd 33895 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
Theorem | or32dd 33896 | A rearrangement of disjuncts, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
Theorem | notornotel1 33897 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
Theorem | notornotel2 33898 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
Theorem | contrd 33899 | A proof by contradiction, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
Theorem | an12i 33900 | An inference from commuting operands in a chain of conjunctions. (Contributed by Giovanni Mascellani, 22-May-2019.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |