HomeTheorem List (p. 198 of 498)
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 498) | < 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-30847) |
Hilbert Space Explorer
(30848-32370) |
Users' Mathboxes
(32371-49794) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | frgpuptinv 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) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ ⟨𝑦, (1o ∖ 𝑧)⟩) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ (𝐼 × 2o)) → (𝑇‘(𝑀‘𝐴)) = (𝑁‘(𝑇‘𝐴))) | ||
| Theorem | frgpuplem 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 ‘𝐼) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∼ 𝐶) → (𝐻 Σg (𝑇 ∘ 𝐴)) = (𝐻 Σg (𝑇 ∘ 𝐶))) | ||
| Theorem | frgpupf 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 (𝑇 ∘ 𝑔))⟩) ⇒ ⊢ (𝜑 → 𝐸:𝑋⟶𝐵) | ||
| Theorem | frgpupval 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.) |
| ⊢ 𝐵 = (Base‘𝐻) & ⊢ 𝑁 = (invg‘𝐻) & ⊢ 𝑇 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ if(𝑧 = ∅, (𝐹‘𝑦), (𝑁‘(𝐹‘𝑦)))) & ⊢ (𝜑 → 𝐻 ∈ Grp) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐼⟶𝐵) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = ran (𝑔 ∈ 𝑊 ↦ ⟨[𝑔] ∼ , (𝐻 Σg (𝑇 ∘ 𝑔))⟩) ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑊) → (𝐸‘[𝐴] ∼ ) = (𝐻 Σg (𝑇 ∘ 𝐴))) | ||
| Theorem | frgpup1 19705* | 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 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‘𝐼) & ⊢ (𝜑 → 𝐴 ∈ 𝐼) ⇒ ⊢ (𝜑 → (𝐸‘(𝑈‘𝐴)) = (𝐹‘𝐴)) | ||
| Theorem | frgpup3lem 19707* | 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 19708* | 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 19709 | The free group on zero generators is trivial. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐺 = (freeGrp‘∅) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 ≈ 1o | ||
| Syntax | ccmn 19710 | Extend class notation with class of all commutative monoids. |
| class CMnd | ||
| Syntax | cabl 19711 | Extend class notation with class of all Abelian groups. |
| class Abel | ||
| Definition | df-cmn 19712* | Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)} | ||
| Definition | df-abl 19713 | Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
| ⊢ Abel = (Grp ∩ CMnd) | ||
| Theorem | isabl 19714 | The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) |
| ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) | ||
| Theorem | ablgrp 19715 | An Abelian group is a group. (Contributed by NM, 26-Aug-2011.) |
| ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) | ||
| Theorem | ablgrpd 19716 | An Abelian group is a group, deduction form of ablgrp 19715. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Abel) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
| Theorem | ablcmn 19717 | An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd) | ||
| Theorem | ablcmnd 19718 | An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
| ⊢ (𝜑 → 𝐺 ∈ Abel) ⇒ ⊢ (𝜑 → 𝐺 ∈ CMnd) | ||
| Theorem | iscmn 19719* | The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥))) | ||
| Theorem | isabl2 19720* | 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 19721* | 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 19722* | 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 19723 | 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 19724* | Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ (𝜑 → 𝐺 ∈ CMnd) | ||
| Theorem | isabld 19725* | Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ (𝜑 → 𝐺 ∈ Abel) | ||
| Theorem | isabli 19726* | Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.) |
| ⊢ 𝐺 ∈ Grp & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ 𝐺 ∈ Abel | ||
| Theorem | cmnmnd 19727 | A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) | ||
| Theorem | cmncom 19728 | A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
| Theorem | ablcom 19729 | An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
| Theorem | cmn32 19730 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌)) | ||
| Theorem | cmn4 19731 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) | ||
| Theorem | cmn12 19732 | 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 19733 | 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 19734 | A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.) |
| ⊢ (𝜑 → 𝐺 ∈ CMnd) ⇒ ⊢ (𝜑 → 𝐺 ∈ Mnd) | ||
| Theorem | cmnbascntr 19735 | The base set of a commutative monoid is its center. (Contributed by SN, 21-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntr‘𝐺) ⇒ ⊢ (𝐺 ∈ CMnd → 𝐵 = 𝑍) | ||
| Theorem | rinvmod 19736* | Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovmo 7626. (Contributed by AV, 31-Dec-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃*𝑤 ∈ 𝐵 (𝐴 + 𝑤) = 0 ) | ||
| Theorem | ablinvadd 19737 | The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁‘(𝑋 + 𝑌)) = ((𝑁‘𝑋) + (𝑁‘𝑌))) | ||
| Theorem | ablsub2inv 19738 | Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) − (𝑁‘𝑌)) = (𝑌 − 𝑋)) | ||
| Theorem | ablsubadd 19739 | Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) = 𝑍 ↔ (𝑌 + 𝑍) = 𝑋)) | ||
| Theorem | ablsub4 19740 | Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) − (𝑍 + 𝑊)) = ((𝑋 − 𝑍) + (𝑌 − 𝑊))) | ||
| Theorem | abladdsub4 19741 | Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) = (𝑍 + 𝑊) ↔ (𝑋 − 𝑍) = (𝑊 − 𝑌))) | ||
| Theorem | abladdsub 19742 | Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) − 𝑍) = ((𝑋 − 𝑍) + 𝑌)) | ||
| Theorem | ablsubadd23 19743 | Commutative/associative law for addition and subtraction in abelian groups. (subadd23d 11555 analog.) (Contributed by AV, 2-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) + 𝑍) = (𝑋 + (𝑍 − 𝑌))) | ||
| Theorem | ablsubaddsub 19744 | Double subtraction and addition in abelian groups. (cnambpcma 47295 analog.) (Contributed by AV, 3-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑋 − 𝑌) + 𝑍) − 𝑋) = (𝑍 − 𝑌)) | ||
| Theorem | ablpncan2 19745 | Cancellation law for subtraction in an Abelian group. (Contributed by NM, 2-Oct-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + 𝑌) − 𝑋) = 𝑌) | ||
| Theorem | ablpncan3 19746 | A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 + (𝑌 − 𝑋)) = 𝑌) | ||
| Theorem | ablsubsub 19747 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 − (𝑌 − 𝑍)) = ((𝑋 − 𝑌) + 𝑍)) | ||
| Theorem | ablsubsub4 19748 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑌 + 𝑍))) | ||
| Theorem | ablpnpcan 19749 | Cancellation law for mixed addition and subtraction. (pnpcan 11461 analog.) (Contributed by NM, 29-May-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) − (𝑋 + 𝑍)) = (𝑌 − 𝑍)) | ||
| Theorem | ablnncan 19750 | Cancellation law for group subtraction. (nncan 11451 analog.) (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 − (𝑋 − 𝑌)) = 𝑌) | ||
| Theorem | ablsub32 19751 | Swap the second and third terms in a double group subtraction. (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = ((𝑋 − 𝑍) − 𝑌)) | ||
| Theorem | ablnnncan 19752 | Cancellation law for group subtraction. (nnncan 11457 analog.) (Contributed by NM, 29-Feb-2008.) (Revised by AV, 27-Aug-2021.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − (𝑌 − 𝑍)) − 𝑍) = (𝑋 − 𝑌)) | ||
| Theorem | ablnnncan1 19753 | Cancellation law for group subtraction. (nnncan1 11458 analog.) (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) − (𝑋 − 𝑍)) = (𝑍 − 𝑌)) | ||
| Theorem | ablsubsub23 19754 | Swap subtrahend and result of group subtraction. (Contributed by NM, 14-Dec-2007.) (Revised by AV, 7-Oct-2021.) |
| ⊢ 𝑉 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)) | ||
| Theorem | mulgnn0di 19755 | Group multiple of a sum, for nonnegative multiples. (Contributed by Mario Carneiro, 13-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) | ||
| Theorem | mulgdi 19756 | Group multiple of a sum. (Contributed by Mario Carneiro, 13-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) | ||
| Theorem | mulgmhm 19757* | 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 19758* | 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 19759 | Group multiple of a difference. (Contributed by Mario Carneiro, 13-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 − 𝑌)) = ((𝑀 · 𝑋) − (𝑀 · 𝑌))) | ||
| Theorem | ghmfghm 19760* | The function fulfilling the conditions of ghmgrp 18998 is a group homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑌 = (Base‘𝐻) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+g‘𝐻) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | ||
| Theorem | ghmcmn 19761* | 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 19762* | 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 19763 | 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 19764 | Value of the subgroup coset equivalence relation on an abelian group. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑆) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐵 − 𝐴) ∈ 𝑆))) | ||
| Theorem | qusecsub 19765 | 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 19766 | A subgroup of an abelian group is also abelian. (Contributed by Mario Carneiro, 3-Dec-2014.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Abel) | ||
| Theorem | subcmn 19767 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝐻 ∈ Mnd) → 𝐻 ∈ CMnd) | ||
| Theorem | submcmn 19768 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ CMnd) | ||
| Theorem | submcmn2 19769 | 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 19770 | 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 19771 | Any subset in a commutative monoid is a subset of its centralizer. (Contributed by AV, 12-Jan-2019.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵) → 𝑆 ⊆ (𝑍‘𝑆)) | ||
| Theorem | cntrcmnd 19772 | The center of a monoid is a commutative submonoid. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
| ⊢ 𝑍 = (𝑀 ↾s (Cntr‘𝑀)) ⇒ ⊢ (𝑀 ∈ Mnd → 𝑍 ∈ CMnd) | ||
| Theorem | cntrabl 19773 | The center of a group is an abelian group. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
| ⊢ 𝑍 = (𝑀 ↾s (Cntr‘𝑀)) ⇒ ⊢ (𝑀 ∈ Grp → 𝑍 ∈ Abel) | ||
| Theorem | cntzspan 19774 | If the generators commute, the generated monoid is commutative. (Contributed by Mario Carneiro, 25-Apr-2016.) |
| ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubMnd‘𝐺)) & ⊢ 𝐻 = (𝐺 ↾s (𝐾‘𝑆)) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ⊆ (𝑍‘𝑆)) → 𝐻 ∈ CMnd) | ||
| Theorem | cntzcmnf 19775 | Discharge the centralizer assumption in a commutative monoid. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) | ||
| Theorem | ghmplusg 19776 | 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 19777 | Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ (𝐺 ∈ Abel → (NrmSGrp‘𝐺) = (SubGrp‘𝐺)) | ||
| Theorem | odadd1 19778 | 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 19779 | 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 19780 | 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 19781 | A group with exponent 2 (or 1) is abelian. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐸 ∥ 2) → 𝐺 ∈ Abel) | ||
| Theorem | gexexlem 19782* | Lemma for gexex 19783. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐸 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑂‘𝑦) ≤ (𝑂‘𝐴)) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) | ||
| Theorem | gexex 19783* | 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 19784 | 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 19785* | 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 19786 | Subgroup sum commutes (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) | ||
| Theorem | ablcntzd 19787 | All subgroups in an abelian group commute. (Contributed by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) | ||
| Theorem | lsmcom 19788 | Subgroup sum commutes. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) | ||
| Theorem | lsmsubg2 19789 | 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 19790 | 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 19791 | The product of a family of commutative monoids is commutative. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶CMnd) ⇒ ⊢ (𝜑 → 𝑌 ∈ CMnd) | ||
| Theorem | prdsabld 19792 | 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 19793 | The structure power on a commutative monoid is commutative. (Contributed by Mario Carneiro, 11-Jan-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ CMnd ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ CMnd) | ||
| Theorem | pwsabl 19794 | The structure power on an Abelian group is Abelian. (Contributed by Mario Carneiro, 21-Jan-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ Abel ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Abel) | ||
| Theorem | qusabl 19795 | 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 19796 | The (smallest) structure representing a trivial abelian group. (Contributed by AV, 28-Apr-2019.) |
| ⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩} ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Abel) | ||
| Theorem | abln0 19797 | Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019.) |
| ⊢ Abel ≠ ∅ | ||
| Theorem | cnaddablx 19798 | The complex numbers are an Abelian group under addition. This version of cnaddabl 19799 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 19799 instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012.) |
| ⊢ 𝐺 = {⟨1, ℂ⟩, ⟨2, + ⟩} ⇒ ⊢ 𝐺 ∈ Abel | ||
| Theorem | cnaddabl 19799 | The complex numbers are an Abelian group under addition. This version of cnaddablx 19798 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 21302. (Contributed by NM, 20-Oct-2012.) (New usage is discouraged.) |
| ⊢ 𝐺 = {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ⇒ ⊢ 𝐺 ∈ Abel | ||
| Theorem | cnaddid 19800 | The group identity element of complex number addition is zero. See also cnfld0 21304. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 26-Aug-2021.) (New usage is discouraged.) |
| ⊢ 𝐺 = {⟨(Base‘ndx), ℂ⟩, ⟨(+g‘ndx), + ⟩} ⇒ ⊢ (0g‘𝐺) = 0 | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |