![]() |
Metamath
Proof Explorer Theorem List (p. 194 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | oppgid 19301 | Zero in a monoid is a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 16-Sep-2015.) |
β’ π = (oppgβπ ) & β’ 0 = (0gβπ ) β β’ 0 = (0gβπ) | ||
Theorem | oppggrp 19302 | The opposite of a group is a group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ π = (oppgβπ ) β β’ (π β Grp β π β Grp) | ||
Theorem | oppggrpb 19303 | Bidirectional form of oppggrp 19302. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ π = (oppgβπ ) β β’ (π β Grp β π β Grp) | ||
Theorem | oppginv 19304 | Inverses in a group are a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ π = (oppgβπ ) & β’ πΌ = (invgβπ ) β β’ (π β Grp β πΌ = (invgβπ)) | ||
Theorem | invoppggim 19305 | The inverse is an antiautomorphism on any group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ π = (oppgβπΊ) & β’ πΌ = (invgβπΊ) β β’ (πΊ β Grp β πΌ β (πΊ GrpIso π)) | ||
Theorem | oppggic 19306 | Every group is (naturally) isomorphic to its opposite. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
β’ π = (oppgβπΊ) β β’ (πΊ β Grp β πΊ βπ π) | ||
Theorem | oppgsubm 19307 | Being a submonoid is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π = (oppgβπΊ) β β’ (SubMndβπΊ) = (SubMndβπ) | ||
Theorem | oppgsubg 19308 | Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π = (oppgβπΊ) β β’ (SubGrpβπΊ) = (SubGrpβπ) | ||
Theorem | oppgcntz 19309 | 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 19310 | 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 19311 | 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.) |
β’ π΅ = (Baseβπ) & β’ π = (oppgβπ) β β’ ((π β Mnd β§ π β 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 19313. However, the
set is allowed to be empty, see symgbas0 19334. Hint: The symmetric groups
should not be confused with "symmetry groups" which is a different topic in
group theory.
| ||
Syntax | csymg 19312 | Extend class notation to include the class of symmetric groups. |
class SymGrp | ||
Definition | df-symg 19313* | 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. This definition is based on the fact that a symmetric group is a restriction of the monoid of endofunctions. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by AV, 28-Mar-2024.) |
β’ SymGrp = (π₯ β V β¦ ((EndoFMndβπ₯) βΎs {β β£ β:π₯β1-1-ontoβπ₯})) | ||
Theorem | symgval 19314* | The value of the symmetric group function at π΄. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 28-Mar-2024.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = {π₯ β£ π₯:π΄β1-1-ontoβπ΄} β β’ πΊ = ((EndoFMndβπ΄) βΎs π΅) | ||
Theorem | permsetexOLD 19315* | Obsolete version of f1osetex 8869 as of 8-Aug-2024. (Contributed by AV, 30-Mar-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π΄ β π β {π β£ π:π΄β1-1-ontoβπ΄} β V) | ||
Theorem | symgbas 19316* | The base set of the symmetric group. (Contributed by Mario Carneiro, 12-Jan-2015.) (Proof shortened by AV, 29-Mar-2024.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ π΅ = {π₯ β£ π₯:π΄β1-1-ontoβπ΄} | ||
Theorem | symgbasexOLD 19317 | Obsolete as of 8-Aug-2024. π΅ β V follows immediatly from fvex 6904. (Contributed by AV, 30-Mar-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β π΅ β V) | ||
Theorem | elsymgbas2 19318 | Two ways of saying a function is a 1-1-onto mapping of A to itself. (Contributed by Mario Carneiro, 28-Jan-2015.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (πΉ β π β (πΉ β π΅ β πΉ:π΄β1-1-ontoβπ΄)) | ||
Theorem | elsymgbas 19319 | Two ways of saying a function is a 1-1-onto mapping of A to itself. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 28-Jan-2015.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β (πΉ β π΅ β πΉ:π΄β1-1-ontoβπ΄)) | ||
Theorem | symgbasf1o 19320 | Elements in the symmetric group are 1-1 onto functions. (Contributed by SO, 9-Jul-2018.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (πΉ β π΅ β πΉ:π΄β1-1-ontoβπ΄) | ||
Theorem | symgbasf 19321 | A permutation (element of the symmetric group) is a function from a set into itself. (Contributed by AV, 1-Jan-2019.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (πΉ β π΅ β πΉ:π΄βΆπ΄) | ||
Theorem | symgbasmap 19322 | A permutation (element of the symmetric group) is a mapping (or set exponentiation) from a set into itself. (Contributed by AV, 30-Mar-2024.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (πΉ β π΅ β πΉ β (π΄ βm π΄)) | ||
Theorem | symghash 19323 | The symmetric group on π objects has cardinality π!. (Contributed by Mario Carneiro, 22-Jan-2015.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β Fin β (β―βπ΅) = (!β(β―βπ΄))) | ||
Theorem | symgbasfi 19324 | The symmetric group on a finite index set is finite. (Contributed by SO, 9-Jul-2018.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β Fin β π΅ β Fin) | ||
Theorem | symgfv 19325 | The function value of a permutation. (Contributed by AV, 1-Jan-2019.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ ((πΉ β π΅ β§ π β π΄) β (πΉβπ) β π΄) | ||
Theorem | symgfvne 19326 | The function values of a permutation for different arguments are different. (Contributed by AV, 8-Jan-2019.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ ((πΉ β π΅ β§ π β π΄ β§ π β π΄) β ((πΉβπ) = π β (π β π β (πΉβπ) β π))) | ||
Theorem | symgressbas 19327 | The symmetric group on π΄ characterized as structure restriction of the monoid of endofunctions on π΄ to its base set. (Contributed by AV, 30-Mar-2024.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π = (EndoFMndβπ΄) β β’ πΊ = (π βΎs π΅) | ||
Theorem | symgplusg 19328* | The group operation of a symmetric group is the function composition. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 28-Jan-2015.) (Proof shortened by AV, 19-Feb-2024.) (Revised by AV, 29-Mar-2024.) (Proof shortened by AV, 14-Aug-2024.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (π΄ βm π΄) & β’ + = (+gβπΊ) β β’ + = (π β π΅, π β π΅ β¦ (π β π)) | ||
Theorem | symgov 19329 | The value of the group operation of the symmetric group on π΄. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 28-Jan-2015.) (Revised by AV, 30-Mar-2024.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((π β π΅ β§ π β π΅) β (π + π) = (π β π)) | ||
Theorem | symgcl 19330 | The group operation of the symmetric group on π΄ is closed, i.e. a magma. (Contributed by Mario Carneiro, 12-Jan-2015.) (Revised by Mario Carneiro, 28-Jan-2015.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((π β π΅ β§ π β π΅) β (π + π) β π΅) | ||
Theorem | idresperm 19331 | The identity function restricted to a set is a permutation of this set. (Contributed by AV, 17-Mar-2019.) |
β’ πΊ = (SymGrpβπ΄) β β’ (π΄ β π β ( I βΎ π΄) β (BaseβπΊ)) | ||
Theorem | symgmov1 19332* | For a permutation of a set, each element of the set replaces an(other) element of the set. (Contributed by AV, 2-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) β β’ (π β π β βπ β π βπ β π (πβπ) = π) | ||
Theorem | symgmov2 19333* | For a permutation of a set, each element of the set is replaced by an(other) element of the set. (Contributed by AV, 2-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) β β’ (π β π β βπ β π βπ β π (πβπ) = π) | ||
Theorem | symgbas0 19334 | The base set of the symmetric group on the empty set is the singleton containing the empty set. (Contributed by AV, 27-Feb-2019.) |
β’ (Baseβ(SymGrpββ )) = {β } | ||
Theorem | symg1hash 19335 | The symmetric group on a singleton has cardinality 1. (Contributed by AV, 9-Dec-2018.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ} β β’ (πΌ β π β (β―βπ΅) = 1) | ||
Theorem | symg1bas 19336 | The symmetric group on a singleton is the symmetric group S1 consisting of the identity only. (Contributed by AV, 9-Dec-2018.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ} β β’ (πΌ β π β π΅ = {{β¨πΌ, πΌβ©}}) | ||
Theorem | symg2hash 19337 | The symmetric group on a (proper) pair has cardinality 2. (Contributed by AV, 9-Dec-2018.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ, π½} β β’ ((πΌ β π β§ π½ β π β§ πΌ β π½) β (β―βπ΅) = 2) | ||
Theorem | symg2bas 19338 | The symmetric group on a pair is the symmetric group S2 consisting of the identity and the transposition. Notice that this statement is valid for proper pairs only. In the case that both elements are identical, i.e., the pairs are actually singletons, this theorem would be about S1, see Theorem symg1bas 19336. (Contributed by AV, 9-Dec-2018.) (Proof shortened by AV, 16-Jun-2022.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ, π½} β β’ ((πΌ β π β§ π½ β π) β π΅ = {{β¨πΌ, πΌβ©, β¨π½, π½β©}, {β¨πΌ, π½β©, β¨π½, πΌβ©}}) | ||
Theorem | 0symgefmndeq 19339 | The symmetric group on the empty set is identical with the monoid of endofunctions on the empty set. (Contributed by AV, 30-Mar-2024.) |
β’ (EndoFMndββ ) = (SymGrpββ ) | ||
Theorem | snsymgefmndeq 19340 | The symmetric group on a singleton π΄ is identical with the monoid of endofunctions on π΄. (Contributed by AV, 31-Mar-2024.) |
β’ (π΄ = {π} β (EndoFMndβπ΄) = (SymGrpβπ΄)) | ||
Theorem | symgpssefmnd 19341 | For a set π΄ with more than one element, the symmetric group on π΄ is a proper subset of the monoid of endofunctions on π΄. (Contributed by AV, 31-Mar-2024.) |
β’ π = (EndoFMndβπ΄) & β’ πΊ = (SymGrpβπ΄) β β’ ((π΄ β π β§ 1 < (β―βπ΄)) β (BaseβπΊ) β (Baseβπ)) | ||
Theorem | symgvalstruct 19342* | The value of the symmetric group function at π΄ represented as extensible structure with three slots. This corresponds to the former definition of SymGrp. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 31-Mar-2024.) (Proof shortened by AV, 6-Nov-2024.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = {π₯ β£ π₯:π΄β1-1-ontoβπ΄} & β’ π = (π΄ βm π΄) & β’ + = (π β π, π β π β¦ (π β π)) & β’ π½ = (βtβ(π΄ Γ {π« π΄})) β β’ (π΄ β π β πΊ = {β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(TopSetβndx), π½β©}) | ||
Theorem | symgvalstructOLD 19343* | Obsolete proof of symgvalstruct 19342 as of 6-Nov-2024. The value of the symmetric group function at π΄ represented as extensible structure with three slots. This corresponds to the former definition of SymGrp. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 31-Mar-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = {π₯ β£ π₯:π΄β1-1-ontoβπ΄} & β’ π = (π΄ βm π΄) & β’ + = (π β π, π β π β¦ (π β π)) & β’ π½ = (βtβ(π΄ Γ {π« π΄})) β β’ (π΄ β π β πΊ = {β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(TopSetβndx), π½β©}) | ||
Theorem | symgsubmefmnd 19344 | The symmetric group on a set π΄ is a submonoid of the monoid of endofunctions on π΄. (Contributed by AV, 18-Feb-2024.) |
β’ π = (EndoFMndβπ΄) & β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β π΅ β (SubMndβπ)) | ||
Theorem | symgtset 19345 | The topology of the symmetric group on π΄. This component is defined on a larger set than the true base - the product topology is defined on the set of all functions, not just bijections - but the definition of TopOpen ensures that it is trimmed down before it gets use. (Contributed by Mario Carneiro, 29-Aug-2015.) (Proof revised by AV, 30-Mar-2024.) |
β’ πΊ = (SymGrpβπ΄) β β’ (π΄ β π β (βtβ(π΄ Γ {π« π΄})) = (TopSetβπΊ)) | ||
Theorem | symggrp 19346 | The symmetric group on a set π΄ is a group. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) (Proof shortened by AV, 28-Jan-2024.) |
β’ πΊ = (SymGrpβπ΄) β β’ (π΄ β π β πΊ β Grp) | ||
Theorem | symgid 19347 | The group identity element of the symmetric group on a set π΄. (Contributed by Paul Chapman, 25-Jul-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) (Proof shortened by AV, 1-Apr-2024.) |
β’ πΊ = (SymGrpβπ΄) β β’ (π΄ β π β ( I βΎ π΄) = (0gβπΊ)) | ||
Theorem | symginv 19348 | The group inverse in the symmetric group corresponds to the functional inverse. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by Mario Carneiro, 2-Sep-2015.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π = (invgβπΊ) β β’ (πΉ β π΅ β (πβπΉ) = β‘πΉ) | ||
Theorem | symgsubmefmndALT 19349 | The symmetric group on a set π΄ is a submonoid of the monoid of endofunctions on π΄. Alternate proof based on issubmndb 18748 and not on injsubmefmnd 18840 and sursubmefmnd 18839. (Contributed by AV, 18-Feb-2024.) (Revised by AV, 30-Mar-2024.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (EndoFMndβπ΄) & β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β π΅ β (SubMndβπ)) | ||
Theorem | galactghm 19350* | The currying of a group action is a group homomorphism between the group πΊ and the symmetric group (SymGrpβπ). (Contributed by FL, 17-May-2010.) (Proof shortened by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ π» = (SymGrpβπ) & β’ πΉ = (π₯ β π β¦ (π¦ β π β¦ (π₯ β π¦))) β β’ ( β β (πΊ GrpAct π) β πΉ β (πΊ GrpHom π»)) | ||
Theorem | lactghmga 19351* | The converse of galactghm 19350. The uncurrying of a homomorphism into (SymGrpβπ) is a group action. Thus, group actions and group homomorphisms into a symmetric group are essentially equivalent notions. (Contributed by Mario Carneiro, 15-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ π» = (SymGrpβπ) & β’ β = (π₯ β π, π¦ β π β¦ ((πΉβπ₯)βπ¦)) β β’ (πΉ β (πΊ GrpHom π») β β β (πΊ GrpAct π)) | ||
Theorem | symgtopn 19352 | The topology of the symmetric group on π΄. (Contributed by Mario Carneiro, 29-Aug-2015.) |
β’ πΊ = (SymGrpβπ) & β’ π΅ = (BaseβπΊ) β β’ (π β π β ((βtβ(π Γ {π« π})) βΎt π΅) = (TopOpenβπΊ)) | ||
Theorem | symgga 19353* | The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015.) |
β’ πΊ = (SymGrpβπ) & β’ π΅ = (BaseβπΊ) & β’ πΉ = (π β π΅, π₯ β π β¦ (πβπ₯)) β β’ (π β π β πΉ β (πΊ GrpAct π)) | ||
Theorem | pgrpsubgsymgbi 19354 | Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β (π β (SubGrpβπΊ) β (π β π΅ β§ (πΊ βΎs π) β Grp))) | ||
Theorem | pgrpsubgsymg 19355* | Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.) (Revised by AV, 30-Mar-2024.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ πΉ = (Baseβπ) β β’ (π΄ β π β ((π β Grp β§ πΉ β π΅ β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π))) β πΉ β (SubGrpβπΊ))) | ||
Theorem | idressubgsymg 19356 | The singleton containing only the identity function restricted to a set is a subgroup of the symmetric group of this set. (Contributed by AV, 17-Mar-2019.) |
β’ πΊ = (SymGrpβπ΄) β β’ (π΄ β π β {( I βΎ π΄)} β (SubGrpβπΊ)) | ||
Theorem | idrespermg 19357 | The structure with the singleton containing only the identity function restricted to a set as base set and the function composition as group operation (constructed by (structure) restricting the symmetric group to that singleton) is a permutation group (group consisting of permutations). (Contributed by AV, 17-Mar-2019.) |
β’ πΊ = (SymGrpβπ΄) & β’ πΈ = (πΊ βΎs {( I βΎ π΄)}) β β’ (π΄ β π β (πΈ β Grp β§ (BaseβπΈ) β (BaseβπΊ))) | ||
Theorem | cayleylem1 19358* | Lemma for cayley 19360. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) & β’ π» = (SymGrpβπ) & β’ π = (Baseβπ») & β’ πΉ = (π β π β¦ (π β π β¦ (π + π))) β β’ (πΊ β Grp β πΉ β (πΊ GrpHom π»)) | ||
Theorem | cayleylem2 19359* | Lemma for cayley 19360. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) & β’ π» = (SymGrpβπ) & β’ π = (Baseβπ») & β’ πΉ = (π β π β¦ (π β π β¦ (π + π))) β β’ (πΊ β Grp β πΉ:πβ1-1βπ) | ||
Theorem | cayley 19360* | Cayley's Theorem (constructive version): given group πΊ, πΉ is an isomorphism between πΊ and the subgroup π of the symmetric group π» on the underlying set π of πΊ. See also Theorem 3.15 in [Rotman] p. 42. (Contributed by Paul Chapman, 3-Mar-2008.) (Proof shortened by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ π» = (SymGrpβπ) & β’ + = (+gβπΊ) & β’ πΉ = (π β π β¦ (π β π β¦ (π + π))) & β’ π = ran πΉ β β’ (πΊ β Grp β (π β (SubGrpβπ») β§ πΉ β (πΊ GrpHom (π» βΎs π)) β§ πΉ:πβ1-1-ontoβπ)) | ||
Theorem | cayleyth 19361* | Cayley's Theorem (existence version): every group πΊ is isomorphic to a subgroup of the symmetric group on the underlying set of πΊ. (For any group πΊ there exists an isomorphism π between πΊ and a subgroup β of the symmetric group on the underlying set of πΊ.) See also Theorem 3.15 in [Rotman] p. 42. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ π» = (SymGrpβπ) β β’ (πΊ β Grp β βπ β (SubGrpβπ»)βπ β (πΊ GrpHom (π» βΎs π ))π:πβ1-1-ontoβπ ) | ||
Theorem | symgfix2 19362* | If a permutation does not move a certain element of a set to a second element, there is a third element which is moved to the second element. (Contributed by AV, 2-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) β β’ (πΏ β π β (π β (π β {π β π β£ (πβπΎ) = πΏ}) β βπ β (π β {πΎ})(πβπ) = πΏ)) | ||
Theorem | symgextf 19363* | The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019.) |
β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((πΎ β π β§ π β π) β πΈ:πβΆπ) | ||
Theorem | symgextfv 19364* | The function value of the extension of a permutation, fixing the additional element, for elements in the original domain. (Contributed by AV, 6-Jan-2019.) |
β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((πΎ β π β§ π β π) β (π β (π β {πΎ}) β (πΈβπ) = (πβπ))) | ||
Theorem | symgextfve 19365* | The function value of the extension of a permutation, fixing the additional element, for the additional element. (Contributed by AV, 6-Jan-2019.) |
β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ (πΎ β π β (π = πΎ β (πΈβπ) = πΎ)) | ||
Theorem | symgextf1lem 19366* | Lemma for symgextf1 19367. (Contributed by AV, 6-Jan-2019.) |
β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((πΎ β π β§ π β π) β ((π β (π β {πΎ}) β§ π β {πΎ}) β (πΈβπ) β (πΈβπ))) | ||
Theorem | symgextf1 19367* | The extension of a permutation, fixing the additional element, is a 1-1 function. (Contributed by AV, 6-Jan-2019.) |
β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((πΎ β π β§ π β π) β πΈ:πβ1-1βπ) | ||
Theorem | symgextfo 19368* | The extension of a permutation, fixing the additional element, is an onto function. (Contributed by AV, 7-Jan-2019.) |
β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((πΎ β π β§ π β π) β πΈ:πβontoβπ) | ||
Theorem | symgextf1o 19369* | The extension of a permutation, fixing the additional element, is a bijection. (Contributed by AV, 7-Jan-2019.) |
β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((πΎ β π β§ π β π) β πΈ:πβ1-1-ontoβπ) | ||
Theorem | symgextsymg 19370* | The extension of a permutation is an element of the extended symmetric group. (Contributed by AV, 9-Mar-2019.) |
β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((π β π β§ πΎ β π β§ π β π) β πΈ β (Baseβ(SymGrpβπ))) | ||
Theorem | symgextres 19371* | The restriction of the extension of a permutation, fixing the additional element, to the original domain. (Contributed by AV, 6-Jan-2019.) |
β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((πΎ β π β§ π β π) β (πΈ βΎ (π β {πΎ})) = π) | ||
Theorem | gsumccatsymgsn 19372 | Homomorphic property of composites of permutations with a singleton. (Contributed by AV, 20-Jan-2019.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ ((π΄ β π β§ π β Word π΅ β§ π β π΅) β (πΊ Ξ£g (π ++ β¨βπββ©)) = ((πΊ Ξ£g π) β π)) | ||
Theorem | gsmsymgrfixlem1 19373* | Lemma 1 for gsmsymgrfix 19374. (Contributed by AV, 20-Jan-2019.) |
β’ π = (SymGrpβπ) & β’ π΅ = (Baseβπ) β β’ (((π β Word π΅ β§ π β π΅) β§ (π β Fin β§ πΎ β π) β§ (βπ β (0..^(β―βπ))((πβπ)βπΎ) = πΎ β ((π Ξ£g π)βπΎ) = πΎ)) β (βπ β (0..^((β―βπ) + 1))(((π ++ β¨βπββ©)βπ)βπΎ) = πΎ β ((π Ξ£g (π ++ β¨βπββ©))βπΎ) = πΎ)) | ||
Theorem | gsmsymgrfix 19374* | The composition of permutations fixing one element also fixes this element. (Contributed by AV, 20-Jan-2019.) |
β’ π = (SymGrpβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Fin β§ πΎ β π β§ π β Word π΅) β (βπ β (0..^(β―βπ))((πβπ)βπΎ) = πΎ β ((π Ξ£g π)βπΎ) = πΎ)) | ||
Theorem | fvcosymgeq 19375* | The values of two compositions of permutations are equal if the values of the composed permutations are pairwise equal. (Contributed by AV, 26-Jan-2019.) |
β’ π = (SymGrpβπ) & β’ π΅ = (Baseβπ) & β’ π = (SymGrpβπ) & β’ π = (Baseβπ) & β’ πΌ = (π β© π) β β’ ((πΊ β π΅ β§ πΎ β π) β ((π β πΌ β§ (πΊβπ) = (πΎβπ) β§ βπ β πΌ (πΉβπ) = (π»βπ)) β ((πΉ β πΊ)βπ) = ((π» β πΎ)βπ))) | ||
Theorem | gsmsymgreqlem1 19376* | Lemma 1 for gsmsymgreq 19378. (Contributed by AV, 26-Jan-2019.) |
β’ π = (SymGrpβπ) & β’ π΅ = (Baseβπ) & β’ π = (SymGrpβπ) & β’ π = (Baseβπ) & β’ πΌ = (π β© π) β β’ (((π β Fin β§ π β Fin β§ π½ β πΌ) β§ ((π β Word π΅ β§ πΆ β π΅) β§ (π β Word π β§ π β π) β§ (β―βπ) = (β―βπ))) β ((βπ β πΌ ((π Ξ£g π)βπ) = ((π Ξ£g π)βπ) β§ (πΆβπ½) = (π βπ½)) β ((π Ξ£g (π ++ β¨βπΆββ©))βπ½) = ((π Ξ£g (π ++ β¨βπ ββ©))βπ½))) | ||
Theorem | gsmsymgreqlem2 19377* | Lemma 2 for gsmsymgreq 19378. (Contributed by AV, 26-Jan-2019.) |
β’ π = (SymGrpβπ) & β’ π΅ = (Baseβπ) & β’ π = (SymGrpβπ) & β’ π = (Baseβπ) & β’ πΌ = (π β© π) β β’ (((π β Fin β§ π β Fin) β§ ((π β Word π΅ β§ πΆ β π΅) β§ (π β Word π β§ π β π) β§ (β―βπ) = (β―βπ))) β ((βπ β (0..^(β―βπ))βπ β πΌ ((πβπ)βπ) = ((πβπ)βπ) β βπ β πΌ ((π Ξ£g π)βπ) = ((π Ξ£g π)βπ)) β (βπ β (0..^(β―β(π ++ β¨βπΆββ©)))βπ β πΌ (((π ++ β¨βπΆββ©)βπ)βπ) = (((π ++ β¨βπ ββ©)βπ)βπ) β βπ β πΌ ((π Ξ£g (π ++ β¨βπΆββ©))βπ) = ((π Ξ£g (π ++ β¨βπ ββ©))βπ)))) | ||
Theorem | gsmsymgreq 19378* | Two combination of permutations moves an element of the intersection of the base sets of the permutations to the same element if each pair of corresponding permutations moves such an element to the same element. (Contributed by AV, 20-Jan-2019.) |
β’ π = (SymGrpβπ) & β’ π΅ = (Baseβπ) & β’ π = (SymGrpβπ) & β’ π = (Baseβπ) & β’ πΌ = (π β© π) β β’ (((π β Fin β§ π β Fin) β§ (π β Word π΅ β§ π β Word π β§ (β―βπ) = (β―βπ))) β (βπ β (0..^(β―βπ))βπ β πΌ ((πβπ)βπ) = ((πβπ)βπ) β βπ β πΌ ((π Ξ£g π)βπ) = ((π Ξ£g π)βπ))) | ||
Theorem | symgfixelq 19379* | A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = {π β π β£ (πβπΎ) = πΎ} β β’ (πΉ β π β (πΉ β π β (πΉ:πβ1-1-ontoβπ β§ (πΉβπΎ) = πΎ))) | ||
Theorem | symgfixels 19380* | The restriction of a permutation to a set with one element removed is an element of the restricted symmetric group if the restriction is a 1-1 onto function. (Contributed by AV, 4-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = {π β π β£ (πβπΎ) = πΎ} & β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ π· = (π β {πΎ}) β β’ (πΉ β π β ((πΉ βΎ π·) β π β (πΉ βΎ π·):π·β1-1-ontoβπ·)) | ||
Theorem | symgfixelsi 19381* | The restriction of a permutation fixing an element to the set with this element removed is an element of the restricted symmetric group. (Contributed by AV, 4-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = {π β π β£ (πβπΎ) = πΎ} & β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ π· = (π β {πΎ}) β β’ ((πΎ β π β§ πΉ β π) β (πΉ βΎ π·) β π) | ||
Theorem | symgfixf 19382* | The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a function. (Contributed by AV, 4-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = {π β π β£ (πβπΎ) = πΎ} & β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ π» = (π β π β¦ (π βΎ (π β {πΎ}))) β β’ (πΎ β π β π»:πβΆπ) | ||
Theorem | symgfixf1 19383* | The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a 1-1 function. (Contributed by AV, 4-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = {π β π β£ (πβπΎ) = πΎ} & β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ π» = (π β π β¦ (π βΎ (π β {πΎ}))) β β’ (πΎ β π β π»:πβ1-1βπ) | ||
Theorem | symgfixfolem1 19384* | Lemma 1 for symgfixfo 19385. (Contributed by AV, 7-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = {π β π β£ (πβπΎ) = πΎ} & β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ π» = (π β π β¦ (π βΎ (π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((π β π β§ πΎ β π β§ π β π) β πΈ β π) | ||
Theorem | symgfixfo 19385* | The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is an onto function. (Contributed by AV, 7-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = {π β π β£ (πβπΎ) = πΎ} & β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ π» = (π β π β¦ (π βΎ (π β {πΎ}))) β β’ ((π β π β§ πΎ β π) β π»:πβontoβπ) | ||
Theorem | symgfixf1o 19386* | The mapping of a permutation of a set fixing an element to a permutation of the set without the fixed element is a bijection. (Contributed by AV, 7-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = {π β π β£ (πβπΎ) = πΎ} & β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ π» = (π β π β¦ (π βΎ (π β {πΎ}))) β β’ ((π β π β§ πΎ β π) β π»:πβ1-1-ontoβπ) | ||
Transpositions are special cases of "cycles" as defined in [Rotman] p. 28: "Let
i1 , i2 , ... , ir be distinct integers
between 1 and n. If Ξ± in Sn fixes the other integers and
Ξ±(i1) = i2, Ξ±(i2) = i3,
..., Ξ±(ir-1 ) = ir, Ξ±(ir) =
i1, then Ξ± is an r-cycle. We also say that Ξ± is a
cycle of length r." and in [Rotman] p. 31: "A 2-cycle is also called
transposition.".
| ||
Syntax | cpmtr 19387 | Syntax for the transposition generator function. |
class pmTrsp | ||
Definition | df-pmtr 19388* | Define a function that generates the transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ pmTrsp = (π β V β¦ (π β {π¦ β π« π β£ π¦ β 2o} β¦ (π§ β π β¦ if(π§ β π, βͺ (π β {π§}), π§)))) | ||
Theorem | f1omvdmvd 19389 | A permutation of any class moves a point which is moved to a different point which is moved. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ ((πΉ:π΄β1-1-ontoβπ΄ β§ π β dom (πΉ β I )) β (πΉβπ) β (dom (πΉ β I ) β {π})) | ||
Theorem | f1omvdcnv 19390 | A permutation and its inverse move the same points. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ (πΉ:π΄β1-1-ontoβπ΄ β dom (β‘πΉ β I ) = dom (πΉ β I )) | ||
Theorem | mvdco 19391 | Composing two permutations moves at most the union of the points. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ dom ((πΉ β πΊ) β I ) β (dom (πΉ β I ) βͺ dom (πΊ β I )) | ||
Theorem | f1omvdconj 19392 | Conjugation of a permutation takes the image of the moved subclass. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ ((πΉ:π΄βΆπ΄ β§ πΊ:π΄β1-1-ontoβπ΄) β dom (((πΊ β πΉ) β β‘πΊ) β I ) = (πΊ β dom (πΉ β I ))) | ||
Theorem | f1otrspeq 19393 | A transposition is characterized by the points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ (((πΉ:π΄β1-1-ontoβπ΄ β§ πΊ:π΄β1-1-ontoβπ΄) β§ (dom (πΉ β I ) β 2o β§ dom (πΊ β I ) = dom (πΉ β I ))) β πΉ = πΊ) | ||
Theorem | f1omvdco2 19394 | If exactly one of two permutations is limited to a set of points, then the composition will not be. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
β’ ((πΉ:π΄β1-1-ontoβπ΄ β§ πΊ:π΄β1-1-ontoβπ΄ β§ (dom (πΉ β I ) β π β» dom (πΊ β I ) β π)) β Β¬ dom ((πΉ β πΊ) β I ) β π) | ||
Theorem | f1omvdco3 19395 | If a point is moved by exactly one of two permutations, then it will be moved by their composite. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
β’ ((πΉ:π΄β1-1-ontoβπ΄ β§ πΊ:π΄β1-1-ontoβπ΄ β§ (π β dom (πΉ β I ) β» π β dom (πΊ β I ))) β π β dom ((πΉ β πΊ) β I )) | ||
Theorem | pmtrfval 19396* | The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ (π· β π β π = (π β {π¦ β π« π· β£ π¦ β 2o} β¦ (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§)))) | ||
Theorem | pmtrval 19397* | A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ π β π· β§ π β 2o) β (πβπ) = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) | ||
Theorem | pmtrfv 19398 | General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ (((π· β π β§ π β π· β§ π β 2o) β§ π β π·) β ((πβπ)βπ) = if(π β π, βͺ (π β {π}), π)) | ||
Theorem | pmtrprfv 19399 | In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ (π β π· β§ π β π· β§ π β π)) β ((πβ{π, π})βπ) = π) | ||
Theorem | pmtrprfv3 19400 | In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ (π β π· β§ π β π· β§ π β π·) β§ (π β π β§ π β π β§ π β π)) β ((πβ{π, π})βπ) = π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |