![]() |
Metamath
Proof Explorer Theorem List (p. 201 of 486) | < 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-30851) |
![]() (30852-32374) |
![]() (32375-48553) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dprddomcld 20001 | 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 20002 | 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 20003* | 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 20004* | 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 20005 | Reverse closure for the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) | ||
Theorem | dprdf 20006 | The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝐺dom DProd 𝑆 → 𝑆:dom 𝑆⟶(SubGrp‘𝐺)) | ||
Theorem | dprdf2 20007 | The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) ⇒ ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) | ||
Theorem | dprdcntz 20008 | The function 𝑆 is a family having pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝐼) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌))) | ||
Theorem | dprddisj 20009 | 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 20010* | 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 20011* | 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 20012* | 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 20013* | 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 20014* | 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 20015* | 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 20016 | 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 20017* | 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 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.) (Revised by AV, 14-Jul-2019.) |
⊢ 0 = (0g‘𝐺) & ⊢ 𝑊 = {ℎ ∈ X𝑖 ∈ 𝐼 (𝑆‘𝑖) ∣ ℎ finSupp 0 } & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐹 ∈ 𝑊) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ (𝐺 DProd 𝑆)) | ||
Theorem | dprdfinv 20019* | 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 20020* | 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 20021* | 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 20022* | 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 20023* | 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 20024 | 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 20025 | Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝐺 DProd 𝑆)) | ||
Theorem | dprdlub 20026* | 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 20027 | 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 20028 | Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐴 ⊆ 𝐼) ⇒ ⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐴) ∧ (𝐺 DProd (𝑆 ↾ 𝐴)) ⊆ (𝐺 DProd 𝑆))) | ||
Theorem | dprdss 20029* | 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 20030* | 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 20031 | 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 20032 | 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 20033 | 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 20034 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubGrp‘𝐺) → (𝐻dom DProd 𝑆 ↔ (𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴))) | ||
Theorem | subgdprd 20035 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 𝐴) ⇒ ⊢ (𝜑 → (𝐻 DProd 𝑆) = (𝐺 DProd 𝑆)) | ||
Theorem | dprdsn 20036 | 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 20037* | Lemma for dmdprdsplit 20047. (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 20038 | The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐶 ⊆ 𝐼) & ⊢ (𝜑 → 𝐷 ⊆ 𝐼) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) | ||
Theorem | dprddisj2 20039 | 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 20040* | 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 20041* | 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 20042* | 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 20043* | 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 20044* | 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 20045 | Lemma for dmdprdsplit 20047. (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 20046 | 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 20047 | 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 20048 | 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 20049 | 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 20050 | 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 20051 | Lemma for theorems about direct product projection. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ {𝑋})) = (𝑆‘𝑋)) | ||
Theorem | dpjcntz 20052 | The two subgroups that appear in dpjval 20056 commute. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))))) | ||
Theorem | dpjdisj 20053 | The two subgroups that appear in dpjval 20056 are disjoint. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝜑 → ((𝑆‘𝑋) ∩ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))) = { 0 }) | ||
Theorem | dpjlsm 20054 | The two subgroups that appear in dpjval 20056 add to the full direct product. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝑆‘𝑋) ⊕ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))))) | ||
Theorem | dpjfval 20055* | 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 20056 | 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 20057 | 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 20058* | 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 20059* | 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 20060* | 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 20061 | 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 20062 | 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 20063 | 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 20064 | 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 20065* | Lemma for ablfacrp2 20067. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} & ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) & ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁)) ⇒ ⊢ (𝜑 → ((♯‘𝐾) gcd 𝑁) = 1) | ||
Theorem | ablfacrp 20066* | 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 20067* | The factors 𝐾, 𝐿 of ablfacrp 20066 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 20068* | Lemma for ablfac1b 20070. Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝑀 = (𝑃↑(𝑃 pCnt (♯‘𝐵))) & ⊢ 𝑁 = ((♯‘𝐵) / 𝑀) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → ((𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ) ∧ (𝑀 gcd 𝑁) = 1 ∧ (♯‘𝐵) = (𝑀 · 𝑁))) | ||
Theorem | ablfac1a 20069* | The factors of ablfac1b 20070 are of prime power order. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) ⇒ ⊢ ((𝜑 ∧ 𝑃 ∈ 𝐴) → (♯‘(𝑆‘𝑃)) = (𝑃↑(𝑃 pCnt (♯‘𝐵)))) | ||
Theorem | ablfac1b 20070* | 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 20071* | The factors of ablfac1b 20070 cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝐵) | ||
Theorem | ablfac1eulem 20072* | Lemma for ablfac1eu 20073. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝐴 ⊆ ℙ) & ⊢ 𝐷 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ (𝜑 → 𝐷 ⊆ 𝐴) & ⊢ (𝜑 → (𝐺dom DProd 𝑇 ∧ (𝐺 DProd 𝑇) = 𝐵)) & ⊢ (𝜑 → dom 𝑇 = 𝐴) & ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → 𝐶 ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑞 ∈ 𝐴) → (♯‘(𝑇‘𝑞)) = (𝑞↑𝐶)) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝐴 ∈ Fin) ⇒ ⊢ (𝜑 → ¬ 𝑃 ∥ (♯‘(𝐺 DProd (𝑇 ↾ (𝐴 ∖ {𝑃}))))) | ||
Theorem | ablfac1eu 20073* | The factorization of ablfac1b 20070 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 20074* | Lemma for pgpfac1 20080. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → (𝑆 ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → (𝑆 ⊕ 𝑊) ⊆ 𝑈) & ⊢ (𝜑 → ∀𝑤 ∈ (SubGrp‘𝐺)((𝑤 ⊊ 𝑈 ∧ 𝐴 ∈ 𝑤) → ¬ (𝑆 ⊕ 𝑊) ⊊ 𝑤)) ⇒ ⊢ ((𝜑 ∧ 𝐶 ∈ (𝑈 ∖ (𝑆 ⊕ 𝑊))) → ((𝑆 ⊕ 𝑊) ⊕ (𝐾‘{𝐶})) = 𝑈) | ||
Theorem | pgpfac1lem2 20075* | Lemma for pgpfac1 20080. (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 20076* | Lemma for pgpfac1 20080. (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 20077* | Lemma for pgpfac1 20080. (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 20078* | Lemma for pgpfac1 20080. (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 20079* | Lemma for pgpfac1 20080. (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 20080* | Factorization of a finite abelian p-group. There is a direct product decomposition of any abelian group of prime-power order where one of the factors is cyclic and generated by an element of maximal order. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) & ⊢ 𝑆 = (𝐾‘{𝐴}) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑡 ∈ (SubGrp‘𝐺)((𝑆 ∩ 𝑡) = { 0 } ∧ (𝑆 ⊕ 𝑡) = 𝐵)) | ||
Theorem | pgpfaclem1 20081* | Lemma for pgpfac 20084. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) & ⊢ 𝐻 = (𝐺 ↾s 𝑈) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻)) & ⊢ 𝑂 = (od‘𝐻) & ⊢ 𝐸 = (gEx‘𝐻) & ⊢ 0 = (0g‘𝐻) & ⊢ ⊕ = (LSSum‘𝐻) & ⊢ (𝜑 → 𝐸 ≠ 1) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → (𝑂‘𝑋) = 𝐸) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻)) & ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) & ⊢ (𝜑 → 𝑆 ∈ Word 𝐶) & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → (𝐺 DProd 𝑆) = 𝑊) & ⊢ 𝑇 = (𝑆 ++ 〈“(𝐾‘{𝑋})”〉) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) | ||
Theorem | pgpfaclem2 20082* | Lemma for pgpfac 20084. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) & ⊢ 𝐻 = (𝐺 ↾s 𝑈) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐻)) & ⊢ 𝑂 = (od‘𝐻) & ⊢ 𝐸 = (gEx‘𝐻) & ⊢ 0 = (0g‘𝐻) & ⊢ ⊕ = (LSSum‘𝐻) & ⊢ (𝜑 → 𝐸 ≠ 1) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) & ⊢ (𝜑 → (𝑂‘𝑋) = 𝐸) & ⊢ (𝜑 → 𝑊 ∈ (SubGrp‘𝐻)) & ⊢ (𝜑 → ((𝐾‘{𝑋}) ∩ 𝑊) = { 0 }) & ⊢ (𝜑 → ((𝐾‘{𝑋}) ⊕ 𝑊) = 𝑈) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) | ||
Theorem | pgpfaclem3 20083* | Lemma for pgpfac 20084. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → ∀𝑡 ∈ (SubGrp‘𝐺)(𝑡 ⊊ 𝑈 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑡))) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)) | ||
Theorem | pgpfac 20084* | Full factorization of a finite abelian p-group, by iterating pgpfac1 20080. There is a direct product decomposition of any abelian group of prime-power order into cyclic subgroups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) | ||
Theorem | ablfaclem1 20085* | Lemma for ablfac 20088. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) ⇒ ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝑊‘𝑈) = {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑈)}) | ||
Theorem | ablfaclem2 20086* | Lemma for ablfac 20088. (Contributed by Mario Carneiro, 27-Apr-2016.) (Proof shortened by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) & ⊢ (𝜑 → 𝐹:𝐴⟶Word 𝐶) & ⊢ (𝜑 → ∀𝑦 ∈ 𝐴 (𝐹‘𝑦) ∈ (𝑊‘(𝑆‘𝑦))) & ⊢ 𝐿 = ∪ 𝑦 ∈ 𝐴 ({𝑦} × dom (𝐹‘𝑦)) & ⊢ (𝜑 → 𝐻:(0..^(♯‘𝐿))–1-1-onto→𝐿) ⇒ ⊢ (𝜑 → (𝑊‘𝐵) ≠ ∅) | ||
Theorem | ablfaclem3 20087* | Lemma for ablfac 20088. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐴 = {𝑤 ∈ ℙ ∣ 𝑤 ∥ (♯‘𝐵)} & ⊢ 𝑆 = (𝑝 ∈ 𝐴 ↦ {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ (𝑝↑(𝑝 pCnt (♯‘𝐵)))}) & ⊢ 𝑊 = (𝑔 ∈ (SubGrp‘𝐺) ↦ {𝑠 ∈ Word 𝐶 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) ⇒ ⊢ (𝜑 → (𝑊‘𝐵) ≠ ∅) | ||
Theorem | ablfac 20088* | The Fundamental Theorem of (finite) Abelian Groups. Any finite abelian group is a direct product of cyclic p-groups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → ∃𝑠 ∈ Word 𝐶(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝐵)) | ||
Theorem | ablfac2 20089* | Choose generators for each cyclic group in ablfac 20088. (Contributed by Mario Carneiro, 28-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐶 = {𝑟 ∈ (SubGrp‘𝐺) ∣ (𝐺 ↾s 𝑟) ∈ (CycGrp ∩ ran pGrp )} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ · = (.g‘𝐺) & ⊢ 𝑆 = (𝑘 ∈ dom 𝑤 ↦ ran (𝑛 ∈ ℤ ↦ (𝑛 · (𝑤‘𝑘)))) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ Word 𝐵(𝑆:dom 𝑤⟶𝐶 ∧ 𝐺dom DProd 𝑆 ∧ (𝐺 DProd 𝑆) = 𝐵)) | ||
Syntax | csimpg 20090 | Extend class notation with the class of simple groups. |
class SimpGrp | ||
Definition | df-simpg 20091 | Define class of all simple groups. A simple group is a group (df-grp 18931) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 20103). (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ SimpGrp = {𝑔 ∈ Grp ∣ (NrmSGrp‘𝑔) ≈ 2o} | ||
Theorem | issimpg 20092 | The predicate "is a simple group". (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝐺 ∈ SimpGrp ↔ (𝐺 ∈ Grp ∧ (NrmSGrp‘𝐺) ≈ 2o)) | ||
Theorem | issimpgd 20093 | Deduce a simple group from its properties. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 2o) ⇒ ⊢ (𝜑 → 𝐺 ∈ SimpGrp) | ||
Theorem | simpggrp 20094 | A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝐺 ∈ SimpGrp → 𝐺 ∈ Grp) | ||
Theorem | simpggrpd 20095 | A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
Theorem | simpg2nsg 20096 | A simple group has two normal subgroups. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ (𝐺 ∈ SimpGrp → (NrmSGrp‘𝐺) ≈ 2o) | ||
Theorem | trivnsimpgd 20097 | Trivial groups are not simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝐵 = { 0 }) ⇒ ⊢ (𝜑 → ¬ 𝐺 ∈ SimpGrp) | ||
Theorem | simpgntrivd 20098 | Simple groups are nontrivial. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → ¬ 𝐵 = { 0 }) | ||
Theorem | simpgnideld 20099* | A simple group contains a nonidentity element. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 ¬ 𝑥 = 0 ) | ||
Theorem | simpgnsgd 20100 | The only normal subgroups of a simple group are the group itself and the trivial group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ SimpGrp) ⇒ ⊢ (𝜑 → (NrmSGrp‘𝐺) = {{ 0 }, 𝐵}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |