Home | Metamath
Proof Explorer Theorem List (p. 182 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 | frgpnabl 18101 | The free group on two or more generators is not abelian. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐺 = (freeGrp‘𝐼) ⇒ ⊢ (1𝑜 ≺ 𝐼 → ¬ 𝐺 ∈ Abel) | ||
Syntax | ccyg 18102 | Cyclic group. |
class CycGrp | ||
Definition | df-cyg 18103* | Define a cyclic group, which is a group with an element 𝑥, called the generator of the group, such that all elements in the group are multiples of 𝑥. A generator is usually not unique. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ CycGrp = {𝑔 ∈ Grp ∣ ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥)) = (Base‘𝑔)} | ||
Theorem | iscyg 18104* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (𝐺 ∈ CycGrp ↔ (𝐺 ∈ Grp ∧ ∃𝑥 ∈ 𝐵 ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵)) | ||
Theorem | iscyggen 18105* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} ⇒ ⊢ (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = 𝐵)) | ||
Theorem | iscyggen2 18106* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} ⇒ ⊢ (𝐺 ∈ Grp → (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑋)))) | ||
Theorem | iscyg2 18107* | A cyclic group is a group which contains a generator. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} ⇒ ⊢ (𝐺 ∈ CycGrp ↔ (𝐺 ∈ Grp ∧ 𝐸 ≠ ∅)) | ||
Theorem | cyggeninv 18108* | The inverse of a cyclic generator is a generator. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) → (𝑁‘𝑋) ∈ 𝐸) | ||
Theorem | cyggenod 18109* | An element is the generator of a finite group iff the order of the generator equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ Fin) → (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ (𝑂‘𝑋) = (#‘𝐵)))) | ||
Theorem | cyggenod2 18110* | In an infinite cyclic group, the generator must have infinite order, but this property no longer characterizes the generators. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐸) → (𝑂‘𝑋) = if(𝐵 ∈ Fin, (#‘𝐵), 0)) | ||
Theorem | iscyg3 18111* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (𝐺 ∈ CycGrp ↔ (𝐺 ∈ Grp ∧ ∃𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑥))) | ||
Theorem | iscygd 18112* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑋)) ⇒ ⊢ (𝜑 → 𝐺 ∈ CycGrp) | ||
Theorem | iscygodd 18113 | Show that a group with an element the same order as the group is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑂‘𝑋) = (#‘𝐵)) ⇒ ⊢ (𝜑 → 𝐺 ∈ CycGrp) | ||
Theorem | cyggrp 18114 | A cyclic group is a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Grp) | ||
Theorem | cygabl 18115 | A cyclic group is abelian. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ (𝐺 ∈ CycGrp → 𝐺 ∈ Abel) | ||
Theorem | cygctb 18116 | A cyclic group is countable. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ CycGrp → 𝐵 ≼ ω) | ||
Theorem | 0cyg 18117 | The trivial group is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐵 ≈ 1𝑜) → 𝐺 ∈ CycGrp) | ||
Theorem | prmcyg 18118 | A group with prime order is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) ∈ ℙ) → 𝐺 ∈ CycGrp) | ||
Theorem | lt6abl 18119 | A group with fewer than 6 elements is abelian. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ (#‘𝐵) < 6) → 𝐺 ∈ Abel) | ||
Theorem | ghmcyg 18120 | The image of a cyclic group under a surjective group homomorphism is cyclic. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = (Base‘𝐻) ⇒ ⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝐹:𝐵–onto→𝐶) → (𝐺 ∈ CycGrp → 𝐻 ∈ CycGrp)) | ||
Theorem | cyggex2 18121 | The exponent of a cyclic group is 0 if the group is infinite, otherwise it equals the order of the group. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) ⇒ ⊢ (𝐺 ∈ CycGrp → 𝐸 = if(𝐵 ∈ Fin, (#‘𝐵), 0)) | ||
Theorem | cyggex 18122 | The exponent of a finite cyclic group is the order of the group. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) ⇒ ⊢ ((𝐺 ∈ CycGrp ∧ 𝐵 ∈ Fin) → 𝐸 = (#‘𝐵)) | ||
Theorem | cyggexb 18123 | A finite abelian group is cyclic iff the exponent equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝐵 ∈ Fin) → (𝐺 ∈ CycGrp ↔ 𝐸 = (#‘𝐵))) | ||
Theorem | giccyg 18124 | Cyclicity is a group property, i.e. it is preserved under isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ (𝐺 ≃𝑔 𝐻 → (𝐺 ∈ CycGrp → 𝐻 ∈ CycGrp)) | ||
Theorem | cycsubgcyg 18125* | The cyclic subgroup generated by 𝐴 is a cyclic group. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝑆 = ran (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐺 ↾s 𝑆) ∈ CycGrp) | ||
Theorem | cycsubgcyg2 18126 | The cyclic subgroup generated by 𝐴 is a cyclic group. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵) → (𝐺 ↾s (𝐾‘{𝐴})) ∈ CycGrp) | ||
Theorem | gsumval3a 18127* | Value of the group sum operation over an index set with finite support. (Contributed by Mario Carneiro, 7-Dec-2014.) (Revised by AV, 29-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → 𝑊 ∈ Fin) & ⊢ (𝜑 → 𝑊 ≠ ∅) & ⊢ 𝑊 = (𝐹 supp 0 ) & ⊢ (𝜑 → ¬ 𝐴 ∈ ran ...) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (℩𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊))))) | ||
Theorem | gsumval3eu 18128* | The group sum as defined in gsumval3a 18127 is uniquely defined. (Contributed by Mario Carneiro, 8-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → 𝑊 ∈ Fin) & ⊢ (𝜑 → 𝑊 ≠ ∅) & ⊢ (𝜑 → 𝑊 ⊆ 𝐴) ⇒ ⊢ (𝜑 → ∃!𝑥∃𝑓(𝑓:(1...(#‘𝑊))–1-1-onto→𝑊 ∧ 𝑥 = (seq1( + , (𝐹 ∘ 𝑓))‘(#‘𝑊)))) | ||
Theorem | gsumval3lem1 18129* | Lemma 1 for gsumval3 18131. (Contributed by AV, 31-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴) & ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻) & ⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 ) ⇒ ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (𝐻 ∘ 𝑓):(1...(#‘(𝐹 supp 0 )))–1-1-onto→(𝐹 supp 0 )) | ||
Theorem | gsumval3lem2 18130* | Lemma 2 for gsumval3 18131. (Contributed by AV, 31-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴) & ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻) & ⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 ) ⇒ ⊢ (((𝜑 ∧ 𝑊 ≠ ∅) ∧ (¬ 𝐴 ∈ ran ... ∧ 𝑓 Isom < , < ((1...(#‘𝑊)), 𝑊))) → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ (𝐻 ∘ 𝑓)))‘(#‘𝑊))) | ||
Theorem | gsumval3 18131 | Value of the group sum operation over an arbitrary finite set. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 31-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝐻:(1...𝑀)–1-1→𝐴) & ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ ran 𝐻) & ⊢ 𝑊 = ((𝐹 ∘ 𝐻) supp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq1( + , (𝐹 ∘ 𝐻))‘𝑀)) | ||
Theorem | gsumcllem 18132* | Lemma for gsumcl 18139 and related theorems. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 31-May-2019.) |
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑍 ∈ 𝑈) & ⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ 𝑊) ⇒ ⊢ ((𝜑 ∧ 𝑊 = ∅) → 𝐹 = (𝑘 ∈ 𝐴 ↦ 𝑍)) | ||
Theorem | gsumzres 18133 | Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 31-May-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝑊)) = (𝐺 Σg 𝐹)) | ||
Theorem | gsumzcl2 18134 | Closure of a finite group sum. This theorem has a weaker hypothesis than gsumzcl 18135, because it is not required that 𝐹 is a function (actually, the hypothesis always holds for any proper class 𝐹). (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 1-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → (𝐹 supp 0 ) ∈ Fin) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵) | ||
Theorem | gsumzcl 18135 | Closure of a finite group sum. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 1-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵) | ||
Theorem | gsumzf1o 18136 | Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 2-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ (𝜑 → 𝐻:𝐶–1-1-onto→𝐴) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻))) | ||
Theorem | gsumres 18137 | Extend a finite group sum by padding outside with zeroes. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ 𝑊)) = (𝐺 Σg 𝐹)) | ||
Theorem | gsumcl2 18138 | Closure of a finite group sum. This theorem has a weaker hypothesis than gsumcl 18139, because it is not required that 𝐹 is a function (actually, the hypothesis always holds for any proper class 𝐹). (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 supp 0 ) ∈ Fin) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵) | ||
Theorem | gsumcl 18139 | Closure of a finite group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵) | ||
Theorem | gsumf1o 18140 | Re-index a finite group sum using a bijection. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ (𝜑 → 𝐻:𝐶–1-1-onto→𝐴) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻))) | ||
Theorem | gsumzsubmcl 18141 | Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝑆) | ||
Theorem | gsumsubmcl 18142 | Closure of a group sum in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 3-Jun-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝑆) | ||
Theorem | gsumsubgcl 18143 | Closure of a group sum in a subgroup. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 3-Jun-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝑆) | ||
Theorem | gsumzaddlem 18144* | The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ (𝜑 → 𝐻 finSupp 0 ) & ⊢ 𝑊 = ((𝐹 ∪ 𝐻) supp 0 ) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐻:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → ran 𝐻 ⊆ (𝑍‘ran 𝐻)) & ⊢ (𝜑 → ran (𝐹 ∘𝑓 + 𝐻) ⊆ (𝑍‘ran (𝐹 ∘𝑓 + 𝐻))) & ⊢ ((𝜑 ∧ (𝑥 ⊆ 𝐴 ∧ 𝑘 ∈ (𝐴 ∖ 𝑥))) → (𝐹‘𝑘) ∈ (𝑍‘{(𝐺 Σg (𝐻 ↾ 𝑥))})) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) | ||
Theorem | gsumzadd 18145 | The sum of two group sums. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ (𝜑 → 𝐻 finSupp 0 ) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) & ⊢ (𝜑 → 𝑆 ⊆ (𝑍‘𝑆)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ (𝜑 → 𝐻:𝐴⟶𝑆) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) | ||
Theorem | gsumadd 18146 | The sum of two group sums. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐻:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ (𝜑 → 𝐻 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) | ||
Theorem | gsummptfsadd 18147* | The sum of two group sums expressed as mappings. (Contributed by AV, 4-Apr-2019.) (Revised by AV, 9-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)) & ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐴 ↦ 𝐷)) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ (𝜑 → 𝐻 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ (𝐶 + 𝐷))) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) | ||
Theorem | gsummptfidmadd 18148* | The sum of two group sums expressed as mappings with finite domain. (Contributed by AV, 23-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ 𝐷) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ (𝐶 + 𝐷))) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) | ||
Theorem | gsummptfidmadd2 18149* | The sum of two group sums expressed as mappings with finite domain, using a function operation. (Contributed by AV, 23-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ 𝐷) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓 + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻))) | ||
Theorem | gsumzsplit 18150 | Split a group sum into two parts. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 5-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷)) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹 ↾ 𝐶)) + (𝐺 Σg (𝐹 ↾ 𝐷)))) | ||
Theorem | gsumsplit 18151 | Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 5-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷)) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹 ↾ 𝐶)) + (𝐺 Σg (𝐹 ↾ 𝐷)))) | ||
Theorem | gsumsplit2 18152* | Split a group sum into two parts. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 5-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷)) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)) + (𝐺 Σg (𝑘 ∈ 𝐷 ↦ 𝑋)))) | ||
Theorem | gsummptfidmsplit 18153* | Split a group sum expressed as mapping with a finite domain into two parts. (Contributed by AV, 23-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷)) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑌)) = ((𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑌)) + (𝐺 Σg (𝑘 ∈ 𝐷 ↦ 𝑌)))) | ||
Theorem | gsummptfidmsplitres 18154* | Split a group sum expressed as mapping with a finite domain into two parts using restrictions. (Contributed by AV, 23-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ (𝜑 → 𝐴 = (𝐶 ∪ 𝐷)) & ⊢ 𝐹 = (𝑘 ∈ 𝐴 ↦ 𝑌) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝐹 ↾ 𝐶)) + (𝐺 Σg (𝐹 ↾ 𝐷)))) | ||
Theorem | gsummptfzsplit 18155* | Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, extracting a singleton from the right. (Contributed by AV, 25-Oct-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (0...(𝑁 + 1)) ↦ 𝑌)) = ((𝐺 Σg (𝑘 ∈ (0...𝑁) ↦ 𝑌)) + (𝐺 Σg (𝑘 ∈ {(𝑁 + 1)} ↦ 𝑌)))) | ||
Theorem | gsummptfzsplitl 18156* | Split a group sum expressed as mapping with a finite set of sequential integers as domain into two parts, , extracting a singleton from the left. (Contributed by AV, 7-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (0...𝑁) ↦ 𝑌)) = ((𝐺 Σg (𝑘 ∈ (1...𝑁) ↦ 𝑌)) + (𝐺 Σg (𝑘 ∈ {0} ↦ 𝑌)))) | ||
Theorem | gsumconst 18157* | Sum of a constant series. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((#‘𝐴) · 𝑋)) | ||
Theorem | gsumconstf 18158* | Sum of a constant series. (Contributed by Thierry Arnoux, 5-Jul-2017.) |
⊢ Ⅎ𝑘𝑋 & ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ Fin ∧ 𝑋 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((#‘𝐴) · 𝑋)) | ||
Theorem | gsummptshft 18159* | Index shift of a finite group sum over a finite set of sequential integers. (Contributed by AV, 24-Aug-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐾 ∈ ℤ) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝑁)) → 𝐴 ∈ 𝐵) & ⊢ (𝑗 = (𝑘 − 𝐾) → 𝐴 = 𝐶) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ (𝑀...𝑁) ↦ 𝐴)) = (𝐺 Σg (𝑘 ∈ ((𝑀 + 𝐾)...(𝑁 + 𝐾)) ↦ 𝐶))) | ||
Theorem | gsumzmhm 18160 | Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 6-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐻 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐾 ∈ (𝐺 MndHom 𝐻)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐻 Σg (𝐾 ∘ 𝐹)) = (𝐾‘(𝐺 Σg 𝐹))) | ||
Theorem | gsummhm 18161 | Apply a group homomorphism to a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Revised by AV, 6-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐻 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐾 ∈ (𝐺 MndHom 𝐻)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐻 Σg (𝐾 ∘ 𝐹)) = (𝐾‘(𝐺 Σg 𝐹))) | ||
Theorem | gsummhm2 18162* | Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015.) (Revised by AV, 6-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐻 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ 𝐶) ∈ (𝐺 MndHom 𝐻)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) & ⊢ (𝑥 = 𝑋 → 𝐶 = 𝐷) & ⊢ (𝑥 = (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) → 𝐶 = 𝐸) ⇒ ⊢ (𝜑 → (𝐻 Σg (𝑘 ∈ 𝐴 ↦ 𝐷)) = 𝐸) | ||
Theorem | gsummptmhm 18163* | Apply a group homomorphism to a group sum expressed with a mapping. (Contributed by Thierry Arnoux, 7-Sep-2018.) (Revised by AV, 8-Sep-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐻 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐾 ∈ (𝐺 MndHom 𝐻)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐻 Σg (𝑥 ∈ 𝐴 ↦ (𝐾‘𝐶))) = (𝐾‘(𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)))) | ||
Theorem | gsummulglem 18164* | Lemma for gsummulg 18165 and gsummulgz 18166. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 6-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑁 ∈ ℤ) & ⊢ (𝜑 → (𝐺 ∈ Abel ∨ 𝑁 ∈ ℕ0)) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (𝑁 · 𝑋))) = (𝑁 · (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)))) | ||
Theorem | gsummulg 18165* | Nonnegative multiple of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 6-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (𝑁 · 𝑋))) = (𝑁 · (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)))) | ||
Theorem | gsummulgz 18166* | Integer multiple of a group sum. (Contributed by Mario Carneiro, 7-Jan-2015.) (Revised by AV, 6-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑁 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ (𝑁 · 𝑋))) = (𝑁 · (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)))) | ||
Theorem | gsumzoppg 18167 | The opposite of a group sum is the same as the original. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 6-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝑂 = (oppg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑂 Σg 𝐹) = (𝐺 Σg 𝐹)) | ||
Theorem | gsumzinv 18168 | Inverse of a group sum. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 6-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐼 ∘ 𝐹)) = (𝐼‘(𝐺 Σg 𝐹))) | ||
Theorem | gsuminv 18169 | Inverse of a group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by Mario Carneiro, 4-May-2015.) (Revised by AV, 6-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐼 ∘ 𝐹)) = (𝐼‘(𝐺 Σg 𝐹))) | ||
Theorem | gsummptfidminv 18170* | Inverse of a group sum expressed as mapping with a finite domain. (Contributed by AV, 23-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐼 ∘ 𝐹)) = (𝐼‘(𝐺 Σg 𝐹))) | ||
Theorem | gsumsub 18171 | The difference of two group sums. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 6-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐻:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ (𝜑 → 𝐻 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐹 ∘𝑓 − 𝐻)) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻))) | ||
Theorem | gsummptfssub 18172* | The difference of two group sums expressed as mappings. (Contributed by AV, 7-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶)) & ⊢ (𝜑 → 𝐻 = (𝑥 ∈ 𝐴 ↦ 𝐷)) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ (𝜑 → 𝐻 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐷))) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻))) | ||
Theorem | gsummptfidmsub 18173* | The difference of two group sums expressed as mappings with finite domain. (Contributed by AV, 7-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐵) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) & ⊢ 𝐻 = (𝑥 ∈ 𝐴 ↦ 𝐷) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ (𝐶 − 𝐷))) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻))) | ||
Theorem | gsumsnfd 18174* | Group sum of a singleton, deduction form, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Revised by AV, 11-Dec-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝐴 = 𝐶) & ⊢ Ⅎ𝑘𝜑 & ⊢ Ⅎ𝑘𝐶 ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ {𝑀} ↦ 𝐴)) = 𝐶) | ||
Theorem | gsumsnd 18175* | Group sum of a singleton, deduction form. (Contributed by Thierry Arnoux, 30-Jan-2017.) (Proof shortened by AV, 11-Dec-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝐴 = 𝐶) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ {𝑀} ↦ 𝐴)) = 𝐶) | ||
Theorem | gsumsnf 18176* | Group sum of a singleton, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Proof shortened by AV, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝐶 & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐶) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ {𝑀} ↦ 𝐴)) = 𝐶) | ||
Theorem | gsumsn 18177* | Group sum of a singleton. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 24-Apr-2016.) (Proof shortened by AV, 11-Dec-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐶) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑀 ∈ 𝑉 ∧ 𝐶 ∈ 𝐵) → (𝐺 Σg (𝑘 ∈ {𝑀} ↦ 𝐴)) = 𝐶) | ||
Theorem | gsumzunsnd 18178* | Append an element to a finite group sum, more general version of gsumunsnd 18180. (Contributed by AV, 7-Oct-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝐹 = (𝑘 ∈ (𝐴 ∪ {𝑀}) ↦ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑀 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) + 𝑌)) | ||
Theorem | gsumunsnfd 18179* | Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 11-Dec-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑀 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌) & ⊢ Ⅎ𝑘𝑌 ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 ∪ {𝑀}) ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) + 𝑌)) | ||
Theorem | gsumunsnd 18180* | Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by AV, 2-Jan-2019.) (Proof shortened by AV, 11-Dec-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑀 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 ∪ {𝑀}) ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) + 𝑌)) | ||
Theorem | gsumunsnf 18181* | Append an element to a finite group sum, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Thierry Arnoux, 28-Mar-2018.) (Proof shortened by AV, 11-Dec-2019.) |
⊢ Ⅎ𝑘𝑌 & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑀 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝑘 = 𝑀 → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 ∪ {𝑀}) ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) + 𝑌)) | ||
Theorem | gsumunsn 18182* | Append an element to a finite group sum. (Contributed by Mario Carneiro, 19-Dec-2014.) (Proof shortened by AV, 8-Mar-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑀 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝑘 = 𝑀 → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 ∪ {𝑀}) ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) + 𝑌)) | ||
Theorem | gsumdifsnd 18183* | Extract a summand from a finitely supported group sum. (Contributed by AV, 21-Apr-2019.) (Revised by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp (0g‘𝐺)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) = ((𝐺 Σg (𝑘 ∈ (𝐴 ∖ {𝑀}) ↦ 𝑋)) + 𝑌)) | ||
Theorem | gsumpt 18184 | Sum of a family that is nonzero at at most one point. (Contributed by Stefan O'Rear, 7-Feb-2015.) (Revised by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 6-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → (𝐹 supp 0 ) ⊆ {𝑋}) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐹‘𝑋)) | ||
Theorem | gsummptf1o 18185* | Re-index a finite group sum using a bijection. (Contributed by Thierry Arnoux, 29-Mar-2018.) |
⊢ Ⅎ𝑥𝐻 & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝑥 = 𝐸 → 𝐶 = 𝐻) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐹) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐸 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 ∈ 𝐷 𝑥 = 𝐸) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝐺 Σg (𝑦 ∈ 𝐷 ↦ 𝐻))) | ||
Theorem | gsummptun 18186* | Group sum of a disjoint union, whereas sums are expressed as mappings. (Contributed by Thierry Arnoux, 28-Mar-2018.) (Proof shortened by AV, 11-Dec-2019.) |
⊢ 𝐵 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ CMnd) & ⊢ (𝜑 → (𝐴 ∪ 𝐶) ∈ Fin) & ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ 𝐶)) → 𝐷 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ (𝐴 ∪ 𝐶) ↦ 𝐷)) = ((𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐷)) + (𝑊 Σg (𝑥 ∈ 𝐶 ↦ 𝐷)))) | ||
Theorem | gsummpt1n0 18187* | If only one summand in a finite group sum is not zero, the whole sum equals this summand. More general version of gsummptif1n0 18188. (Contributed by AV, 11-Oct-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ 𝐹 = (𝑛 ∈ 𝐼 ↦ if(𝑛 = 𝑋, 𝐴, 0 )) & ⊢ (𝜑 → ∀𝑛 ∈ 𝐼 𝐴 ∈ (Base‘𝐺)) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = ⦋𝑋 / 𝑛⦌𝐴) | ||
Theorem | gsummptif1n0 18188* | If only one summand in a finite group sum is not zero, the whole sum equals this summand. (Contributed by AV, 17-Feb-2019.) (Proof shortened by AV, 11-Oct-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ 𝐹 = (𝑛 ∈ 𝐼 ↦ if(𝑛 = 𝑋, 𝐴, 0 )) & ⊢ (𝜑 → 𝐴 ∈ (Base‘𝐺)) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = 𝐴) | ||
Theorem | gsummptcl 18189* | Closure of a finite group sum over a finite set as map. (Contributed by AV, 29-Dec-2018.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ 𝑁 ↦ 𝑋)) ∈ 𝐵) | ||
Theorem | gsummptfif1o 18190* | Re-index a finite group sum as map, using a bijection. (Contributed by by AV, 23-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐵) & ⊢ 𝐹 = (𝑖 ∈ 𝑁 ↦ 𝑋) & ⊢ (𝜑 → 𝐻:𝐶–1-1-onto→𝑁) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ 𝐻))) | ||
Theorem | gsummptfzcl 18191* | Closure of a finite group sum over a finite set of sequential integers as map. (Contributed by AV, 14-Dec-2018.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐼 = (𝑀...𝑁)) & ⊢ (𝜑 → ∀𝑖 ∈ 𝐼 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ 𝐼 ↦ 𝑋)) ∈ 𝐵) | ||
Theorem | gsum2dlem1 18192* | Lemma 1 for gsum2d 18194. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → dom 𝐴 ⊆ 𝐷) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) | ||
Theorem | gsum2dlem2 18193* | Lemma for gsum2d 18194. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → dom 𝐴 ⊆ 𝐷) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ↾ dom (𝐹 supp 0 )))) = (𝐺 Σg (𝑗 ∈ dom (𝐹 supp 0 ) ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) | ||
Theorem | gsum2d 18194* | Write a sum over a two-dimensional region as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → dom 𝐴 ⊆ 𝐷) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑗 ∈ 𝐷 ↦ (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘)))))) | ||
Theorem | gsum2d2lem 18195* | Lemma for gsum2d2 18196: show the function is finitely supported. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 9-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 ) ⇒ ⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 ) | ||
Theorem | gsum2d2 18196* | Write a group sum over a two-dimensional region as a double sum. (Note that 𝐶(𝑗) is a function of 𝑗.) (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋))))) | ||
Theorem | gsumcom2 18197* | Two-dimensional commutation of a group sum. Note that while 𝐴 and 𝐷 are constants w.r.t. 𝑗, 𝑘, 𝐶(𝑗) and 𝐸(𝑘) are not. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 ) & ⊢ (𝜑 → 𝐷 ∈ 𝑌) & ⊢ (𝜑 → ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ↔ (𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸))) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑘 ∈ 𝐷, 𝑗 ∈ 𝐸 ↦ 𝑋))) | ||
Theorem | gsumxp 18198* | Write a group sum over a cartesian product as a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 9-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)))))) | ||
Theorem | gsumcom 18199* | Commute the arguments of a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑘 ∈ 𝐶, 𝑗 ∈ 𝐴 ↦ 𝑋))) | ||
Theorem | prdsgsum 18200* | Finite commutative sums in a product structure are taken componentwise. (Contributed by Stefan O'Rear, 1-Feb-2015.) (Revised by Mario Carneiro, 3-Jul-2015.) (Revised by AV, 9-Jun-2019.) |
⊢ 𝑌 = (𝑆Xs(𝑥 ∈ 𝐼 ↦ 𝑅)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑌) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑅 ∈ CMnd) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |