![]() |
Metamath
Proof Explorer Theorem List (p. 201 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gsummptfzcl 20001* | 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 20002* | Lemma 1 for gsum2d 20004. (Contributed by Mario Carneiro, 28-Dec-2014.) (Revised by AV, 8-Jun-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝐷 ∈ 𝑊) & ⊢ (𝜑 → dom 𝐴 ⊆ 𝐷) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ (𝐴 “ {𝑗}) ↦ (𝑗𝐹𝑘))) ∈ 𝐵) | ||
Theorem | gsum2dlem2 20003* | Lemma for gsum2d 20004. (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 20004* | 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 20005* | Lemma for gsum2d2 20006: 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 20006* | 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 20007* | 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 20008* | 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 20009* | Commute the arguments of a double sum. (Contributed by Mario Carneiro, 28-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑊) & ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ Fin) & ⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑘 ∈ 𝐶, 𝑗 ∈ 𝐴 ↦ 𝑋))) | ||
Theorem | gsumcom3 20010* | 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 20011* | 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 20012* | 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 20013* | 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 20014* | 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 20015* | 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 20016* | 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 20017* | 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 20018* | 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 20019* | 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 20020* | Lemma for telgsumfzs 20021 (induction step). (Contributed by AV, 23-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝑦 ∈ (ℤ≥‘𝑀) ∧ (𝜑 ∧ ∀𝑘 ∈ (𝑀...((𝑦 + 1) + 1))𝐶 ∈ 𝐵)) → ((𝐺 Σg (𝑖 ∈ (𝑀...𝑦) ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = (⦋𝑀 / 𝑘⦌𝐶 − ⦋(𝑦 + 1) / 𝑘⦌𝐶) → (𝐺 Σg (𝑖 ∈ (𝑀...(𝑦 + 1)) ↦ (⦋𝑖 / 𝑘⦌𝐶 − ⦋(𝑖 + 1) / 𝑘⦌𝐶))) = (⦋𝑀 / 𝑘⦌𝐶 − ⦋((𝑦 + 1) + 1) / 𝑘⦌𝐶))) | ||
Theorem | telgsumfzs 20021* | 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 20022* | Telescoping group sum ranging over a finite set of sequential integers, using implicit substitution, analogous to telfsum 15836. (Contributed by AV, 23-Nov-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → ∀𝑘 ∈ (𝑀...(𝑁 + 1))𝐴 ∈ 𝐵) & ⊢ (𝑘 = 𝑖 → 𝐴 = 𝐿) & ⊢ (𝑘 = (𝑖 + 1) → 𝐴 = 𝐶) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐷) & ⊢ (𝑘 = (𝑁 + 1) → 𝐴 = 𝐸) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (𝑀...𝑁) ↦ (𝐿 − 𝐶))) = (𝐷 − 𝐸)) | ||
Theorem | telgsumfz0s 20023* | 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 20024* | Telescoping finite group sum ranging over nonnegative integers, using implicit substitution, analogous to telfsum 15836. (Contributed by AV, 23-Nov-2019.) |
⊢ 𝐾 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ ℕ0) & ⊢ (𝜑 → ∀𝑘 ∈ (0...(𝑆 + 1))𝐴 ∈ 𝐾) & ⊢ (𝑘 = 𝑖 → 𝐴 = 𝐵) & ⊢ (𝑘 = (𝑖 + 1) → 𝐴 = 𝐶) & ⊢ (𝑘 = 0 → 𝐴 = 𝐷) & ⊢ (𝑘 = (𝑆 + 1) → 𝐴 = 𝐸) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑖 ∈ (0...𝑆) ↦ (𝐵 − 𝐶))) = (𝐷 − 𝐸)) | ||
Theorem | telgsums 20025* | 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 20026* | 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 20027 | Internal direct product of a family of subgroups. |
class DProd | ||
Syntax | cdpj 20028 | Projection operator for a direct product. |
class dProj | ||
Definition | df-dprd 20029* | 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 20030* | 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 20031 | 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 20032* | 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 20033* | 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 20034 | 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 20035 | 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 20036 | 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 20037* | 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 20038* | 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 20039 | Reverse closure for the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝐺dom DProd 𝑆 → 𝐺 ∈ Grp) | ||
Theorem | dprdf 20040 | The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝐺dom DProd 𝑆 → 𝑆:dom 𝑆⟶(SubGrp‘𝐺)) | ||
Theorem | dprdf2 20041 | The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) ⇒ ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) | ||
Theorem | dprdcntz 20042 | The function 𝑆 is a family having pairwise commuting values. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ (𝜑 → 𝑌 ∈ 𝐼) & ⊢ (𝜑 → 𝑋 ≠ 𝑌) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝑆‘𝑌))) | ||
Theorem | dprddisj 20043 | 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 20044* | 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 20045* | 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 20046* | 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 20047* | 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 20048* | 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 20049* | 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 20050 | 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 20051* | 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 20052* | 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 20053* | 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 20054* | 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 20055* | 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 20056* | 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 20057* | 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 20058 | 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 20059 | Each factor is a subset of the internal direct product. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝐺 DProd 𝑆)) | ||
Theorem | dprdlub 20060* | 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 20061 | 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 20062 | Restriction of a direct product (dropping factors). (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐴 ⊆ 𝐼) ⇒ ⊢ (𝜑 → (𝐺dom DProd (𝑆 ↾ 𝐴) ∧ (𝐺 DProd (𝑆 ↾ 𝐴)) ⊆ (𝐺 DProd 𝑆))) | ||
Theorem | dprdss 20063* | 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 20064* | 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 20065 | 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 20066 | 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 20067 | 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 20068 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) ⇒ ⊢ (𝐴 ∈ (SubGrp‘𝐺) → (𝐻dom DProd 𝑆 ↔ (𝐺dom DProd 𝑆 ∧ ran 𝑆 ⊆ 𝒫 𝐴))) | ||
Theorem | subgdprd 20069 | A direct product in a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ (𝜑 → 𝐴 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → ran 𝑆 ⊆ 𝒫 𝐴) ⇒ ⊢ (𝜑 → (𝐻 DProd 𝑆) = (𝐺 DProd 𝑆)) | ||
Theorem | dprdsn 20070 | 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 20071* | Lemma for dmdprdsplit 20081. (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 20072 | The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝐶 ⊆ 𝐼) & ⊢ (𝜑 → 𝐷 ⊆ 𝐼) & ⊢ (𝜑 → (𝐶 ∩ 𝐷) = ∅) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ 𝐶)) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ 𝐷)))) | ||
Theorem | dprddisj2 20073 | 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 20074* | 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 20075* | 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 20076* | 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 20077* | 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 20078* | 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 20079 | Lemma for dmdprdsplit 20081. (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 20080 | 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 20081 | 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 20082 | 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 20083 | 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 20084 | 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 20085 | Lemma for theorems about direct product projection. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝐺 DProd (𝑆 ↾ {𝑋})) = (𝑆‘𝑋)) | ||
Theorem | dpjcntz 20086 | The two subgroups that appear in dpjval 20090 commute. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝑆‘𝑋) ⊆ (𝑍‘(𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))))) | ||
Theorem | dpjdisj 20087 | The two subgroups that appear in dpjval 20090 are disjoint. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝜑 → ((𝑆‘𝑋) ∩ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋})))) = { 0 }) | ||
Theorem | dpjlsm 20088 | The two subgroups that appear in dpjval 20090 add to the full direct product. (Contributed by Mario Carneiro, 26-Apr-2016.) |
⊢ (𝜑 → 𝐺dom DProd 𝑆) & ⊢ (𝜑 → dom 𝑆 = 𝐼) & ⊢ (𝜑 → 𝑋 ∈ 𝐼) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝜑 → (𝐺 DProd 𝑆) = ((𝑆‘𝑋) ⊕ (𝐺 DProd (𝑆 ↾ (𝐼 ∖ {𝑋}))))) | ||
Theorem | dpjfval 20089* | 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 20090 | 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 20091 | 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 20092* | 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 20093* | 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 20094* | 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 20095 | 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 20096 | 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 20097 | 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 20098 | 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 20099* | Lemma for ablfacrp2 20101. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑀} & ⊢ 𝐿 = {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → (𝑀 gcd 𝑁) = 1) & ⊢ (𝜑 → (♯‘𝐵) = (𝑀 · 𝑁)) ⇒ ⊢ (𝜑 → ((♯‘𝐾) gcd 𝑁) = 1) | ||
Theorem | ablfacrp 20100* | 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 } ∧ (𝐾 ⊕ 𝐿) = 𝐵)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |