HomeTheorem List (p. 334 of 499)
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. 334 of 499) | < 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-30888) |
Hilbert Space Explorer
(30889-32411) |
Users' Mathboxes
(32412-49816) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | rearchi 33301 | The field of the real numbers is Archimedean. See also arch 12370. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
| ⊢ ℝfld ∈ Archi | ||
| Theorem | nn0archi 33302 | The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
| ⊢ (ℂfld ↾s ℕ0) ∈ Archi | ||
| Theorem | xrge0slmod 33303 | The extended nonnegative real numbers form a semiring left module. One could also have used subringAlg to get the same structure. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) & ⊢ 𝑊 = (𝐺 ↾v (0[,)+∞)) ⇒ ⊢ 𝑊 ∈ SLMod | ||
| Theorem | qusker 33304* | The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑉 = (Base‘𝑀) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺)) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ 0 = (0g‘𝑁) ⇒ ⊢ (𝐺 ∈ (NrmSGrp‘𝑀) → (◡𝐹 “ { 0 }) = 𝐺) | ||
| Theorem | eqgvscpbl 33305 | The left coset equivalence relation is compatible with the scalar multiplication operation. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ∼ = (𝑀 ~QG 𝐺) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋 ∼ 𝑌 → (𝐾 · 𝑋) ∼ (𝐾 · 𝑌))) | ||
| Theorem | qusvscpbl 33306* | The quotient map distributes over the scalar multiplication. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ∼ = (𝑀 ~QG 𝐺) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ ∙ = ( ·𝑠 ‘𝑁) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝑀 ~QG 𝐺)) & ⊢ (𝜑 → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → 𝑉 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝐹‘𝑈) = (𝐹‘𝑉) → (𝐹‘(𝐾 · 𝑈)) = (𝐹‘(𝐾 · 𝑉)))) | ||
| Theorem | qusvsval 33307 | Value of the scalar multiplication operation on the quotient structure. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ∼ = (𝑀 ~QG 𝐺) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ (𝜑 → 𝐾 ∈ 𝑆) & ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ ∙ = ( ·𝑠 ‘𝑁) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐾 ∙ [𝑋](𝑀 ~QG 𝐺)) = [(𝐾 · 𝑋)](𝑀 ~QG 𝐺)) | ||
| Theorem | imaslmod 33308* | The image structure of a left module is a left module. (Contributed by Thierry Arnoux, 15-May-2023.) |
| ⊢ (𝜑 → 𝑁 = (𝐹 “s 𝑀)) & ⊢ 𝑉 = (Base‘𝑀) & ⊢ 𝑆 = (Base‘(Scalar‘𝑀)) & ⊢ + = (+g‘𝑀) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝑆 ∧ 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → (𝐹‘(𝑘 · 𝑎)) = (𝐹‘(𝑘 · 𝑏)))) & ⊢ (𝜑 → 𝑀 ∈ LMod) ⇒ ⊢ (𝜑 → 𝑁 ∈ LMod) | ||
| Theorem | imasmhm 33309* | Given a function 𝐹 with homomorphic properties, build the image of a monoid. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ + = (+g‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ (𝜑 → 𝑊 ∈ Mnd) ⇒ ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ Mnd ∧ 𝐹 ∈ (𝑊 MndHom (𝐹 “s 𝑊)))) | ||
| Theorem | imasghm 33310* | Given a function 𝐹 with homomorphic properties, build the image of a group. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ + = (+g‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ (𝜑 → 𝑊 ∈ Grp) ⇒ ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ Grp ∧ 𝐹 ∈ (𝑊 GrpHom (𝐹 “s 𝑊)))) | ||
| Theorem | imasrhm 33311* | Given a function 𝐹 with homomorphic properties, build the image of a ring. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ + = (+g‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ · = (.r‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → 𝑊 ∈ Ring) ⇒ ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ Ring ∧ 𝐹 ∈ (𝑊 RingHom (𝐹 “s 𝑊)))) | ||
| Theorem | imaslmhm 33312* | Given a function 𝐹 with homomorphic properties, build the image of a left module. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ + = (+g‘𝑊) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) ∧ (𝑝 ∈ 𝐵 ∧ 𝑞 ∈ 𝐵)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ 𝐷 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐷) & ⊢ ((𝜑 ∧ (𝑘 ∈ 𝐾 ∧ 𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → (𝐹‘(𝑘 × 𝑎)) = (𝐹‘(𝑘 × 𝑏)))) & ⊢ (𝜑 → 𝑊 ∈ LMod) & ⊢ × = ( ·𝑠 ‘𝑊) ⇒ ⊢ (𝜑 → ((𝐹 “s 𝑊) ∈ LMod ∧ 𝐹 ∈ (𝑊 LMHom (𝐹 “s 𝑊)))) | ||
| Theorem | quslmod 33313 | If 𝐺 is a submodule in 𝑀, then 𝑁 = 𝑀 / 𝐺 is a left module, called the quotient module of 𝑀 by 𝐺. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ 𝑉 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) ⇒ ⊢ (𝜑 → 𝑁 ∈ LMod) | ||
| Theorem | quslmhm 33314* | If 𝐺 is a submodule of 𝑀, then the "natural map" from elements to their cosets is a left module homomorphism from 𝑀 to 𝑀 / 𝐺. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝑁 = (𝑀 /s (𝑀 ~QG 𝐺)) & ⊢ 𝑉 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝐺 ∈ (LSubSp‘𝑀)) & ⊢ 𝐹 = (𝑥 ∈ 𝑉 ↦ [𝑥](𝑀 ~QG 𝐺)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑀 LMHom 𝑁)) | ||
| Theorem | quslvec 33315 | If 𝑆 is a vector subspace in 𝑊, then 𝑄 = 𝑊 / 𝑆 is a vector space, called the quotient space of 𝑊 by 𝑆. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝑄 = (𝑊 /s (𝑊 ~QG 𝑆)) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑆 ∈ (LSubSp‘𝑊)) ⇒ ⊢ (𝜑 → 𝑄 ∈ LVec) | ||
| Theorem | ecxpid 33316 | The equivalence class of a cartesian product is the whole set. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| ⊢ (𝑋 ∈ 𝐴 → [𝑋](𝐴 × 𝐴) = 𝐴) | ||
| Theorem | qsxpid 33317 | The quotient set of a cartesian product is trivial. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ (𝐴 ≠ ∅ → (𝐴 / (𝐴 × 𝐴)) = {𝐴}) | ||
| Theorem | qusxpid 33318 | The Group quotient equivalence relation for the whole group is the cartesian product, i.e. all elements are in the same equivalence class. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (𝐺 ~QG 𝐵) = (𝐵 × 𝐵)) | ||
| Theorem | qustriv 33319 | The quotient of a group 𝐺 by itself is trivial. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐵)) ⇒ ⊢ (𝐺 ∈ Grp → (Base‘𝑄) = {𝐵}) | ||
| Theorem | qustrivr 33320 | Converse of qustriv 33319. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐻)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ (SubGrp‘𝐺) ∧ (Base‘𝑄) = {𝐻}) → 𝐻 = 𝐵) | ||
| Theorem | znfermltl 33321 | Fermat's little theorem in ℤ/nℤ. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| ⊢ 𝑍 = (ℤ/nℤ‘𝑃) & ⊢ 𝐵 = (Base‘𝑍) & ⊢ ↑ = (.g‘(mulGrp‘𝑍)) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝐴 ∈ 𝐵) → (𝑃 ↑ 𝐴) = 𝐴) | ||
| Theorem | islinds5 33322* | A set is linearly independent if and only if it has no non-trivial representations of zero. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑂 = (0g‘𝑊) & ⊢ 0 = (0g‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑉 ⊆ 𝐵) → (𝑉 ∈ (LIndS‘𝑊) ↔ ∀𝑎 ∈ (𝐾 ↑m 𝑉)((𝑎 finSupp 0 ∧ (𝑊 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣))) = 𝑂) → 𝑎 = (𝑉 × { 0 })))) | ||
| Theorem | ellspds 33323* | Variation on ellspd 21732. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ 𝑁 = (LSpan‘𝑀) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 𝑆 = (Scalar‘𝑀) & ⊢ 0 = (0g‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ LMod) & ⊢ (𝜑 → 𝑉 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝑉) ↔ ∃𝑎 ∈ (𝐾 ↑m 𝑉)(𝑎 finSupp 0 ∧ 𝑋 = (𝑀 Σg (𝑣 ∈ 𝑉 ↦ ((𝑎‘𝑣) · 𝑣)))))) | ||
| Theorem | 0ellsp 33324 | Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023.) |
| ⊢ 0 = (0g‘𝑊) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑆 ⊆ 𝐵) → 0 ∈ (𝑁‘𝑆)) | ||
| Theorem | 0nellinds 33325 | The group identity cannot be an element of an independent set. (Contributed by Thierry Arnoux, 8-May-2023.) |
| ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐹 ∈ (LIndS‘𝑊)) → ¬ 0 ∈ 𝐹) | ||
| Theorem | rspsnid 33326 | A principal ideal contains the element that generates it. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐺 ∈ 𝐵) → 𝐺 ∈ (𝐾‘{𝐺})) | ||
| Theorem | elrsp 33327* | Write the elements of a ring span as finite linear combinations. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝑁 = (RSpan‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑁‘𝐼) ↔ ∃𝑎 ∈ (𝐵 ↑m 𝐼)(𝑎 finSupp 0 ∧ 𝑋 = (𝑅 Σg (𝑖 ∈ 𝐼 ↦ ((𝑎‘𝑖) · 𝑖)))))) | ||
| Theorem | ellpi 33328 | 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 33329* | In a principal ideal ring, ideals are principal. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ LPIR) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝐽 = (𝐾‘{𝑥})) | ||
| Theorem | rspidlid 33330 | The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈) → (𝐾‘𝐼) = 𝐼) | ||
| Theorem | pidlnz 33331 | 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 33332* | 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 33333 | 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 33334 | 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 33335* | 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 33336 | 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 33337* | 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 33338* | 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 33339 | 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 33340* | 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 33341* | A reformulation of dvdsruasso 33340. (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 33342 | 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 33343 | 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 33344 | 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 33345* | Membership in a sumset with a singleton for a group operation. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝐴 ⊕ {𝑋}) ↔ ∃𝑥 ∈ 𝐴 𝑍 = (𝑥 + 𝑋))) | ||
| Theorem | lsmsnorb 33346* | The sumset of a group with a single element is the element's orbit by the group action. See gaorb 19212. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ ∃𝑔 ∈ 𝐴 (𝑔 + 𝑥) = 𝑦)} & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐴 ⊕ {𝑋}) = [𝑋] ∼ ) | ||
| Theorem | lsmsnorb2 33347* | The sumset of a single element with a group is the element's orbit by the group action. See gaorb 19212. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝐵 ∧ ∃𝑔 ∈ 𝐴 (𝑥 + 𝑔) = 𝑦)} & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ({𝑋} ⊕ 𝐴) = [𝑋] ∼ ) | ||
| Theorem | elringlsm 33348* | Membership in a product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑍 ∈ (𝐸 × 𝐹) ↔ ∃𝑥 ∈ 𝐸 ∃𝑦 ∈ 𝐹 𝑍 = (𝑥 · 𝑦))) | ||
| Theorem | elringlsmd 33349 | 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 33350 | Closure of the product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ × = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐸 ⊆ 𝐵) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝐸 × 𝐹) ⊆ 𝐵) | ||
| Theorem | ringlsmss1 33351 | 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 33352 | 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 33353 | 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 33354 | 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 33355 | 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 33356 | The sum of two ideals is an ideal. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ ⊕ = (LSSum‘𝑅) & ⊢ 𝐾 = (RSpan‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) & ⊢ (𝜑 → 𝐽 ∈ (LIdeal‘𝑅)) ⇒ ⊢ (𝜑 → (𝐼 ⊕ 𝐽) ∈ (LIdeal‘𝑅)) | ||
| Theorem | lsmssass 33357 | Group sum is associative, subset version (see lsmass 19574). (Contributed by Thierry Arnoux, 1-Jun-2024.) |
| ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑅 ⊆ 𝐵) & ⊢ (𝜑 → 𝑇 ⊆ 𝐵) & ⊢ (𝜑 → 𝑈 ⊆ 𝐵) ⇒ ⊢ (𝜑 → ((𝑅 ⊕ 𝑇) ⊕ 𝑈) = (𝑅 ⊕ (𝑇 ⊕ 𝑈))) | ||
| Theorem | grplsm0l 33358 | Sumset with the identity singleton is the original set. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ⊆ 𝐵 ∧ 𝐴 ≠ ∅) → ({ 0 } ⊕ 𝐴) = 𝐴) | ||
| Theorem | grplsmid 33359 | The direct sum of an element 𝑋 of a subgroup 𝐴 is the subgroup itself. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐴 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝐴) → ({𝑋} ⊕ 𝐴) = 𝐴) | ||
| Theorem | quslsm 33360 | 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 33361* | 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 33362 | The identity element of a quotient group. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
| ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) ⇒ ⊢ (𝑁 ∈ (NrmSGrp‘𝐺) → (0g‘𝑄) = 𝑁) | ||
| Theorem | qusima 33363* | 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 33364* | The natural map from elements to their cosets is surjective. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑈 = (𝐵 / (𝐺 ~QG 𝑁)) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝐺 ~QG 𝑁)) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → ran 𝐹 = 𝑈) | ||
| Theorem | nsgqus0 33365 | 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 33366* | Lemma for nsgmgc 33367. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) & ⊢ (𝜑 → 𝐹 ∈ (SubGrp‘𝑄)) ⇒ ⊢ (𝜑 → {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝐹} ∈ (SubGrp‘𝐺)) | ||
| Theorem | nsgmgc 33367* | 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 33368* | Lemma for nsgqusf1o 33371. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} & ⊢ 𝑇 = (SubGrp‘𝑄) & ⊢ ≤ = (le‘(toInc‘𝑆)) & ⊢ ≲ = (le‘(toInc‘𝑇)) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (((𝜑 ∧ ℎ ∈ (SubGrp‘𝐺)) ∧ 𝑁 ⊆ ℎ) → ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁)) ∈ 𝑇) | ||
| Theorem | nsgqusf1olem2 33369* | Lemma for nsgqusf1o 33371. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} & ⊢ 𝑇 = (SubGrp‘𝑄) & ⊢ ≤ = (le‘(toInc‘𝑆)) & ⊢ ≲ = (le‘(toInc‘𝑇)) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → ran 𝐸 = 𝑇) | ||
| Theorem | nsgqusf1olem3 33370* | Lemma for nsgqusf1o 33371. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = {ℎ ∈ (SubGrp‘𝐺) ∣ 𝑁 ⊆ ℎ} & ⊢ 𝑇 = (SubGrp‘𝑄) & ⊢ ≤ = (le‘(toInc‘𝑆)) & ⊢ ≲ = (le‘(toInc‘𝑇)) & ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐸 = (ℎ ∈ 𝑆 ↦ ran (𝑥 ∈ ℎ ↦ ({𝑥} ⊕ 𝑁))) & ⊢ 𝐹 = (𝑓 ∈ 𝑇 ↦ {𝑎 ∈ 𝐵 ∣ ({𝑎} ⊕ 𝑁) ∈ 𝑓}) & ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → ran 𝐹 = 𝑆) | ||
| Theorem | nsgqusf1o 33371* | 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 33372* | 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 33373 | 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 33374 | 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 33375 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Thierry Arnoux, 8-Jun-2024.) |
| ⊢ ((𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (LIdeal‘𝑅)) → ∩ 𝐶 ∈ (LIdeal‘𝑅)) | ||
| Theorem | 0ringidl 33376 | 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 33377 | 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 33378 | 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 33379 | 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 33380* | 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 33381* | 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 33382 | 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 33383* | 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 33384* | 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 33385 | Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024.) |
| ⊢ 𝑈 = (LIdeal‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝐽 ∈ 𝑈) → (𝐼 ∩ 𝐽) ∈ 𝑈) | ||
| Theorem | idlinsubrg 33386 | 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 33387 | 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 33388 | 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 33389 | 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 33390 | Extend class notation with the class of prime ideals. |
| class PrmIdeal | ||
| Definition | df-prmidl 33391* | 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 33396 and isprmidlc 33402. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 14-Jan-2024.) |
| ⊢ PrmIdeal = (𝑟 ∈ Ring ↦ {𝑖 ∈ (LIdeal‘𝑟) ∣ (𝑖 ≠ (Base‘𝑟) ∧ ∀𝑎 ∈ (LIdeal‘𝑟)∀𝑏 ∈ (LIdeal‘𝑟)(∀𝑥 ∈ 𝑎 ∀𝑦 ∈ 𝑏 (𝑥(.r‘𝑟)𝑦) ∈ 𝑖 → (𝑎 ⊆ 𝑖 ∨ 𝑏 ⊆ 𝑖)))}) | ||
| Theorem | prmidlval 33392* | 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 33393* | 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 33394 | 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 33395* | 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 33396* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 38089 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 33397 | 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 33398 | A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅) ∧ 𝐼 ≠ 𝐵) → ¬ 1 ∈ 𝐼) | ||
| Theorem | prmidlidl 33399 | 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 33400 | Prime ideals as a subset of ideals. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) ⊆ (LIdeal‘𝑅)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |