| Metamath
Proof Explorer Theorem List (p. 202 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 | ||
| Theorem | pgpfaclem1 20101* | Lemma for pgpfac 20104. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) & ⊢ 𝐻 = (𝐺 ↾s 𝑈) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻)) & ⊢ 𝑂 = (od‘𝐻) & ⊢ 𝐸 = (gEx‘𝐻) & ⊢ 0 = (0g‘𝐻) & ⊢ ⊕ = (LSSum‘𝐻) & ⊢ (𝜑 → 𝐸 ≠ 1) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → (𝑂‘𝑋) = 𝐸) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻)) & ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) & ⊢ (𝜑 → 𝑆 ∈ Word 𝐶) & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝑊) & ⊢ 𝑇 = (𝑆 ++ 〈“(𝐾‘{𝑋})”〉) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) | ||
| Theorem | pgpfaclem2 20102* | Lemma for pgpfac 20104. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) & ⊢ 𝐻 = (𝐺 ↾s 𝑈) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻)) & ⊢ 𝑂 = (od‘𝐻) & ⊢ 𝐸 = (gEx‘𝐻) & ⊢ 0 = (0g‘𝐻) & ⊢ ⊕ = (LSSum‘𝐻) & ⊢ (𝜑 → 𝐸 ≠ 1) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → (𝑂‘𝑋) = 𝐸) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻)) & ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) | ||
| Theorem | pgpfaclem3 20103* | Lemma for pgpfac 20104. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) | ||
| Theorem | pgpfac 20104* | Full factorization of a finite abelian p-group, by iterating pgpfac1 20100. There is a direct product decomposition of any abelian group of prime-power order into cyclic subgroups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) | ||
| Theorem | ablfaclem1 20105* | Lemma for ablfac 20108. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) ⇒ ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝑊‘𝑈) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)}) | ||
| Theorem | ablfaclem2 20106* | Lemma for ablfac 20108. (Contributed by Mario Carneiro, 27-Apr-2016.) (Proof shortened by Mario Carneiro, 3-May-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) & ⊢ (𝜑 → 𝐹:𝐴⟶Word 𝐶) & ⊢ (𝜑 → ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) ∈ (𝑊‘(𝑆‘𝑦))) & ⊢ 𝐿 = ∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝐹‘𝑦)) & ⊢ (𝜑 → 𝐻:(0..^(♯‘𝐿))–1-1-onto→𝐿) ⇒ ⊢ (𝜑 → (𝑊‘𝐵) ≠ ∅) | ||
| Theorem | ablfaclem3 20107* | Lemma for ablfac 20108. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) ⇒ ⊢ (𝜑 → (𝑊‘𝐵) ≠ ∅) | ||
| Theorem | ablfac 20108* | The Fundamental Theorem of (finite) Abelian Groups. Any finite abelian group is a direct product of cyclic p-groups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) | ||
| Theorem | ablfac2 20109* | Choose generators for each cyclic group in ablfac 20108. (Contributed by Mario Carneiro, 28-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ · = (.g‘𝐺) & ⊢ 𝑆 = (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤‘𝑘)))) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ Word 𝐵(𝑆:dom 𝑤⟶𝐶 ∧ 𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵)) | ||
| Syntax | csimpg 20110 | Extend class notation with the class of simple groups. |
| class SimpGrp | ||
| Definition | df-simpg 20111 | Define class of all simple groups. A simple group is a group (df-grp 18954) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 20123). (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o} | ||
| Theorem | issimpg 20112 | The predicate "is a simple group". (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝐺 ∈ SimpGrp ↔ (𝐺 ∈ Grp ∧ (NrmSGrp‘𝐺) ≈ 2o)) | ||
| Theorem | issimpgd 20113 | Deduce a simple group from its properties. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 2o) ⇒ ⊢ (𝜑 → 𝐺 ∈ SimpGrp) | ||
| Theorem | simpggrp 20114 | A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝐺 ∈ SimpGrp → 𝐺 ∈ Grp) | ||
| Theorem | simpggrpd 20115 | A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
| Theorem | simpg2nsg 20116 | A simple group has two normal subgroups. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝐺 ∈ SimpGrp → (NrmSGrp‘𝐺) ≈ 2o) | ||
| Theorem | trivnsimpgd 20117 | Trivial groups are not simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = { 0 }) ⇒ ⊢ (𝜑 → ¬ 𝐺 ∈ SimpGrp) | ||
| Theorem | simpgntrivd 20118 | Simple groups are nontrivial. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → ¬ 𝐵 = { 0 }) | ||
| Theorem | simpgnideld 20119* | A simple group contains a nonidentity element. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ¬ 𝑥 = 0 ) | ||
| Theorem | simpgnsgd 20120 | The only normal subgroups of a simple group are the group itself and the trivial group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → (NrmSGrp‘𝐺) = {{ 0 }, 𝐵}) | ||
| Theorem | simpgnsgeqd 20121 | A normal subgroup of a simple group is either the whole group or the trivial subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) & ⊢ (𝜑 → 𝐴 ∈ (NrmSGrp‘𝐺)) ⇒ ⊢ (𝜑 → (𝐴 = { 0 } ∨ 𝐴 = 𝐵)) | ||
| Theorem | 2nsgsimpgd 20122* | If any normal subgroup of a nontrivial group is either the trivial subgroup or the whole group, the group is simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → ¬ { 0 } = 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ (NrmSGrp‘𝐺)) → (𝑥 = { 0 } ∨ 𝑥 = 𝐵)) ⇒ ⊢ (𝜑 → 𝐺 ∈ SimpGrp) | ||
| Theorem | simpgnsgbid 20123 | A nontrivial group is simple if and only if its normal subgroups are exactly the group itself and the trivial subgroup. (Contributed by Rohan Ridenour, 4-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → ¬ { 0 } = 𝐵) ⇒ ⊢ (𝜑 → (𝐺 ∈ SimpGrp ↔ (NrmSGrp‘𝐺) = {{ 0 }, 𝐵})) | ||
| Theorem | ablsimpnosubgd 20124 | A subgroup of an abelian simple group containing a nonidentity element is the whole group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → ¬ 𝐴 = 0 ) ⇒ ⊢ (𝜑 → 𝑆 = 𝐵) | ||
| Theorem | ablsimpg1gend 20125* | An abelian simple group is generated by any non-identity element. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ¬ 𝐴 = 0 ) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ ℤ 𝐶 = (𝑛 · 𝐴)) | ||
| Theorem | ablsimpgcygd 20126 | An abelian simple group is cyclic. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof shortened by Rohan Ridenour, 31-Oct-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → 𝐺 ∈ CycGrp) | ||
| Theorem | ablsimpgfindlem1 20127* | Lemma for ablsimpgfind 20130. An element of an abelian finite simple group which doesn't square to the identity has finite order. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof shortened by Rohan Ridenour, 31-Oct-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (2 · 𝑥) ≠ 0 ) → (𝑂‘𝑥) ≠ 0) | ||
| Theorem | ablsimpgfindlem2 20128* | Lemma for ablsimpgfind 20130. An element of an abelian finite simple group which squares to the identity has finite order. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (2 · 𝑥) = 0 ) → (𝑂‘𝑥) ≠ 0) | ||
| Theorem | cycsubggenodd 20129* | Relationship between the order of a subgroup and the order of a generator of the subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 = ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴))) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) = if(𝐶 ∈ Fin, (♯‘𝐶), 0)) | ||
| Theorem | ablsimpgfind 20130 | An abelian simple group is finite. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → 𝐵 ∈ Fin) | ||
| Theorem | fincygsubgd 20131* | The subgroup referenced in fincygsubgodd 20132 is a subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐻 = (𝑛 ∈ ℤ ↦ (𝑛 · (𝐶 · 𝐴))) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝐶 ∈ ℕ) ⇒ ⊢ (𝜑 → ran 𝐻 ∈ (SubGrp‘𝐺)) | ||
| Theorem | fincygsubgodd 20132* | Calculate the order of a subgroup of a finite cyclic group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐷 = ((♯‘𝐵) / 𝐶) & ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴)) & ⊢ 𝐻 = (𝑛 ∈ ℤ ↦ (𝑛 · (𝐶 · 𝐴))) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ (𝜑 → ran 𝐹 = 𝐵) & ⊢ (𝜑 → 𝐶 ∥ (♯‘𝐵)) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ ℕ) ⇒ ⊢ (𝜑 → (♯‘ran 𝐻) = 𝐷) | ||
| Theorem | fincygsubgodexd 20133* | A finite cyclic group has subgroups of every possible order. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CycGrp) & ⊢ (𝜑 → 𝐶 ∥ (♯‘𝐵)) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ ℕ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ (SubGrp‘𝐺)(♯‘𝑥) = 𝐶) | ||
| Theorem | prmgrpsimpgd 20134 | A group of prime order is simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ) ⇒ ⊢ (𝜑 → 𝐺 ∈ SimpGrp) | ||
| Theorem | ablsimpgprmd 20135 | An abelian simple group has prime order. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → (♯‘𝐵) ∈ ℙ) | ||
| Theorem | ablsimpgd 20136 | An abelian group is simple if and only if its order is prime. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) ⇒ ⊢ (𝜑 → (𝐺 ∈ SimpGrp ↔ (♯‘𝐵) ∈ ℙ)) | ||
| Syntax | cmgp 20137 | Multiplicative group. |
| class mulGrp | ||
| Definition | df-mgp 20138 | Define a structure that puts the multiplication operation of a ring in the addition slot. Note that this will not actually be a group for the average ring, or even for a field, but it will be a monoid, and unitgrp 20383 shows that we get a group if we restrict to the elements that have inverses. This allows to formalize such notions as "the multiplication operation of a ring is a monoid" (ringmgp 20236) or "the multiplicative identity" in terms of the identity of a monoid (df-ur 20179). (Contributed by Mario Carneiro, 21-Dec-2014.) |
| ⊢ mulGrp = (𝑤 ∈ V ↦ (𝑤 sSet 〈(+g‘ndx), (.r‘𝑤)〉)) | ||
| Theorem | fnmgp 20139 | The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.) |
| ⊢ mulGrp Fn V | ||
| Theorem | mgpval 20140 | Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ 𝑀 = (𝑅 sSet 〈(+g‘ndx), · 〉) | ||
| Theorem | mgpplusg 20141 | Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ · = (+g‘𝑀) | ||
| Theorem | mgpbas 20142 | Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐵 = (Base‘𝑀) | ||
| Theorem | mgpsca 20143 | The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 20324. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑆 = (Scalar‘𝑅) ⇒ ⊢ 𝑆 = (Scalar‘𝑀) | ||
| Theorem | mgptset 20144 | Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (TopSet‘𝑅) = (TopSet‘𝑀) | ||
| Theorem | mgptopn 20145 | Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑅) ⇒ ⊢ 𝐽 = (TopOpen‘𝑀) | ||
| Theorem | mgpds 20146 | Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
| ⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐵 = (dist‘𝑅) ⇒ ⊢ 𝐵 = (dist‘𝑀) | ||
| Theorem | mgpress 20147 | Subgroup commutes with the multiplicative group operator. (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof shortened by AV, 18-Oct-2024.) |
| ⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑀 ↾s 𝐴) = (mulGrp‘𝑆)) | ||
| Theorem | prdsmgp 20148 | The multiplicative monoid of a product is the product of the multiplicative monoids of the factors. (Contributed by Mario Carneiro, 11-Mar-2015.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝑀 = (mulGrp‘𝑌) & ⊢ 𝑍 = (𝑆Xs(mulGrp ∘ 𝑅)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 Fn 𝐼) ⇒ ⊢ (𝜑 → ((Base‘𝑀) = (Base‘𝑍) ∧ (+g‘𝑀) = (+g‘𝑍))) | ||
According to Wikipedia, "... in abstract algebra, a rng (or non-unital ring or pseudo-ring) is an algebraic structure satisfying the same properties as a [unital] ring, without assuming the existence of a multiplicative identity. The term "rng" (pronounced rung) is meant to suggest that it is a "ring" without "i", i.e. without the requirement for an "identity element"." (see https://en.wikipedia.org/wiki/Rng_(algebra), 28-Mar-2025). | ||
| Syntax | crng 20149 | Extend class notation with class of all non-unital rings. |
| class Rng | ||
| Definition | df-rng 20150* | Define the class of all non-unital rings. A non-unital ring (or rng, or pseudoring) is a set equipped with two everywhere-defined internal operations, whose first one is an additive abelian group operation and the second one is a multiplicative semigroup operation, and where the addition is left- and right-distributive for the multiplication. Definition of a pseudo-ring in section I.8.1 of [BourbakiAlg1] p. 93 or the definition of a ring in part Preliminaries of [Roman] p. 18. As almost always in mathematics, "non-unital" means "not necessarily unital". Therefore, by talking about a ring (in general) or a non-unital ring the "unital" case is always included. In contrast to a unital ring, the commutativity of addition must be postulated and cannot be proven from the other conditions. (Contributed by AV, 6-Jan-2020.) |
| ⊢ Rng = {𝑓 ∈ Abel ∣ ((mulGrp‘𝑓) ∈ Smgrp ∧ [(Base‘𝑓) / 𝑏][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))} | ||
| Theorem | isrng 20151* | The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ 𝐺 ∈ Smgrp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) | ||
| Theorem | rngabl 20152 | A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.) |
| ⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel) | ||
| Theorem | rngmgp 20153 | A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020.) |
| ⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → 𝐺 ∈ Smgrp) | ||
| Theorem | rngmgpf 20154 | Restricted functionality of the multiplicative group on non-unital rings (mgpf 20245 analog). (Contributed by AV, 22-Feb-2025.) |
| ⊢ (mulGrp ↾ Rng):Rng⟶Smgrp | ||
| Theorem | rnggrp 20155 | A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.) |
| ⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp) | ||
| Theorem | rngass 20156 | Associative law for the multiplication operation of a non-unital ring. (Contributed by NM, 27-Aug-2011.) (Revised by AV, 13-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 · 𝑌) · 𝑍) = (𝑋 · (𝑌 · 𝑍))) | ||
| Theorem | rngdi 20157 | Distributive law for the multiplication operation of a non-unital ring (left-distributivity). (Contributed by AV, 14-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍))) | ||
| Theorem | rngdir 20158 | Distributive law for the multiplication operation of a non-unital ring (right-distributivity). (Contributed by AV, 17-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) | ||
| Theorem | rngacl 20159 | Closure of the addition operation of a non-unital ring. (Contributed by AV, 16-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) | ||
| Theorem | rng0cl 20160 | The zero element of a non-unital ring belongs to its base set. (Contributed by AV, 16-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Rng → 0 ∈ 𝐵) | ||
| Theorem | rngcl 20161 | Closure of the multiplication operation of a non-unital ring. (Contributed by AV, 17-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵) | ||
| Theorem | rnglz 20162 | The zero of a non-unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringlz 20290. (Revised by AV, 17-Apr-2020.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 ) | ||
| Theorem | rngrz 20163 | The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringrz 20291. (Revised by AV, 16-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Rng ∧ 𝑋 ∈ 𝐵) → (𝑋 · 0 ) = 0 ) | ||
| Theorem | rngmneg1 20164 | Negation of a product in a non-unital ring (mulneg1 11699 analog). In contrast to ringmneg1 20301, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) · 𝑌) = (𝑁‘(𝑋 · 𝑌))) | ||
| Theorem | rngmneg2 20165 | Negation of a product in a non-unital ring (mulneg2 11700 analog). In contrast to ringmneg2 20302, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑁‘𝑌)) = (𝑁‘(𝑋 · 𝑌))) | ||
| Theorem | rngm2neg 20166 | Double negation of a product in a non-unital ring (mul2neg 11702 analog). (Contributed by Mario Carneiro, 4-Dec-2014.) Generalization of ringm2neg 20303. (Revised by AV, 17-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑁 = (invg‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) · (𝑁‘𝑌)) = (𝑋 · 𝑌)) | ||
| Theorem | rngansg 20167 | Every additive subgroup of a non-unital ring is normal. (Contributed by AV, 25-Feb-2025.) |
| ⊢ (𝑅 ∈ Rng → (NrmSGrp‘𝑅) = (SubGrp‘𝑅)) | ||
| Theorem | rngsubdi 20168 | Ring multiplication distributes over subtraction. (subdi 11696 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdi 20304. (Revised by AV, 23-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 · (𝑌 − 𝑍)) = ((𝑋 · 𝑌) − (𝑋 · 𝑍))) | ||
| Theorem | rngsubdir 20169 | Ring multiplication distributes over subtraction. (subdir 11697 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.) Generalization of ringsubdir 20305. (Revised by AV, 23-Feb-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Rng) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) · 𝑍) = ((𝑋 · 𝑍) − (𝑌 · 𝑍))) | ||
| Theorem | isrngd 20170* | Properties that determine a non-unital ring. (Contributed by AV, 14-Feb-2025.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → + = (+g‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Abel) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 · 𝑦) · 𝑧) = (𝑥 · (𝑦 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → (𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧))) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ⇒ ⊢ (𝜑 → 𝑅 ∈ Rng) | ||
| Theorem | rngpropd 20171* | If two structures have the same base set, and the values of their group (addition) and ring (multiplication) operations are equal for all pairs of elements of the base set, one is a non-unital ring iff the other one is. (Contributed by AV, 15-Feb-2025.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(.r‘𝐾)𝑦) = (𝑥(.r‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ Rng ↔ 𝐿 ∈ Rng)) | ||
| Theorem | prdsmulrngcl 20172 | Closure of the multiplication in a structure product of non-unital rings. (Contributed by Mario Carneiro, 11-Mar-2015.) Generalization of prdsmulrcl 20317. (Revised by AV, 21-Feb-2025.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ · = (.r‘𝑌) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑅:𝐼⟶Rng) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹 · 𝐺) ∈ 𝐵) | ||
| Theorem | prdsrngd 20173 | A product of non-unital rings is a non-unital ring. (Contributed by AV, 22-Feb-2025.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Rng) ⇒ ⊢ (𝜑 → 𝑌 ∈ Rng) | ||
| Theorem | imasrng 20174* | The image structure of a non-unital ring is a non-unital ring (imasring 20327 analog). (Contributed by AV, 22-Feb-2025.) |
| ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 · 𝑏)) = (𝐹‘(𝑝 · 𝑞)))) & ⊢ (𝜑 → 𝑅 ∈ Rng) ⇒ ⊢ (𝜑 → 𝑈 ∈ Rng) | ||
| Theorem | imasrngf1 20175 | The image of a non-unital ring under an injection is a non-unital ring (imasmndf1 18789 analog). (Contributed by AV, 22-Feb-2025.) |
| ⊢ 𝑈 = (𝐹 “s 𝑅) & ⊢ 𝑉 = (Base‘𝑅) ⇒ ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ 𝑅 ∈ Rng) → 𝑈 ∈ Rng) | ||
| Theorem | xpsrngd 20176 | A product of two non-unital rings is a non-unital ring (xpsmnd 18790 analog). (Contributed by AV, 22-Feb-2025.) |
| ⊢ 𝑌 = (𝑆 ×s 𝑅) & ⊢ (𝜑 → 𝑆 ∈ Rng) & ⊢ (𝜑 → 𝑅 ∈ Rng) ⇒ ⊢ (𝜑 → 𝑌 ∈ Rng) | ||
| Theorem | qusrng 20177* | The quotient structure of a non-unital ring is a non-unital ring (qusring2 20331 analog). (Contributed by AV, 23-Feb-2025.) |
| ⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ )) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → ∼ Er 𝑉) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞))) & ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 · 𝑏) ∼ (𝑝 · 𝑞))) & ⊢ (𝜑 → 𝑅 ∈ Rng) ⇒ ⊢ (𝜑 → 𝑈 ∈ Rng) | ||
In Wikipedia "Identity element", see https://en.wikipedia.org/wiki/Identity_element (18-Jan-2025): "... an identity with respect to multiplication is called a multiplicative identity (often denoted as 1). ... The distinction between additive and multiplicative identity is used most often for sets that support both binary operations, such as rings, integral domains, and fields. The multiplicative identity is often called unity in the latter context (a ring with unity). This should not be confused with a unit in ring theory, which is any element having a multiplicative inverse. By its own definition, unity itself is necessarily a unit." Calling the multiplicative identity of a ring a unity is taken from the definition of a ring with unity in section 17.3 of [BeauregardFraleigh] p. 135, "A ring ( R , + , . ) is a ring with unity if R is not the zero ring and ( R , . ) is a monoid. In this case, the identity element of ( R , . ) is denoted by 1 and is called the unity of R." This definition of a "ring with unity" corresponds to our definition of a unital ring (see df-ring 20232). Some authors call the multiplicative identity "unit" or "unit element" (for example in section I, 2.2 of [BourbakiAlg1] p. 14, definition in section 1.3 of [Hall] p. 4, or in section I, 1 of [Lang] p. 3), whereas other authors use the term "unit" for an element having a multiplicative inverse (for example in section 17.3 of [BeauregardFraleigh] p. 135, in definition in [Roman] p. 26, or even in section II, 1 of [Lang] p. 84). Sometimes, the multiplicative identity is simply called "one" (see, for example, chapter 8 in [Schechter] p. 180). To avoid this ambiguity of the term "unit", also mentioned in Wikipedia, we call the multiplicative identity of a structure with a multiplication (usually a ring) a "ring unity", or straightly "multiplicative identity". The term "unit" will be used for an element having a multiplicative inverse (see df-unit 20358), and we have "the ring unity is a unit", see 1unit 20374. | ||
| Syntax | cur 20178 | Extend class notation with ring unity. |
| class 1r | ||
| Definition | df-ur 20179 |
Define the multiplicative identity, i.e., the monoid identity (df-0g 17486)
of the multiplicative monoid (df-mgp 20138) of a ring-like structure. This
multiplicative identity is also called "ring unity" or
"unity element".
This definition works by transferring the multiplicative operation from the .r slot to the +g slot and then looking at the element which is then the 0g element, that is an identity with respect to the operation which started out in the .r slot. See also dfur2 20181, which derives the "traditional" definition as the unique element of a ring which is left- and right-neutral under multiplication. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
| ⊢ 1r = (0g ∘ mulGrp) | ||
| Theorem | ringidval 20180 | The value of the unity element of a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
| ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ 1 = (0g‘𝐺) | ||
| Theorem | dfur2 20181* | The multiplicative identity is the unique element of the ring that is left- and right-neutral on all elements under multiplication. (Contributed by Mario Carneiro, 10-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ 1 = (℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 · 𝑥) = 𝑥 ∧ (𝑥 · 𝑒) = 𝑥))) | ||
| Theorem | ringurd 20182* | Deduce the unity element of a ring from its properties. (Contributed by Thierry Arnoux, 6-Sep-2016.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝑅)) & ⊢ (𝜑 → · = (.r‘𝑅)) & ⊢ (𝜑 → 1 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 1 · 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 · 1 ) = 𝑥) ⇒ ⊢ (𝜑 → 1 = (1r‘𝑅)) | ||
| Syntax | csrg 20183 | Extend class notation with the class of all semirings. |
| class SRing | ||
| Definition | df-srg 20184* | Define class of all semirings. A semiring is a set equipped with two everywhere-defined internal operations, whose first one is an additive commutative monoid structure and the second one is a multiplicative monoid structure, and where multiplication is (left- and right-) distributive over addition. Like with rings (df-ring 20232), the additive identity is an absorbing element of the multiplicative law, but in the case of semirings, this has to be part of the definition, as it cannot be deduced from distributivity alone. Definition of [Golan] p. 1. Note that our semirings are unital. Such semirings are sometimes called "rigs", being "rings without negatives". (Contributed by Thierry Arnoux, 21-Mar-2018.) |
| ⊢ SRing = {𝑓 ∈ CMnd ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡][(0g‘𝑓) / 𝑛]∀𝑥 ∈ 𝑟 (∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))) ∧ ((𝑛𝑡𝑥) = 𝑛 ∧ (𝑥𝑡𝑛) = 𝑛)))} | ||
| Theorem | issrg 20185* | The predicate "is a semiring". (Contributed by Thierry Arnoux, 21-Mar-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ SRing ↔ (𝑅 ∈ CMnd ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 (∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))) ∧ (( 0 · 𝑥) = 0 ∧ (𝑥 · 0 ) = 0 )))) | ||
| Theorem | srgcmn 20186 | A semiring is a commutative monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
| ⊢ (𝑅 ∈ SRing → 𝑅 ∈ CMnd) | ||
| Theorem | srgmnd 20187 | A semiring is a monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
| ⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) | ||
| Theorem | srgmgp 20188 | A semiring is a monoid under multiplication. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
| ⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ SRing → 𝐺 ∈ Mnd) | ||
| Theorem | srgdilem 20189 | Lemma for srgdi 20194 and srgdir 20195. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)) ∧ ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))) | ||
| Theorem | srgcl 20190 | Closure of the multiplication operation of a semiring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵) | ||
| Theorem | srgass 20191 | Associative law for the multiplication operation of a semiring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 · 𝑌) · 𝑍) = (𝑋 · (𝑌 · 𝑍))) | ||
| Theorem | srgideu 20192* | The unity element of a semiring is unique. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ SRing → ∃!𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 · 𝑥) = 𝑥 ∧ (𝑥 · 𝑢) = 𝑥)) | ||
| Theorem | srgfcl 20193 | Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by AV, 24-Aug-2021.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ · Fn (𝐵 × 𝐵)) → · :(𝐵 × 𝐵)⟶𝐵) | ||
| Theorem | srgdi 20194 | Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍))) | ||
| Theorem | srgdir 20195 | Distributive law for the multiplication operation of a semiring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) | ||
| Theorem | srgidcl 20196 | The unity element of a semiring belongs to the base set of the semiring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ SRing → 1 ∈ 𝐵) | ||
| Theorem | srg0cl 20197 | The zero element of a semiring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ SRing → 0 ∈ 𝐵) | ||
| Theorem | srgidmlem 20198 | Lemma for srglidm 20199 and srgridm 20200. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (( 1 · 𝑋) = 𝑋 ∧ (𝑋 · 1 ) = 𝑋)) | ||
| Theorem | srglidm 20199 | The unity element of a semiring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ( 1 · 𝑋) = 𝑋) | ||
| Theorem | srgridm 20200 | The unity element of a semiring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑋 · 1 ) = 𝑋) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |