![]() |
Metamath
Proof Explorer Theorem List (p. 198 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ablpropd 19701* | 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 19702 | 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 19703* | Properties that determine a commutative monoid. (Contributed by Mario Carneiro, 7-Jan-2015.) |
โข (๐ โ ๐ต = (Baseโ๐บ)) & โข (๐ โ + = (+gโ๐บ)) & โข (๐ โ ๐บ โ Mnd) & โข ((๐ โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)) โ โข (๐ โ ๐บ โ CMnd) | ||
Theorem | isabld 19704* | Properties that determine an Abelian group. (Contributed by NM, 6-Aug-2013.) |
โข (๐ โ ๐ต = (Baseโ๐บ)) & โข (๐ โ + = (+gโ๐บ)) & โข (๐ โ ๐บ โ Grp) & โข ((๐ โง ๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)) โ โข (๐ โ ๐บ โ Abel) | ||
Theorem | isabli 19705* | Properties that determine an Abelian group. (Contributed by NM, 4-Sep-2011.) |
โข ๐บ โ Grp & โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข ((๐ฅ โ ๐ต โง ๐ฆ โ ๐ต) โ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)) โ โข ๐บ โ Abel | ||
Theorem | cmnmnd 19706 | A commutative monoid is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
โข (๐บ โ CMnd โ ๐บ โ Mnd) | ||
Theorem | cmncom 19707 | A commutative monoid is commutative. (Contributed by Mario Carneiro, 6-Jan-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ CMnd โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ + ๐) = (๐ + ๐)) | ||
Theorem | ablcom 19708 | An Abelian group operation is commutative. (Contributed by NM, 26-Aug-2011.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Abel โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ + ๐) = (๐ + ๐)) | ||
Theorem | cmn32 19709 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ CMnd โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) + ๐) = ((๐ + ๐) + ๐)) | ||
Theorem | cmn4 19710 | Commutative/associative law for commutative monoids. (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ CMnd โง (๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) + (๐ + ๐)) = ((๐ + ๐) + (๐ + ๐))) | ||
Theorem | cmn12 19711 | 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 19712 | 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 19713 | A commutative monoid is a monoid. (Contributed by SN, 1-Jun-2024.) |
โข (๐ โ ๐บ โ CMnd) โ โข (๐ โ ๐บ โ Mnd) | ||
Theorem | cmnbascntr 19714 | The base set of a commutative monoid is its center. (Contributed by SN, 21-Mar-2025.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (Cntrโ๐บ) โ โข (๐บ โ CMnd โ ๐ต = ๐) | ||
Theorem | rinvmod 19715* | Uniqueness of a right inverse element in a commutative monoid, if it exists. Corresponds to caovmo 7646. (Contributed by AV, 31-Dec-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข + = (+gโ๐บ) & โข (๐ โ ๐บ โ CMnd) & โข (๐ โ ๐ด โ ๐ต) โ โข (๐ โ โ*๐ค โ ๐ต (๐ด + ๐ค) = 0 ) | ||
Theorem | ablinvadd 19716 | The inverse of an Abelian group operation. (Contributed by NM, 31-Mar-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข ๐ = (invgโ๐บ) โ โข ((๐บ โ Abel โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐โ(๐ + ๐)) = ((๐โ๐) + (๐โ๐))) | ||
Theorem | ablsub2inv 19717 | Abelian group subtraction of two inverses. (Contributed by Stefan O'Rear, 24-May-2015.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข ๐ = (invgโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐โ๐) โ (๐โ๐)) = (๐ โ ๐)) | ||
Theorem | ablsubadd 19718 | Relationship between Abelian group subtraction and addition. (Contributed by NM, 31-Mar-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ ๐) = ๐ โ (๐ + ๐) = ๐)) | ||
Theorem | ablsub4 19719 | Commutative/associative subtraction law for Abelian groups. (Contributed by NM, 31-Mar-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) โ (๐ + ๐)) = ((๐ โ ๐) + (๐ โ ๐))) | ||
Theorem | abladdsub4 19720 | Abelian group addition/subtraction law. (Contributed by NM, 31-Mar-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต) โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) = (๐ + ๐) โ (๐ โ ๐) = (๐ โ ๐))) | ||
Theorem | abladdsub 19721 | Associative-type law for group subtraction and addition. (Contributed by NM, 19-Apr-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) โ ๐) = ((๐ โ ๐) + ๐)) | ||
Theorem | ablsubadd23 19722 | Commutative/associative law for addition and subtraction in abelian groups. (subadd23d 11597 analog.) (Contributed by AV, 2-Mar-2025.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ ๐) + ๐) = (๐ + (๐ โ ๐))) | ||
Theorem | ablsubaddsub 19723 | Double subtraction and addition in abelian groups. (cnambpcma 46300 analog.) (Contributed by AV, 3-Mar-2025.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (((๐ โ ๐) + ๐) โ ๐) = (๐ โ ๐)) | ||
Theorem | ablpncan2 19724 | Cancellation law for subtraction in an Abelian group. (Contributed by NM, 2-Oct-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ + ๐) โ ๐) = ๐) | ||
Theorem | ablpncan3 19725 | A cancellation law for Abelian groups. (Contributed by NM, 23-Mar-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ + (๐ โ ๐)) = ๐) | ||
Theorem | ablsubsub 19726 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐ โ (๐ โ ๐)) = ((๐ โ ๐) + ๐)) | ||
Theorem | ablsubsub4 19727 | Law for double subtraction. (Contributed by NM, 7-Apr-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐ โ ๐) โ ๐) = (๐ โ (๐ + ๐))) | ||
Theorem | ablpnpcan 19728 | Cancellation law for mixed addition and subtraction. (pnpcan 11503 analog.) (Contributed by NM, 29-May-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐ + ๐) โ (๐ + ๐)) = (๐ โ ๐)) | ||
Theorem | ablnncan 19729 | Cancellation law for group subtraction. (nncan 11493 analog.) (Contributed by NM, 7-Apr-2015.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐ โ (๐ โ ๐)) = ๐) | ||
Theorem | ablsub32 19730 | Swap the second and third terms in a double group subtraction. (Contributed by NM, 7-Apr-2015.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐ โ ๐) โ ๐) = ((๐ โ ๐) โ ๐)) | ||
Theorem | ablnnncan 19731 | Cancellation law for group subtraction. (nnncan 11499 analog.) (Contributed by NM, 29-Feb-2008.) (Revised by AV, 27-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐ โ (๐ โ ๐)) โ ๐) = (๐ โ ๐)) | ||
Theorem | ablnnncan1 19732 | Cancellation law for group subtraction. (nnncan1 11500 analog.) (Contributed by NM, 7-Apr-2015.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐ โ ๐) โ (๐ โ ๐)) = (๐ โ ๐)) | ||
Theorem | ablsubsub23 19733 | Swap subtrahend and result of group subtraction. (Contributed by NM, 14-Dec-2007.) (Revised by AV, 7-Oct-2021.) |
โข ๐ = (Baseโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ด โ ๐ โง ๐ต โ ๐ โง ๐ถ โ ๐)) โ ((๐ด โ ๐ต) = ๐ถ โ (๐ด โ ๐ถ) = ๐ต)) | ||
Theorem | mulgnn0di 19734 | Group multiple of a sum, for nonnegative multiples. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ CMnd โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) | ||
Theorem | mulgdi 19735 | Group multiple of a sum. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) | ||
Theorem | mulgmhm 19736* | 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 19737* | 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 19738 | Group multiple of a difference. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Abel โง (๐ โ โค โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ โ ๐)) = ((๐ ยท ๐) โ (๐ ยท ๐))) | ||
Theorem | ghmfghm 19739* | The function fulfilling the conditions of ghmgrp 18985 is a group homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.) |
โข ๐ = (Baseโ๐บ) & โข ๐ = (Baseโ๐ป) & โข + = (+gโ๐บ) & โข โจฃ = (+gโ๐ป) & โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐นโ(๐ฅ + ๐ฆ)) = ((๐นโ๐ฅ) โจฃ (๐นโ๐ฆ))) & โข (๐ โ ๐น:๐โontoโ๐) & โข (๐ โ ๐บ โ Grp) โ โข (๐ โ ๐น โ (๐บ GrpHom ๐ป)) | ||
Theorem | ghmcmn 19740* | 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 19741* | 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 19742 | 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 19743 | Value of the subgroup coset equivalence relation on an abelian group. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข ๐ = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข โผ = (๐บ ~QG ๐) โ โข ((๐บ โ Abel โง ๐ โ ๐) โ (๐ด โผ ๐ต โ (๐ด โ ๐ โง ๐ต โ ๐ โง (๐ต โ ๐ด) โ ๐))) | ||
Theorem | qusecsub 19744 | 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 19745 | A subgroup of an abelian group is also abelian. (Contributed by Mario Carneiro, 3-Dec-2014.) |
โข ๐ป = (๐บ โพs ๐) โ โข ((๐บ โ Abel โง ๐ โ (SubGrpโ๐บ)) โ ๐ป โ Abel) | ||
Theorem | subcmn 19746 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 10-Jan-2015.) |
โข ๐ป = (๐บ โพs ๐) โ โข ((๐บ โ CMnd โง ๐ป โ Mnd) โ ๐ป โ CMnd) | ||
Theorem | submcmn 19747 | A submonoid of a commutative monoid is also commutative. (Contributed by Mario Carneiro, 24-Apr-2016.) |
โข ๐ป = (๐บ โพs ๐) โ โข ((๐บ โ CMnd โง ๐ โ (SubMndโ๐บ)) โ ๐ป โ CMnd) | ||
Theorem | submcmn2 19748 | 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 19749 | 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 19750 | Any subset in a commutative monoid is a subset of its centralizer. (Contributed by AV, 12-Jan-2019.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (Cntzโ๐บ) โ โข ((๐บ โ CMnd โง ๐ โ ๐ต) โ ๐ โ (๐โ๐)) | ||
Theorem | cntrcmnd 19751 | The center of a monoid is a commutative submonoid. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
โข ๐ = (๐ โพs (Cntrโ๐)) โ โข (๐ โ Mnd โ ๐ โ CMnd) | ||
Theorem | cntrabl 19752 | The center of a group is an abelian group. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
โข ๐ = (๐ โพs (Cntrโ๐)) โ โข (๐ โ Grp โ ๐ โ Abel) | ||
Theorem | cntzspan 19753 | If the generators commute, the generated monoid is commutative. (Contributed by Mario Carneiro, 25-Apr-2016.) |
โข ๐ = (Cntzโ๐บ) & โข ๐พ = (mrClsโ(SubMndโ๐บ)) & โข ๐ป = (๐บ โพs (๐พโ๐)) โ โข ((๐บ โ Mnd โง ๐ โ (๐โ๐)) โ ๐ป โ CMnd) | ||
Theorem | cntzcmnf 19754 | Discharge the centralizer assumption in a commutative monoid. (Contributed by Mario Carneiro, 24-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (Cntzโ๐บ) & โข (๐ โ ๐บ โ CMnd) & โข (๐ โ ๐น:๐ดโถ๐ต) โ โข (๐ โ ran ๐น โ (๐โran ๐น)) | ||
Theorem | ghmplusg 19755 | 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 19756 | Every subgroup of an abelian group is normal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข (๐บ โ Abel โ (NrmSGrpโ๐บ) = (SubGrpโ๐บ)) | ||
Theorem | odadd1 19757 | 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 19758 | 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 19759 | 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 19760 | A group with exponent 2 (or 1) is abelian. (Contributed by Mario Carneiro, 24-Apr-2016.) |
โข ๐ = (Baseโ๐บ) & โข ๐ธ = (gExโ๐บ) โ โข ((๐บ โ Grp โง ๐ธ โฅ 2) โ ๐บ โ Abel) | ||
Theorem | gexexlem 19761* | Lemma for gexex 19762. (Contributed by Mario Carneiro, 24-Apr-2016.) |
โข ๐ = (Baseโ๐บ) & โข ๐ธ = (gExโ๐บ) & โข ๐ = (odโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ธ โ โ) & โข (๐ โ ๐ด โ ๐) & โข ((๐ โง ๐ฆ โ ๐) โ (๐โ๐ฆ) โค (๐โ๐ด)) โ โข (๐ โ (๐โ๐ด) = ๐ธ) | ||
Theorem | gexex 19762* | 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 19763 | 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 19764* | 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 19765 | Subgroup sum commutes (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (LSSumโ๐บ) โ โข ((๐บ โ Abel โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ ๐) = (๐ โ ๐)) | ||
Theorem | ablcntzd 19766 | All subgroups in an abelian group commute. (Contributed by Mario Carneiro, 19-Apr-2016.) |
โข ๐ = (Cntzโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) โ โข (๐ โ ๐ โ (๐โ๐)) | ||
Theorem | lsmcom 19767 | Subgroup sum commutes. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
โข โ = (LSSumโ๐บ) โ โข ((๐บ โ Abel โง ๐ โ (SubGrpโ๐บ) โง ๐ โ (SubGrpโ๐บ)) โ (๐ โ ๐) = (๐ โ ๐)) | ||
Theorem | lsmsubg2 19768 | 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 19769 | 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 19770 | The product of a family of commutative monoids is commutative. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
โข ๐ = (๐Xs๐ ) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ :๐ผโถCMnd) โ โข (๐ โ ๐ โ CMnd) | ||
Theorem | prdsabld 19771 | 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 19772 | The structure power on a commutative monoid is commutative. (Contributed by Mario Carneiro, 11-Jan-2015.) |
โข ๐ = (๐ โs ๐ผ) โ โข ((๐ โ CMnd โง ๐ผ โ ๐) โ ๐ โ CMnd) | ||
Theorem | pwsabl 19773 | The structure power on an Abelian group is Abelian. (Contributed by Mario Carneiro, 21-Jan-2015.) |
โข ๐ = (๐ โs ๐ผ) โ โข ((๐ โ Abel โง ๐ผ โ ๐) โ ๐ โ Abel) | ||
Theorem | qusabl 19774 | 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 19775 | The (smallest) structure representing a trivial abelian group. (Contributed by AV, 28-Apr-2019.) |
โข ๐ = {โจ(Baseโndx), {๐ผ}โฉ, โจ(+gโndx), {โจโจ๐ผ, ๐ผโฉ, ๐ผโฉ}โฉ} โ โข (๐ผ โ ๐ โ ๐ โ Abel) | ||
Theorem | abln0 19776 | Abelian groups (and therefore also groups and monoids) exist. (Contributed by AV, 29-Apr-2019.) |
โข Abel โ โ | ||
Theorem | cnaddablx 19777 | The complex numbers are an Abelian group under addition. This version of cnaddabl 19778 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 19778 instead. (New usage is discouraged.) (Contributed by NM, 18-Oct-2012.) |
โข ๐บ = {โจ1, โโฉ, โจ2, + โฉ} โ โข ๐บ โ Abel | ||
Theorem | cnaddabl 19778 | The complex numbers are an Abelian group under addition. This version of cnaddablx 19777 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 21167. (Contributed by NM, 20-Oct-2012.) (New usage is discouraged.) |
โข ๐บ = {โจ(Baseโndx), โโฉ, โจ(+gโndx), + โฉ} โ โข ๐บ โ Abel | ||
Theorem | cnaddid 19779 | The group identity element of complex number addition is zero. See also cnfld0 21169. (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 19780 | Value of the group inverse of complex number addition. See also cnfldneg 21171. (Contributed by Steve Rodriguez, 3-Dec-2006.) (Revised by AV, 26-Aug-2021.) (New usage is discouraged.) |
โข ๐บ = {โจ(Baseโndx), โโฉ, โจ(+gโndx), + โฉ} โ โข (๐ด โ โ โ ((invgโ๐บ)โ๐ด) = -๐ด) | ||
Theorem | zaddablx 19781 | 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 21198 instead. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.) |
โข ๐บ = {โจ1, โคโฉ, โจ2, + โฉ} โ โข ๐บ โ Abel | ||
Theorem | frgpnabllem1 19782* | Lemma for frgpnabl 19784. (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 19783* | Lemma for frgpnabl 19784. (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 19784 | The free group on two or more generators is not abelian. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐บ = (freeGrpโ๐ผ) โ โข (1o โบ ๐ผ โ ยฌ ๐บ โ Abel) | ||
Theorem | imasabl 19785* | The image structure of an abelian group is an abelian group (imasgrp 18975 analog). (Contributed by AV, 22-Feb-2025.) |
โข (๐ โ ๐ = (๐น โs ๐ )) & โข (๐ โ ๐ = (Baseโ๐ )) & โข (๐ โ + = (+gโ๐ )) & โข (๐ โ ๐น:๐โontoโ๐ต) & โข ((๐ โง (๐ โ ๐ โง ๐ โ ๐) โง (๐ โ ๐ โง ๐ โ ๐)) โ (((๐นโ๐) = (๐นโ๐) โง (๐นโ๐) = (๐นโ๐)) โ (๐นโ(๐ + ๐)) = (๐นโ(๐ + ๐)))) & โข (๐ โ ๐ โ Abel) & โข 0 = (0gโ๐ ) โ โข (๐ โ (๐ โ Abel โง (๐นโ 0 ) = (0gโ๐))) | ||
Syntax | ccyg 19786 | Cyclic group. |
class CycGrp | ||
Definition | df-cyg 19787* | 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 19788* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข (๐บ โ CycGrp โ (๐บ โ Grp โง โ๐ฅ โ ๐ต ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต)) | ||
Theorem | iscyggen 19789* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} โ โข (๐ โ ๐ธ โ (๐ โ ๐ต โง ran (๐ โ โค โฆ (๐ ยท ๐)) = ๐ต)) | ||
Theorem | iscyggen2 19790* | The property of being a cyclic generator for a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} โ โข (๐บ โ Grp โ (๐ โ ๐ธ โ (๐ โ ๐ต โง โ๐ฆ โ ๐ต โ๐ โ โค ๐ฆ = (๐ ยท ๐)))) | ||
Theorem | iscyg2 19791* | A cyclic group is a group which contains a generator. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} โ โข (๐บ โ CycGrp โ (๐บ โ Grp โง ๐ธ โ โ )) | ||
Theorem | cyggeninv 19792* | The inverse of a cyclic generator is a generator. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} & โข ๐ = (invgโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ธ) โ (๐โ๐) โ ๐ธ) | ||
Theorem | cyggenod 19793* | An element is the generator of a finite group iff the order of the generator equals the order of the group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} & โข ๐ = (odโ๐บ) โ โข ((๐บ โ Grp โง ๐ต โ Fin) โ (๐ โ ๐ธ โ (๐ โ ๐ต โง (๐โ๐) = (โฏโ๐ต)))) | ||
Theorem | cyggenod2 19794* | In an infinite cyclic group, the generator must have infinite order, but this property no longer characterizes the generators. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ธ = {๐ฅ โ ๐ต โฃ ran (๐ โ โค โฆ (๐ ยท ๐ฅ)) = ๐ต} & โข ๐ = (odโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ธ) โ (๐โ๐) = if(๐ต โ Fin, (โฏโ๐ต), 0)) | ||
Theorem | iscyg3 19795* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข (๐บ โ CycGrp โ (๐บ โ Grp โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ โ โค ๐ฆ = (๐ ยท ๐ฅ))) | ||
Theorem | iscygd 19796* | Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ โ ๐ต) & โข ((๐ โง ๐ฆ โ ๐ต) โ โ๐ โ โค ๐ฆ = (๐ ยท ๐)) โ โข (๐ โ ๐บ โ CycGrp) | ||
Theorem | iscygodd 19797 | Show that a group with an element the same order as the group is cyclic. (Contributed by Mario Carneiro, 27-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ (๐โ๐) = (โฏโ๐ต)) โ โข (๐ โ ๐บ โ CycGrp) | ||
Theorem | cycsubmcmn 19798* | The set of nonnegative integer powers of an element ๐ด of a monoid forms a commutative monoid. (Contributed by AV, 20-Jan-2024.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐น = (๐ฅ โ โ0 โฆ (๐ฅ ยท ๐ด)) & โข ๐ถ = ran ๐น โ โข ((๐บ โ Mnd โง ๐ด โ ๐ต) โ (๐บ โพs ๐ถ) โ CMnd) | ||
Theorem | cyggrp 19799 | A cyclic group is a group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข (๐บ โ CycGrp โ ๐บ โ Grp) | ||
Theorem | cygabl 19800 | A cyclic group is abelian. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 20-Jan-2024.) |
โข (๐บ โ CycGrp โ ๐บ โ Abel) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |