| Metamath
Proof Explorer Theorem List (p. 199 of 494) | < Previous Next > | |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Definition | df-abl 19801 | Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
| ⊢ Abel = (Grp ∩ CMnd) | ||
| Theorem | isabl 19802 | The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) |
| ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd)) | ||
| Theorem | ablgrp 19803 | An Abelian group is a group. (Contributed by NM, 26-Aug-2011.) |
| ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) | ||
| Theorem | ablgrpd 19804 | An Abelian group is a group, deduction form of ablgrp 19803. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
| ⊢ (𝜑 → 𝐺 ∈ Abel) ⇒ ⊢ (𝜑 → 𝐺 ∈ Grp) | ||
| Theorem | ablcmn 19805 | An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd) | ||
| Theorem | ablcmnd 19806 | An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.) |
| ⊢ (𝜑 → 𝐺 ∈ Abel) ⇒ ⊢ (𝜑 → 𝐺 ∈ CMnd) | ||
| Theorem | iscmn 19807* | The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥))) | ||
| Theorem | isabl2 19808* | 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 19809* | 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 19810* | 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 19811 | 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 19812* | Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ (𝜑 → 𝐺 ∈ CMnd) | ||
| Theorem | isabld 19813* | Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ (𝜑 → 𝐺 ∈ Abel) | ||
| Theorem | isabli 19814* | Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.) |
| ⊢ 𝐺 ∈ Grp & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑦 + 𝑥)) ⇒ ⊢ 𝐺 ∈ Abel | ||
| Theorem | cmnmnd 19815 | A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ (𝐺 ∈ CMnd → 𝐺 ∈ Mnd) | ||
| Theorem | cmncom 19816 | A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
| Theorem | ablcom 19817 | An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
| Theorem | cmn32 19818 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌)) | ||
| Theorem | cmn4 19819 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) | ||
| Theorem | cmn12 19820 | 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 19821 | 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 19822 | A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.) |
| ⊢ (𝜑 → 𝐺 ∈ CMnd) ⇒ ⊢ (𝜑 → 𝐺 ∈ Mnd) | ||
| Theorem | cmnbascntr 19823 | The base set of a commutative monoid is its center. (Contributed by SN, 21-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntr‘𝐺) ⇒ ⊢ (𝐺 ∈ CMnd → 𝐵 = 𝑍) | ||
| Theorem | rinvmod 19824* | Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovmo 7670. (Contributed by AV, 31-Dec-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃*𝑤 ∈ 𝐵 (𝐴 + 𝑤) = 0 ) | ||
| Theorem | ablinvadd 19825 | The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁‘(𝑋 + 𝑌)) = ((𝑁‘𝑋) + (𝑁‘𝑌))) | ||
| Theorem | ablsub2inv 19826 | Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ 𝑁 = (invg‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑁‘𝑋) − (𝑁‘𝑌)) = (𝑌 − 𝑋)) | ||
| Theorem | ablsubadd 19827 | Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) = 𝑍 ↔ (𝑌 + 𝑍) = 𝑋)) | ||
| Theorem | ablsub4 19828 | Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) − (𝑍 + 𝑊)) = ((𝑋 − 𝑍) + (𝑌 − 𝑊))) | ||
| Theorem | abladdsub4 19829 | Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 + 𝑌) = (𝑍 + 𝑊) ↔ (𝑋 − 𝑍) = (𝑊 − 𝑌))) | ||
| Theorem | abladdsub 19830 | Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) − 𝑍) = ((𝑋 − 𝑍) + 𝑌)) | ||
| Theorem | ablsubadd23 19831 | Commutative/associative law for addition and subtraction in abelian groups. (subadd23d 11642 analog.) (Contributed by AV, 2-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) + 𝑍) = (𝑋 + (𝑍 − 𝑌))) | ||
| Theorem | ablsubaddsub 19832 | Double subtraction and addition in abelian groups. (cnambpcma 47306 analog.) (Contributed by AV, 3-Mar-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (((𝑋 − 𝑌) + 𝑍) − 𝑋) = (𝑍 − 𝑌)) | ||
| Theorem | ablpncan2 19833 | Cancellation law for subtraction in an Abelian group. (Contributed by NM, 2-Oct-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + 𝑌) − 𝑋) = 𝑌) | ||
| Theorem | ablpncan3 19834 | A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 + (𝑌 − 𝑋)) = 𝑌) | ||
| Theorem | ablsubsub 19835 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 − (𝑌 − 𝑍)) = ((𝑋 − 𝑌) + 𝑍)) | ||
| Theorem | ablsubsub4 19836 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑌 + 𝑍))) | ||
| Theorem | ablpnpcan 19837 | Cancellation law for mixed addition and subtraction. (pnpcan 11548 analog.) (Contributed by NM, 29-May-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) − (𝑋 + 𝑍)) = (𝑌 − 𝑍)) | ||
| Theorem | ablnncan 19838 | Cancellation law for group subtraction. (nncan 11538 analog.) (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 − (𝑋 − 𝑌)) = 𝑌) | ||
| Theorem | ablsub32 19839 | Swap the second and third terms in a double group subtraction. (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) − 𝑍) = ((𝑋 − 𝑍) − 𝑌)) | ||
| Theorem | ablnnncan 19840 | Cancellation law for group subtraction. (nnncan 11544 analog.) (Contributed by NM, 29-Feb-2008.) (Revised by AV, 27-Aug-2021.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − (𝑌 − 𝑍)) − 𝑍) = (𝑋 − 𝑌)) | ||
| Theorem | ablnnncan1 19841 | Cancellation law for group subtraction. (nnncan1 11545 analog.) (Contributed by NM, 7-Apr-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 − 𝑌) − (𝑋 − 𝑍)) = (𝑍 − 𝑌)) | ||
| Theorem | ablsubsub23 19842 | Swap subtrahend and result of group subtraction. (Contributed by NM, 14-Dec-2007.) (Revised by AV, 7-Oct-2021.) |
| ⊢ 𝑉 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) = 𝐶 ↔ (𝐴 − 𝐶) = 𝐵)) | ||
| Theorem | mulgnn0di 19843 | Group multiple of a sum, for nonnegative multiples. (Contributed by Mario Carneiro, 13-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) | ||
| Theorem | mulgdi 19844 | Group multiple of a sum. (Contributed by Mario Carneiro, 13-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 + 𝑌)) = ((𝑀 · 𝑋) + (𝑀 · 𝑌))) | ||
| Theorem | mulgmhm 19845* | 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 19846* | 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 19847 | Group multiple of a difference. (Contributed by Mario Carneiro, 13-Dec-2014.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ (𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑀 · (𝑋 − 𝑌)) = ((𝑀 · 𝑋) − (𝑀 · 𝑌))) | ||
| Theorem | ghmfghm 19848* | The function fulfilling the conditions of ghmgrp 19084 is a group homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑌 = (Base‘𝐻) & ⊢ + = (+g‘𝐺) & ⊢ ⨣ = (+g‘𝐻) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ (𝜑 → 𝐺 ∈ Grp) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | ||
| Theorem | ghmcmn 19849* | 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 19850* | 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 19851 | 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 19852 | Value of the subgroup coset equivalence relation on an abelian group. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝑆) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑆 ⊆ 𝑋) → (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ (𝐵 − 𝐴) ∈ 𝑆))) | ||
| Theorem | qusecsub 19853 | 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 19854 | A subgroup of an abelian group is also abelian. (Contributed by Mario Carneiro, 3-Dec-2014.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝐻 ∈ Abel) | ||
| Theorem | subcmn 19855 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝐻 ∈ Mnd) → 𝐻 ∈ CMnd) | ||
| Theorem | submcmn 19856 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑆 ∈ (SubMnd‘𝐺)) → 𝐻 ∈ CMnd) | ||
| Theorem | submcmn2 19857 | 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 19858 | 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 19859 | Any subset in a commutative monoid is a subset of its centralizer. (Contributed by AV, 12-Jan-2019.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝐺 ∈ CMnd ∧ 𝑆 ⊆ 𝐵) → 𝑆 ⊆ (𝑍‘𝑆)) | ||
| Theorem | cntrcmnd 19860 | The center of a monoid is a commutative submonoid. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
| ⊢ 𝑍 = (𝑀 ↾s (Cntr‘𝑀)) ⇒ ⊢ (𝑀 ∈ Mnd → 𝑍 ∈ CMnd) | ||
| Theorem | cntrabl 19861 | The center of a group is an abelian group. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
| ⊢ 𝑍 = (𝑀 ↾s (Cntr‘𝑀)) ⇒ ⊢ (𝑀 ∈ Grp → 𝑍 ∈ Abel) | ||
| Theorem | cntzspan 19862 | If the generators commute, the generated monoid is commutative. (Contributed by Mario Carneiro, 25-Apr-2016.) |
| ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubMnd‘𝐺)) & ⊢ 𝐻 = (𝐺 ↾s (𝐾‘𝑆)) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ⊆ (𝑍‘𝑆)) → 𝐻 ∈ CMnd) | ||
| Theorem | cntzcmnf 19863 | Discharge the centralizer assumption in a commutative monoid. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) ⇒ ⊢ (𝜑 → ran 𝐹 ⊆ (𝑍‘ran 𝐹)) | ||
| Theorem | ghmplusg 19864 | 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 19865 | Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
| ⊢ (𝐺 ∈ Abel → (NrmSGrp‘𝐺) = (SubGrp‘𝐺)) | ||
| Theorem | odadd1 19866 | 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 19867 | 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 19868 | 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 19869 | A group with exponent 2 (or 1) is abelian. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐸 ∥ 2) → 𝐺 ∈ Abel) | ||
| Theorem | gexexlem 19870* | Lemma for gexex 19871. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝐸 ∈ ℕ) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑂‘𝑦) ≤ (𝑂‘𝐴)) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) = 𝐸) | ||
| Theorem | gexex 19871* | 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 19872 | 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 19873* | 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 19874 | Subgroup sum commutes (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) | ||
| Theorem | ablcntzd 19875 | All subgroups in an abelian group commute. (Contributed by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Abel) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) | ||
| Theorem | lsmcom 19876 | Subgroup sum commutes. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Abel ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) | ||
| Theorem | lsmsubg2 19877 | 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 19878 | 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 19879 | The product of a family of commutative monoids is commutative. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
| ⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶CMnd) ⇒ ⊢ (𝜑 → 𝑌 ∈ CMnd) | ||
| Theorem | prdsabld 19880 | 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 19881 | The structure power on a commutative monoid is commutative. (Contributed by Mario Carneiro, 11-Jan-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ CMnd ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ CMnd) | ||
| Theorem | pwsabl 19882 | The structure power on an Abelian group is Abelian. (Contributed by Mario Carneiro, 21-Jan-2015.) |
| ⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ Abel ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Abel) | ||
| Theorem | qusabl 19883 | 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 19884 | The (smallest) structure representing a trivial abelian group. (Contributed by AV, 28-Apr-2019.) |
| ⊢ 𝑀 = {〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉} ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Abel) | ||
| Theorem | abln0 19885 | Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019.) |
| ⊢ Abel ≠ ∅ | ||
| Theorem | cnaddablx 19886 | The complex numbers are an Abelian group under addition. This version of cnaddabl 19887 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 19887 instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012.) |
| ⊢ 𝐺 = {〈1, ℂ〉, 〈2, + 〉} ⇒ ⊢ 𝐺 ∈ Abel | ||
| Theorem | cnaddabl 19887 | The complex numbers are an Abelian group under addition. This version of cnaddablx 19886 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 21403. (Contributed by NM, 20-Oct-2012.) (New usage is discouraged.) |
| ⊢ 𝐺 = {〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ⇒ ⊢ 𝐺 ∈ Abel | ||
| Theorem | cnaddid 19888 | The group identity element of complex number addition is zero. See also cnfld0 21405. (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 19889 | Value of the group inverse of complex number addition. See also cnfldneg 21408. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 26-Aug-2021.) (New usage is discouraged.) |
| ⊢ 𝐺 = {〈(Base‘ndx), ℂ〉, 〈(+g‘ndx), + 〉} ⇒ ⊢ (𝐴 ∈ ℂ → ((invg‘𝐺)‘𝐴) = -𝐴) | ||
| Theorem | zaddablx 19890 | The integers are an Abelian group under addition. Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. Use zsubrg 21438 instead. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.) |
| ⊢ 𝐺 = {〈1, ℤ〉, 〈2, + 〉} ⇒ ⊢ 𝐺 ∈ Abel | ||
| Theorem | frgpnabllem1 19891* | Lemma for frgpnabl 19893. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 25-Apr-2024.) |
| ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ + = (+g‘𝐺) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑈 = (varFGrp‘𝐼) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐼) & ⊢ (𝜑 → 𝐵 ∈ 𝐼) ⇒ ⊢ (𝜑 → 〈“〈𝐴, ∅〉〈𝐵, ∅〉”〉 ∈ (𝐷 ∩ ((𝑈‘𝐴) + (𝑈‘𝐵)))) | ||
| Theorem | frgpnabllem2 19892* | Lemma for frgpnabl 19893. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 25-Apr-2024.) |
| ⊢ 𝐺 = (freeGrp‘𝐼) & ⊢ 𝑊 = ( I ‘Word (𝐼 × 2o)) & ⊢ ∼ = ( ~FG ‘𝐼) & ⊢ + = (+g‘𝐺) & ⊢ 𝑀 = (𝑦 ∈ 𝐼, 𝑧 ∈ 2o ↦ 〈𝑦, (1o ∖ 𝑧)〉) & ⊢ 𝑇 = (𝑣 ∈ 𝑊 ↦ (𝑛 ∈ (0...(♯‘𝑣)), 𝑤 ∈ (𝐼 × 2o) ↦ (𝑣 splice 〈𝑛, 𝑛, 〈“𝑤(𝑀‘𝑤)”〉〉))) & ⊢ 𝐷 = (𝑊 ∖ ∪ 𝑥 ∈ 𝑊 ran (𝑇‘𝑥)) & ⊢ 𝑈 = (varFGrp‘𝐼) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐼) & ⊢ (𝜑 → 𝐵 ∈ 𝐼) & ⊢ (𝜑 → ((𝑈‘𝐴) + (𝑈‘𝐵)) = ((𝑈‘𝐵) + (𝑈‘𝐴))) ⇒ ⊢ (𝜑 → 𝐴 = 𝐵) | ||
| Theorem | frgpnabl 19893 | The free group on two or more generators is not abelian. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐺 = (freeGrp‘𝐼) ⇒ ⊢ (1o ≺ 𝐼 → ¬ 𝐺 ∈ Abel) | ||
| Theorem | imasabl 19894* | The image structure of an abelian group is an abelian group (imasgrp 19074 analog). (Contributed by AV, 22-Feb-2025.) |
| ⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) & ⊢ (𝜑 → 𝑉 = (Base‘𝑅)) & ⊢ (𝜑 → + = (+g‘𝑅)) & ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) & ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞)))) & ⊢ (𝜑 → 𝑅 ∈ Abel) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ (𝜑 → (𝑈 ∈ Abel ∧ (𝐹‘ 0 ) = (0g‘𝑈))) | ||
| Syntax | ccyg 19895 | Cyclic group. |
| class CycGrp | ||
| Definition | df-cyg 19896* | Define a cyclic group, which is a group with an element 𝑥, called the generator of the group, such that all elements in the group are multiples of 𝑥. A generator is usually not unique. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ CycGrp = {𝑔 ∈ Grp ∣ ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥)) = (Base‘𝑔)} | ||
| Theorem | iscyg 19897* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) ⇒ ⊢ (𝐺 ∈ CycGrp ↔ (𝐺 ∈ Grp ∧ ∃𝑥 ∈ 𝐵 ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵)) | ||
| Theorem | iscyggen 19898* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} ⇒ ⊢ (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑋)) = 𝐵)) | ||
| Theorem | iscyggen2 19899* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} ⇒ ⊢ (𝐺 ∈ Grp → (𝑋 ∈ 𝐸 ↔ (𝑋 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑛 ∈ ℤ 𝑦 = (𝑛 · 𝑋)))) | ||
| Theorem | iscyg2 19900* | A cyclic group is a group which contains a generator. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 𝐸 = {𝑥 ∈ 𝐵 ∣ ran (𝑛 ∈ ℤ ↦ (𝑛 · 𝑥)) = 𝐵} ⇒ ⊢ (𝐺 ∈ CycGrp ↔ (𝐺 ∈ Grp ∧ 𝐸 ≠ ∅)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |