![]() |
Metamath
Proof Explorer Theorem List (p. 373 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | inidl 37201 | The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ ((π β RingOps β§ πΌ β (Idlβπ ) β§ π½ β (Idlβπ )) β (πΌ β© π½) β (Idlβπ )) | ||
Theorem | unichnidl 37202* | The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ ((π β RingOps β§ (πΆ β β β§ πΆ β (Idlβπ ) β§ βπ β πΆ βπ β πΆ (π β π β¨ π β π))) β βͺ πΆ β (Idlβπ )) | ||
Theorem | keridl 37203 | The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.) |
β’ πΊ = (1st βπ) & β’ π = (GIdβπΊ) β β’ ((π β RingOps β§ π β RingOps β§ πΉ β (π RingOpsHom π)) β (β‘πΉ β {π}) β (Idlβπ )) | ||
Theorem | pridlval 37204* | 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 37205* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (π β RingOps β (π β (PrIdlβπ ) β (π β (Idlβπ ) β§ π β π β§ βπ β (Idlβπ )βπ β (Idlβπ )(βπ₯ β π βπ¦ β π (π₯π»π¦) β π β (π β π β¨ π β π))))) | ||
Theorem | pridlidl 37206 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ ((π β RingOps β§ π β (PrIdlβπ )) β π β (Idlβπ )) | ||
Theorem | pridlnr 37207 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π β (PrIdlβπ )) β π β π) | ||
Theorem | pridl 37208* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ π» = (2nd βπ ) β β’ (((π β RingOps β§ π β (PrIdlβπ )) β§ (π΄ β (Idlβπ ) β§ π΅ β (Idlβπ ) β§ βπ₯ β π΄ βπ¦ β π΅ (π₯π»π¦) β π)) β (π΄ β π β¨ π΅ β π)) | ||
Theorem | ispridl2 37209* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 37241 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ (π β (Idlβπ ) β§ π β π β§ βπ β π βπ β π ((ππ»π) β π β (π β π β¨ π β π)))) β π β (PrIdlβπ )) | ||
Theorem | maxidlval 37210* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (π β RingOps β (MaxIdlβπ ) = {π β (Idlβπ ) β£ (π β π β§ βπ β (Idlβπ )(π β π β (π = π β¨ π = π)))}) | ||
Theorem | ismaxidl 37211* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (π β RingOps β (π β (MaxIdlβπ ) β (π β (Idlβπ ) β§ π β π β§ βπ β (Idlβπ )(π β π β (π = π β¨ π = π))))) | ||
Theorem | maxidlidl 37212 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
β’ ((π β RingOps β§ π β (MaxIdlβπ )) β π β (Idlβπ )) | ||
Theorem | maxidlnr 37213 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π β (MaxIdlβπ )) β π β π) | ||
Theorem | maxidlmax 37214 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ (((π β RingOps β§ π β (MaxIdlβπ )) β§ (πΌ β (Idlβπ ) β§ π β πΌ)) β (πΌ = π β¨ πΌ = π)) | ||
Theorem | maxidln1 37215 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) |
β’ π» = (2nd βπ ) & β’ π = (GIdβπ») β β’ ((π β RingOps β§ π β (MaxIdlβπ )) β Β¬ π β π) | ||
Theorem | maxidln0 37216 | 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 37217 | Extend class notation with the class of prime rings. |
class PrRing | ||
Syntax | cdmn 37218 | Extend class notation with the class of domains. |
class Dmn | ||
Definition | df-prrngo 37219 | 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 37220 | 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 37221 | The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = (GIdβπΊ) β β’ (π β PrRing β (π β RingOps β§ {π} β (PrIdlβπ ))) | ||
Theorem | prrngorngo 37222 | A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (π β PrRing β π β RingOps) | ||
Theorem | smprngopr 37223 | 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 37224 | A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ (π β DivRingOps β π β PrRing) | ||
Theorem | isdmn 37225 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (π β Dmn β (π β PrRing β§ π β Com2)) | ||
Theorem | isdmn2 37226 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (π β Dmn β (π β PrRing β§ π β CRingOps)) | ||
Theorem | dmncrng 37227 | A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ (π β Dmn β π β CRingOps) | ||
Theorem | dmnrngo 37228 | A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ (π β Dmn β π β RingOps) | ||
Theorem | flddmn 37229 | A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ (πΎ β Fld β πΎ β Dmn) | ||
Syntax | cigen 37230 | Extend class notation with the ideal generation function. |
class IdlGen | ||
Definition | df-igen 37231* | Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ IdlGen = (π β RingOps, π β π« ran (1st βπ) β¦ β© {π β (Idlβπ) β£ π β π}) | ||
Theorem | igenval 37232* | 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 37233 | A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π β π) β π β (π IdlGen π)) | ||
Theorem | igenidl 37234 | The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π β π) β (π IdlGen π) β (Idlβπ )) | ||
Theorem | igenmin 37235 | 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 37236 | The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ ((π β RingOps β§ πΌ β (Idlβπ )) β (π IdlGen πΌ) = πΌ) | ||
Theorem | igenval2 37237* | The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π = ran πΊ β β’ ((π β RingOps β§ π β π) β ((π IdlGen π) = πΌ β (πΌ β (Idlβπ ) β§ π β πΌ β§ βπ β (Idlβπ )(π β π β πΌ β π)))) | ||
Theorem | prnc 37238* | 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 37239 | 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 37240 | 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 37241* | 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 37242 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (((π β CRingOps β§ π β (PrIdlβπ )) β§ (π΄ β π β§ π΅ β π β§ (π΄π»π΅) β π)) β (π΄ β π β¨ π΅ β π)) | ||
Theorem | pridlc2 37243 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (((π β CRingOps β§ π β (PrIdlβπ )) β§ (π΄ β (π β π) β§ π΅ β π β§ (π΄π»π΅) β π)) β π΅ β π) | ||
Theorem | pridlc3 37244 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ β β’ (((π β CRingOps β§ π β (PrIdlβπ )) β§ (π΄ β (π β π) β§ π΅ β (π β π))) β (π΄π»π΅) β (π β π)) | ||
Theorem | isdmn3 37245* | The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) & β’ π = (GIdβπ») β β’ (π β Dmn β (π β CRingOps β§ π β π β§ βπ β π βπ β π ((ππ»π) = π β (π = π β¨ π = π)))) | ||
Theorem | dmnnzd 37246 | A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ ((π β Dmn β§ (π΄ β π β§ π΅ β π β§ (π΄π»π΅) = π)) β (π΄ = π β¨ π΅ = π)) | ||
Theorem | dmncan1 37247 | Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.) |
β’ πΊ = (1st βπ ) & β’ π» = (2nd βπ ) & β’ π = ran πΊ & β’ π = (GIdβπΊ) β β’ (((π β Dmn β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β§ π΄ β π) β ((π΄π»π΅) = (π΄π»πΆ) β π΅ = πΆ)) | ||
Theorem | dmncan2 37248 | 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 37249 | A proof by contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (Β¬ π β β₯) β β’ π | ||
Theorem | notbinot1 37250 | Simplification rule of negation across a biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (Β¬ (Β¬ π β π) β (π β π)) | ||
Theorem | bicontr 37251 | Biconditional of its own negation is a contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ ((Β¬ π β π) β β₯) | ||
Theorem | impor 37252 | An equivalent formula for implying a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ ((π β (π β¨ π)) β ((Β¬ π β¨ π) β¨ π)) | ||
Theorem | orfa 37253 | The falsum β₯ can be removed from a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ ((π β¨ β₯) β π) | ||
Theorem | notbinot2 37254 | Commutation rule between negation and biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (Β¬ (π β π) β (Β¬ π β π)) | ||
Theorem | biimpor 37255 | A rewriting rule for biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (((π β π) β π) β ((Β¬ π β π) β¨ π)) | ||
Theorem | orfa1 37256 | Add a contradicting disjunct to an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (π β π) β β’ ((π β¨ β₯) β π) | ||
Theorem | orfa2 37257 | Remove a contradicting disjunct from an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (π β β₯) β β’ ((π β¨ π) β π) | ||
Theorem | bifald 37258 | Infer the equivalence to a contradiction from a negation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (π β Β¬ π) β β’ (π β (π β β₯)) | ||
Theorem | orsild 37259 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (π β Β¬ (π β¨ π)) β β’ (π β Β¬ π) | ||
Theorem | orsird 37260 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
β’ (π β Β¬ (π β¨ π)) β β’ (π β Β¬ π) | ||
Theorem | cnf1dd 37261 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
β’ (π β (π β Β¬ π)) & β’ (π β (π β (π β¨ π))) β β’ (π β (π β π)) | ||
Theorem | cnf2dd 37262 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
β’ (π β (π β Β¬ π)) & β’ (π β (π β (π β¨ π))) β β’ (π β (π β π)) | ||
Theorem | cnfn1dd 37263 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
β’ (π β (π β π)) & β’ (π β (π β (Β¬ π β¨ π))) β β’ (π β (π β π)) | ||
Theorem | cnfn2dd 37264 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
β’ (π β (π β π)) & β’ (π β (π β (π β¨ Β¬ π))) β β’ (π β (π β π)) | ||
Theorem | or32dd 37265 | A rearrangement of disjuncts, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
β’ (π β (π β ((π β¨ π) β¨ π))) β β’ (π β (π β ((π β¨ π) β¨ π))) | ||
Theorem | notornotel1 37266 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
β’ (π β Β¬ (Β¬ π β¨ π)) β β’ (π β π) | ||
Theorem | notornotel2 37267 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
β’ (π β Β¬ (π β¨ Β¬ π)) β β’ (π β π) | ||
Theorem | contrd 37268 | A proof by contradiction, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
β’ (π β (Β¬ π β π)) & β’ (π β (Β¬ π β Β¬ π)) β β’ (π β π) | ||
Theorem | an12i 37269 | An inference from commuting operands in a chain of conjunctions. (Contributed by Giovanni Mascellani, 22-May-2019.) |
β’ (π β§ (π β§ π)) β β’ (π β§ (π β§ π)) | ||
Theorem | exmid2 37270 | An excluded middle law. (Contributed by Giovanni Mascellani, 23-May-2019.) |
β’ ((π β§ π) β π) & β’ ((Β¬ π β§ π) β π) β β’ ((π β§ π) β π) | ||
Theorem | selconj 37271 | An inference for selecting one of a list of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.) |
β’ (π β (π β§ π)) β β’ ((π β§ π) β (π β§ (π β§ π))) | ||
Theorem | truconj 37272 | Add true as a conjunct. (Contributed by Giovanni Mascellani, 23-May-2019.) |
β’ (π β (β€ β§ π)) | ||
Theorem | orel 37273 | An inference for disjunction elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
β’ ((π β§ π) β π) & β’ ((π β§ π) β π) & β’ (π β (π β¨ π)) β β’ ((π β§ (π β§ π)) β π) | ||
Theorem | negel 37274 | An inference for negation elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
β’ (π β π) & β’ (π β Β¬ π) β β’ ((π β§ π) β β₯) | ||
Theorem | botel 37275 | An inference for bottom elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
β’ (π β β₯) β β’ (π β π) | ||
Theorem | tradd 37276 | Add top ad a conjunct. (Contributed by Giovanni Mascellani, 24-May-2019.) |
β’ (π β π) β β’ (π β (β€ β§ π)) | ||
Theorem | gm-sbtru 37277 | Substitution does not change truth. (Contributed by Giovanni Mascellani, 24-May-2019.) |
β’ π΄ β V β β’ ([π΄ / π₯]β€ β β€) | ||
Theorem | sbfal 37278 | Substitution does not change falsity. (Contributed by Giovanni Mascellani, 24-May-2019.) |
β’ π΄ β V β β’ ([π΄ / π₯]β₯ β β₯) | ||
Theorem | sbcani 37279 | Distribution of class substitution over conjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
β’ ([π΄ / π₯]π β π) & β’ ([π΄ / π₯]π β π) β β’ ([π΄ / π₯](π β§ π) β (π β§ π)) | ||
Theorem | sbcori 37280 | Distribution of class substitution over disjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
β’ ([π΄ / π₯]π β π) & β’ ([π΄ / π₯]π β π) β β’ ([π΄ / π₯](π β¨ π) β (π β¨ π)) | ||
Theorem | sbcimi 37281 | Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
β’ π΄ β V & β’ ([π΄ / π₯]π β π) & β’ ([π΄ / π₯]π β π) β β’ ([π΄ / π₯](π β π) β (π β π)) | ||
Theorem | sbcni 37282 | Move class substitution inside a negation, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
β’ π΄ β V & β’ ([π΄ / π₯]π β π) β β’ ([π΄ / π₯] Β¬ π β Β¬ π) | ||
Theorem | sbali 37283 | Discard class substitution in a universal quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
β’ π΄ β V β β’ ([π΄ / π₯]βπ₯π β βπ₯π) | ||
Theorem | sbexi 37284 | Discard class substitution in an existential quantification when substituting the quantified variable, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
β’ π΄ β V β β’ ([π΄ / π₯]βπ₯π β βπ₯π) | ||
Theorem | sbcalf 37285* | Move universal quantifier in and out of class substitution, with an explicit nonfree variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.) |
β’ β²π¦π΄ β β’ ([π΄ / π₯]βπ¦π β βπ¦[π΄ / π₯]π) | ||
Theorem | sbcexf 37286* | Move existential quantifier in and out of class substitution, with an explicit nonfree variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.) |
β’ β²π¦π΄ β β’ ([π΄ / π₯]βπ¦π β βπ¦[π΄ / π₯]π) | ||
Theorem | sbcalfi 37287* | Move universal quantifier in and out of class substitution, with an explicit nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
β’ β²π¦π΄ & β’ ([π΄ / π₯]π β π) β β’ ([π΄ / π₯]βπ¦π β βπ¦π) | ||
Theorem | sbcexfi 37288* | Move existential quantifier in and out of class substitution, with an explicit nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
β’ β²π¦π΄ & β’ ([π΄ / π₯]π β π) β β’ ([π΄ / π₯]βπ¦π β βπ¦π) | ||
Theorem | spsbcdi 37289 | A lemma for eliminating a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
β’ π΄ β V & β’ (π β βπ₯π) & β’ ([π΄ / π₯]π β π) β β’ (π β π) | ||
Theorem | alrimii 37290* | A lemma for introducing a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
β’ β²π¦π & β’ (π β π) & β’ ([π¦ / π₯]π β π) & β’ β²π¦π β β’ (π β βπ₯π) | ||
Theorem | spesbcdi 37291 | A lemma for introducing an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
β’ (π β π) & β’ ([π΄ / π₯]π β π) β β’ (π β βπ₯π) | ||
Theorem | exlimddvf 37292 | A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019.) |
β’ (π β βπ₯π) & β’ β²π₯π & β’ ((π β§ π) β π) & β’ β²π₯π β β’ ((π β§ π) β π) | ||
Theorem | exlimddvfi 37293 | A lemma for eliminating an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.) |
β’ (π β βπ₯π) & β’ β²π¦π & β’ β²π¦π & β’ ([π¦ / π₯]π β π) & β’ ((π β§ π) β π) & β’ β²π¦π β β’ ((π β§ π) β π) | ||
Theorem | sbceq1ddi 37294 | A lemma for eliminating inequality, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.) |
β’ (π β π΄ = π΅) & β’ (π β π) & β’ ([π΄ / π₯]π β π) & β’ ([π΅ / π₯]π β π) β β’ ((π β§ π) β π) | ||
Theorem | sbccom2lem 37295* | Lemma for sbccom2 37296. (Contributed by Giovanni Mascellani, 31-May-2019.) |
β’ π΄ β V β β’ ([π΄ / π₯][π΅ / π¦]π β [β¦π΄ / π₯β¦π΅ / π¦][π΄ / π₯]π) | ||
Theorem | sbccom2 37296* | Commutative law for double class substitution. (Contributed by Giovanni Mascellani, 31-May-2019.) |
β’ π΄ β V β β’ ([π΄ / π₯][π΅ / π¦]π β [β¦π΄ / π₯β¦π΅ / π¦][π΄ / π₯]π) | ||
Theorem | sbccom2f 37297* | Commutative law for double class substitution, with nonfree variable condition. (Contributed by Giovanni Mascellani, 31-May-2019.) |
β’ π΄ β V & β’ β²π¦π΄ β β’ ([π΄ / π₯][π΅ / π¦]π β [β¦π΄ / π₯β¦π΅ / π¦][π΄ / π₯]π) | ||
Theorem | sbccom2fi 37298* | Commutative law for double class substitution, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.) |
β’ π΄ β V & β’ β²π¦π΄ & β’ β¦π΄ / π₯β¦π΅ = πΆ & β’ ([π΄ / π₯]π β π) β β’ ([π΄ / π₯][π΅ / π¦]π β [πΆ / π¦]π) | ||
Theorem | csbcom2fi 37299* | Commutative law for double class substitution in a class, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 4-Jun-2019.) |
β’ π΄ β V & β’ β²π¦π΄ & β’ β¦π΄ / π₯β¦π΅ = πΆ & β’ β¦π΄ / π₯β¦π· = πΈ β β’ β¦π΄ / π₯β¦β¦π΅ / π¦β¦π· = β¦πΆ / π¦β¦πΈ | ||
A collection of Tseitin axioms used to convert a wff to Conjunctive Normal Form. | ||
Theorem | fald 37300 | Refutation of falsity, in deduction form. (Contributed by Giovanni Mascellani, 24-Mar-2018.) |
β’ (π β Β¬ β₯) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |