HomeTheorem List (p. 198 of 501)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 198 of 501) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-30993) |
Hilbert Space Explorer
(30994-32516) |
Users' Mathboxes
(32517-50046) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | frgpuplem 19701* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))) | ||
| Theorem | frgpupf 19702* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ ⟨[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))⟩) ⇒ ⊢ (𝜑 → 𝐸:𝑋⟶𝐵) | ||
| Theorem | frgpupval 19703* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) |
| ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ ⟨[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))⟩) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑊) → (𝐸‘[𝐴] ∼ ) = (𝐻 Σg (𝑇 ∘ 𝐴))) | ||
| Theorem | frgpup1 19704* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
| ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ ⟨[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))⟩) ⇒ ⊢ (𝜑 → 𝐸 ∈ (𝐺 GrpHom 𝐻)) | ||
| Theorem | frgpup2 19705* | The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
| ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ ⟨[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))⟩) & ⊢ 𝑈 = (varFGrp‘𝐼) & ⊢ (𝜑 → 𝐴 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝐸‘(𝑈‘𝐴)) = (𝐹‘𝐴)) | ||
| Theorem | frgpup3lem 19706* | The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
| ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ ⟨[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))⟩) & ⊢ 𝑈 = (varFGrp‘𝐼) & ⊢ (𝜑 → 𝐾 ∈ (𝐺 GrpHom 𝐻)) & ⊢ (𝜑 → (𝐾 ∘ 𝑈) = 𝐹) ⇒ ⊢ (𝜑 → 𝐾 = 𝐸) | ||
| Theorem | frgpup3 19707* | Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
| ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑈 = (varFGrp‘𝐼) ⇒ ⊢ ((𝐻 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝐹:𝐼⟶𝐵) → ∃!𝑚 ∈ (𝐺 GrpHom 𝐻)(𝑚 ∘ 𝑈) = 𝐹) | ||
| Theorem | 0frgp 19708 | The free group on zero generators is trivial. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐺 = (freeGrp‘∅) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 ≈ 1o | ||
| Syntax | ccmn 19709 | Extend class notation with class of all commutative monoids. |
| class CMnd | ||
| Syntax | cabl 19710 | Extend class notation with class of all Abelian groups. |
| class Abel | ||
| Definition | df-cmn 19711* | Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)} | ||
| Definition | df-abl 19712 | Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
| ⊢ Abel = (Grp ∩ CMnd) | ||
| Theorem | isabl 19713 | The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) |
| ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) | ||
| Theorem | ablgrp 19714 | An Abelian group is a group. (Contributed by NM, 26-Aug-2011.) |
| ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) | ||
| Theorem | ablgrpd 19715 | An Abelian group is a group, deduction form of ablgrp 19714. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Abel) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
| Theorem | ablcmn 19716 | An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd) | ||
| Theorem | ablcmnd 19717 | An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
| ⊢ (𝜑 → 𝐺 ∈ Abel) ⇒ ⊢ (𝜑 → 𝐺 ∈ CMnd) | ||
| Theorem | iscmn 19718* | The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥))) | ||
| Theorem | isabl2 19719* | The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥))) | ||
| Theorem | cmnpropd 19720* | If two structures have the same group components (properties), one is a commutative monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ CMnd ↔ 𝐿 ∈ CMnd)) | ||
| Theorem | ablpropd 19721* | If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 6-Dec-2014.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) ⇒ ⊢ (𝜑 → (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel)) | ||
| Theorem | ablprop 19722 | If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 11-Oct-2013.) |
| ⊢ (Base‘𝐾) = (Base‘𝐿) & ⊢ (+g‘𝐾) = (+g‘𝐿) ⇒ ⊢ (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel) | ||
| Theorem | iscmnd 19723* | Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ (𝜑 → 𝐺 ∈ CMnd) | ||
| Theorem | isabld 19724* | Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ (𝜑 → 𝐺 ∈ Abel) | ||
| Theorem | isabli 19725* | Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.) |
| ⊢ 𝐺 ∈ Grp & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ 𝐺 ∈ Abel | ||
| Theorem | cmnmnd 19726 | A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) | ||
| Theorem | cmncom 19727 | A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
| Theorem | ablcom 19728 | An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
| Theorem | cmn32 19729 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌)) | ||
| Theorem | cmn4 19730 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) | ||
| Theorem | cmn12 19731 | Commutative/associative law for commutative monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 + (𝑌 + 𝑍)) = (𝑌 + (𝑋 + 𝑍))) | ||
| Theorem | abl32 19732 | Commutative/associative law for Abelian groups. (Contributed by Stefan O'Rear, 10-Apr-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌)) | ||
| Theorem | cmnmndd 19733 | A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.) |
| ⊢ (𝜑 → 𝐺 ∈ CMnd) ⇒ ⊢ (𝜑 → 𝐺 ∈ Mnd) | ||
| Theorem | cmnbascntr 19734 | The base set of a commutative monoid is its center. (Contributed by SN, 21-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntr‘𝐺) ⇒ ⊢ (𝐺 ∈ CMnd → 𝐵 = 𝑍) | ||
| Theorem | rinvmod 19735* | Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovmo 7595. (Contributed by AV, 31-Dec-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃*𝑤 ∈ 𝐵 (𝐴 + 𝑤) = 0 ) | ||
| Theorem | ablinvadd 19736 | The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁‘(𝑋 + 𝑌)) = ((𝑁‘𝑋) + (𝑁‘𝑌))) | ||
| Theorem | ablsub2inv 19737 | Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) − (𝑁‘𝑌)) = (𝑌 − 𝑋)) | ||
| Theorem | ablsubadd 19738 | Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) = 𝑍 ↔ (𝑌 + 𝑍) = 𝑋)) | ||
| Theorem | ablsub4 19739 | Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) − (𝑍 + 𝑊)) = ((𝑋 − 𝑍) + (𝑌 − 𝑊))) | ||
| Theorem | abladdsub4 19740 | Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) = (𝑍 + 𝑊) ↔ (𝑋 − 𝑍) = (𝑊 − 𝑌))) | ||
| Theorem | abladdsub 19741 | Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) − 𝑍) = ((𝑋 − 𝑍) + 𝑌)) | ||
| Theorem | ablsubadd23 19742 | Commutative/associative law for addition and subtraction in abelian groups. (subadd23d 11514 analog.) (Contributed by AV, 2-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) + 𝑍) = (𝑋 + (𝑍 − 𝑌))) | ||
| Theorem | ablsubaddsub 19743 | Double subtraction and addition in abelian groups. (cnambpcma 47536 analog.) (Contributed by AV, 3-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑋 − 𝑌) + 𝑍) − 𝑋) = (𝑍 − 𝑌)) | ||
| Theorem | ablpncan2 19744 | Cancellation law for subtraction in an Abelian group. (Contributed by NM, 2-Oct-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + 𝑌) − 𝑋) = 𝑌) | ||
| Theorem | ablpncan3 19745 | A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 + (𝑌 − 𝑋)) = 𝑌) | ||
| Theorem | ablsubsub 19746 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 − (𝑌 − 𝑍)) = ((𝑋 − 𝑌) + 𝑍)) | ||
| Theorem | ablsubsub4 19747 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑌 + 𝑍))) | ||
| Theorem | ablpnpcan 19748 | Cancellation law for mixed addition and subtraction. (pnpcan 11420 analog.) (Contributed by NM, 29-May-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) − (𝑋 + 𝑍)) = (𝑌 − 𝑍)) | ||
| Theorem | ablnncan 19749 | Cancellation law for group subtraction. (nncan 11410 analog.) (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 − (𝑋 − 𝑌)) = 𝑌) | ||
| Theorem | ablsub32 19750 | Swap the second and third terms in a double group subtraction. (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = ((𝑋 − 𝑍) − 𝑌)) | ||
| Theorem | ablnnncan 19751 | Cancellation law for group subtraction. (nnncan 11416 analog.) (Contributed by NM, 29-Feb-2008.) (Revised by AV, 27-Aug-2021.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − (𝑌 − 𝑍)) − 𝑍) = (𝑋 − 𝑌)) | ||
| Theorem | ablnnncan1 19752 | Cancellation law for group subtraction. (nnncan1 11417 analog.) (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) − (𝑋 − 𝑍)) = (𝑍 − 𝑌)) | ||
| Theorem | ablsubsub23 19753 | Swap subtrahend and result of group subtraction. (Contributed by NM, 14-Dec-2007.) (Revised by AV, 7-Oct-2021.) |
| ⊢ 𝑉 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)) | ||
| Theorem | mulgnn0di 19754 | Group multiple of a sum, for nonnegative multiples. (Contributed by Mario Carneiro, 13-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) | ||
| Theorem | mulgdi 19755 | Group multiple of a sum. (Contributed by Mario Carneiro, 13-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) | ||
| Theorem | mulgmhm 19756* | The map from 𝑥 to 𝑛𝑥 for a fixed positive integer 𝑛 is a monoid homomorphism if the monoid is commutative. (Contributed by Mario Carneiro, 4-May-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑀 ∈ ℕ0) → (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) ∈ (𝐺 MndHom 𝐺)) | ||
| Theorem | mulgghm 19757* | The map from 𝑥 to 𝑛𝑥 for a fixed integer 𝑛 is a group homomorphism if the group is commutative. (Contributed by Mario Carneiro, 4-May-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑀 ∈ ℤ) → (𝑥 ∈ 𝐵 ↦ (𝑀 · 𝑥)) ∈ (𝐺 GrpHom 𝐺)) | ||
| Theorem | mulgsubdi 19758 | Group multiple of a difference. (Contributed by Mario Carneiro, 13-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 − 𝑌)) = ((𝑀 · 𝑋) − (𝑀 · 𝑌))) | ||
| Theorem | ghmfghm 19759* | The function fulfilling the conditions of ghmgrp 18996 is a group homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑌 = (Base‘𝐻) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+g‘𝐻) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | ||
| Theorem | ghmcmn 19760* | The image of a commutative monoid 𝐺 under a group homomorphism 𝐹 is a commutative monoid. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑌 = (Base‘𝐻) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+g‘𝐻) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ CMnd) ⇒ ⊢ (𝜑 → 𝐻 ∈ CMnd) | ||
| Theorem | ghmabl 19761* | The image of an abelian group 𝐺 under a group homomorphism 𝐹 is an abelian group. (Contributed by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 26-Jan-2020.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑌 = (Base‘𝐻) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+g‘𝐻) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ Abel) ⇒ ⊢ (𝜑 → 𝐻 ∈ Abel) | ||
| Theorem | invghm 19762 | The inversion map is a group automorphism if and only if the group is abelian. (In general it is only a group homomorphism into the opposite group, but in an abelian group the opposite group coincides with the group itself.) (Contributed by Mario Carneiro, 4-May-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Abel ↔ 𝐼 ∈ (𝐺 GrpHom 𝐺)) | ||
| Theorem | eqgabl 19763 | Value of the subgroup coset equivalence relation on an abelian group. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑆) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐵 − 𝐴) ∈ 𝑆))) | ||
| Theorem | qusecsub 19764 | Two subgroup cosets are equal if and only if the difference of their representatives is a member of the subgroup. (Contributed by AV, 7-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑆) ⇒ ⊢ (((𝐺 ∈ Abel ∧ 𝑆 ∈ (SubGrp‘𝐺)) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ([𝑋] ∼ = [𝑌] ∼ ↔ (𝑌 − 𝑋) ∈ 𝑆)) | ||
| Theorem | subgabl 19765 | A subgroup of an abelian group is also abelian. (Contributed by Mario Carneiro, 3-Dec-2014.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Abel) | ||
| Theorem | subcmn 19766 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝐻 ∈ Mnd) → 𝐻 ∈ CMnd) | ||
| Theorem | submcmn 19767 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ CMnd) | ||
| Theorem | submcmn2 19768 | A submonoid is commutative iff it is a subset of its own centralizer. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝐺) → (𝐻 ∈ CMnd ↔ 𝑆 ⊆ (𝑍‘𝑆))) | ||
| Theorem | cntzcmn 19769 | The centralizer of any subset in a commutative monoid is the whole monoid. (Contributed by Mario Carneiro, 3-Oct-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) = 𝐵) | ||
| Theorem | cntzcmnss 19770 | Any subset in a commutative monoid is a subset of its centralizer. (Contributed by AV, 12-Jan-2019.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵) → 𝑆 ⊆ (𝑍‘𝑆)) | ||
| Theorem | cntrcmnd 19771 | The center of a monoid is a commutative submonoid. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
| ⊢ 𝑍 = (𝑀 ↾s (Cntr‘𝑀)) ⇒ ⊢ (𝑀 ∈ Mnd → 𝑍 ∈ CMnd) | ||
| Theorem | cntrabl 19772 | The center of a group is an abelian group. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
| ⊢ 𝑍 = (𝑀 ↾s (Cntr‘𝑀)) ⇒ ⊢ (𝑀 ∈ Grp → 𝑍 ∈ Abel) | ||
| Theorem | cntzspan 19773 | If the generators commute, the generated monoid is commutative. (Contributed by Mario Carneiro, 25-Apr-2016.) |
| ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubMnd‘𝐺)) & ⊢ 𝐻 = (𝐺 ↾s (𝐾‘𝑆)) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ⊆ (𝑍‘𝑆)) → 𝐻 ∈ CMnd) | ||
| Theorem | cntzcmnf 19774 | Discharge the centralizer assumption in a commutative monoid. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) | ||
| Theorem | ghmplusg 19775 | The pointwise sum of two linear functions is linear. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
| ⊢ + = (+g‘𝑁) ⇒ ⊢ ((𝑁 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpHom 𝑁) ∧ 𝐺 ∈ (𝑀 GrpHom 𝑁)) → (𝐹 ∘f + 𝐺) ∈ (𝑀 GrpHom 𝑁)) | ||
| Theorem | ablnsg 19776 | Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ (𝐺 ∈ Abel → (NrmSGrp‘𝐺) = (SubGrp‘𝐺)) | ||
| Theorem | odadd1 19777 | The order of a product in an abelian group divides the LCM of the orders of the factors. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑂‘(𝐴 + 𝐵)) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∥ ((𝑂‘𝐴) · (𝑂‘𝐵))) | ||
| Theorem | odadd2 19778 | The order of a product in an abelian group is divisible by the LCM of the orders of the factors divided by the GCD. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑂‘𝐴) · (𝑂‘𝐵)) ∥ ((𝑂‘(𝐴 + 𝐵)) · (((𝑂‘𝐴) gcd (𝑂‘𝐵))↑2))) | ||
| Theorem | odadd 19779 | The order of a product is the product of the orders, if the factors have coprime order. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) = 1) → (𝑂‘(𝐴 + 𝐵)) = ((𝑂‘𝐴) · (𝑂‘𝐵))) | ||
| Theorem | gex2abl 19780 | A group with exponent 2 (or 1) is abelian. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐸 ∥ 2) → 𝐺 ∈ Abel) | ||
| Theorem | gexexlem 19781* | Lemma for gexex 19782. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐸 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑂‘𝑦) ≤ (𝑂‘𝐴)) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) | ||
| Theorem | gexex 19782* | In an abelian group with finite exponent, there is an element in the group with order equal to the exponent. In other words, all orders of elements divide the largest order of an element of the group. This fails if 𝐸 = 0, for example in an infinite p-group, where there are elements of arbitrarily large orders (so 𝐸 is zero) but no elements of infinite order. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝐸 ∈ ℕ) → ∃𝑥 ∈ 𝑋 (𝑂‘𝑥) = 𝐸) | ||
| Theorem | torsubg 19783 | The set of all elements of finite order forms a subgroup of any abelian group, called the torsion subgroup. (Contributed by Mario Carneiro, 20-Oct-2015.) |
| ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ (𝐺 ∈ Abel → (◡𝑂 “ ℕ) ∈ (SubGrp‘𝐺)) | ||
| Theorem | oddvdssubg 19784* | The set of all elements whose order divides a fixed integer is a subgroup of any abelian group. (Contributed by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑁 ∈ ℤ) → {𝑥 ∈ 𝐵 ∣ (𝑂‘𝑥) ∥ 𝑁} ∈ (SubGrp‘𝐺)) | ||
| Theorem | lsmcomx 19785 | Subgroup sum commutes (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) | ||
| Theorem | ablcntzd 19786 | All subgroups in an abelian group commute. (Contributed by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) | ||
| Theorem | lsmcom 19787 | Subgroup sum commutes. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) | ||
| Theorem | lsmsubg2 19788 | The sum of two subgroups is a subgroup. (Contributed by NM, 4-Feb-2014.) (Proof shortened by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊕ 𝑈) ∈ (SubGrp‘𝐺)) | ||
| Theorem | lsm4 19789 | Commutative/associative law for subgroup sum. (Contributed by NM, 26-Sep-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑄 ∈ (SubGrp‘𝐺) ∧ 𝑅 ∈ (SubGrp‘𝐺)) ∧ (𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺))) → ((𝑄 ⊕ 𝑅) ⊕ (𝑇 ⊕ 𝑈)) = ((𝑄 ⊕ 𝑇) ⊕ (𝑅 ⊕ 𝑈))) | ||
| Theorem | prdscmnd 19790 | The product of a family of commutative monoids is commutative. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶CMnd) ⇒ ⊢ (𝜑 → 𝑌 ∈ CMnd) | ||
| Theorem | prdsabld 19791 | The product of a family of Abelian groups is an Abelian group. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Abel) ⇒ ⊢ (𝜑 → 𝑌 ∈ Abel) | ||
| Theorem | pwscmn 19792 | The structure power on a commutative monoid is commutative. (Contributed by Mario Carneiro, 11-Jan-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ CMnd ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ CMnd) | ||
| Theorem | pwsabl 19793 | The structure power on an Abelian group is Abelian. (Contributed by Mario Carneiro, 21-Jan-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ Abel ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Abel) | ||
| Theorem | qusabl 19794 | If 𝑌 is a subgroup of the abelian group 𝐺, then 𝐻 = 𝐺 / 𝑌 is an abelian group. (Contributed by Mario Carneiro, 26-Apr-2016.) |
| ⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆)) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Abel) | ||
| Theorem | abl1 19795 | The (smallest) structure representing a trivial abelian group. (Contributed by AV, 28-Apr-2019.) |
| ⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩} ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Abel) | ||
| Theorem | abln0 19796 | Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019.) |
| ⊢ Abel ≠ ∅ | ||
| Theorem | cnaddablx 19797 | The complex numbers are an Abelian group under addition. This version of cnaddabl 19798 shows the explicit structure "scaffold" we chose for the definition for Abelian groups. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use; use cnaddabl 19798 instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012.) |
| ⊢ 𝐺 = {⟨1, ℂ⟩, ⟨2, + ⟩} ⇒ ⊢ 𝐺 ∈ Abel | ||
| Theorem | cnaddabl 19798 | The complex numbers are an Abelian group under addition. This version of cnaddablx 19797 hides the explicit structure indices i.e. is "scaffold-independent". Note that the proof also does not reference explicit structure indices. The actual structure is dependent on how Base and +g is defined. This theorem should not be referenced in any proof. For the group/ring properties of the complex numbers, see cnring 21345. (Contributed by NM, 20-Oct-2012.) (New usage is discouraged.) |
| ⊢ 𝐺 = {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ⇒ ⊢ 𝐺 ∈ Abel | ||
| Theorem | cnaddid 19799 | The group identity element of complex number addition is zero. See also cnfld0 21347. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 26-Aug-2021.) (New usage is discouraged.) |
| ⊢ 𝐺 = {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ⇒ ⊢ (0g‘𝐺) = 0 | ||
| Theorem | cnaddinv 19800 | Value of the group inverse of complex number addition. See also cnfldneg 21350. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 26-Aug-2021.) (New usage is discouraged.) |
| ⊢ 𝐺 = {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ⇒ ⊢ (𝐴 ∈ ℂ → ((invg‘𝐺)‘𝐴) = -𝐴) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |