HomeTheorem List (p. 335 of 494)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 335 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: | Metamath Proof Explorer
(1-30937) |
Hilbert Space Explorer
(30938-32460) |
Users' Mathboxes
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | ellpi 33401 | Elementhood in a left principal ideal in terms of the "divides" relation. (Contributed by Thierry Arnoux, 18-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑌 ∈ (𝐾‘{𝑋}) ↔ 𝑋 ∥ 𝑌)) | ||
| Theorem | lpirlidllpi 33402* | In a principal ideal ring, ideals are principal. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ LPIR) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐽 = (𝐾‘{𝑥})) | ||
| Theorem | rspidlid 33403 | The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝐾‘𝐼) = 𝐼) | ||
| Theorem | pidlnz 33404 | A principal ideal generated by a nonzero element is not the zero ideal. (Contributed by Thierry Arnoux, 11-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝐾‘{𝑋}) ≠ { 0 }) | ||
| Theorem | lbslsp 33405* | Any element of a left module 𝑀 can be expressed as a linear combination of the elements of a basis 𝑉 of 𝑀. (Contributed by Thierry Arnoux, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝑉 ∈ (LBasis‘𝑀)) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐵 ↔ ∃𝑎 ∈ (𝐾 ↑m 𝑉)(𝑎 finSupp 0 ∧ 𝑋 = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣)))))) | ||
| Theorem | lindssn 33406 | Any singleton of a nonzero element is an independent set. (Contributed by Thierry Arnoux, 5-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LIndS‘𝑊)) | ||
| Theorem | lindflbs 33407 | Conditions for an independent family to be a basis. (Contributed by Thierry Arnoux, 21-Jul-2023.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑂 = (0g‘𝑊) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑆 ∈ NzRing) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼–1-1→𝐵) ⇒ ⊢ (𝜑 → (ran 𝐹 ∈ (LBasis‘𝑊) ↔ (𝐹 LIndF 𝑊 ∧ (𝑁‘ran 𝐹) = 𝐵))) | ||
| Theorem | islbs5 33408* | An equivalent formulation of the basis predicate in a vector space, using a function 𝐹 for generating the base. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑆 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑂 = (0g‘𝑊) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ (𝜑 → 𝑆 ∈ NzRing) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼–1-1→𝐵) ⇒ ⊢ (𝜑 → (ran 𝐹 ∈ (LBasis‘𝑊) ↔ (∀𝑎 ∈ (𝐾 ↑m 𝐼)((𝑎 finSupp 0 ∧ (𝑊 Σg (𝑎 ∘f · 𝐹)) = 𝑂) → 𝑎 = (𝐼 × { 0 })) ∧ (𝑁‘ran 𝐹) = 𝐵))) | ||
| Theorem | linds2eq 33409 | Deduce equality of elements in an independent set. (Contributed by Thierry Arnoux, 18-Jul-2023.) |
| ⊢ 𝐹 = (Base‘(Scalar‘𝑊)) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ 0 = (0g‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝐵 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ 𝐹) & ⊢ (𝜑 → 𝐿 ∈ 𝐹) & ⊢ (𝜑 → 𝐾 ≠ 0 ) & ⊢ (𝜑 → (𝐾 · 𝑋) = (𝐿 · 𝑌)) ⇒ ⊢ (𝜑 → (𝑋 = 𝑌 ∧ 𝐾 = 𝐿)) | ||
| Theorem | lindfpropd 33410* | Property deduction for linearly independent families. (Contributed by Thierry Arnoux, 16-Jul-2023.) |
| ⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (Base‘(Scalar‘𝐾)) = (Base‘(Scalar‘𝐿))) & ⊢ (𝜑 → (0g‘(Scalar‘𝐾)) = (0g‘(Scalar‘𝐿))) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ (Base‘𝐾)) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝐿 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → (𝑋 LIndF 𝐾 ↔ 𝑋 LIndF 𝐿)) | ||
| Theorem | lindspropd 33411* | Property deduction for linearly independent sets. (Contributed by Thierry Arnoux, 16-Jul-2023.) |
| ⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (Base‘(Scalar‘𝐾)) = (Base‘(Scalar‘𝐿))) & ⊢ (𝜑 → (0g‘(Scalar‘𝐾)) = (0g‘(Scalar‘𝐿))) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐾) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·𝑠 ‘𝐾)𝑦) ∈ (Base‘𝐾)) & ⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘(Scalar‘𝐾)) ∧ 𝑦 ∈ (Base‘𝐾))) → (𝑥( ·𝑠 ‘𝐾)𝑦) = (𝑥( ·𝑠 ‘𝐿)𝑦)) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝐿 ∈ 𝑊) ⇒ ⊢ (𝜑 → (LIndS‘𝐾) = (LIndS‘𝐿)) | ||
| Theorem | dvdsruassoi 33412 | If two elements 𝑋 and 𝑌 of a ring 𝑅 are unit multiples, then they are associates, i.e. each divides the other. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑉 ∈ 𝑈) & ⊢ (𝜑 → (𝑉 · 𝑋) = 𝑌) ⇒ ⊢ (𝜑 → (𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋)) | ||
| Theorem | dvdsruasso 33413* | Two elements 𝑋 and 𝑌 of a ring 𝑅 are associates, i.e. each divides the other, iff they are unit multiples of each other. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ ∃𝑢 ∈ 𝑈 (𝑢 · 𝑋) = 𝑌)) | ||
| Theorem | dvdsruasso2 33414* | A reformulation of dvdsruasso 33413. (Proposed by Gerard Lang, 28-May-2025.) (Contributed by Thiery Arnoux, 29-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ ∃𝑢 ∈ 𝑈 ∃𝑣 ∈ 𝑈 ((𝑢 · 𝑋) = 𝑌 ∧ (𝑣 · 𝑌) = 𝑋 ∧ (𝑢 · 𝑣) = 1 ))) | ||
| Theorem | dvdsrspss 33415 | In a ring, an element 𝑋 divides 𝑌 iff the ideal generated by 𝑌 is a subset of the ideal generated by 𝑋 (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝑋 ∥ 𝑌 ↔ (𝐾‘{𝑌}) ⊆ (𝐾‘{𝑋}))) | ||
| Theorem | rspsnasso 33416 | Two elements 𝑋 and 𝑌 of a ring 𝑅 are associates, i.e. each divides the other, iff the ideals they generate are equal. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ ∥ = (∥r‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → ((𝑋 ∥ 𝑌 ∧ 𝑌 ∥ 𝑋) ↔ (𝐾‘{𝑌}) = (𝐾‘{𝑋}))) | ||
| Theorem | unitprodclb 33417 | A finite product is a unit iff all factors are units. (Contributed by Thierry Arnoux, 27-May-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐹 ∈ Word 𝐵) ⇒ ⊢ (𝜑 → ((𝑀 Σg 𝐹) ∈ 𝑈 ↔ ran 𝐹 ⊆ 𝑈)) | ||
The sumset (also called the Minkowski sum) of two subsets 𝐴 and 𝐵, is defined to be the set of all sums of an element from 𝐴 with an element from 𝐵. The sumset operation can be used for both group (additive) operations and ring (multiplicative) operations. | ||
| Theorem | elgrplsmsn 33418* | Membership in a sumset with a singleton for a group operation. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝐴 ⊕ {𝑋}) ↔ ∃𝑥 ∈ 𝐴 𝑍 = (𝑥 + 𝑋))) | ||
| Theorem | lsmsnorb 33419* | The sumset of a group with a single element is the element's orbit by the group action. See gaorb 19325. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ ∃𝑔 ∈ 𝐴 (𝑔 + 𝑥) = 𝑦)} & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⊕ {𝑋}) = [𝑋] ∼ ) | ||
| Theorem | lsmsnorb2 33420* | The sumset of a single element with a group is the element's orbit by the group action. See gaorb 19325. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ ∃𝑔 ∈ 𝐴 (𝑥 + 𝑔) = 𝑦)} & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ({𝑋} ⊕ 𝐴) = [𝑋] ∼ ) | ||
| Theorem | elringlsm 33421* | Membership in a product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝐸 × 𝐹) ↔ ∃𝑥 ∈ 𝐸 ∃𝑦 ∈ 𝐹 𝑍 = (𝑥 · 𝑦))) | ||
| Theorem | elringlsmd 33422 | Membership in a product of two subsets of a ring, one direction. (Contributed by Thierry Arnoux, 13-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) & ⊢ (𝜑 → 𝑌 ∈ 𝐹) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ (𝐸 × 𝐹)) | ||
| Theorem | ringlsmss 33423 | Closure of the product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐸 × 𝐹) ⊆ 𝐵) | ||
| Theorem | ringlsmss1 33424 | The product of an ideal 𝐼 of a commutative ring 𝑅 with some set E is a subset of the ideal. (Contributed by Thierry Arnoux, 8-Jun-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝐼 × 𝐸) ⊆ 𝐼) | ||
| Theorem | ringlsmss2 33425 | The product with an ideal of a ring is a subset of that ideal. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝐸 × 𝐼) ⊆ 𝐼) | ||
| Theorem | lsmsnpridl 33426 | The product of the ring with a single element is equal to the principal ideal generated by that element. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐵 × {𝑋}) = (𝐾‘{𝑋})) | ||
| Theorem | lsmsnidl 33427 | The product of the ring with a single element is a principal ideal. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐵 × {𝑋}) ∈ (LPIdeal‘𝑅)) | ||
| Theorem | lsmidllsp 33428 | The sum of two ideals is the ideal generated by their union. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⊕ = (LSSum‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝐼 ⊕ 𝐽) = (𝐾‘(𝐼 ∪ 𝐽))) | ||
| Theorem | lsmidl 33429 | The sum of two ideals is an ideal. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⊕ = (LSSum‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝐼 ⊕ 𝐽) ∈ (LIdeal‘𝑅)) | ||
| Theorem | lsmssass 33430 | Group sum is associative, subset version (see lsmass 19687). (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑅 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ⊆ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ((𝑅 ⊕ 𝑇) ⊕ 𝑈) = (𝑅 ⊕ (𝑇 ⊕ 𝑈))) | ||
| Theorem | grplsm0l 33431 | Sumset with the identity singleton is the original set. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ({ 0 } ⊕ 𝐴) = 𝐴) | ||
| Theorem | grplsmid 33432 | The direct sum of an element 𝑋 of a subgroup 𝐴 is the subgroup itself. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝐴) → ({𝑋} ⊕ 𝐴) = 𝐴) | ||
| Theorem | quslsm 33433 | Express the image by the quotient map in terms of direct sum. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → [𝑋](𝐺 ~QG 𝑆) = ({𝑋} ⊕ 𝑆)) | ||
| Theorem | qusbas2 33434* | Alternate definition of the group quotient set, as the set of all cosets of the form ({𝑥} ⊕ 𝑁). (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → (𝐵 / (𝐺 ~QG 𝑁)) = ran (𝑥 ∈ 𝐵 ↦ ({𝑥} ⊕ 𝑁))) | ||
| Theorem | qus0g 33435 | The identity element of a quotient group. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) ⇒ ⊢ (𝑁 ∈ (NrmSGrp‘𝐺) → (0g‘𝑄) = 𝑁) | ||
| Theorem | qusima 33436* | The image of a subgroup by the natural map from elements to their cosets. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝐺 ~QG 𝑁)) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) & ⊢ (𝜑 → 𝐻 ∈ 𝑆) & ⊢ (𝜑 → 𝑆 ⊆ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → (𝐸‘𝐻) = (𝐹 “ 𝐻)) | ||
| Theorem | qusrn 33437* | The natural map from elements to their cosets is surjective. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑈 = (𝐵 / (𝐺 ~QG 𝑁)) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝐺 ~QG 𝑁)) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → ran 𝐹 = 𝑈) | ||
| Theorem | nsgqus0 33438 | A normal subgroup 𝑁 is a member of all subgroups 𝐹 of the quotient group by 𝑁. In fact, it is the identity element of the quotient group. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) ⇒ ⊢ ((𝑁 ∈ (NrmSGrp‘𝐺) ∧ 𝐹 ∈ (SubGrp‘𝑄)) → 𝑁 ∈ 𝐹) | ||
| Theorem | nsgmgclem 33439* | Lemma for nsgmgc 33440. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) & ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝑄)) ⇒ ⊢ (𝜑 → {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} ∈ (SubGrp‘𝐺)) | ||
| Theorem | nsgmgc 33440* | There is a monotone Galois connection between the lattice of subgroups of a group 𝐺 containing a normal subgroup 𝑁 and the lattice of subgroups of the quotient group 𝐺 / 𝑁. This is sometimes called the lattice theorem. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} & ⊢ 𝑇 = (SubGrp‘𝑄) & ⊢ 𝐽 = (𝑉MGalConn𝑊) & ⊢ 𝑉 = (toInc‘𝑆) & ⊢ 𝑊 = (toInc‘𝑇) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → 𝐸𝐽𝐹) | ||
| Theorem | nsgqusf1olem1 33441* | Lemma for nsgqusf1o 33444. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} & ⊢ 𝑇 = (SubGrp‘𝑄) & ⊢ ≤ = (le‘(toInc‘𝑆)) & ⊢ ≲ = (le‘(toInc‘𝑇)) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) → ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) ∈ 𝑇) | ||
| Theorem | nsgqusf1olem2 33442* | Lemma for nsgqusf1o 33444. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} & ⊢ 𝑇 = (SubGrp‘𝑄) & ⊢ ≤ = (le‘(toInc‘𝑆)) & ⊢ ≲ = (le‘(toInc‘𝑇)) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → ran 𝐸 = 𝑇) | ||
| Theorem | nsgqusf1olem3 33443* | Lemma for nsgqusf1o 33444. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} & ⊢ 𝑇 = (SubGrp‘𝑄) & ⊢ ≤ = (le‘(toInc‘𝑆)) & ⊢ ≲ = (le‘(toInc‘𝑇)) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → ran 𝐹 = 𝑆) | ||
| Theorem | nsgqusf1o 33444* | The canonical projection homomorphism 𝐸 defines a bijective correspondence between the set 𝑆 of subgroups of 𝐺 containing a normal subgroup 𝑁 and the subgroups of the quotient group 𝐺 / 𝑁. This theorem is sometimes called the correspondence theorem, or the fourth isomorphism theorem. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} & ⊢ 𝑇 = (SubGrp‘𝑄) & ⊢ ≤ = (le‘(toInc‘𝑆)) & ⊢ ≲ = (le‘(toInc‘𝑇)) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → 𝐸:𝑆–1-1-onto→𝑇) | ||
| Theorem | lmhmqusker 33445* | A surjective module homomorphism 𝐹 from 𝐺 to 𝐻 induces an isomorphism 𝐽 from 𝑄 to 𝐻, where 𝑄 is the factor group of 𝐺 by 𝐹's kernel 𝐾. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 LMHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) ⇒ ⊢ (𝜑 → 𝐽 ∈ (𝑄 LMIso 𝐻)) | ||
| Theorem | lmicqusker 33446 | The image 𝐻 of a module homomorphism 𝐹 is isomorphic with the quotient module 𝑄 over 𝐹's kernel 𝐾. This is part of what is sometimes called the first isomorphism theorem for modules. (Contributed by Thierry Arnoux, 10-Mar-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 LMHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻)) ⇒ ⊢ (𝜑 → 𝑄 ≃𝑚 𝐻) | ||
| Theorem | lidlmcld 33447 | An ideal is closed under left-multiplication by elements of the full ring. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ 𝑈) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ 𝐼) | ||
| Theorem | intlidl 33448 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Thierry Arnoux, 8-Jun-2024.) |
| ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → ∩ 𝐶 ∈ (LIdeal‘𝑅)) | ||
| Theorem | 0ringidl 33449 | The zero ideal is the only ideal of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → (LIdeal‘𝑅) = {{ 0 }}) | ||
| Theorem | pidlnzb 33450 | A principal ideal is nonzero iff it is generated by a nonzero elements (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 ≠ 0 ↔ (𝐾‘{𝑋}) ≠ { 0 })) | ||
| Theorem | lidlunitel 33451 | If an ideal 𝐼 contains a unit 𝐽, then it is the whole ring. (Contributed by Thierry Arnoux, 19-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑈 = (Unit‘𝑅) & ⊢ (𝜑 → 𝐽 ∈ 𝑈) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → 𝐼 = 𝐵) | ||
| Theorem | unitpidl1 33452 | The ideal 𝐼 generated by an element 𝑋 of an integral domain 𝑅 is the unit ideal 𝐵 iff 𝑋 is a ring unit. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝑈 = (Unit‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝐼 = (𝐾‘{𝑋}) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ IDomn) ⇒ ⊢ (𝜑 → (𝐼 = 𝐵 ↔ 𝑋 ∈ 𝑈)) | ||
| Theorem | rhmquskerlem 33453* | The mapping 𝐽 induced by a ring homomorphism 𝐹 from the quotient group 𝑄 over 𝐹's kernel 𝐾 is a ring homomorphism. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 RingHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) & ⊢ (𝜑 → 𝐺 ∈ CRing) ⇒ ⊢ (𝜑 → 𝐽 ∈ (𝑄 RingHom 𝐻)) | ||
| Theorem | rhmqusker 33454* | A surjective ring homomorphism 𝐹 from 𝐺 to 𝐻 induces an isomorphism 𝐽 from 𝑄 to 𝐻, where 𝑄 is the factor group of 𝐺 by 𝐹's kernel 𝐾. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 RingHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻)) & ⊢ (𝜑 → 𝐺 ∈ CRing) & ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞)) ⇒ ⊢ (𝜑 → 𝐽 ∈ (𝑄 RingIso 𝐻)) | ||
| Theorem | ricqusker 33455 | The image 𝐻 of a ring homomorphism 𝐹 is isomorphic with the quotient ring 𝑄 over 𝐹's kernel 𝐾. This a part of what is sometimes called the first isomorphism theorem for rings. (Contributed by Thierry Arnoux, 10-Mar-2025.) |
| ⊢ 0 = (0g‘𝐻) & ⊢ (𝜑 → 𝐹 ∈ (𝐺 RingHom 𝐻)) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾)) & ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻)) & ⊢ (𝜑 → 𝐺 ∈ CRing) ⇒ ⊢ (𝜑 → 𝑄 ≃𝑟 𝐻) | ||
| Theorem | elrspunidl 33456* | Elementhood in the span of a union of ideals. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
| ⊢ 𝑁 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑆 ⊆ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘∪ 𝑆) ↔ ∃𝑎 ∈ (𝐵 ↑m 𝑆)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg 𝑎) ∧ ∀𝑘 ∈ 𝑆 (𝑎‘𝑘) ∈ 𝑘))) | ||
| Theorem | elrspunsn 33457* | Membership to the span of an ideal 𝑅 and a single element 𝑋. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑁 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ + = (+g‘𝑅) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑋 ∈ (𝐵 ∖ 𝐼)) ⇒ ⊢ (𝜑 → (𝐴 ∈ (𝑁‘(𝐼 ∪ {𝑋})) ↔ ∃𝑟 ∈ 𝐵 ∃𝑖 ∈ 𝐼 𝐴 = ((𝑟 · 𝑋) + 𝑖))) | ||
| Theorem | lidlincl 33458 | Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024.) |
| ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑈) → (𝐼 ∩ 𝐽) ∈ 𝑈) | ||
| Theorem | idlinsubrg 33459 | The intersection between an ideal and a subring is an ideal of the subring. (Contributed by Thierry Arnoux, 6-Jul-2024.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑈 = (LIdeal‘𝑅) & ⊢ 𝑉 = (LIdeal‘𝑆) ⇒ ⊢ ((𝐴 ∈ (SubRing‘𝑅) ∧ 𝐼 ∈ 𝑈) → (𝐼 ∩ 𝐴) ∈ 𝑉) | ||
| Theorem | rhmimaidl 33460 | The image of an ideal 𝐼 by a surjective ring homomorphism 𝐹 is an ideal. (Contributed by Thierry Arnoux, 6-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑇 = (LIdeal‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑆) ⇒ ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = 𝐵 ∧ 𝐼 ∈ 𝑇) → (𝐹 “ 𝐼) ∈ 𝑈) | ||
| Theorem | drngidl 33461 | A nonzero ring is a division ring if and only if its only left ideals are the zero ideal and the unit ideal. (Proposed by Gerard Lang, 13-Mar-2025.) (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ NzRing → (𝑅 ∈ DivRing ↔ 𝑈 = {{ 0 }, 𝐵})) | ||
| Theorem | drngidlhash 33462 | A ring is a division ring if and only if it admits exactly two ideals. (Proposed by Gerard Lang, 13-Mar-2025.) (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑅 ∈ DivRing ↔ (♯‘𝑈) = 2)) | ||
| Syntax | cprmidl 33463 | Extend class notation with the class of prime ideals. |
| class PrmIdeal | ||
| Definition | df-prmidl 33464* | 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 prmidl2 33469 and isprmidlc 33475. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 14-Jan-2024.) |
| ⊢ PrmIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | ||
| Theorem | prmidlval 33465* | The class of prime ideals of a ring 𝑅. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) = {𝑖 ∈ (LIdeal‘𝑅) ∣ (𝑖 ≠ 𝐵 ∧ ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥 · 𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | ||
| Theorem | isprmidl 33466* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑃 ∈ (PrmIdeal‘𝑅) ↔ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑎 ∈ (LIdeal‘𝑅)∀𝑏 ∈ (LIdeal‘𝑅)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥 · 𝑦) ∈ 𝑃 → (𝑎 ⊆ 𝑃 ∨ 𝑏 ⊆ 𝑃))))) | ||
| Theorem | prmidlnr 33467 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ≠ 𝐵) | ||
| Theorem | prmidl 33468* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐽 ∈ (LIdeal‘𝑅))) ∧ ∀𝑥 ∈ 𝐼 ∀𝑦 ∈ 𝐽 (𝑥 · 𝑦) ∈ 𝑃) → (𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃)) | ||
| Theorem | prmidl2 33469* | 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.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑃 ∈ (LIdeal‘𝑅)) ∧ (𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃)))) → 𝑃 ∈ (PrmIdeal‘𝑅)) | ||
| Theorem | idlmulssprm 33470 | Let 𝑃 be a prime ideal containing the product (𝐼 × 𝐽) of two ideals 𝐼 and 𝐽. Then 𝐼 ⊆ 𝑃 or 𝐽 ⊆ 𝑃. (Contributed by Thierry Arnoux, 13-Apr-2024.) |
| ⊢ × = (LSSum‘(mulGrp‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑃 ∈ (PrmIdeal‘𝑅)) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → (𝐼 × 𝐽) ⊆ 𝑃) ⇒ ⊢ (𝜑 → (𝐼 ⊆ 𝑃 ∨ 𝐽 ⊆ 𝑃)) | ||
| Theorem | pridln1 33471 | A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ¬ 1 ∈ 𝐼) | ||
| Theorem | prmidlidl 33472 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ ((𝑅 ∈ Ring ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) → 𝑃 ∈ (LIdeal‘𝑅)) | ||
| Theorem | prmidlssidl 33473 | Prime ideals as a subset of ideals. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) ⊆ (LIdeal‘𝑅)) | ||
| Theorem | cringm4 33474 | Commutative/associative law for commutative ring. (Contributed by Thierry Arnoux, 14-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 · 𝑌) · (𝑍 · 𝑊)) = ((𝑋 · 𝑍) · (𝑌 · 𝑊))) | ||
| Theorem | isprmidlc 33475* | The predicate "is prime ideal" for commutative rings. Alternate definition for commutative rings. See definition in [Lang] p. 92. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → (𝑃 ∈ (PrmIdeal‘𝑅) ↔ (𝑃 ∈ (LIdeal‘𝑅) ∧ 𝑃 ≠ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 · 𝑦) ∈ 𝑃 → (𝑥 ∈ 𝑃 ∨ 𝑦 ∈ 𝑃))))) | ||
| Theorem | prmidlc 33476 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑃 ∈ (PrmIdeal‘𝑅)) ∧ (𝐼 ∈ 𝐵 ∧ 𝐽 ∈ 𝐵 ∧ (𝐼 · 𝐽) ∈ 𝑃)) → (𝐼 ∈ 𝑃 ∨ 𝐽 ∈ 𝑃)) | ||
| Theorem | 0ringprmidl 33477 | The trivial ring does not have any prime ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (♯‘𝐵) = 1) → (PrmIdeal‘𝑅) = ∅) | ||
| Theorem | prmidl0 33478 | The zero ideal of a commutative ring 𝑅 is a prime ideal if and only if 𝑅 is an integral domain. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
| ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ { 0 } ∈ (PrmIdeal‘𝑅)) ↔ 𝑅 ∈ IDomn) | ||
| Theorem | rhmpreimaprmidl 33479 | The preimage of a prime ideal by a ring homomorphism is a prime ideal. (Contributed by Thierry Arnoux, 29-Jun-2024.) |
| ⊢ 𝑃 = (PrmIdeal‘𝑅) ⇒ ⊢ (((𝑆 ∈ CRing ∧ 𝐹 ∈ (𝑅 RingHom 𝑆)) ∧ 𝐽 ∈ (PrmIdeal‘𝑆)) → (◡𝐹 “ 𝐽) ∈ 𝑃) | ||
| Theorem | qsidomlem1 33480 | If the quotient ring of a commutative ring relative to an ideal is an integral domain, that ideal must be prime. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) ∧ 𝑄 ∈ IDomn) → 𝐼 ∈ (PrmIdeal‘𝑅)) | ||
| Theorem | qsidomlem2 33481 | A quotient by a prime ideal is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (PrmIdeal‘𝑅)) → 𝑄 ∈ IDomn) | ||
| Theorem | qsidom 33482 | An ideal 𝐼 in the commutative ring 𝑅 is prime if and only if the factor ring 𝑄 is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝐼 ∈ (LIdeal‘𝑅)) → (𝑄 ∈ IDomn ↔ 𝐼 ∈ (PrmIdeal‘𝑅))) | ||
| Theorem | qsnzr 33483 | A quotient of a non-zero ring by a proper ideal is a non-zero ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑅 ∈ NzRing) & ⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) & ⊢ (𝜑 → 𝐼 ≠ 𝐵) ⇒ ⊢ (𝜑 → 𝑄 ∈ NzRing) | ||
| Theorem | ssdifidllem 33484* | Lemma for ssdifidl 33485: The set 𝑃 used in the proof of ssdifidl 33485 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅) & ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)} & ⊢ (𝜑 → 𝑍 ⊆ 𝑃) & ⊢ (𝜑 → 𝑍 ≠ ∅) & ⊢ (𝜑 → [⊊] Or 𝑍) ⇒ ⊢ (𝜑 → ∪ 𝑍 ∈ 𝑃) | ||
| Theorem | ssdifidl 33485* | Let 𝑅 be a ring, and let 𝐼 be an ideal of 𝑅 disjoint with a set 𝑆. Then there exists an ideal 𝑖, maximal among the set 𝑃 of ideals containing 𝐼 and disjoint with 𝑆. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑆 ⊆ 𝐵) & ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅) & ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)} ⇒ ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗) | ||
| Theorem | ssdifidlprm 33486* | If the set 𝑆 of ssdifidl 33485 is multiplicatively closed, then the ideal 𝑖 is prime. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀)) & ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ (𝜑 → (𝑆 ∩ 𝐼) = ∅) & ⊢ 𝑃 = {𝑝 ∈ (LIdeal‘𝑅) ∣ ((𝑆 ∩ 𝑝) = ∅ ∧ 𝐼 ⊆ 𝑝)} ⇒ ⊢ (𝜑 → ∃𝑖 ∈ 𝑃 (𝑖 ∈ (PrmIdeal‘𝑅) ∧ ∀𝑗 ∈ 𝑃 ¬ 𝑖 ⊊ 𝑗)) | ||
| Syntax | cmxidl 33487 | Extend class notation with the class of maximal ideals. |
| class MaxIdeal | ||
| Definition | df-mxidl 33488* | 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.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ MaxIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑗 ∈ (LIdeal‘𝑟)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = (Base‘𝑟))))}) | ||
| Theorem | mxidlval 33489* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (MaxIdeal‘𝑅) = {𝑖 ∈ (LIdeal‘𝑅) ∣ (𝑖 ≠ 𝐵 ∧ ∀𝑗 ∈ (LIdeal‘𝑅)(𝑖 ⊆ 𝑗 → (𝑗 = 𝑖 ∨ 𝑗 = 𝐵)))}) | ||
| Theorem | ismxidl 33490* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ (𝑀 ∈ (LIdeal‘𝑅) ∧ 𝑀 ≠ 𝐵 ∧ ∀𝑗 ∈ (LIdeal‘𝑅)(𝑀 ⊆ 𝑗 → (𝑗 = 𝑀 ∨ 𝑗 = 𝐵))))) | ||
| Theorem | mxidlidl 33491 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (LIdeal‘𝑅)) | ||
| Theorem | mxidlnr 33492 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ≠ 𝐵) | ||
| Theorem | mxidlmax 33493 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ (((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) ∧ (𝐼 ∈ (LIdeal‘𝑅) ∧ 𝑀 ⊆ 𝐼)) → (𝐼 = 𝑀 ∨ 𝐼 = 𝐵)) | ||
| Theorem | mxidln1 33494 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → ¬ 1 ∈ 𝑀) | ||
| Theorem | mxidlnzr 33495 | A ring with a maximal ideal is a nonzero ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑅 ∈ NzRing) | ||
| Theorem | mxidlmaxv 33496 | An ideal 𝐼 strictly containing a maximal ideal 𝑀 is the whole ring 𝐵. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝑀 ⊆ 𝐼) & ⊢ (𝜑 → 𝑋 ∈ (𝐼 ∖ 𝑀)) ⇒ ⊢ (𝜑 → 𝐼 = 𝐵) | ||
| Theorem | crngmxidl 33497 | In a commutative ring, maximal ideals of the opposite ring coincide with maximal ideals. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑀 = (MaxIdeal‘𝑅) & ⊢ 𝑂 = (oppr‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝑀 = (MaxIdeal‘𝑂)) | ||
| Theorem | mxidlprm 33498 | Every maximal ideal is prime. Statement in [Lang] p. 92. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ × = (LSSum‘(mulGrp‘𝑅)) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ (MaxIdeal‘𝑅)) → 𝑀 ∈ (PrmIdeal‘𝑅)) | ||
| Theorem | mxidlirredi 33499 | In an integral domain, the generator of a maximal ideal is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑀 = (𝐾‘{𝑋}) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑀 ∈ (MaxIdeal‘𝑅)) ⇒ ⊢ (𝜑 → 𝑋 ∈ (Irred‘𝑅)) | ||
| Theorem | mxidlirred 33500 | In a principal ideal domain, maximal ideals are exactly the ideals generated by irreducible elements. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑀 = (𝐾‘{𝑋}) & ⊢ (𝜑 → 𝑅 ∈ PID) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≠ 0 ) & ⊢ (𝜑 → 𝑀 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝑀 ∈ (MaxIdeal‘𝑅) ↔ 𝑋 ∈ (Irred‘𝑅))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |