Home | Metamath
Proof Explorer Theorem List (p. 354 of 449) | < 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-28689) |
Hilbert Space Explorer
(28690-30212) |
Users' Mathboxes
(30213-44900) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | intidl 35301 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∩ 𝐶 ∈ (Idl‘𝑅)) | ||
Theorem | inidl 35302 | The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅) ∧ 𝐽 ∈ (Idl‘𝑅)) → (𝐼 ∩ 𝐽) ∈ (Idl‘𝑅)) | ||
Theorem | unichnidl 35303* | The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (Idl‘𝑅)) | ||
Theorem | keridl 35304 | The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑆) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RngHom 𝑆)) → (◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅)) | ||
Theorem | pridlval 35305* | 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 35306* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃))))) | ||
Theorem | pridlidl 35307 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ∈ (Idl‘𝑅)) | ||
Theorem | pridlnr 35308 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ≠ 𝑋) | ||
Theorem | pridl 35309* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐻 = (2nd ‘𝑅) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (Idl‘𝑅) ∧ 𝐵 ∈ (Idl‘𝑅) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) ∈ 𝑃)) → (𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃)) | ||
Theorem | ispridl2 35310* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 35342 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅)) | ||
Theorem | maxidlval 35311* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (MaxIdl‘𝑅) = {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = 𝑋)))}) | ||
Theorem | ismaxidl 35312* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (𝑀 ∈ (MaxIdl‘𝑅) ↔ (𝑀 ∈ (Idl‘𝑅) ∧ 𝑀 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑀 ⊆ 𝑗 → (𝑗 = 𝑀 ∨ 𝑗 = 𝑋))))) | ||
Theorem | maxidlidl 35313 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ∈ (Idl‘𝑅)) | ||
Theorem | maxidlnr 35314 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ≠ 𝑋) | ||
Theorem | maxidlmax 35315 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) ∧ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑀 ⊆ 𝐼)) → (𝐼 = 𝑀 ∨ 𝐼 = 𝑋)) | ||
Theorem | maxidln1 35316 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) |
⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → ¬ 𝑈 ∈ 𝑀) | ||
Theorem | maxidln0 35317 | 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 35318 | Extend class notation with the class of prime rings. |
class PrRing | ||
Syntax | cdmn 35319 | Extend class notation with the class of domains. |
class Dmn | ||
Definition | df-prrngo 35320 | 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 35321 | 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 35322 | The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅))) | ||
Theorem | prrngorngo 35323 | A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑅 ∈ PrRing → 𝑅 ∈ RingOps) | ||
Theorem | smprngopr 35324 | 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 35325 | A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
⊢ (𝑅 ∈ DivRingOps → 𝑅 ∈ PrRing) | ||
Theorem | isdmn 35326 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ Com2)) | ||
Theorem | isdmn2 35327 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps)) | ||
Theorem | dmncrng 35328 | A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ CRingOps) | ||
Theorem | dmnrngo 35329 | A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
⊢ (𝑅 ∈ Dmn → 𝑅 ∈ RingOps) | ||
Theorem | flddmn 35330 | A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ (𝐾 ∈ Fld → 𝐾 ∈ Dmn) | ||
Syntax | cigen 35331 | Extend class notation with the ideal generation function. |
class IdlGen | ||
Definition | df-igen 35332* | Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}) | ||
Theorem | igenval 35333* | 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 35334 | A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (𝑅 IdlGen 𝑆)) | ||
Theorem | igenidl 35335 | The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) ∈ (Idl‘𝑅)) | ||
Theorem | igenmin 35336 | 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 35337 | The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑅 IdlGen 𝐼) = 𝐼) | ||
Theorem | igenval2 35338* | The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → ((𝑅 IdlGen 𝑆) = 𝐼 ↔ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗)))) | ||
Theorem | prnc 35339* | 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 35340 | 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 35341 | 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 35342* | 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 35343 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → (𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃)) | ||
Theorem | pridlc2 35344 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → 𝐵 ∈ 𝑃) | ||
Theorem | pridlc3 35345 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ (𝑋 ∖ 𝑃))) → (𝐴𝐻𝐵) ∈ (𝑋 ∖ 𝑃)) | ||
Theorem | isdmn3 35346* | The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍)))) | ||
Theorem | dmnnzd 35347 | A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) = 𝑍)) → (𝐴 = 𝑍 ∨ 𝐵 = 𝑍)) | ||
Theorem | dmncan1 35348 | Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.) |
⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → ((𝐴𝐻𝐵) = (𝐴𝐻𝐶) → 𝐵 = 𝐶)) | ||
Theorem | dmncan2 35349 | 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 35350 | A proof by contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (¬ 𝜑 → ⊥) ⇒ ⊢ 𝜑 | ||
Theorem | notbinot1 35351 | Simplification rule of negation across a biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (¬ (¬ 𝜑 ↔ 𝜓) ↔ (𝜑 ↔ 𝜓)) | ||
Theorem | bicontr 35352 | Biimplication of its own negation is a contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ ((¬ 𝜑 ↔ 𝜑) ↔ ⊥) | ||
Theorem | impor 35353 | An equivalent formula for implying a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ ((𝜑 → (𝜓 ∨ 𝜒)) ↔ ((¬ 𝜑 ∨ 𝜓) ∨ 𝜒)) | ||
Theorem | orfa 35354 | The falsum ⊥ can be removed from a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ ((𝜑 ∨ ⊥) ↔ 𝜑) | ||
Theorem | notbinot2 35355 | Commutation rule between negation and biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (¬ (𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ 𝜓)) | ||
Theorem | biimpor 35356 | A rewriting rule for biimplication. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((¬ 𝜑 ↔ 𝜓) ∨ 𝜒)) | ||
Theorem | orfa1 35357 | Add a contradicting disjunct to an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∨ ⊥) → 𝜓) | ||
Theorem | orfa2 35358 | Remove a contradicting disjunct from an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (𝜑 → ⊥) ⇒ ⊢ ((𝜑 ∨ 𝜓) → 𝜓) | ||
Theorem | bifald 35359 | Infer the equivalence to a contradiction from a negation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ ⊥)) | ||
Theorem | orsild 35360 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
Theorem | orsird 35361 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
Theorem | cnf1dd 35362 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → (𝜓 → ¬ 𝜒)) & ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | cnf2dd 35363 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → (𝜓 → ¬ 𝜃)) & ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | cnfn1dd 35364 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → (¬ 𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
Theorem | cnfn2dd 35365 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → (𝜓 → 𝜃)) & ⊢ (𝜑 → (𝜓 → (𝜒 ∨ ¬ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
Theorem | or32dd 35366 | A rearrangement of disjuncts, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜃) ∨ 𝜏))) ⇒ ⊢ (𝜑 → (𝜓 → ((𝜒 ∨ 𝜏) ∨ 𝜃))) | ||
Theorem | notornotel1 35367 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → ¬ (¬ 𝜓 ∨ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | notornotel2 35368 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → ¬ (𝜓 ∨ ¬ 𝜒)) ⇒ ⊢ (𝜑 → 𝜒) | ||
Theorem | contrd 35369 | A proof by contradiction, in deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
⊢ (𝜑 → (¬ 𝜓 → 𝜒)) & ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒)) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | an12i 35370 | An inference from commuting operands in a chain of conjunctions. (Contributed by Giovanni Mascellani, 22-May-2019.) |
⊢ (𝜑 ∧ (𝜓 ∧ 𝜒)) ⇒ ⊢ (𝜓 ∧ (𝜑 ∧ 𝜒)) | ||
Theorem | exmid2 35371 | An excluded middle law. (Contributed by Giovanni Mascellani, 23-May-2019.) |
⊢ ((𝜓 ∧ 𝜑) → 𝜒) & ⊢ ((¬ 𝜓 ∧ 𝜂) → 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜂) → 𝜒) | ||
Theorem | selconj 35372 | An inference for selecting one of a list of conjuncts. (Contributed by Giovanni Mascellani, 23-May-2019.) |
⊢ (𝜑 ↔ (𝜓 ∧ 𝜒)) ⇒ ⊢ ((𝜂 ∧ 𝜑) ↔ (𝜓 ∧ (𝜂 ∧ 𝜒))) | ||
Theorem | truconj 35373 | Add true as a conjunct. (Contributed by Giovanni Mascellani, 23-May-2019.) |
⊢ (𝜑 ↔ (⊤ ∧ 𝜑)) | ||
Theorem | orel 35374 | An inference for disjunction elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ ((𝜓 ∧ 𝜂) → 𝜃) & ⊢ ((𝜒 ∧ 𝜌) → 𝜃) & ⊢ (𝜑 → (𝜓 ∨ 𝜒)) ⇒ ⊢ ((𝜑 ∧ (𝜂 ∧ 𝜌)) → 𝜃) | ||
Theorem | negel 35375 | An inference for negation elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ (𝜓 → 𝜒) & ⊢ (𝜑 → ¬ 𝜒) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ⊥) | ||
Theorem | botel 35376 | An inference for bottom elimination. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ (𝜑 → ⊥) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | tradd 35377 | Add top ad a conjunct. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ (𝜑 ↔ 𝜓) ⇒ ⊢ (𝜑 ↔ (⊤ ∧ 𝜓)) | ||
Theorem | gm-sbtru 35378 | Substitution does not change truth. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]⊤ ↔ ⊤) | ||
Theorem | sbfal 35379 | Substitution does not change falsity. (Contributed by Giovanni Mascellani, 24-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥]⊥ ↔ ⊥) | ||
Theorem | sbcani 35380 | Distribution of class substitution over conjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒) & ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂) ⇒ ⊢ ([𝐴 / 𝑥](𝜑 ∧ 𝜓) ↔ (𝜒 ∧ 𝜂)) | ||
Theorem | sbcori 35381 | Distribution of class substitution over disjunction, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒) & ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂) ⇒ ⊢ ([𝐴 / 𝑥](𝜑 ∨ 𝜓) ↔ (𝜒 ∨ 𝜂)) | ||
Theorem | sbcimi 35382 | Distribution of class substitution over implication, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜒) & ⊢ ([𝐴 / 𝑥]𝜓 ↔ 𝜂) ⇒ ⊢ ([𝐴 / 𝑥](𝜑 → 𝜓) ↔ (𝜒 → 𝜂)) | ||
Theorem | sbcni 35383 | Move class substitution inside a negation, in inference form. (Contributed by Giovanni Mascellani, 27-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥] ¬ 𝜑 ↔ ¬ 𝜓) | ||
Theorem | sbali 35384 | 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 35385 | 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 35386* | 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 35387* | 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 35388* | 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 35389* | 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 | spsbcdi 35390 | A lemma for eliminating a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ (𝜑 → ∀𝑥𝜒) & ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 → 𝜓) | ||
Theorem | alrimii 35391* | A lemma for introducing a universal quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ Ⅎ𝑦𝜑 & ⊢ (𝜑 → 𝜓) & ⊢ ([𝑦 / 𝑥]𝜒 ↔ 𝜓) & ⊢ Ⅎ𝑦𝜒 ⇒ ⊢ (𝜑 → ∀𝑥𝜒) | ||
Theorem | spesbcdi 35392 | A lemma for introducing an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ (𝜑 → 𝜓) & ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜓) ⇒ ⊢ (𝜑 → ∃𝑥𝜒) | ||
Theorem | exlimddvf 35393 | A lemma for eliminating an existential quantifier. (Contributed by Giovanni Mascellani, 30-May-2019.) |
⊢ (𝜑 → ∃𝑥𝜃) & ⊢ Ⅎ𝑥𝜓 & ⊢ ((𝜃 ∧ 𝜓) → 𝜒) & ⊢ Ⅎ𝑥𝜒 ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | exlimddvfi 35394 | A lemma for eliminating an existential quantifier, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ (𝜑 → ∃𝑥𝜃) & ⊢ Ⅎ𝑦𝜃 & ⊢ Ⅎ𝑦𝜓 & ⊢ ([𝑦 / 𝑥]𝜃 ↔ 𝜂) & ⊢ ((𝜂 ∧ 𝜓) → 𝜒) & ⊢ Ⅎ𝑦𝜒 ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | ||
Theorem | sbceq1ddi 35395 | A lemma for eliminating inequality, in inference form. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ (𝜑 → 𝐴 = 𝐵) & ⊢ (𝜓 → 𝜃) & ⊢ ([𝐴 / 𝑥]𝜒 ↔ 𝜃) & ⊢ ([𝐵 / 𝑥]𝜒 ↔ 𝜂) ⇒ ⊢ ((𝜑 ∧ 𝜓) → 𝜂) | ||
Theorem | sbccom2lem 35396* | Lemma for sbccom2 35397. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
Theorem | sbccom2 35397* | Commutative law for double class substitution. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ 𝐴 ∈ V ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
Theorem | sbccom2f 35398* | Commutative law for double class substitution, with nonfree variable condition. (Contributed by Giovanni Mascellani, 31-May-2019.) |
⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑦𝐴 ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦][𝐴 / 𝑥]𝜑) | ||
Theorem | sbccom2fi 35399* | Commutative law for double class substitution, with nonfree variable condition and in inference form. (Contributed by Giovanni Mascellani, 1-Jun-2019.) |
⊢ 𝐴 ∈ V & ⊢ Ⅎ𝑦𝐴 & ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 & ⊢ ([𝐴 / 𝑥]𝜑 ↔ 𝜓) ⇒ ⊢ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐶 / 𝑦]𝜓) | ||
Theorem | csbcom2fi 35400* | 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 & ⊢ Ⅎ𝑦𝐴 & ⊢ ⦋𝐴 / 𝑥⦌𝐵 = 𝐶 & ⊢ ⦋𝐴 / 𝑥⦌𝐷 = 𝐸 ⇒ ⊢ ⦋𝐴 / 𝑥⦌⦋𝐵 / 𝑦⦌𝐷 = ⦋𝐶 / 𝑦⦌𝐸 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |