Home | Metamath
Proof Explorer Theorem List (p. 178 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-gim 17701* | An isomorphism of groups is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group operation. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
GrpIso | ||
Definition | df-gic 17702 | Two groups are said to be isomorphic iff they are connected by at least one isomorphism. Isomorphic groups share all global group properties, but to relate local properties requires knowledge of a specific isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
𝑔 GrpIso | ||
Theorem | gimfn 17703 | The group isomorphism function is a well-defined function. (Contributed by Mario Carneiro, 23-Aug-2015.) |
GrpIso | ||
Theorem | isgim 17704 | An isomorphism of groups is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
GrpIso | ||
Theorem | gimf1o 17705 | An isomorphism of groups is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
GrpIso | ||
Theorem | gimghm 17706 | An isomorphism of groups is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
GrpIso | ||
Theorem | isgim2 17707 | A group isomorphism is a homomorphism whose converse is also a homomorphism. Characterization of isomorphisms similar to ishmeo 21562. (Contributed by Mario Carneiro, 6-May-2015.) |
GrpIso | ||
Theorem | subggim 17708 | Behavior of subgroups under isomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
GrpIso SubGrp SubGrp | ||
Theorem | gimcnv 17709 | The converse of a bijective group homomorphism is a bijective group homomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
GrpIso GrpIso | ||
Theorem | gimco 17710 | The composition of group isomorphisms is a group isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
GrpIso GrpIso GrpIso | ||
Theorem | brgic 17711 | The relation "is isomorphic to" for groups. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
𝑔 GrpIso | ||
Theorem | brgici 17712 | Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
GrpIso 𝑔 | ||
Theorem | gicref 17713 | Isomorphism is reflexive. (Contributed by Mario Carneiro, 21-Apr-2016.) |
𝑔 | ||
Theorem | giclcl 17714 | Isomorphism implies the left side is a group. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
𝑔 | ||
Theorem | gicrcl 17715 | Isomorphism implies the right side is a group. (Contributed by Mario Carneiro, 6-May-2015.) |
𝑔 | ||
Theorem | gicsym 17716 | Isomorphism is symmetric. (Contributed by Mario Carneiro, 21-Apr-2016.) |
𝑔 𝑔 | ||
Theorem | gictr 17717 | Isomorphism is transitive. (Contributed by Mario Carneiro, 21-Apr-2016.) |
𝑔 𝑔 𝑔 | ||
Theorem | gicer 17718 | Isomorphism is an equivalence relation on groups. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 1-May-2021.) |
𝑔 | ||
Theorem | gicerOLD 17719 | Obsolete proof of gicer 17718 as of 1-May-2021. Isomorphism is an equivalence relation on groups. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof modification is discouraged.) (New usage is discouraged.) |
𝑔 | ||
Theorem | gicen 17720 | Isomorphic groups have equinumerous base sets. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
𝑔 | ||
Theorem | gicsubgen 17721 | A less trivial example of a group invariant: cardinality of the subgroup lattice. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
𝑔 SubGrp SubGrp | ||
Syntax | cga 17722 | Extend class definition to include the class of group actions. |
Definition | df-ga 17723* | Define the class of all group actions. A group acts on a set if a permutation on is associated with every element of in such a way that the identity permutation on is associated with the neutral element of , and the composition of the permutations associated with two elements of is identical with the permutation associated with the composition of these two elements (in the same order) in the group . (Contributed by Jeff Hankins, 10-Aug-2009.) |
Theorem | isga 17724* | The predicate "is a (left) group action." The group is said to act on the base set of the action, which is not assumed to have any special properties. There is a related notion of right group action, but as the Wikipedia article explains, it is not mathematically interesting. The way actions are usually thought of is that each element of is a permutation of the elements of (see gapm 17739). Since group theory was classically about symmetry groups, it is therefore likely that the notion of group action was useful even in early group theory. (Contributed by Jeff Hankins, 10-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
Theorem | gagrp 17725 | The left argument of a group action is a group. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 30-Apr-2015.) |
Theorem | gaset 17726 | The right argument of a group action is a set. (Contributed by Mario Carneiro, 30-Apr-2015.) |
Theorem | gagrpid 17727 | The identity of the group does not alter the base set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
Theorem | gaf 17728 | The mapping of the group action operation. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
Theorem | gafo 17729 | A group action is onto its base set. (Contributed by Jeff Hankins, 10-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
Theorem | gaass 17730 | An "associative" property for group actions. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
Theorem | ga0 17731 | The action of a group on the empty set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
Theorem | gaid 17732 | The trivial action of a group on any set. Each group element corresponds to the identity permutation. (Contributed by Jeff Hankins, 11-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.) |
Theorem | subgga 17733* | A subgroup acts on its parent group. (Contributed by Jeff Hankins, 13-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.) |
↾s SubGrp | ||
Theorem | gass 17734* | A subset of a group action is a group action iff it is closed under the group action operation. (Contributed by Mario Carneiro, 17-Jan-2015.) |
Theorem | gasubg 17735 | The restriction of a group action to a subgroup is a group action. (Contributed by Mario Carneiro, 17-Jan-2015.) |
↾s SubGrp | ||
Theorem | gaid2 17736* | A group operation is a left group action of the group on itself. (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 13-Jan-2015.) |
Theorem | galcan 17737 | The action of a particular group element is left-cancelable. (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 13-Jan-2015.) |
Theorem | gacan 17738 | Group inverses cancel in a group action. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
Theorem | gapm 17739* | The action of a particular group element is a permutation of the base set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.) |
Theorem | gaorb 17740* | The orbit equivalence relation puts two points in the group action in the same equivalence class iff there is a group element that takes one element to the other. (Contributed by Mario Carneiro, 14-Jan-2015.) |
Theorem | gaorber 17741* | The orbit equivalence relation is an equivalence relation on the target set of the group action. (Contributed by NM, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
Theorem | gastacl 17742* | The stabilizer subgroup in a group action. (Contributed by Mario Carneiro, 15-Jan-2015.) |
SubGrp | ||
Theorem | gastacos 17743* | Write the coset relation for the stabilizer subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.) |
~QG | ||
Theorem | orbstafun 17744* | Existence and uniqueness for the function of orbsta 17746. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
~QG | ||
Theorem | orbstaval 17745* | Value of the function at a given equivalence class element. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
~QG | ||
Theorem | orbsta 17746* | The Orbit-Stabilizer theorem. The mapping is a bijection from the cosets of the stabilizer subgroup of to the orbit of . (Contributed by Mario Carneiro, 15-Jan-2015.) |
~QG | ||
Theorem | orbsta2 17747* | Relation between the size of the orbit and the size of the stabilizer of a point in a finite group action. (Contributed by Mario Carneiro, 16-Jan-2015.) |
~QG | ||
Syntax | ccntz 17748 | Syntax for the centralizer of a set in a monoid. |
Cntz | ||
Syntax | ccntr 17749 | Syntax for the centralizer of a monoid. |
Cntr | ||
Definition | df-cntz 17750* | Define the centralizer of a subset of a magma, which is the set of elements each of which commutes with each element of the given subset. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
Cntz | ||
Definition | df-cntr 17751 | Define the center of a magma, which is the elements that commute with all others. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
Cntr Cntz | ||
Theorem | cntrval 17752 | Substitute definition of the center. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
Cntz Cntr | ||
Theorem | cntzfval 17753* | First level substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
Cntz | ||
Theorem | cntzval 17754* | Definition substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
Cntz | ||
Theorem | elcntz 17755* | Elementhood in the centralizer. (Contributed by Mario Carneiro, 22-Sep-2015.) |
Cntz | ||
Theorem | cntzel 17756* | Membership in a centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
Cntz | ||
Theorem | cntzsnval 17757* | Special substitution for the centralizer of a singleton. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
Cntz | ||
Theorem | elcntzsn 17758 | Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016.) |
Cntz | ||
Theorem | sscntz 17759* | A centralizer expression for two sets elementwise commuting. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
Cntz | ||
Theorem | cntzrcl 17760 | Reverse closure for elements of the centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
Cntz | ||
Theorem | cntzssv 17761 | The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
Cntz | ||
Theorem | cntzi 17762 | Membership in a centralizer (inference). (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 22-Sep-2015.) |
Cntz | ||
Theorem | cntri 17763 | Defining property of the center of a group. (Contributed by Mario Carneiro, 22-Sep-2015.) |
Cntr | ||
Theorem | resscntz 17764 | Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015.) |
↾s Cntz Cntz | ||
Theorem | cntz2ss 17765 | Centralizers reverse the subset relation. (Contributed by Mario Carneiro, 3-Oct-2015.) |
Cntz | ||
Theorem | cntzrec 17766 | Reciprocity relationship for centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
Cntz | ||
Theorem | cntziinsn 17767* | Express any centralizer as an intersection of singleton centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
Cntz | ||
Theorem | cntzsubm 17768 | Centralizers in a monoid are submonoids. (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
Cntz SubMnd | ||
Theorem | cntzsubg 17769 | Centralizers in a group are subgroups. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
Cntz SubGrp | ||
Theorem | cntzidss 17770 | If the elements of commute, the elements of a subset also commute. (Contributed by Mario Carneiro, 25-Apr-2016.) |
Cntz | ||
Theorem | cntzmhm 17771 | Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.) |
Cntz Cntz MndHom | ||
Theorem | cntzmhm2 17772 | Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.) |
Cntz Cntz MndHom | ||
Theorem | cntrsubgnsg 17773 | A central subgroup is normal. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
Cntr SubGrp NrmSGrp | ||
Theorem | cntrnsg 17774 | The center of a group is a normal subgroup. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
Cntr NrmSGrp | ||
Syntax | coppg 17775 | The opposite group operation. |
oppg | ||
Definition | df-oppg 17776 | Define an opposite group, which is the same as the original group but with addition written the other way around. df-oppr 18623 does the same thing for multiplication. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
oppg sSet tpos | ||
Theorem | oppgval 17777 | Value of the opposite group. (Contributed by Stefan O'Rear, 25-Aug-2015.) (Revised by Mario Carneiro, 16-Sep-2015.) (Revised by Fan Zheng, 26-Jun-2016.) |
oppg sSet tpos | ||
Theorem | oppgplusfval 17778 | Value of the addition operation of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Fan Zheng, 26-Jun-2016.) |
oppg tpos | ||
Theorem | oppgplus 17779 | Value of the addition operation of an opposite ring. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Fan Zheng, 26-Jun-2016.) |
oppg | ||
Theorem | oppglem 17780 | Lemma for oppgbas 17781. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
oppg Slot | ||
Theorem | oppgbas 17781 | Base set of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
oppg | ||
Theorem | oppgtset 17782 | Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
oppg TopSet TopSet | ||
Theorem | oppgtopn 17783 | Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
oppg | ||
Theorem | oppgmnd 17784 | The opposite of a monoid is a monoid. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 16-Sep-2015.) |
oppg | ||
Theorem | oppgmndb 17785 | Bidirectional form of oppgmnd 17784. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
oppg | ||
Theorem | oppgid 17786 | Zero in a monoid is a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 16-Sep-2015.) |
oppg | ||
Theorem | oppggrp 17787 | The opposite of a group is a group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
oppg | ||
Theorem | oppggrpb 17788 | Bidirectional form of oppggrp 17787. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
oppg | ||
Theorem | oppginv 17789 | Inverses in a group are a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
oppg | ||
Theorem | invoppggim 17790 | The inverse is an antiautomorphism on any group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
oppg GrpIso | ||
Theorem | oppggic 17791 | Every group is (naturally) isomorphic to its opposite. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
oppg 𝑔 | ||
Theorem | oppgsubm 17792 | Being a submonoid is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.) |
oppg SubMnd SubMnd | ||
Theorem | oppgsubg 17793 | Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.) |
oppg SubGrp SubGrp | ||
Theorem | oppgcntz 17794 | A centralizer in a group is the same as the centralizer in the opposite group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
oppg Cntz Cntz | ||
Theorem | oppgcntr 17795 | The center of a group is the same as the center of the opposite group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
oppg Cntr Cntr | ||
Theorem | gsumwrev 17796 | A sum in an opposite monoid is the regular sum of a reversed word. (Contributed by Stefan O'Rear, 27-Aug-2015.) (Proof shortened by Mario Carneiro, 28-Feb-2016.) |
oppg Word g g reverse | ||
According to Wikipedia ("Symmetric group", 09-Mar-2019,
https://en.wikipedia.org/wiki/symmetric_group) "In abstract algebra, the
symmetric group defined over any set is the group whose elements are all the
bijections from the set to itself, and whose group operation is the composition
of functions." and according to Encyclopedia of Mathematics ("Symmetric group",
09-Mar-2019, https://www.encyclopediaofmath.org/index.php/Symmetric_group)
"The group of all permutations (self-bijections) of a set with the operation of
composition (see Permutation group).". In [Rotman] p. 27 "If X is a nonempty
set, a permutation of X is a function a : X -> X that is a one-to-one
correspondence." and "If X is a nonempty set, the symmetric group on X, denoted
SX, is the group whose elements are the permutations of X and whose
binary operation is composition of functions.". Therefore, we define the
symmetric group on a set as the set of one-to-one onto functions
from to itself under function composition, see df-symg 17798. However, the
set is allowed to be empty, see symgbas0 17814. Hint: The symmetric groups
should not be confused with "symmetry groups" which is a different topic in
group theory.
| ||
Syntax | csymg 17797 | Extend class notation to include the class of symmetric groups. |
Definition | df-symg 17798* | Define the symmetric group on set . We represent the group as the set of one-to-one onto functions from to itself under function composition, and topologize it as a function space assuming the set is discrete. (Contributed by Paul Chapman, 25-Feb-2008.) |
TopSet | ||
Theorem | symgval 17799* | The value of the symmetric group function at . (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 12-Jan-2015.) |
TopSet | ||
Theorem | symgbas 17800* | The base set of the symmetric group. (Contributed by Mario Carneiro, 12-Jan-2015.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |