Home | Metamath
Proof Explorer Theorem List (p. 184 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pgpfac1lem5 18301* | Lemma for pgpfac1 18302. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → ∀𝑠 ∈ (SubGrp‘𝐺)((𝑠 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑠) → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑠))) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑈)) | ||
Theorem | pgpfac1 18302* | Factorization of a finite abelian p-group. There is a direct product decomposition of any abelian group of prime-power order where one of the factors is cyclic and generated by an element of maximal order. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝐵)) | ||
Theorem | pgpfaclem1 18303* | Lemma for pgpfac 18306. (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 18304* | Lemma for pgpfac 18306. (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 18305* | Lemma for pgpfac 18306. (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 18306* | Full factorization of a finite abelian p-group, by iterating pgpfac1 18302. 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 18307* | Lemma for ablfac 18310. (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 18308* | Lemma for ablfac 18310. (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 18309* | Lemma for ablfac 18310. (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 18310* | 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 18311* | Choose generators for each cyclic group in ablfac 18310. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ · = (.g‘𝐺) & ⊢ 𝑆 = (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤‘𝑘)))) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ Word 𝐵(𝑆:dom 𝑤⟶𝐶 ∧ 𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵)) | ||
Syntax | cmgp 18312 | Multiplicative group. |
class mulGrp | ||
Definition | df-mgp 18313 | 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 18490 shows that we get a group if we restrict to the elements that have inverses. This allows us to formalize such notions as "the multiplication operation of a ring is a monoid" (ringmgp 18376) or "the multiplicative identity" in terms of the identity of a monoid (df-1r 9762). (Contributed by Mario Carneiro, 21-Dec-2014.) |
⊢ mulGrp = (𝑤 ∈ V ↦ (𝑤 sSet 〈(+g‘ndx), (.r‘𝑤)〉)) | ||
Theorem | fnmgp 18314 | The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.) |
⊢ mulGrp Fn V | ||
Theorem | mgpval 18315 | Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ 𝑀 = (𝑅 sSet 〈(+g‘ndx), · 〉) | ||
Theorem | mgpplusg 18316 | Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ · = (+g‘𝑀) | ||
Theorem | mgplem 18317 | Lemma for mgpbas 18318. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 ≠ 2 ⇒ ⊢ (𝐸‘𝑅) = (𝐸‘𝑀) | ||
Theorem | mgpbas 18318 | 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 18319 | The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 18441. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝑆 = (Scalar‘𝑅) ⇒ ⊢ 𝑆 = (Scalar‘𝑀) | ||
Theorem | mgptset 18320 | Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ (TopSet‘𝑅) = (TopSet‘𝑀) | ||
Theorem | mgptopn 18321 | Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑅) ⇒ ⊢ 𝐽 = (TopOpen‘𝑀) | ||
Theorem | mgpds 18322 | Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
⊢ 𝑀 = (mulGrp‘𝑅) & ⊢ 𝐵 = (dist‘𝑅) ⇒ ⊢ 𝐵 = (dist‘𝑀) | ||
Theorem | mgpress 18323 | Subgroup commutes with the multiplication group operator. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝑀 = (mulGrp‘𝑅) ⇒ ⊢ ((𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊) → (𝑀 ↾s 𝐴) = (mulGrp‘𝑆)) | ||
Syntax | cur 18324 | Extend class notation with ring unit. |
class 1r | ||
Definition | df-ur 18325 | Define the multiplicative neutral element of a ring. This definition works by extracting the 0g element, i.e. the neutral element in a group or monoid, and transferring it to the multiplicative monoid via the mulGrp function (df-mgp 18313). See also dfur2 18327, 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 18326 | 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 18327* | 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 = (℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 · 𝑥) = 𝑥 ∧ (𝑥 · 𝑒) = 𝑥))) | ||
Syntax | csrg 18328 | Extend class notation with the class of all semirings. |
class SRing | ||
Definition | df-srg 18329* | 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. Compared to the definition of a ring, this definition also adds that the additive identity is an absorbing element of the multiplicative law, as this 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 18330* | 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 18331 | A semiring is a commutative monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
⊢ (𝑅 ∈ SRing → 𝑅 ∈ CMnd) | ||
Theorem | srgmnd 18332 | A semiring is a monoid. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
⊢ (𝑅 ∈ SRing → 𝑅 ∈ Mnd) | ||
Theorem | srgmgp 18333 | A semiring is a monoid under multiplication. (Contributed by Thierry Arnoux, 21-Mar-2018.) |
⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ SRing → 𝐺 ∈ Mnd) | ||
Theorem | srgi 18334 | Properties of a semiring. (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 18335 | 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 18336 | 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 18337* | The unit 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 18338 | 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 18339 | 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 18340 | 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 18341 | The unit 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 18342 | 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 18343 | Lemma for srglidm 18344 and srgridm 18345. (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 18344 | The unit 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 18345 | The unit 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 ) = 𝑋) | ||
Theorem | issrgid 18346* | Properties showing that an element 𝐼 is the unity element of a semiring. (Contributed by NM, 7-Aug-2013.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ SRing → ((𝐼 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥)) ↔ 1 = 𝐼)) | ||
Theorem | srgacl 18347 | Closure of the addition operation of a semiring. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) | ||
Theorem | srgcom 18348 | Commutativity of the additive group of a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | srgrz 18349 | The zero of a semiring is a right-absorbing element. (Contributed by Thierry Arnoux, 1-Apr-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑋 · 0 ) = 0 ) | ||
Theorem | srglz 18350 | The zero of a semiring is a left-absorbing element. (Contributed by AV, 23-Aug-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → ( 0 · 𝑋) = 0 ) | ||
Theorem | srgisid 18351* | In a semiring, the only left-absorbing element is the additive identity. Remark in [Golan] p. 1. (Contributed by Thierry Arnoux, 1-May-2018.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ SRing) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑍 · 𝑥) = 𝑍) ⇒ ⊢ (𝜑 → 𝑍 = 0 ) | ||
Theorem | srg1zr 18352 | The only semiring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ∗ = (.r‘𝑅) ⇒ ⊢ (((𝑅 ∈ SRing ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) ∧ 𝑍 ∈ 𝐵) → (𝐵 = {𝑍} ↔ ( + = {〈〈𝑍, 𝑍〉, 𝑍〉} ∧ ∗ = {〈〈𝑍, 𝑍〉, 𝑍〉}))) | ||
Theorem | srgen1zr 18353 | The only semiring with one element is the zero ring (at least if its operations are internal binary operations). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 25-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ ∗ = (.r‘𝑅) & ⊢ 𝑍 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ + Fn (𝐵 × 𝐵) ∧ ∗ Fn (𝐵 × 𝐵)) → (𝐵 ≈ 1𝑜 ↔ ( + = {〈〈𝑍, 𝑍〉, 𝑍〉} ∧ ∗ = {〈〈𝑍, 𝑍〉, 𝑍〉}))) | ||
Theorem | srgmulgass 18354 | An associative property between group multiple and ring multiplication for semirings. (Contributed by AV, 23-Aug-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ × = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ (𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑁 · 𝑋) × 𝑌) = (𝑁 · (𝑋 × 𝑌))) | ||
Theorem | srgpcomp 18355 | If two elements of a semiring commute, they also commute if one of the elements is raised to a higher power. (Contributed by AV, 23-Aug-2019.) |
⊢ 𝑆 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ SRing) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴)) ⇒ ⊢ (𝜑 → ((𝐾 ↑ 𝐵) × 𝐴) = (𝐴 × (𝐾 ↑ 𝐵))) | ||
Theorem | srgpcompp 18356 | If two elements of a semiring commute, they also commute if the elements are raised to a higher power. (Contributed by AV, 23-Aug-2019.) |
⊢ 𝑆 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ SRing) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (((𝑁 ↑ 𝐴) × (𝐾 ↑ 𝐵)) × 𝐴) = (((𝑁 + 1) ↑ 𝐴) × (𝐾 ↑ 𝐵))) | ||
Theorem | srgpcomppsc 18357 | If two elements of a semiring commute, they also commute if the elements are raised to a higher power and a scalar multiplication is involved. (Contributed by AV, 23-Aug-2019.) |
⊢ 𝑆 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ SRing) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐾 ∈ ℕ0) & ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ · = (.g‘𝑅) & ⊢ (𝜑 → 𝐶 ∈ ℕ0) ⇒ ⊢ (𝜑 → ((𝐶 · ((𝑁 ↑ 𝐴) × (𝐾 ↑ 𝐵))) × 𝐴) = (𝐶 · (((𝑁 + 1) ↑ 𝐴) × (𝐾 ↑ 𝐵)))) | ||
Theorem | srglmhm 18358* | Left-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism, analogous to ringlghm 18427. (Contributed by AV, 23-Aug-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑋 · 𝑥)) ∈ (𝑅 MndHom 𝑅)) | ||
Theorem | srgrmhm 18359* | Right-multiplication in a semiring by a fixed element of the ring is a monoid homomorphism, analogous to ringrghm 18428. (Contributed by AV, 23-Aug-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ 𝑋 ∈ 𝐵) → (𝑥 ∈ 𝐵 ↦ (𝑥 · 𝑋)) ∈ (𝑅 MndHom 𝑅)) | ||
Theorem | srgsummulcr 18360* | A finite semiring sum multiplied by a constant, analogous to gsummulc1 18429. (Contributed by AV, 23-Aug-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ SRing) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = ((𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) · 𝑌)) | ||
Theorem | sgsummulcl 18361* | A finite semiring sum multiplied by a constant, analogous to gsummulc2 18430. (Contributed by AV, 23-Aug-2019.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ SRing) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑌 · 𝑋))) = (𝑌 · (𝑅 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)))) | ||
Theorem | srg1expzeq1 18362 | The exponentiation (by a nonnegative integer) of the unity element of a (semi)ring, analogous to mulgnn0z 17390. (Contributed by AV, 25-Nov-2019.) |
⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ · = (.g‘𝐺) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ0) → (𝑁 · 1 ) = 1 ) | ||
In this section, we prove the binomial theorem for semirings, srgbinom 18368, which is a generalization of the binomial theorem for complex numbers, binom 14401: (𝐴 + 𝐵)↑𝑁 is the sum from 𝑘 = 0 to 𝑁 of (𝑁C𝑘) · ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)). Notice that the binomial theorem would also hold in the non-unital case (that is, in a "rg") and actually, the additive unit is not needed in its proof either. Therefore, it could be proven for even more general cases. An example would be the integrable nonnegative (resp. positive) bounded functions on ℝ. Special cases of the binomial theorem are csrgbinom 18369 (binomial theorem for commutative semirings) and crngbinom 18444 (binomial theorem for commutative rings). | ||
Theorem | srgbinomlem1 18363 | Lemma 1 for srgbinomlem 18367. (Contributed by AV, 23-Aug-2019.) |
⊢ 𝑆 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ SRing) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ ((𝜑 ∧ (𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0)) → ((𝐷 ↑ 𝐴) × (𝐸 ↑ 𝐵)) ∈ 𝑆) | ||
Theorem | srgbinomlem2 18364 | Lemma 2 for srgbinomlem 18367. (Contributed by AV, 23-Aug-2019.) |
⊢ 𝑆 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ SRing) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ ((𝜑 ∧ (𝐶 ∈ ℕ0 ∧ 𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0)) → (𝐶 · ((𝐷 ↑ 𝐴) × (𝐸 ↑ 𝐵))) ∈ 𝑆) | ||
Theorem | srgbinomlem3 18365* | Lemma 3 for srgbinomlem 18367. (Contributed by AV, 23-Aug-2019.) (Proof shortened by AV, 27-Oct-2019.) |
⊢ 𝑆 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ SRing) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜓 → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐴) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) | ||
Theorem | srgbinomlem4 18366* | Lemma 4 for srgbinomlem 18367. (Contributed by AV, 24-Aug-2019.) (Proof shortened by AV, 19-Nov-2019.) |
⊢ 𝑆 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ SRing) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜓 → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 ↑ (𝐴 + 𝐵)) × 𝐵) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ ((𝑁C(𝑘 − 1)) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) | ||
Theorem | srgbinomlem 18367* | Lemma for srgbinom 18368. Inductive step, analogous to binomlem 14400. (Contributed by AV, 24-Aug-2019.) |
⊢ 𝑆 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝐺) & ⊢ (𝜑 → 𝑅 ∈ SRing) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → (𝐴 × 𝐵) = (𝐵 × 𝐴)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜓 → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ((𝑁 + 1) ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ (((𝑁 + 1)C𝑘) · ((((𝑁 + 1) − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) | ||
Theorem | srgbinom 18368* | The binomial theorem for commuting elements of a semiring: (𝐴 + 𝐵)↑𝑁 is the sum from 𝑘 = 0 to 𝑁 of (𝑁C𝑘) · ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)) (generalization of binom 14401). (Contributed by AV, 24-Aug-2019.) |
⊢ 𝑆 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝐺) ⇒ ⊢ (((𝑅 ∈ SRing ∧ 𝑁 ∈ ℕ0) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ (𝐴 × 𝐵) = (𝐵 × 𝐴))) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) | ||
Theorem | csrgbinom 18369* | The binomial theorem for commutative semirings. (Contributed by AV, 24-Aug-2019.) |
⊢ 𝑆 = (Base‘𝑅) & ⊢ × = (.r‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ ↑ = (.g‘𝐺) ⇒ ⊢ (((𝑅 ∈ SRing ∧ 𝐺 ∈ CMnd ∧ 𝑁 ∈ ℕ0) ∧ (𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆)) → (𝑁 ↑ (𝐴 + 𝐵)) = (𝑅 Σg (𝑘 ∈ (0...𝑁) ↦ ((𝑁C𝑘) · (((𝑁 − 𝑘) ↑ 𝐴) × (𝑘 ↑ 𝐵)))))) | ||
Syntax | crg 18370 | Extend class notation with class of all (unital) rings. |
class Ring | ||
Syntax | ccrg 18371 | Extend class notation with class of all (unital) commutative rings. |
class CRing | ||
Definition | df-ring 18372* | Define class of all (unital) rings. A unital ring is a set equipped with two everywhere-defined internal operations, whose first one is an additive group structure and the second one is a multiplicative monoid structure, and where the addition is left- and right-distributive for the multiplication. Definition 1 in [BourbakiAlg1] p. 92 or definition of a ring with identity in part Preliminaries of [Roman] p. 19. So that the additive structure must be abelian (see ringcom 18402), care must be taken that in the case of a non-unital ring, the commutativity of addition must be postulated and cannot be proved from the other conditions. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ Ring = {𝑓 ∈ Grp ∣ ((mulGrp‘𝑓) ∈ Mnd ∧ [(Base‘𝑓) / 𝑟][(+g‘𝑓) / 𝑝][(.r‘𝑓) / 𝑡]∀𝑥 ∈ 𝑟 ∀𝑦 ∈ 𝑟 ∀𝑧 ∈ 𝑟 ((𝑥𝑡(𝑦𝑝𝑧)) = ((𝑥𝑡𝑦)𝑝(𝑥𝑡𝑧)) ∧ ((𝑥𝑝𝑦)𝑡𝑧) = ((𝑥𝑡𝑧)𝑝(𝑦𝑡𝑧))))} | ||
Definition | df-cring 18373 | Define class of all commutative rings. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ CRing = {𝑓 ∈ Ring ∣ (mulGrp‘𝑓) ∈ CMnd} | ||
Theorem | isring 18374* | The predicate "is a (unital) ring." Definition of ring with unit in [Schechter] p. 187. (Contributed by NM, 18-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring ↔ (𝑅 ∈ Grp ∧ 𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 · (𝑦 + 𝑧)) = ((𝑥 · 𝑦) + (𝑥 · 𝑧)) ∧ ((𝑥 + 𝑦) · 𝑧) = ((𝑥 · 𝑧) + (𝑦 · 𝑧))))) | ||
Theorem | ringgrp 18375 | A ring is a group. (Contributed by NM, 15-Sep-2011.) |
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Grp) | ||
Theorem | ringmgp 18376 | A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 𝐺 ∈ Mnd) | ||
Theorem | iscrng 18377 | A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ 𝐺 ∈ CMnd)) | ||
Theorem | crngmgp 18378 | A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐺 = (mulGrp‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing → 𝐺 ∈ CMnd) | ||
Theorem | ringmnd 18379 | A ring is a monoid under addition. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mnd) | ||
Theorem | ringmgm 18380 | A ring is a magma. (Contributed by AV, 31-Jan-2020.) |
⊢ (𝑅 ∈ Ring → 𝑅 ∈ Mgm) | ||
Theorem | crngring 18381 | A commutative ring is a ring. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring) | ||
Theorem | mgpf 18382 | Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015.) |
⊢ (mulGrp ↾ Ring):Ring⟶Mnd | ||
Theorem | ringi 18383 | Properties of a unital ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍)) ∧ ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍)))) | ||
Theorem | ringcl 18384 | Closure of the multiplication operation of a ring. (Contributed by NM, 26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) ∈ 𝐵) | ||
Theorem | crngcom 18385 | A commutative ring's multiplication operation is commutative. (Contributed by Mario Carneiro, 7-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 · 𝑌) = (𝑌 · 𝑋)) | ||
Theorem | iscrng2 18386* | A commutative ring is a ring whose multiplication is a commutative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ CRing ↔ (𝑅 ∈ Ring ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 · 𝑦) = (𝑦 · 𝑥))) | ||
Theorem | ringass 18387 | Associative law for the multiplication operation of a ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 · 𝑌) · 𝑍) = (𝑋 · (𝑌 · 𝑍))) | ||
Theorem | ringideu 18388* | The unit element of a ring is unique. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → ∃!𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 · 𝑥) = 𝑥 ∧ (𝑥 · 𝑢) = 𝑥)) | ||
Theorem | ringdi 18389 | Distributive law for the multiplication operation of a ring (left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 · (𝑌 + 𝑍)) = ((𝑋 · 𝑌) + (𝑋 · 𝑍))) | ||
Theorem | ringdir 18390 | Distributive law for the multiplication operation of a ring (right-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) · 𝑍) = ((𝑋 · 𝑍) + (𝑌 · 𝑍))) | ||
Theorem | ringidcl 18391 | The unit element of a ring belongs to the base set of the ring. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 1 ∈ 𝐵) | ||
Theorem | ring0cl 18392 | The zero element of a ring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → 0 ∈ 𝐵) | ||
Theorem | ringidmlem 18393 | Lemma for ringlidm 18394 and ringridm 18395. (Contributed by NM, 15-Sep-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (( 1 · 𝑋) = 𝑋 ∧ (𝑋 · 1 ) = 𝑋)) | ||
Theorem | ringlidm 18394 | The unit element of a ring is a left multiplicative identity. (Contributed by NM, 15-Sep-2011.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ( 1 · 𝑋) = 𝑋) | ||
Theorem | ringridm 18395 | The unit element of a ring is a right multiplicative identity. (Contributed by NM, 15-Sep-2011.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → (𝑋 · 1 ) = 𝑋) | ||
Theorem | isringid 18396* | Properties showing that an element 𝐼 is the unity element of a ring. (Contributed by NM, 7-Aug-2013.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → ((𝐼 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝐼 · 𝑥) = 𝑥 ∧ (𝑥 · 𝐼) = 𝑥)) ↔ 1 = 𝐼)) | ||
Theorem | ringid 18397* | The multiplication operation of a unital ring has (one or more) identity elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (Revised by AV, 24-Aug-2021.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ∃𝑢 ∈ 𝐵 ((𝑢 · 𝑋) = 𝑋 ∧ (𝑋 · 𝑢) = 𝑋)) | ||
Theorem | ringadd2 18398* | A ring element plus itself is two times the element. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.) (Revised by AV, 24-Aug-2021.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝑋 ∈ 𝐵) → ∃𝑥 ∈ 𝐵 (𝑋 + 𝑋) = ((𝑥 + 𝑥) · 𝑋)) | ||
Theorem | rngo2times 18399 | A ring element plus itself is two times the element. "Two" in an arbitrary unital ring is the sum of the unit with itself. (Contributed by AV, 24-Aug-2021.) |
⊢ 𝐵 = (Base‘𝑅) & ⊢ + = (+g‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ∈ 𝐵) → (𝐴 + 𝐴) = (( 1 + 1 ) · 𝐴)) | ||
Theorem | ringidss 18400 | A subset of the multiplicative group has the multiplicative identity as its identity if the identity is in the subset. (Contributed by Mario Carneiro, 27-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
⊢ 𝑀 = ((mulGrp‘𝑅) ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 1 = (1r‘𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ 𝐴 ⊆ 𝐵 ∧ 1 ∈ 𝐴) → 1 = (0g‘𝑀)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |