| Metamath
Proof Explorer Theorem List (p. 201 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | fsfnn0gsumfsffz 20001* | 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 20002* | 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 20003* | 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 20004* | 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 20005* | 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 20006* | Lemma for telgsumfzs 20007 (induction step). (Contributed by AV, 23-Nov-2019.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝑦 ∈ (ℤ≥‘𝑀) ∧ (𝜑 ∧ ∀𝑘 ∈ (𝑀...((𝑦 + 1) + 1))𝐶 ∈ 𝐵)) → ((𝐺 Σg (𝑖 ∈ (𝑀...𝑦) ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = (⦋𝑀 / 𝑘⦌𝐶 − ⦋(𝑦 + 1) / 𝑘⦌𝐶) → (𝐺 Σg (𝑖 ∈ (𝑀...(𝑦 + 1)) ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = (⦋𝑀 / 𝑘⦌𝐶 − ⦋((𝑦 + 1) + 1) / 𝑘⦌𝐶))) | ||
| Theorem | telgsumfzs 20007* | 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 20008* | Telescoping group sum ranging over a finite set of sequential integers, using implicit substitution, analogous to telfsum 15840. (Contributed by AV, 23-Nov-2019.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...(𝑁 + 1))𝐴 ∈ 𝐵) & ⊢ (𝑘 = 𝑖 → 𝐴 = 𝐿) & ⊢ (𝑘 = (𝑖 + 1) → 𝐴 = 𝐶) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷) & ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐸) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (𝑀...𝑁) ↦ (𝐿 − 𝐶))) = (𝐷 − 𝐸)) | ||
| Theorem | telgsumfz0s 20009* | 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 20010* | Telescoping finite group sum ranging over nonnegative integers, using implicit substitution, analogous to telfsum 15840. (Contributed by AV, 23-Nov-2019.) |
| ⊢ 𝐾 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑘 ∈ (0...(𝑆 + 1))𝐴 ∈ 𝐾) & ⊢ (𝑘 = 𝑖 → 𝐴 = 𝐵) & ⊢ (𝑘 = (𝑖 + 1) → 𝐴 = 𝐶) & ⊢ (𝑘 = 0 → 𝐴 = 𝐷) & ⊢ (𝑘 = (𝑆 + 1) → 𝐴 = 𝐸) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (0...𝑆) ↦ (𝐵 − 𝐶))) = (𝐷 − 𝐸)) | ||
| Theorem | telgsums 20011* | 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 20012* | 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 20013 | Internal direct product of a family of subgroups. |
| class DProd | ||
| Syntax | cdpj 20014 | Projection operator for a direct product. |
| class dProj | ||
| Definition | df-dprd 20015* | 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 20016* | 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 20017 | 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 20018* | 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 20019* | 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 20020 | 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 20021 | 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 20022 | 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 20023* | 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 20024* | 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 20025 | Reverse closure for the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
| ⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) | ||
| Theorem | dprdf 20026 | The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
| ⊢ (𝐺dom DProd 𝑆 → 𝑆:dom 𝑆⟶(SubGrp‘𝐺)) | ||
| Theorem | dprdf2 20027 | The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) ⇒ ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) | ||
| Theorem | dprdcntz 20028 | The function 𝑆 is a family having pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝐼) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌))) | ||
| Theorem | dprddisj 20029 | 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 20030* | 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 20031* | 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 20032* | 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 20033* | 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 20034* | 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 20035* | 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 20036 | 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 20037* | 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 20038* | 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 20039* | 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 20040* | 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 20041* | 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 20042* | 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 20043* | 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 20044 | 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 20045 | Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝐺 DProd 𝑆)) | ||
| Theorem | dprdlub 20046* | 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 20047 | 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 20048 | Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐴 ⊆ 𝐼) ⇒ ⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐴) ∧ (𝐺 DProd (𝑆 ↾ 𝐴)) ⊆ (𝐺 DProd 𝑆))) | ||
| Theorem | dprdss 20049* | 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 20050* | 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 20051 | 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 20052 | 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 20053 | 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 20054 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubGrp‘𝐺) → (𝐻dom DProd 𝑆 ↔ (𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴))) | ||
| Theorem | subgdprd 20055 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 𝐴) ⇒ ⊢ (𝜑 → (𝐻 DProd 𝑆) = (𝐺 DProd 𝑆)) | ||
| Theorem | dprdsn 20056 | 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 20057* | Lemma for dmdprdsplit 20067. (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 20058 | The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐶 ⊆ 𝐼) & ⊢ (𝜑 → 𝐷 ⊆ 𝐼) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) | ||
| Theorem | dprddisj2 20059 | 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 20060* | 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 20061* | 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 20062* | 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 20063* | 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 20064* | 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 20065 | Lemma for dmdprdsplit 20067. (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 20066 | 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 20067 | 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 }))) | ||
| Theorem | dprdsplit 20068 | The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 25-Apr-2016.) |
| ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ (𝜑 → 𝐼 = (𝐶 ∪ 𝐷)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝐺dom DProd 𝑆) ⇒ ⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝐺 DProd (𝑆 ↾ 𝐶)) ⊕ (𝐺 DProd (𝑆 ↾ 𝐷)))) | ||
| Theorem | dmdprdpr 20069 | A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.) |
| ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → (𝐺dom DProd {〈∅, 𝑆〉, 〈1o, 𝑇〉} ↔ (𝑆 ⊆ (𝑍‘𝑇) ∧ (𝑆 ∩ 𝑇) = { 0 }))) | ||
| Theorem | dprdpr 20070 | A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ⊆ (𝑍‘𝑇)) & ⊢ (𝜑 → (𝑆 ∩ 𝑇) = { 0 }) ⇒ ⊢ (𝜑 → (𝐺 DProd {〈∅, 𝑆〉, 〈1o, 𝑇〉}) = (𝑆 ⊕ 𝑇)) | ||
| Theorem | dpjlem 20071 | Lemma for theorems about direct product projection. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ {𝑋})) = (𝑆‘𝑋)) | ||
| Theorem | dpjcntz 20072 | The two subgroups that appear in dpjval 20076 commute. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))))) | ||
| Theorem | dpjdisj 20073 | The two subgroups that appear in dpjval 20076 are disjoint. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝜑 → ((𝑆‘𝑋) ∩ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))) = { 0 }) | ||
| Theorem | dpjlsm 20074 | The two subgroups that appear in dpjval 20076 add to the full direct product. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝑆‘𝑋) ⊕ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))))) | ||
| Theorem | dpjfval 20075* | Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ 𝑄 = (proj1‘𝐺) ⇒ ⊢ (𝜑 → 𝑃 = (𝑖 ∈ 𝐼 ↦ ((𝑆‘𝑖)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑖})))))) | ||
| Theorem | dpjval 20076 | Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ 𝑄 = (proj1‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑃‘𝑋) = ((𝑆‘𝑋)𝑄(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))))) | ||
| Theorem | dpjf 20077 | The 𝑋-th index projection is a function from the direct product to the 𝑋-th factor. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑃‘𝑋):(𝐺 DProd 𝑆)⟶(𝑆‘𝑋)) | ||
| Theorem | dpjidcl 20078* | The key property of projections: the sum of all the projections of 𝐴 is 𝐴. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝐴 ∈ (𝐺 DProd 𝑆)) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } ⇒ ⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ ((𝑃‘𝑥)‘𝐴)) ∈ 𝑊 ∧ 𝐴 = (𝐺 Σg (𝑥 ∈ 𝐼 ↦ ((𝑃‘𝑥)‘𝐴))))) | ||
| Theorem | dpjeq 20079* | Decompose a group sum into projections. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝐴 ∈ (𝐺 DProd 𝑆)) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐶) ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐴 = (𝐺 Σg (𝑥 ∈ 𝐼 ↦ 𝐶)) ↔ ∀𝑥 ∈ 𝐼 ((𝑃‘𝑥)‘𝐴) = 𝐶)) | ||
| Theorem | dpjid 20080* | The key property of projections: the sum of all the projections of 𝐴 is 𝐴. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝐴 ∈ (𝐺 DProd 𝑆)) ⇒ ⊢ (𝜑 → 𝐴 = (𝐺 Σg (𝑥 ∈ 𝐼 ↦ ((𝑃‘𝑥)‘𝐴)))) | ||
| Theorem | dpjlid 20081 | The 𝑋-th index projection acts as the identity on elements of the 𝑋-th factor. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ (𝑆‘𝑋)) ⇒ ⊢ (𝜑 → ((𝑃‘𝑋)‘𝐴) = 𝐴) | ||
| Theorem | dpjrid 20082 | The 𝑌-th index projection annihilates elements of other factors. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ (𝑆‘𝑋)) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝑌 ∈ 𝐼) & ⊢ (𝜑 → 𝑌 ≠ 𝑋) ⇒ ⊢ (𝜑 → ((𝑃‘𝑌)‘𝐴) = 0 ) | ||
| Theorem | dpjghm 20083 | The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑃‘𝑋) ∈ ((𝐺 ↾s (𝐺 DProd 𝑆)) GrpHom 𝐺)) | ||
| Theorem | dpjghm2 20084 | The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ 𝑃 = (𝐺dProj𝑆) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑃‘𝑋) ∈ ((𝐺 ↾s (𝐺 DProd 𝑆)) GrpHom (𝐺 ↾s (𝑆‘𝑋)))) | ||
| Theorem | ablfacrplem 20085* | Lemma for ablfacrp2 20087. (Contributed by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} & ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) & ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁)) ⇒ ⊢ (𝜑 → ((♯‘𝐾) gcd 𝑁) = 1) | ||
| Theorem | ablfacrp 20086* | A finite abelian group whose order factors into relatively prime integers, itself "factors" into two subgroups 𝐾, 𝐿 that have trivial intersection and whose product is the whole group. Lemma 6.1C.2 of [Shapiro], p. 199. (Contributed by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} & ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) & ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁)) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝜑 → ((𝐾 ∩ 𝐿) = { 0 } ∧ (𝐾 ⊕ 𝐿) = 𝐵)) | ||
| Theorem | ablfacrp2 20087* | The factors 𝐾, 𝐿 of ablfacrp 20086 have the expected orders (which allows for repeated application to decompose 𝐺 into subgroups of prime-power order). Lemma 6.1C.2 of [Shapiro], p. 199. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} & ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) & ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁)) ⇒ ⊢ (𝜑 → ((♯‘𝐾) = 𝑀 ∧ (♯‘𝐿) = 𝑁)) | ||
| Theorem | ablfac1lem 20088* | Lemma for ablfac1b 20090. Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝑀 = (𝑃↑(𝑃 pCnt (♯‘𝐵))) & ⊢ 𝑁 = ((♯‘𝐵) / 𝑀) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑀 gcd 𝑁) = 1 ∧ (♯‘𝐵) = (𝑀 · 𝑁))) | ||
| Theorem | ablfac1a 20089* | The factors of ablfac1b 20090 are of prime power order. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → (♯‘(𝑆‘𝑃)) = (𝑃↑(𝑃 pCnt (♯‘𝐵)))) | ||
| Theorem | ablfac1b 20090* | Any abelian group is the direct product of factors of prime power order (with the exact order further matching the prime factorization of the group order). (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) ⇒ ⊢ (𝜑 → 𝐺dom DProd 𝑆) | ||
| Theorem | ablfac1c 20091* | The factors of ablfac1b 20090 cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝐵) | ||
| Theorem | ablfac1eulem 20092* | Lemma for ablfac1eu 20093. (Contributed by Mario Carneiro, 27-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵)) & ⊢ (𝜑 → dom 𝑇 = 𝐴) & ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → ¬ 𝑃 ∥ (♯‘(𝐺 DProd (𝑇 ↾ (𝐴 ∖ {𝑃}))))) | ||
| Theorem | ablfac1eu 20093* | The factorization of ablfac1b 20090 is unique, in that any other factorization into prime power factors (even if the exponents are different) must be equal to 𝑆. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵)) & ⊢ (𝜑 → dom 𝑇 = 𝐴) & ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) ⇒ ⊢ (𝜑 → 𝑇 = 𝑆) | ||
| Theorem | pgpfac1lem1 20094* | Lemma for pgpfac1 20100. (Contributed by Mario Carneiro, 27-Apr-2016.) |
| ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) & ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) = 𝑈) | ||
| Theorem | pgpfac1lem2 20095* | Lemma for pgpfac1 20100. (Contributed by Mario Carneiro, 27-Apr-2016.) |
| ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) & ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) & ⊢ (𝜑 → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (𝜑 → (𝑃 · 𝐶) ∈ (𝑆 ⊕ 𝑊)) | ||
| Theorem | pgpfac1lem3a 20096* | Lemma for pgpfac1 20100. (Contributed by Mario Carneiro, 4-Jun-2016.) |
| ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) & ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) & ⊢ (𝜑 → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ((𝑃 · 𝐶)(+g‘𝐺)(𝑀 · 𝐴)) ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝑃 ∥ 𝐸 ∧ 𝑃 ∥ 𝑀)) | ||
| Theorem | pgpfac1lem3 20097* | Lemma for pgpfac1 20100. (Contributed by Mario Carneiro, 27-Apr-2016.) |
| ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) & ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) & ⊢ (𝜑 → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → ((𝑃 · 𝐶)(+g‘𝐺)(𝑀 · 𝐴)) ∈ 𝑊) & ⊢ 𝐷 = (𝐶(+g‘𝐺)((𝑀 / 𝑃) · 𝐴)) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑈)) | ||
| Theorem | pgpfac1lem4 20098* | Lemma for pgpfac1 20100. (Contributed by Mario Carneiro, 27-Apr-2016.) |
| ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) & ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) & ⊢ (𝜑 → 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝑈)) | ||
| Theorem | pgpfac1lem5 20099* | Lemma for pgpfac1 20100. (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 20100* | 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 } ∧ (𝑆 ⊕ 𝑡) = 𝐵)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |