Home | Metamath
Proof Explorer Theorem List (p. 331 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | keridl 33001 | The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑆) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅)) | ||
Theorem | pridlval 33002* | 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 33003* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃))))) | ||
Theorem | pridlidl 33004 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ∈ (Idl‘𝑅)) | ||
Theorem | pridlnr 33005 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ≠ 𝑋) | ||
Theorem | pridl 33006* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐻 = (2nd ‘𝑅) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (Idl‘𝑅) ∧ 𝐵 ∈ (Idl‘𝑅) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) ∈ 𝑃)) → (𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃)) | ||
Theorem | ispridl2 33007* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 33039 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅)) | ||
Theorem | maxidlval 33008* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (MaxIdl‘𝑅) = {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = 𝑋)))}) | ||
Theorem | ismaxidl 33009* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (𝑀 ∈ (MaxIdl‘𝑅) ↔ (𝑀 ∈ (Idl‘𝑅) ∧ 𝑀 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑀 ⊆ 𝑗 → (𝑗 = 𝑀 ∨ 𝑗 = 𝑋))))) | ||
Theorem | maxidlidl 33010 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ∈ (Idl‘𝑅)) | ||
Theorem | maxidlnr 33011 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ≠ 𝑋) | ||
Theorem | maxidlmax 33012 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) ∧ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑀 ⊆ 𝐼)) → (𝐼 = 𝑀 ∨ 𝐼 = 𝑋)) | ||
Theorem | maxidln1 33013 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) |
⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → ¬ 𝑈 ∈ 𝑀) | ||
Theorem | maxidln0 33014 | 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 33015 | Extend class notation with the class of prime rings. |
class PrRing | ||
Syntax | cdmn 33016 | Extend class notation with the class of domains. |
class Dmn | ||
Definition | df-prrngo 33017 | 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 33018 | 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 33019 | The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅))) | ||
Theorem | prrngorngo 33020 | A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑅 ∈ PrRing → 𝑅 ∈ RingOps) | ||
Theorem | smprngopr 33021 | 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 33022 | A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
⊢ (𝑅 ∈ DivRingOps → 𝑅 ∈ PrRing) | ||
Theorem | isdmn 33023 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ Com2)) | ||
Theorem | isdmn2 33024 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps)) | ||
Theorem | dmncrng 33025 | A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ CRingOps) | ||
Theorem | dmnrngo 33026 | A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ RingOps) | ||
Theorem | flddmn 33027 | A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝐾 ∈ Fld → 𝐾 ∈ Dmn) | ||
Syntax | cigen 33028 | Extend class notation with the ideal generation function. |
class IdlGen | ||
Definition | df-igen 33029* | Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}) | ||
Theorem | igenval 33030* | 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 33031 | A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (𝑅 IdlGen 𝑆)) | ||
Theorem | igenidl 33032 | The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) ∈ (Idl‘𝑅)) | ||
Theorem | igenmin 33033 | 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 33034 | The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑅 IdlGen 𝐼) = 𝐼) | ||
Theorem | igenval2 33035* | The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → ((𝑅 IdlGen 𝑆) = 𝐼 ↔ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗)))) | ||
Theorem | prnc 33036* | 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 33037 | 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 33038 | 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 33039* | 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 33040 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → (𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃)) | ||
Theorem | pridlc2 33041 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → 𝐵 ∈ 𝑃) | ||
Theorem | pridlc3 33042 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ (𝑋 ∖ 𝑃))) → (𝐴𝐻𝐵) ∈ (𝑋 ∖ 𝑃)) | ||
Theorem | isdmn3 33043* | The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍)))) | ||
Theorem | dmnnzd 33044 | A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) = 𝑍)) → (𝐴 = 𝑍 ∨ 𝐵 = 𝑍)) | ||
Theorem | dmncan1 33045 | Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → ((𝐴𝐻𝐵) = (𝐴𝐻𝐶) → 𝐵 = 𝐶)) | ||
Theorem | dmncan2 33046 | 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 33047 | A proof by contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (¬ 𝜑 → ⊥) ⇒ ⊢ 𝜑 | ||
Theorem | notbinot1 33048 | Simplification rule of negation across a biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (¬ (¬ 𝜑 ↔ 𝜓) ↔ (𝜑 ↔ 𝜓)) | ||
Theorem | bicontr 33049 | Biimplication of its own negation is a contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ ((¬ 𝜑 ↔ 𝜑) ↔ ⊥) | ||
Theorem | impor 33050 | An equivalent formula for implying a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ ((𝜑 → (𝜓 ∨ 𝜒)) ↔ ((¬ 𝜑 ∨ 𝜓) ∨ 𝜒)) | ||
Theorem | orfa 33051 | The falsum ⊥ can be removed from a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ ((𝜑 ∨ ⊥) ↔ 𝜑) | ||
Theorem | notbinot2 33052 | Commutation rule between negation and biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (¬ (𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ 𝜓)) | ||
Theorem | biimpor 33053 | A rewriting rule for biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((¬ 𝜑 ↔ 𝜓) ∨ 𝜒)) | ||
Theorem | unitresl 33054 | A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (𝜑 → (𝜓 ∨ 𝜒)) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | unitresr 33055 | A lemma for Conjunctive Normal Form unit propagation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (𝜑 → (𝜓 ∨ 𝜒)) & ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | orfa1 33056 | Add a contradicting disjunct to an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∨ ⊥) → 𝜓) | ||
Theorem | orfa2 33057 | Remove a contradicting disjunct from an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (𝜑 → ⊥) ⇒ ⊢ ((𝜑 ∨ 𝜓) → 𝜓) | ||
Theorem | bifald 33058 | Infer the equivalence to a contradiction from a negation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ ⊥)) | ||
Theorem | orsild 33059 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | orsird 33060 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | orcomdd 33061 | Commutativity of logic disjunction, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → (𝜃 ∨ 𝜒))) | ||
Theorem | cnf1dd 33062 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → (𝜓 → ¬ 𝜒)) & ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | cnf2dd 33063 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → (𝜓 → ¬ 𝜃)) & ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | cnfn1dd 33064 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → (¬ 𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | cnfn2dd 33065 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → (𝜒 ∨ ¬ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | or32dd 33066 | A rearrangement of disjuncts, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃) ∨ 𝜏))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) ∨ 𝜃))) | ||
Theorem | notornotel1 33067 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → ¬ (¬ 𝜓 ∨ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | notornotel2 33068 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → ¬ (𝜓 ∨ ¬ 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | contrd 33069 | A proof by contradiction, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜒)) & ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | an12i 33070 | An inference from commuting operands in a chain of conjunctions. (Contributed by Giovanni Mascellani, 22-May-2019.) |
⊢ (𝜑 ∧ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 ∧ (𝜑 ∧ 𝜒)) | ||
Theorem | exmid2 33071 | An excluded middle law. (Contributed by Giovanni Mascellani, 23-May-2019.) |
⊢ ((𝜓 ∧ 𝜑) → 𝜒) & ⊢ ((¬ 𝜓 ∧ 𝜂) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜂) → 𝜒) | ||
Theorem | selconj 33072 | An inference for selecting one of a list of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ ((𝜂 ∧ 𝜑) ↔ (𝜓 ∧ (𝜂 ∧ 𝜒))) | ||
Theorem | truconj 33073 | Add true as a conjunct. (Contributed by Giovanni Mascellani, 23-May-2019.) |
⊢ (𝜑 ↔ (⊤ ∧ 𝜑)) | ||
Theorem | orel 33074 | An inference for disjunction elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ ((𝜓 ∧ 𝜂) → 𝜃) & ⊢ ((𝜒 ∧ 𝜌) → 𝜃) & ⊢ (𝜑 → (𝜓 ∨ 𝜒)) ⇒ ⊢ ((𝜑 ∧ (𝜂 ∧ 𝜌)) → 𝜃) | ||
Theorem | negel 33075 | An inference for negation elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ (𝜓 → 𝜒) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ⊥) | ||
Theorem | botel 33076 | An inference for bottom elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ (𝜑 → ⊥) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | tradd 33077 | Add top ad a conjunct. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ (⊤ ∧ 𝜓)) | ||
Theorem | sbtru 33078 | Substitution does not change truth. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]⊤ ↔ ⊤) | ||
Theorem | sbfal 33079 | Substitution does not change falsity. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]⊥ ↔ ⊥) | ||
Theorem | sbcani 33080 | Distribution of class substitution over conjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒) & ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂) ⇒ ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ (𝜒 ∧ 𝜂)) | ||
Theorem | sbcori 33081 | Distribution of class substitution over disjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒) & ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂) ⇒ ⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ (𝜒 ∨ 𝜂)) | ||
Theorem | sbcimi 33082 | Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒) & ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂) ⇒ ⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ (𝜒 → 𝜂)) | ||
Theorem | sbceqi 33083 | Distribution of class substitution over equality, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐷 & ⊢ ⦋𝐴 / 𝑥⦌𝐶 = 𝐸 ⇒ ⊢ ([𝐴 / 𝑥]𝐵 = 𝐶 ↔ 𝐷 = 𝐸) | ||
Theorem | sbcni 33084 | Move class substitution inside a negation, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ 𝜓) | ||
Theorem | sbali 33085 | 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 33086 | 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 33087* | Move universal quantifier in and out of class substitution, with an explicit non-free variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ ([𝐴 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦[𝐴 / 𝑥]𝜑) | ||
Theorem | sbcexf 33088* | Move existential quantifier in and out of class substitution, with an explicit non-free variable condition. (Contributed by Giovanni Mascellani, 29-May-2019.) |
⊢ Ⅎ𝑦𝐴 ⇒ ⊢ ([𝐴 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦[𝐴 / 𝑥]𝜑) | ||
Theorem | sbcalfi 33089* | Move universal quantifier in and out of class substitution, with an explicit non-free variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ Ⅎ𝑦𝐴 & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥]∀𝑦𝜑 ↔ ∀𝑦𝜓) | ||
Theorem | sbcexfi 33090* | Move existential quantifier in and out of class substitution, with an explicit non-free variable condition and in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ Ⅎ𝑦𝐴 & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥]∃𝑦𝜑 ↔ ∃𝑦𝜓) | ||
Theorem | csbvargi 33091 | The proper substitution of a class for a variable in that variable results in the class (if the class exists), in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝑥 = 𝐴 | ||
Theorem | csbconstgi 33092* | The proper substitution of a class for a variable in another variable does not modify it, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ⦋𝐴 / 𝑥⦌𝑦 = 𝑦 | ||
Theorem | spsbcdi 33093 | A lemma for eliminating a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ (𝜑 → ∀𝑥𝜒) & ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | alrimii 33094* | A lemma for introducing a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝜓) & ⊢ ([𝑦 / 𝑥]𝜒 ↔ 𝜓) & ⊢ Ⅎ𝑦𝜒 ⇒ ⊢ (𝜑 → ∀𝑥𝜒) | ||
Theorem | spesbcdi 33095 | A lemma for introducing an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ (𝜑 → 𝜓) & ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥𝜒) | ||
Theorem | exlimddvf 33096 | A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ (𝜑 → ∃𝑥𝜃) & ⊢ Ⅎ𝑥𝜓 & ⊢ ((𝜃 ∧ 𝜓) → 𝜒) & ⊢ Ⅎ𝑥𝜒 ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | exlimddvfi 33097 | A lemma for eliminating an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ (𝜑 → ∃𝑥𝜃) & ⊢ Ⅎ𝑦𝜃 & ⊢ Ⅎ𝑦𝜓 & ⊢ ([𝑦 / 𝑥]𝜃 ↔ 𝜂) & ⊢ ((𝜂 ∧ 𝜓) → 𝜒) & ⊢ Ⅎ𝑦𝜒 ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | sbceq1ddi 33098 | A lemma for eliminating inequality, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝜃) & ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜃) & ⊢ ([𝐵 / 𝑥]𝜒 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜂) | ||
Theorem | sbccom2lem 33099* | Lemma for sbccom2 33100. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
Theorem | sbccom2 33100* | Commutative law for double class substitution. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |