Home | Metamath
Proof Explorer Theorem List (p. 191 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gsummptfidmsub 19001* | 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 19002* | 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 19003* | 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 19004* | 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 19005* | 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 | gsumpr 19006* | Group sum of a pair. (Contributed by AV, 6-Dec-2018.) (Proof shortened by AV, 28-Jul-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐶) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐷) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ∧ 𝑀 ≠ 𝑁) ∧ (𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵)) → (𝐺 Σg (𝑘 ∈ {𝑀, 𝑁} ↦ 𝐴)) = (𝐶 + 𝐷)) | ||
Theorem | gsumzunsnd 19007* | Append an element to a finite group sum, more general version of gsumunsnd 19009. (Contributed by AV, 7-Oct-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝐹 = (𝑘 ∈ (𝐴 ∪ {𝑀}) ↦ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → ¬ 𝑀 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 = 𝑀) → 𝑋 = 𝑌) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐺 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) + 𝑌)) | ||
Theorem | gsumunsnfd 19008* | 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 19009* | 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 19010* | 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 19011* | 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 19012* | 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 19013 | 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 19014* | 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 19015* | 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‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ CMnd) & ⊢ (𝜑 → (𝐴 ∪ 𝐶) ∈ Fin) & ⊢ (𝜑 → (𝐴 ∩ 𝐶) = ∅) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∪ 𝐶)) → 𝐷 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ (𝐴 ∪ 𝐶) ↦ 𝐷)) = ((𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐷)) + (𝑊 Σg (𝑥 ∈ 𝐶 ↦ 𝐷)))) | ||
Theorem | gsummpt1n0 19016* | If only one summand in a finite group sum is not zero, the whole sum equals this summand. More general version of gsummptif1n0 19017. (Contributed by AV, 11-Oct-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ 𝐹 = (𝑛 ∈ 𝐼 ↦ if(𝑛 = 𝑋, 𝐴, 0 )) & ⊢ (𝜑 → ∀𝑛 ∈ 𝐼 𝐴 ∈ (Base‘𝐺)) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = ⦋𝑋 / 𝑛⦌𝐴) | ||
Theorem | gsummptif1n0 19017* | 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 19018* | Closure of a finite group sum over a finite set as map. (Contributed by AV, 29-Dec-2018.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → ∀𝑖 ∈ 𝑁 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ 𝑁 ↦ 𝑋)) ∈ 𝐵) | ||
Theorem | gsummptfif1o 19019* | 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 19020* | 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 19021* | Lemma 1 for gsum2d 19023. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → dom 𝐴 ⊆ 𝐷) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) | ||
Theorem | gsum2dlem2 19022* | Lemma for gsum2d 19023. (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 19023* | 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 19024* | Lemma for gsum2d2 19025: 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 19025* | 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 19026* | 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 19027* | 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 19028* | Commute the arguments of a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑘 ∈ 𝐶, 𝑗 ∈ 𝐴 ↦ 𝑋))) | ||
Theorem | gsumcom3 19029* | A commutative law for finitely supported iterated sums. (Contributed by Stefan O'Rear, 2-Nov-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)))) = (𝐺 Σg (𝑘 ∈ 𝐶 ↦ (𝐺 Σg (𝑗 ∈ 𝐴 ↦ 𝑋))))) | ||
Theorem | gsumcom3fi 19030* | A commutative law for finite iterated sums. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐶 ∈ Fin) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)))) = (𝐺 Σg (𝑘 ∈ 𝐶 ↦ (𝐺 Σg (𝑗 ∈ 𝐴 ↦ 𝑋))))) | ||
Theorem | gsumxp2 19031* | Write a group sum over a cartesian product as a double sum in two ways. This corresponds to the first equation in [Lang] p. 6. (Contributed by AV, 27-Dec-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ (𝜑 → 𝐹:(𝐴 × 𝐶)⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ 𝐶 ↦ (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝑗𝐹𝑘))))) = (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ (𝑗𝐹𝑘)))))) | ||
Theorem | prdsgsum 19032* | 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 (𝑦 ∈ 𝐽 ↦ 𝑈)))) | ||
Theorem | pwsgsum 19033* | Finite commutative sums in a power 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.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑌) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝑊) & ⊢ (𝜑 → 𝑅 ∈ CMnd) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽)) → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈)) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑌 Σg (𝑦 ∈ 𝐽 ↦ (𝑥 ∈ 𝐼 ↦ 𝑈))) = (𝑥 ∈ 𝐼 ↦ (𝑅 Σg (𝑦 ∈ 𝐽 ↦ 𝑈)))) | ||
Theorem | fsfnn0gsumfsffz 19034* | Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m ℕ0)) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ 𝐻 = (𝐹 ↾ (0...𝑆)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 0 ) → (𝐺 Σg 𝐹) = (𝐺 Σg 𝐻))) | ||
Theorem | nn0gsumfz 19035* | Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m ℕ0)) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∃𝑓 ∈ (𝐵 ↑m (0...𝑠))(𝑓 = (𝐹 ↾ (0...𝑠)) ∧ ∀𝑥 ∈ ℕ0 (𝑠 < 𝑥 → (𝐹‘𝑥) = 0 ) ∧ (𝐺 Σg 𝐹) = (𝐺 Σg 𝑓))) | ||
Theorem | nn0gsumfz0 19036* | Replacing a finitely supported function over the nonnegative integers by a function over a finite set of sequential integers in a finite group sum. (Contributed by AV, 9-Oct-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m ℕ0)) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ ℕ0 ∃𝑓 ∈ (𝐵 ↑m (0...𝑠))(𝐺 Σg 𝐹) = (𝐺 Σg 𝑓)) | ||
Theorem | gsummptnn0fz 19037* | A final group sum over a function over the nonnegative integers (given as mapping) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 3-Jul-2022.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝑆 < 𝑘 → 𝐶 = 0 )) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ ℕ0 ↦ 𝐶)) = (𝐺 Σg (𝑘 ∈ (0...𝑆) ↦ 𝐶))) | ||
Theorem | gsummptnn0fzfv 19038* | A final group sum over a function over the nonnegative integers (given as mapping to its function values) is equal to a final group sum over a finite interval of nonnegative integers. (Contributed by AV, 10-Oct-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑m ℕ0)) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 0 )) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ ℕ0 ↦ (𝐹‘𝑘))) = (𝐺 Σg (𝑘 ∈ (0...𝑆) ↦ (𝐹‘𝑘)))) | ||
Theorem | telgsumfzslem 19039* | Lemma for telgsumfzs 19040 (induction step). (Contributed by AV, 23-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝑦 ∈ (ℤ≥‘𝑀) ∧ (𝜑 ∧ ∀𝑘 ∈ (𝑀...((𝑦 + 1) + 1))𝐶 ∈ 𝐵)) → ((𝐺 Σg (𝑖 ∈ (𝑀...𝑦) ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = (⦋𝑀 / 𝑘⦌𝐶 − ⦋(𝑦 + 1) / 𝑘⦌𝐶) → (𝐺 Σg (𝑖 ∈ (𝑀...(𝑦 + 1)) ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = (⦋𝑀 / 𝑘⦌𝐶 − ⦋((𝑦 + 1) + 1) / 𝑘⦌𝐶))) | ||
Theorem | telgsumfzs 19040* | Telescoping group sum ranging over a finite set of sequential integers, using explicit substitution. (Contributed by AV, 23-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...(𝑁 + 1))𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (𝑀...𝑁) ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = (⦋𝑀 / 𝑘⦌𝐶 − ⦋(𝑁 + 1) / 𝑘⦌𝐶)) | ||
Theorem | telgsumfz 19041* | Telescoping group sum ranging over a finite set of sequential integers, using implicit substitution, analogous to telfsum 15149. (Contributed by AV, 23-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...(𝑁 + 1))𝐴 ∈ 𝐵) & ⊢ (𝑘 = 𝑖 → 𝐴 = 𝐿) & ⊢ (𝑘 = (𝑖 + 1) → 𝐴 = 𝐶) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷) & ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐸) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (𝑀...𝑁) ↦ (𝐿 − 𝐶))) = (𝐷 − 𝐸)) | ||
Theorem | telgsumfz0s 19042* | Telescoping finite group sum ranging over nonnegative integers, using explicit substitution. (Contributed by AV, 24-Oct-2019.) (Proof shortened by AV, 25-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑘 ∈ (0...(𝑆 + 1))𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (0...𝑆) ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = (⦋0 / 𝑘⦌𝐶 − ⦋(𝑆 + 1) / 𝑘⦌𝐶)) | ||
Theorem | telgsumfz0 19043* | Telescoping finite group sum ranging over nonnegative integers, using implicit substitution, analogous to telfsum 15149. (Contributed by AV, 23-Nov-2019.) |
⊢ 𝐾 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑘 ∈ (0...(𝑆 + 1))𝐴 ∈ 𝐾) & ⊢ (𝑘 = 𝑖 → 𝐴 = 𝐵) & ⊢ (𝑘 = (𝑖 + 1) → 𝐴 = 𝐶) & ⊢ (𝑘 = 0 → 𝐴 = 𝐷) & ⊢ (𝑘 = (𝑆 + 1) → 𝐴 = 𝐸) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (0...𝑆) ↦ (𝐵 − 𝐶))) = (𝐷 − 𝐸)) | ||
Theorem | telgsums 19044* | Telescoping finitely supported group sum ranging over nonnegative integers, using explicit substitution. (Contributed by AV, 24-Oct-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ − = (-g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝑆 < 𝑘 → 𝐶 = 0 )) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ ℕ0 ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = ⦋0 / 𝑘⦌𝐶) | ||
Theorem | telgsum 19045* | Telescoping finitely supported group sum ranging over nonnegative integers, using implicit substitution. (Contributed by AV, 31-Dec-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ − = (-g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 𝐴 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑘 ∈ ℕ0 (𝑆 < 𝑘 → 𝐴 = 0 )) & ⊢ (𝑘 = 𝑖 → 𝐴 = 𝐶) & ⊢ (𝑘 = (𝑖 + 1) → 𝐴 = 𝐷) & ⊢ (𝑘 = 0 → 𝐴 = 𝐸) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ ℕ0 ↦ (𝐶 − 𝐷))) = 𝐸) | ||
Syntax | cdprd 19046 | Internal direct product of a family of subgroups. |
class DProd | ||
Syntax | cdpj 19047 | Projection operator for a direct product. |
class dProj | ||
Definition | df-dprd 19048* | Define the internal direct product of a family of subgroups. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
⊢ DProd = (𝑔 ∈ Grp, 𝑠 ∈ {ℎ ∣ (ℎ:dom ℎ⟶(SubGrp‘𝑔) ∧ ∀𝑥 ∈ dom ℎ(∀𝑦 ∈ (dom ℎ ∖ {𝑥})(ℎ‘𝑥) ⊆ ((Cntz‘𝑔)‘(ℎ‘𝑦)) ∧ ((ℎ‘𝑥) ∩ ((mrCls‘(SubGrp‘𝑔))‘∪ (ℎ “ (dom ℎ ∖ {𝑥})))) = {(0g‘𝑔)}))} ↦ ran (𝑓 ∈ {ℎ ∈ X𝑥 ∈ dom 𝑠(𝑠‘𝑥) ∣ ℎ finSupp (0g‘𝑔)} ↦ (𝑔 Σg 𝑓))) | ||
Definition | df-dpj 19049* | Define the projection operator for a direct product. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ dProj = (𝑔 ∈ Grp, 𝑠 ∈ (dom DProd “ {𝑔}) ↦ (𝑖 ∈ dom 𝑠 ↦ ((𝑠‘𝑖)(proj1‘𝑔)(𝑔 DProd (𝑠 ↾ (dom 𝑠 ∖ {𝑖})))))) | ||
Theorem | reldmdprd 19050 | The domain of the internal direct product operation is a relation. (Contributed by Mario Carneiro, 25-Apr-2016.) (Proof shortened by AV, 11-Jul-2019.) |
⊢ Rel dom DProd | ||
Theorem | dmdprd 19051* | The domain of definition of the internal direct product, which states that 𝑆 is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.) (Proof shortened by AV, 11-Jul-2019.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ dom 𝑆 = 𝐼) → (𝐺dom DProd 𝑆 ↔ (𝐺 ∈ Grp ∧ 𝑆:𝐼⟶(SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝐼 (∀𝑦 ∈ (𝐼 ∖ {𝑥})(𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦)) ∧ ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) = { 0 })))) | ||
Theorem | dmdprdd 19052* | Show that a given family is a direct product decomposition. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐼 ∧ 𝑥 ≠ 𝑦)) → (𝑆‘𝑥) ⊆ (𝑍‘(𝑆‘𝑦))) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑆‘𝑥) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑥})))) ⊆ { 0 }) ⇒ ⊢ (𝜑 → 𝐺dom DProd 𝑆) | ||
Theorem | dprddomprc 19053 | A family of subgroups indexed by a proper class cannot be a family of subgroups for an internal direct product. (Contributed by AV, 13-Jul-2019.) |
⊢ (dom 𝑆 ∉ V → ¬ 𝐺dom DProd 𝑆) | ||
Theorem | dprddomcld 19054 | If a family of subgroups is a family of subgroups for an internal direct product, then it is indexed by a set. (Contributed by AV, 13-Jul-2019.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) ⇒ ⊢ (𝜑 → 𝐼 ∈ V) | ||
Theorem | dprdval0prc 19055 | The internal direct product of a family of subgroups indexed by a proper class is empty. (Contributed by AV, 13-Jul-2019.) |
⊢ (dom 𝑆 ∉ V → (𝐺 DProd 𝑆) = ∅) | ||
Theorem | dprdval 19056* | The value of the internal direct product operation, which is a function mapping the (infinite, but finitely supported) cartesian product of subgroups (which mutually commute and have trivial intersections) to its (group) sum . (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } ⇒ ⊢ ((𝐺dom DProd 𝑆 ∧ dom 𝑆 = 𝐼) → (𝐺 DProd 𝑆) = ran (𝑓 ∈ 𝑊 ↦ (𝐺 Σg 𝑓))) | ||
Theorem | eldprd 19057* | A class 𝐴 is an internal direct product iff it is the (group) sum of an infinite, but finitely supported cartesian product of subgroups (which mutually commute and have trivial intersections). (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } ⇒ ⊢ (dom 𝑆 = 𝐼 → (𝐴 ∈ (𝐺 DProd 𝑆) ↔ (𝐺dom DProd 𝑆 ∧ ∃𝑓 ∈ 𝑊 𝐴 = (𝐺 Σg 𝑓)))) | ||
Theorem | dprdgrp 19058 | Reverse closure for the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) | ||
Theorem | dprdf 19059 | The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝐺dom DProd 𝑆 → 𝑆:dom 𝑆⟶(SubGrp‘𝐺)) | ||
Theorem | dprdf2 19060 | The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) ⇒ ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) | ||
Theorem | dprdcntz 19061 | The function 𝑆 is a family having pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝐼) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌))) | ||
Theorem | dprddisj 19062 | The function 𝑆 is a family having trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) = { 0 }) | ||
Theorem | dprdw 19063* | The property of being a finitely supported function in the family 𝑆. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) ⇒ ⊢ (𝜑 → (𝐹 ∈ 𝑊 ↔ (𝐹 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝐹‘𝑥) ∈ (𝑆‘𝑥) ∧ 𝐹 finSupp 0 ))) | ||
Theorem | dprdwd 19064* | A mapping being a finitely supported function in the family 𝑆. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) (Proof shortened by OpenAI, 30-Mar-2020.) |
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐴 ∈ (𝑆‘𝑥)) & ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐴) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐴) ∈ 𝑊) | ||
Theorem | dprdff 19065* | A finitely supported function in 𝑆 is a function into the base. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) | ||
Theorem | dprdfcl 19066* | A finitely supported function in 𝑆 has its 𝑋-th element in 𝑆(𝑋). (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐼) → (𝐹‘𝑋) ∈ (𝑆‘𝑋)) | ||
Theorem | dprdffsupp 19067* | A finitely supported function in 𝑆 is a finitely supported function. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) ⇒ ⊢ (𝜑 → 𝐹 finSupp 0 ) | ||
Theorem | dprdfcntz 19068* | A function on the elements of an internal direct product has pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 11-Jul-2019.) |
⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) | ||
Theorem | dprdssv 19069 | The internal direct product of a family of subgroups is a subset of the base. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 DProd 𝑆) ⊆ 𝐵 | ||
Theorem | dprdfid 19070* | A function mapping all but one arguments to zero sums to the value of this argument in a direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ (𝑆‘𝑋)) & ⊢ 𝐹 = (𝑛 ∈ 𝐼 ↦ if(𝑛 = 𝑋, 𝐴, 0 )) ⇒ ⊢ (𝜑 → (𝐹 ∈ 𝑊 ∧ (𝐺 Σg 𝐹) = 𝐴)) | ||
Theorem | eldprdi 19071* | The domain of definition of the internal direct product, which states that 𝑆 is a family of subgroups that mutually commute and have trivial intersections. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ (𝐺 DProd 𝑆)) | ||
Theorem | dprdfinv 19072* | Take the inverse of a group sum over a family of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ (𝜑 → ((𝑁 ∘ 𝐹) ∈ 𝑊 ∧ (𝐺 Σg (𝑁 ∘ 𝐹)) = (𝑁‘(𝐺 Σg 𝐹)))) | ||
Theorem | dprdfadd 19073* | Take the sum of group sums over two families of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝜑 → ((𝐹 ∘f + 𝐻) ∈ 𝑊 ∧ (𝐺 Σg (𝐹 ∘f + 𝐻)) = ((𝐺 Σg 𝐹) + (𝐺 Σg 𝐻)))) | ||
Theorem | dprdfsub 19074* | Take the difference of group sums over two families of elements of disjoint subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝜑 → ((𝐹 ∘f − 𝐻) ∈ 𝑊 ∧ (𝐺 Σg (𝐹 ∘f − 𝐻)) = ((𝐺 Σg 𝐹) − (𝐺 Σg 𝐻)))) | ||
Theorem | dprdfeq0 19075* | The zero function is the only function that sums to zero in a direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) ⇒ ⊢ (𝜑 → ((𝐺 Σg 𝐹) = 0 ↔ 𝐹 = (𝑥 ∈ 𝐼 ↦ 0 ))) | ||
Theorem | dprdf11 19076* | Two group sums over a direct product that give the same value are equal as functions. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) & ⊢ (𝜑 → 𝐻 ∈ 𝑊) ⇒ ⊢ (𝜑 → ((𝐺 Σg 𝐹) = (𝐺 Σg 𝐻) ↔ 𝐹 = 𝐻)) | ||
Theorem | dprdsubg 19077 | The internal direct product of a family of subgroups is a subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) ∈ (SubGrp‘𝐺)) | ||
Theorem | dprdub 19078 | Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝐺 DProd 𝑆)) | ||
Theorem | dprdlub 19079* | The direct product is smaller than any subgroup which contains the factors. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑆‘𝑘) ⊆ 𝑇) ⇒ ⊢ (𝜑 → (𝐺 DProd 𝑆) ⊆ 𝑇) | ||
Theorem | dprdspan 19080 | The direct product is the span of the union of the factors. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ (𝐺dom DProd 𝑆 → (𝐺 DProd 𝑆) = (𝐾‘∪ ran 𝑆)) | ||
Theorem | dprdres 19081 | Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐴 ⊆ 𝐼) ⇒ ⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐴) ∧ (𝐺 DProd (𝑆 ↾ 𝐴)) ⊆ (𝐺 DProd 𝑆))) | ||
Theorem | dprdss 19082* | Create a direct product by finding subgroups inside each factor of another direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑇) & ⊢ (𝜑 → dom 𝑇 = 𝐼) & ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐼) → (𝑆‘𝑘) ⊆ (𝑇‘𝑘)) ⇒ ⊢ (𝜑 → (𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) ⊆ (𝐺 DProd 𝑇))) | ||
Theorem | dprdz 19083* | A family consisting entirely of trivial groups is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐼 ∈ 𝑉) → (𝐺dom DProd (𝑥 ∈ 𝐼 ↦ { 0 }) ∧ (𝐺 DProd (𝑥 ∈ 𝐼 ↦ { 0 })) = { 0 })) | ||
Theorem | dprd0 19084 | The empty family is an internal direct product, the product of which is the trivial subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → (𝐺dom DProd ∅ ∧ (𝐺 DProd ∅) = { 0 })) | ||
Theorem | dprdf1o 19085 | Rearrange the index set of a direct product family. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐹:𝐽–1-1-onto→𝐼) ⇒ ⊢ (𝜑 → (𝐺dom DProd (𝑆 ∘ 𝐹) ∧ (𝐺 DProd (𝑆 ∘ 𝐹)) = (𝐺 DProd 𝑆))) | ||
Theorem | dprdf1 19086 | Rearrange the index set of a direct product family. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐹:𝐽–1-1→𝐼) ⇒ ⊢ (𝜑 → (𝐺dom DProd (𝑆 ∘ 𝐹) ∧ (𝐺 DProd (𝑆 ∘ 𝐹)) ⊆ (𝐺 DProd 𝑆))) | ||
Theorem | subgdmdprd 19087 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubGrp‘𝐺) → (𝐻dom DProd 𝑆 ↔ (𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴))) | ||
Theorem | subgdprd 19088 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 𝐴) ⇒ ⊢ (𝜑 → (𝐻 DProd 𝑆) = (𝐺 DProd 𝑆)) | ||
Theorem | dprdsn 19089 | A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → (𝐺dom DProd {〈𝐴, 𝑆〉} ∧ (𝐺 DProd {〈𝐴, 𝑆〉}) = 𝑆)) | ||
Theorem | dmdprdsplitlem 19090* | Lemma for dmdprdsplit 19100. (Contributed by Mario Carneiro, 25-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐴 ⊆ 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) & ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ (𝐺 DProd (𝑆 ↾ 𝐴))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ (𝐼 ∖ 𝐴)) → (𝐹‘𝑋) = 0 ) | ||
Theorem | dprdcntz2 19091 | The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐶 ⊆ 𝐼) & ⊢ (𝜑 → 𝐷 ⊆ 𝐼) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) | ||
Theorem | dprddisj2 19092 | The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐶 ⊆ 𝐼) & ⊢ (𝜑 → 𝐷 ⊆ 𝐼) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 }) | ||
Theorem | dprd2dlem2 19093* | The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) & ⊢ (𝜑 → dom 𝐴 ⊆ 𝐼) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) & ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐴) → (𝑆‘𝑋) ⊆ (𝐺 DProd (𝑗 ∈ (𝐴 “ {(1st ‘𝑋)}) ↦ ((1st ‘𝑋)𝑆𝑗)))) | ||
Theorem | dprd2dlem1 19094* | The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) & ⊢ (𝜑 → dom 𝐴 ⊆ 𝐼) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) & ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐶 ⊆ 𝐼) ⇒ ⊢ (𝜑 → (𝐾‘∪ (𝑆 “ (𝐴 ↾ 𝐶))) = (𝐺 DProd (𝑖 ∈ 𝐶 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) | ||
Theorem | dprd2da 19095* | The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) & ⊢ (𝜑 → dom 𝐴 ⊆ 𝐼) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) & ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → 𝐺dom DProd 𝑆) | ||
Theorem | dprd2db 19096* | The direct product of a collection of direct products. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝑆:𝐴⟶(SubGrp‘𝐺)) & ⊢ (𝜑 → dom 𝐴 ⊆ 𝐼) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))) & ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗))))) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → (𝐺 DProd 𝑆) = (𝐺 DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ (𝐴 “ {𝑖}) ↦ (𝑖𝑆𝑗)))))) | ||
Theorem | dprd2d2 19097* | The direct product of a collection of direct products. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ ((𝜑 ∧ (𝑖 ∈ 𝐼 ∧ 𝑗 ∈ 𝐽)) → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → 𝐺dom DProd (𝑗 ∈ 𝐽 ↦ 𝑆)) & ⊢ (𝜑 → 𝐺dom DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ 𝐽 ↦ 𝑆)))) ⇒ ⊢ (𝜑 → (𝐺dom DProd (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ 𝑆) ∧ (𝐺 DProd (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ 𝑆)) = (𝐺 DProd (𝑖 ∈ 𝐼 ↦ (𝐺 DProd (𝑗 ∈ 𝐽 ↦ 𝑆)))))) | ||
Theorem | dmdprdsplit2lem 19098 | Lemma for dmdprdsplit 19100. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷)) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐶)) & ⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐷)) & ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) & ⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 }) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝐶) → ((𝑌 ∈ 𝐼 → (𝑋 ≠ 𝑌 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌)))) ∧ ((𝑆‘𝑋) ∩ (𝐾‘∪ (𝑆 “ (𝐼 ∖ {𝑋})))) ⊆ { 0 })) | ||
Theorem | dmdprdsplit2 19099 | The direct product splits into the direct product of any partition of the index set. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷)) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐶)) & ⊢ (𝜑 → 𝐺dom DProd (𝑆 ↾ 𝐷)) & ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) & ⊢ (𝜑 → ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 }) ⇒ ⊢ (𝜑 → 𝐺dom DProd 𝑆) | ||
Theorem | dmdprdsplit 19100 | The direct product splits into the direct product of any partition of the index set. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷)) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝜑 → (𝐺dom DProd 𝑆 ↔ ((𝐺dom DProd (𝑆 ↾ 𝐶) ∧ 𝐺dom DProd (𝑆 ↾ 𝐷)) ∧ (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷))) ∧ ((𝐺 DProd (𝑆 ↾ 𝐶)) ∩ (𝐺 DProd (𝑆 ↾ 𝐷))) = { 0 }))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |