| Metamath
Proof Explorer Theorem List (p. 381 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-crngo 38001 | Define the class of commutative rings. (Contributed by Jeff Madsen, 8-Jun-2010.) |
| ⊢ CRingOps = (RingOps ∩ Com2) | ||
| Theorem | iscom2 38002* | 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 38003 | The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
| ⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ 𝑅 ∈ Com2)) | ||
| Theorem | iscrngo2 38004* | The predicate "is a commutative ring". (Contributed by Jeff Madsen, 8-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ CRingOps ↔ (𝑅 ∈ RingOps ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (𝑥𝐻𝑦) = (𝑦𝐻𝑥))) | ||
| Theorem | iscringd 38005* | 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 38006 | 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 38007 | A commutative ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ (𝑅 ∈ CRingOps → 𝑅 ∈ RingOps) | ||
| Theorem | crngocom 38008 | The multiplication operation of a commutative ring is commutative. (Contributed by Jeff Madsen, 8-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ CRingOps ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐻𝐵) = (𝐵𝐻𝐴)) | ||
| Theorem | crngm23 38009 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ CRingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻𝐶) = ((𝐴𝐻𝐶)𝐻𝐵)) | ||
| Theorem | crngm4 38010 | Commutative/associative law for commutative rings. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ CRingOps ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ (𝐶 ∈ 𝑋 ∧ 𝐷 ∈ 𝑋)) → ((𝐴𝐻𝐵)𝐻(𝐶𝐻𝐷)) = ((𝐴𝐻𝐶)𝐻(𝐵𝐻𝐷))) | ||
| Theorem | fldcrngo 38011 | A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010.) |
| ⊢ (𝐾 ∈ Fld → 𝐾 ∈ CRingOps) | ||
| Theorem | isfld2 38012 | The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ (𝐾 ∈ Fld ↔ (𝐾 ∈ DivRingOps ∧ 𝐾 ∈ CRingOps)) | ||
| Theorem | crngohomfo 38013 | 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 38014 | Extend class notation with the class of ideals. |
| class Idl | ||
| Syntax | cpridl 38015 | Extend class notation with the class of prime ideals. |
| class PrIdl | ||
| Syntax | cmaxidl 38016 | Extend class notation with the class of maximal ideals. |
| class MaxIdl | ||
| Definition | df-idl 38017* | 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 38018* | 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 38045 and ispridlc 38077. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ PrIdl = (𝑟 ∈ RingOps ↦ {𝑖 ∈ (Idl‘𝑟) ∣ (𝑖 ≠ ran (1st ‘𝑟) ∧ ∀𝑎 ∈ (Idl‘𝑟)∀𝑏 ∈ (Idl‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(2nd ‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | ||
| Definition | df-maxidl 38019* | 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 38020* | The class of ideals of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → (Idl‘𝑅) = {𝑖 ∈ 𝒫 𝑋 ∣ (𝑍 ∈ 𝑖 ∧ ∀𝑥 ∈ 𝑖 (∀𝑦 ∈ 𝑖 (𝑥𝐺𝑦) ∈ 𝑖 ∧ ∀𝑧 ∈ 𝑋 ((𝑧𝐻𝑥) ∈ 𝑖 ∧ (𝑥𝐻𝑧) ∈ 𝑖)))}) | ||
| Theorem | isidl 38021* | The predicate "is an ideal of the ring 𝑅". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ 𝑋 ((𝑧𝐻𝑥) ∈ 𝐼 ∧ (𝑥𝐻𝑧) ∈ 𝐼))))) | ||
| Theorem | isidlc 38022* | The predicate "is an ideal of the commutative ring 𝑅". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ CRingOps → (𝐼 ∈ (Idl‘𝑅) ↔ (𝐼 ⊆ 𝑋 ∧ 𝑍 ∈ 𝐼 ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ 𝐼 (𝑥𝐺𝑦) ∈ 𝐼 ∧ ∀𝑧 ∈ 𝑋 (𝑧𝐻𝑥) ∈ 𝐼)))) | ||
| Theorem | idlss 38023 | An ideal of 𝑅 is a subset of 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → 𝐼 ⊆ 𝑋) | ||
| Theorem | idlcl 38024 | An element of an ideal is an element of the ring. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝐼) → 𝐴 ∈ 𝑋) | ||
| Theorem | idl0cl 38025 | An ideal contains 0. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → 𝑍 ∈ 𝐼) | ||
| Theorem | idladdcl 38026 | An ideal is closed under addition. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼)) → (𝐴𝐺𝐵) ∈ 𝐼) | ||
| Theorem | idllmulcl 38027 | An ideal is closed under multiplication on the left. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋)) → (𝐵𝐻𝐴) ∈ 𝐼) | ||
| Theorem | idlrmulcl 38028 | An ideal is closed under multiplication on the right. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝑋)) → (𝐴𝐻𝐵) ∈ 𝐼) | ||
| Theorem | idlnegcl 38029 | An ideal is closed under negation. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑁 = (inv‘𝐺) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ 𝐴 ∈ 𝐼) → (𝑁‘𝐴) ∈ 𝐼) | ||
| Theorem | idlsubcl 38030 | An ideal is closed under subtraction. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐷 = ( /𝑔 ‘𝐺) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) ∧ (𝐴 ∈ 𝐼 ∧ 𝐵 ∈ 𝐼)) → (𝐴𝐷𝐵) ∈ 𝐼) | ||
| Theorem | rngoidl 38031 | A ring 𝑅 is an 𝑅 ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → 𝑋 ∈ (Idl‘𝑅)) | ||
| Theorem | 0idl 38032 | The set containing only 0 is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ RingOps → {𝑍} ∈ (Idl‘𝑅)) | ||
| Theorem | 1idl 38033 | Two ways of expressing the unit ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑈 ∈ 𝐼 ↔ 𝐼 = 𝑋)) | ||
| Theorem | 0rngo 38034 | 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 38035 | 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 38036 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∩ 𝐶 ∈ (Idl‘𝑅)) | ||
| Theorem | inidl 38037 | The intersection of two ideals is an ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅) ∧ 𝐽 ∈ (Idl‘𝑅)) → (𝐼 ∩ 𝐽) ∈ (Idl‘𝑅)) | ||
| Theorem | unichnidl 38038* | The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (Idl‘𝑅)) | ||
| Theorem | keridl 38039 | The kernel of a ring homomorphism is an ideal. (Contributed by Jeff Madsen, 3-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑆) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ∈ RingOps ∧ 𝐹 ∈ (𝑅 RingOpsHom 𝑆)) → (◡𝐹 “ {𝑍}) ∈ (Idl‘𝑅)) | ||
| Theorem | pridlval 38040* | 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 38041* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (𝑃 ∈ (PrIdl‘𝑅) ↔ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ (Idl‘𝑅)∀𝑏 ∈ (Idl‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥𝐻𝑦) ∈ 𝑃 → (𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃))))) | ||
| Theorem | pridlidl 38042 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ∈ (Idl‘𝑅)) | ||
| Theorem | pridlnr 38043 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) → 𝑃 ≠ 𝑋) | ||
| Theorem | pridl 38044* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐻 = (2nd ‘𝑅) ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (Idl‘𝑅) ∧ 𝐵 ∈ (Idl‘𝑅) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐵 (𝑥𝐻𝑦) ∈ 𝑃)) → (𝐴 ⊆ 𝑃 ∨ 𝐵 ⊆ 𝑃)) | ||
| Theorem | ispridl2 38045* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 38077 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ (𝑃 ∈ (Idl‘𝑅) ∧ 𝑃 ≠ 𝑋 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) ∈ 𝑃 → (𝑎 ∈ 𝑃 ∨ 𝑏 ∈ 𝑃)))) → 𝑃 ∈ (PrIdl‘𝑅)) | ||
| Theorem | maxidlval 38046* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (MaxIdl‘𝑅) = {𝑖 ∈ (Idl‘𝑅) ∣ (𝑖 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = 𝑋)))}) | ||
| Theorem | ismaxidl 38047* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (𝑅 ∈ RingOps → (𝑀 ∈ (MaxIdl‘𝑅) ↔ (𝑀 ∈ (Idl‘𝑅) ∧ 𝑀 ≠ 𝑋 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑀 ⊆ 𝑗 → (𝑗 = 𝑀 ∨ 𝑗 = 𝑋))))) | ||
| Theorem | maxidlidl 38048 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ∈ (Idl‘𝑅)) | ||
| Theorem | maxidlnr 38049 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → 𝑀 ≠ 𝑋) | ||
| Theorem | maxidlmax 38050 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) ∧ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑀 ⊆ 𝐼)) → (𝐼 = 𝑀 ∨ 𝐼 = 𝑋)) | ||
| Theorem | maxidln1 38051 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) |
| ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑀 ∈ (MaxIdl‘𝑅)) → ¬ 𝑈 ∈ 𝑀) | ||
| Theorem | maxidln0 38052 | 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 38053 | Extend class notation with the class of prime rings. |
| class PrRing | ||
| Syntax | cdmn 38054 | Extend class notation with the class of domains. |
| class Dmn | ||
| Definition | df-prrngo 38055 | 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 38056 | 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 38057 | The predicate "is a prime ring". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (𝑅 ∈ PrRing ↔ (𝑅 ∈ RingOps ∧ {𝑍} ∈ (PrIdl‘𝑅))) | ||
| Theorem | prrngorngo 38058 | A prime ring is a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ (𝑅 ∈ PrRing → 𝑅 ∈ RingOps) | ||
| Theorem | smprngopr 38059 | 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 38060 | A division ring is a prime ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ (𝑅 ∈ DivRingOps → 𝑅 ∈ PrRing) | ||
| Theorem | isdmn 38061 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ Com2)) | ||
| Theorem | isdmn2 38062 | The predicate "is a domain". (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ PrRing ∧ 𝑅 ∈ CRingOps)) | ||
| Theorem | dmncrng 38063 | A domain is a commutative ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ (𝑅 ∈ Dmn → 𝑅 ∈ CRingOps) | ||
| Theorem | dmnrngo 38064 | A domain is a ring. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ (𝑅 ∈ Dmn → 𝑅 ∈ RingOps) | ||
| Theorem | flddmn 38065 | A field is a domain. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ (𝐾 ∈ Fld → 𝐾 ∈ Dmn) | ||
| Syntax | cigen 38066 | Extend class notation with the ideal generation function. |
| class IdlGen | ||
| Definition | df-igen 38067* | Define the ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ IdlGen = (𝑟 ∈ RingOps, 𝑠 ∈ 𝒫 ran (1st ‘𝑟) ↦ ∩ {𝑗 ∈ (Idl‘𝑟) ∣ 𝑠 ⊆ 𝑗}) | ||
| Theorem | igenval 38068* | 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 38069 | A set is a subset of the ideal it generates. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → 𝑆 ⊆ (𝑅 IdlGen 𝑆)) | ||
| Theorem | igenidl 38070 | The ideal generated by a set is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → (𝑅 IdlGen 𝑆) ∈ (Idl‘𝑅)) | ||
| Theorem | igenmin 38071 | 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 38072 | The ideal generated by an ideal is that ideal. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ ((𝑅 ∈ RingOps ∧ 𝐼 ∈ (Idl‘𝑅)) → (𝑅 IdlGen 𝐼) = 𝐼) | ||
| Theorem | igenval2 38073* | The ideal generated by a subset of a ring. (Contributed by Jeff Madsen, 10-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝑅 ∈ RingOps ∧ 𝑆 ⊆ 𝑋) → ((𝑅 IdlGen 𝑆) = 𝐼 ↔ (𝐼 ∈ (Idl‘𝑅) ∧ 𝑆 ⊆ 𝐼 ∧ ∀𝑗 ∈ (Idl‘𝑅)(𝑆 ⊆ 𝑗 → 𝐼 ⊆ 𝑗)))) | ||
| Theorem | prnc 38074* | 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 38075 | 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 38076 | 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 38077* | 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 38078 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → (𝐴 ∈ 𝑃 ∨ 𝐵 ∈ 𝑃)) | ||
| Theorem | pridlc2 38079 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) ∈ 𝑃)) → 𝐵 ∈ 𝑃) | ||
| Theorem | pridlc3 38080 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ (((𝑅 ∈ CRingOps ∧ 𝑃 ∈ (PrIdl‘𝑅)) ∧ (𝐴 ∈ (𝑋 ∖ 𝑃) ∧ 𝐵 ∈ (𝑋 ∖ 𝑃))) → (𝐴𝐻𝐵) ∈ (𝑋 ∖ 𝑃)) | ||
| Theorem | isdmn3 38081* | The predicate "is a domain", alternate expression. (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) & ⊢ 𝑈 = (GId‘𝐻) ⇒ ⊢ (𝑅 ∈ Dmn ↔ (𝑅 ∈ CRingOps ∧ 𝑈 ≠ 𝑍 ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 ((𝑎𝐻𝑏) = 𝑍 → (𝑎 = 𝑍 ∨ 𝑏 = 𝑍)))) | ||
| Theorem | dmnnzd 38082 | A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ ((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐴𝐻𝐵) = 𝑍)) → (𝐴 = 𝑍 ∨ 𝐵 = 𝑍)) | ||
| Theorem | dmncan1 38083 | Cancellation law for domains. (Contributed by Jeff Madsen, 6-Jan-2011.) |
| ⊢ 𝐺 = (1st ‘𝑅) & ⊢ 𝐻 = (2nd ‘𝑅) & ⊢ 𝑋 = ran 𝐺 & ⊢ 𝑍 = (GId‘𝐺) ⇒ ⊢ (((𝑅 ∈ Dmn ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) ∧ 𝐴 ≠ 𝑍) → ((𝐴𝐻𝐵) = (𝐴𝐻𝐶) → 𝐵 = 𝐶)) | ||
| Theorem | dmncan2 38084 | 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 38085 | A proof by contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (¬ 𝜑 → ⊥) ⇒ ⊢ 𝜑 | ||
| Theorem | notbinot1 38086 | Simplification rule of negation across a biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (¬ (¬ 𝜑 ↔ 𝜓) ↔ (𝜑 ↔ 𝜓)) | ||
| Theorem | bicontr 38087 | Biconditional of its own negation is a contradiction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ ((¬ 𝜑 ↔ 𝜑) ↔ ⊥) | ||
| Theorem | impor 38088 | An equivalent formula for implying a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ ((𝜑 → (𝜓 ∨ 𝜒)) ↔ ((¬ 𝜑 ∨ 𝜓) ∨ 𝜒)) | ||
| Theorem | orfa 38089 | The falsum ⊥ can be removed from a disjunction. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ ((𝜑 ∨ ⊥) ↔ 𝜑) | ||
| Theorem | notbinot2 38090 | Commutation rule between negation and biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (¬ (𝜑 ↔ 𝜓) ↔ (¬ 𝜑 ↔ 𝜓)) | ||
| Theorem | biimpor 38091 | A rewriting rule for biconditional. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (((𝜑 ↔ 𝜓) → 𝜒) ↔ ((¬ 𝜑 ↔ 𝜓) ∨ 𝜒)) | ||
| Theorem | orfa1 38092 | Add a contradicting disjunct to an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (𝜑 → 𝜓) ⇒ ⊢ ((𝜑 ∨ ⊥) → 𝜓) | ||
| Theorem | orfa2 38093 | Remove a contradicting disjunct from an antecedent. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (𝜑 → ⊥) ⇒ ⊢ ((𝜑 ∨ 𝜓) → 𝜓) | ||
| Theorem | bifald 38094 | Infer the equivalence to a contradiction from a negation, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (𝜑 → ¬ 𝜓) ⇒ ⊢ (𝜑 → (𝜓 ↔ ⊥)) | ||
| Theorem | orsild 38095 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜓) | ||
| Theorem | orsird 38096 | A lemma for not-or-not elimination, in deduction form. (Contributed by Giovanni Mascellani, 15-Sep-2017.) |
| ⊢ (𝜑 → ¬ (𝜓 ∨ 𝜒)) ⇒ ⊢ (𝜑 → ¬ 𝜒) | ||
| Theorem | cnf1dd 38097 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
| ⊢ (𝜑 → (𝜓 → ¬ 𝜒)) & ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
| Theorem | cnf2dd 38098 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
| ⊢ (𝜑 → (𝜓 → ¬ 𝜃)) & ⊢ (𝜑 → (𝜓 → (𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜒)) | ||
| Theorem | cnfn1dd 38099 | A lemma for Conjunctive Normal Form unit propagation, in double deduction form. (Contributed by Giovanni Mascellani, 19-Mar-2018.) |
| ⊢ (𝜑 → (𝜓 → 𝜒)) & ⊢ (𝜑 → (𝜓 → (¬ 𝜒 ∨ 𝜃))) ⇒ ⊢ (𝜑 → (𝜓 → 𝜃)) | ||
| Theorem | cnfn2dd 38100 | 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 > |