Home | Metamath
Proof Explorer Theorem List (p. 192 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | symgmov2 19101* | 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 19102 | 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 19103 | The symmetric group on a singleton has cardinality 1. (Contributed by AV, 9-Dec-2018.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ} β β’ (πΌ β π β (β―βπ΅) = 1) | ||
Theorem | symg1bas 19104 | 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 19105 | The symmetric group on a (proper) pair has cardinality 2. (Contributed by AV, 9-Dec-2018.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ, π½} β β’ ((πΌ β π β§ π½ β π β§ πΌ β π½) β (β―βπ΅) = 2) | ||
Theorem | symg2bas 19106 | 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 19104. (Contributed by AV, 9-Dec-2018.) (Proof shortened by AV, 16-Jun-2022.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ, π½} β β’ ((πΌ β π β§ π½ β π) β π΅ = {{β¨πΌ, πΌβ©, β¨π½, π½β©}, {β¨πΌ, π½β©, β¨π½, πΌβ©}}) | ||
Theorem | 0symgefmndeq 19107 | 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 19108 | The symmetric group on a singleton π΄ is identical with the monoid of endofunctions on π΄. (Contributed by AV, 31-Mar-2024.) |
β’ (π΄ = {π} β (EndoFMndβπ΄) = (SymGrpβπ΄)) | ||
Theorem | symgpssefmnd 19109 | 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 19110* | 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 19111* | Obsolete proof of symgvalstruct 19110 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 19112 | 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 19113 | 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 19114 | 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 19115 | 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 19116 | 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 19117 | The symmetric group on a set π΄ is a submonoid of the monoid of endofunctions on π΄. Alternate proof based on issubmndb 18551 and not on injsubmefmnd 18642 and sursubmefmnd 18641. (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 19118* | 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 19119* | The converse of galactghm 19118. 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 19120 | The topology of the symmetric group on π΄. (Contributed by Mario Carneiro, 29-Aug-2015.) |
β’ πΊ = (SymGrpβπ) & β’ π΅ = (BaseβπΊ) β β’ (π β π β ((βtβ(π Γ {π« π})) βΎt π΅) = (TopOpenβπΊ)) | ||
Theorem | symgga 19121* | The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015.) |
β’ πΊ = (SymGrpβπ) & β’ π΅ = (BaseβπΊ) & β’ πΉ = (π β π΅, π₯ β π β¦ (πβπ₯)) β β’ (π β π β πΉ β (πΊ GrpAct π)) | ||
Theorem | pgrpsubgsymgbi 19122 | Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β (π β (SubGrpβπΊ) β (π β π΅ β§ (πΊ βΎs π) β Grp))) | ||
Theorem | pgrpsubgsymg 19123* | 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 19124 | 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 19125 | 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 19126* | Lemma for cayley 19128. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) & β’ π» = (SymGrpβπ) & β’ π = (Baseβπ») & β’ πΉ = (π β π β¦ (π β π β¦ (π + π))) β β’ (πΊ β Grp β πΉ β (πΊ GrpHom π»)) | ||
Theorem | cayleylem2 19127* | Lemma for cayley 19128. (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 19128* | 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 19129* | 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 19130* | 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 19131* | The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019.) |
β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((πΎ β π β§ π β π) β πΈ:πβΆπ) | ||
Theorem | symgextfv 19132* | 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 19133* | 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 19134* | Lemma for symgextf1 19135. (Contributed by AV, 6-Jan-2019.) |
β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((πΎ β π β§ π β π) β ((π β (π β {πΎ}) β§ π β {πΎ}) β (πΈβπ) β (πΈβπ))) | ||
Theorem | symgextf1 19135* | 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 19136* | 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 19137* | 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 19138* | 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 19139* | 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 19140 | Homomorphic property of composites of permutations with a singleton. (Contributed by AV, 20-Jan-2019.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ ((π΄ β π β§ π β Word π΅ β§ π β π΅) β (πΊ Ξ£g (π ++ β¨βπββ©)) = ((πΊ Ξ£g π) β π)) | ||
Theorem | gsmsymgrfixlem1 19141* | Lemma 1 for gsmsymgrfix 19142. (Contributed by AV, 20-Jan-2019.) |
β’ π = (SymGrpβπ) & β’ π΅ = (Baseβπ) β β’ (((π β Word π΅ β§ π β π΅) β§ (π β Fin β§ πΎ β π) β§ (βπ β (0..^(β―βπ))((πβπ)βπΎ) = πΎ β ((π Ξ£g π)βπΎ) = πΎ)) β (βπ β (0..^((β―βπ) + 1))(((π ++ β¨βπββ©)βπ)βπΎ) = πΎ β ((π Ξ£g (π ++ β¨βπββ©))βπΎ) = πΎ)) | ||
Theorem | gsmsymgrfix 19142* | 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 19143* | 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 19144* | Lemma 1 for gsmsymgreq 19146. (Contributed by AV, 26-Jan-2019.) |
β’ π = (SymGrpβπ) & β’ π΅ = (Baseβπ) & β’ π = (SymGrpβπ) & β’ π = (Baseβπ) & β’ πΌ = (π β© π) β β’ (((π β Fin β§ π β Fin β§ π½ β πΌ) β§ ((π β Word π΅ β§ πΆ β π΅) β§ (π β Word π β§ π β π) β§ (β―βπ) = (β―βπ))) β ((βπ β πΌ ((π Ξ£g π)βπ) = ((π Ξ£g π)βπ) β§ (πΆβπ½) = (π βπ½)) β ((π Ξ£g (π ++ β¨βπΆββ©))βπ½) = ((π Ξ£g (π ++ β¨βπ ββ©))βπ½))) | ||
Theorem | gsmsymgreqlem2 19145* | Lemma 2 for gsmsymgreq 19146. (Contributed by AV, 26-Jan-2019.) |
β’ π = (SymGrpβπ) & β’ π΅ = (Baseβπ) & β’ π = (SymGrpβπ) & β’ π = (Baseβπ) & β’ πΌ = (π β© π) β β’ (((π β Fin β§ π β Fin) β§ ((π β Word π΅ β§ πΆ β π΅) β§ (π β Word π β§ π β π) β§ (β―βπ) = (β―βπ))) β ((βπ β (0..^(β―βπ))βπ β πΌ ((πβπ)βπ) = ((πβπ)βπ) β βπ β πΌ ((π Ξ£g π)βπ) = ((π Ξ£g π)βπ)) β (βπ β (0..^(β―β(π ++ β¨βπΆββ©)))βπ β πΌ (((π ++ β¨βπΆββ©)βπ)βπ) = (((π ++ β¨βπ ββ©)βπ)βπ) β βπ β πΌ ((π Ξ£g (π ++ β¨βπΆββ©))βπ) = ((π Ξ£g (π ++ β¨βπ ββ©))βπ)))) | ||
Theorem | gsmsymgreq 19146* | 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 19147* | A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = {π β π β£ (πβπΎ) = πΎ} β β’ (πΉ β π β (πΉ β π β (πΉ:πβ1-1-ontoβπ β§ (πΉβπΎ) = πΎ))) | ||
Theorem | symgfixels 19148* | 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 19149* | 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 19150* | 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 19151* | 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 19152* | Lemma 1 for symgfixfo 19153. (Contributed by AV, 7-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = {π β π β£ (πβπΎ) = πΎ} & β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ π» = (π β π β¦ (π βΎ (π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((π β π β§ πΎ β π β§ π β π) β πΈ β π) | ||
Theorem | symgfixfo 19153* | 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 19154* | 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 19155 | Syntax for the transposition generator function. |
class pmTrsp | ||
Definition | df-pmtr 19156* | Define a function that generates the transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ pmTrsp = (π β V β¦ (π β {π¦ β π« π β£ π¦ β 2o} β¦ (π§ β π β¦ if(π§ β π, βͺ (π β {π§}), π§)))) | ||
Theorem | f1omvdmvd 19157 | 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 19158 | 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 19159 | 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 19160 | 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 19161 | 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 19162 | 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 19163 | 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 19164* | The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ (π· β π β π = (π β {π¦ β π« π· β£ π¦ β 2o} β¦ (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§)))) | ||
Theorem | pmtrval 19165* | A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ π β π· β§ π β 2o) β (πβπ) = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) | ||
Theorem | pmtrfv 19166 | General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ (((π· β π β§ π β π· β§ π β 2o) β§ π β π·) β ((πβπ)βπ) = if(π β π, βͺ (π β {π}), π)) | ||
Theorem | pmtrprfv 19167 | In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ (π β π· β§ π β π· β§ π β π)) β ((πβ{π, π})βπ) = π) | ||
Theorem | pmtrprfv3 19168 | In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ (π β π· β§ π β π· β§ π β π·) β§ (π β π β§ π β π β§ π β π)) β ((πβ{π, π})βπ) = π) | ||
Theorem | pmtrf 19169 | Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ π β π· β§ π β 2o) β (πβπ):π·βΆπ·) | ||
Theorem | pmtrmvd 19170 | A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ π β π· β§ π β 2o) β dom ((πβπ) β I ) = π) | ||
Theorem | pmtrrn 19171 | Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ ((π· β π β§ π β π· β§ π β 2o) β (πβπ) β π ) | ||
Theorem | pmtrfrn 19172 | A transposition (as a kind of function) is the function transposing the two points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π & β’ π = dom (πΉ β I ) β β’ (πΉ β π β ((π· β V β§ π β π· β§ π β 2o) β§ πΉ = (πβπ))) | ||
Theorem | pmtrffv 19173 | Mapping of a point under a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π & β’ π = dom (πΉ β I ) β β’ ((πΉ β π β§ π β π·) β (πΉβπ) = if(π β π, βͺ (π β {π}), π)) | ||
Theorem | pmtrrn2 19174* | For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ (πΉ β π β βπ₯ β π· βπ¦ β π· (π₯ β π¦ β§ πΉ = (πβ{π₯, π¦}))) | ||
Theorem | pmtrfinv 19175 | A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ (πΉ β π β (πΉ β πΉ) = ( I βΎ π·)) | ||
Theorem | pmtrfmvdn0 19176 | A transposition moves at least one point. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ (πΉ β π β dom (πΉ β I ) β β ) | ||
Theorem | pmtrff1o 19177 | A transposition function is a permutation. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ (πΉ β π β πΉ:π·β1-1-ontoβπ·) | ||
Theorem | pmtrfcnv 19178 | A transposition function is its own inverse. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ (πΉ β π β β‘πΉ = πΉ) | ||
Theorem | pmtrfb 19179 | An intrinsic characterization of the transposition permutations. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ (πΉ β π β (π· β V β§ πΉ:π·β1-1-ontoβπ· β§ dom (πΉ β I ) β 2o)) | ||
Theorem | pmtrfconj 19180 | Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ ((πΉ β π β§ πΊ:π·β1-1-ontoβπ·) β ((πΊ β πΉ) β β‘πΊ) β π ) | ||
Theorem | symgsssg 19181* | The symmetric group has subgroups restricting the set of non-fixed points. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
β’ πΊ = (SymGrpβπ·) & β’ π΅ = (BaseβπΊ) β β’ (π· β π β {π₯ β π΅ β£ dom (π₯ β I ) β π} β (SubGrpβπΊ)) | ||
Theorem | symgfisg 19182* | The symmetric group has a subgroup of permutations that move finitely many points. (Contributed by Stefan O'Rear, 24-Aug-2015.) |
β’ πΊ = (SymGrpβπ·) & β’ π΅ = (BaseβπΊ) β β’ (π· β π β {π₯ β π΅ β£ dom (π₯ β I ) β Fin} β (SubGrpβπΊ)) | ||
Theorem | symgtrf 19183 | Transpositions are elements of the symmetric group. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
β’ π = ran (pmTrspβπ·) & β’ πΊ = (SymGrpβπ·) & β’ π΅ = (BaseβπΊ) β β’ π β π΅ | ||
Theorem | symggen 19184* | The span of the transpositions is the subgroup that moves finitely many points. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
β’ π = ran (pmTrspβπ·) & β’ πΊ = (SymGrpβπ·) & β’ π΅ = (BaseβπΊ) & β’ πΎ = (mrClsβ(SubMndβπΊ)) β β’ (π· β π β (πΎβπ) = {π₯ β π΅ β£ dom (π₯ β I ) β Fin}) | ||
Theorem | symggen2 19185 | A finite permutation group is generated by the transpositions, see also Theorem 3.4 in [Rotman] p. 31. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
β’ π = ran (pmTrspβπ·) & β’ πΊ = (SymGrpβπ·) & β’ π΅ = (BaseβπΊ) & β’ πΎ = (mrClsβ(SubMndβπΊ)) β β’ (π· β Fin β (πΎβπ) = π΅) | ||
Theorem | symgtrinv 19186 | To invert a permutation represented as a sequence of transpositions, reverse the sequence. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
β’ π = ran (pmTrspβπ·) & β’ πΊ = (SymGrpβπ·) & β’ πΌ = (invgβπΊ) β β’ ((π· β π β§ π β Word π) β (πΌβ(πΊ Ξ£g π)) = (πΊ Ξ£g (reverseβπ))) | ||
Theorem | pmtr3ncomlem1 19187 | Lemma 1 for pmtr3ncom 19189. (Contributed by AV, 17-Mar-2018.) |
β’ π = (pmTrspβπ·) & β’ πΉ = (πβ{π, π}) & β’ πΊ = (πβ{π, π}) β β’ ((π· β π β§ (π β π· β§ π β π· β§ π β π·) β§ (π β π β§ π β π β§ π β π)) β ((πΊ β πΉ)βπ) β ((πΉ β πΊ)βπ)) | ||
Theorem | pmtr3ncomlem2 19188 | Lemma 2 for pmtr3ncom 19189. (Contributed by AV, 17-Mar-2018.) |
β’ π = (pmTrspβπ·) & β’ πΉ = (πβ{π, π}) & β’ πΊ = (πβ{π, π}) β β’ ((π· β π β§ (π β π· β§ π β π· β§ π β π·) β§ (π β π β§ π β π β§ π β π)) β (πΊ β πΉ) β (πΉ β πΊ)) | ||
Theorem | pmtr3ncom 19189* | Transpositions over sets with at least 3 elements are not commutative, see also the remark in [Rotman] p. 28. (Contributed by AV, 21-Mar-2019.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ 3 β€ (β―βπ·)) β βπ β ran πβπ β ran π(π β π) β (π β π)) | ||
Theorem | pmtrdifellem1 19190 | Lemma 1 for pmtrdifel 19194. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = ((pmTrspβπ)βdom (π β I )) β β’ (π β π β π β π ) | ||
Theorem | pmtrdifellem2 19191 | Lemma 2 for pmtrdifel 19194. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = ((pmTrspβπ)βdom (π β I )) β β’ (π β π β dom (π β I ) = dom (π β I )) | ||
Theorem | pmtrdifellem3 19192* | Lemma 3 for pmtrdifel 19194. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = ((pmTrspβπ)βdom (π β I )) β β’ (π β π β βπ₯ β (π β {πΎ})(πβπ₯) = (πβπ₯)) | ||
Theorem | pmtrdifellem4 19193 | Lemma 4 for pmtrdifel 19194. (Contributed by AV, 28-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = ((pmTrspβπ)βdom (π β I )) β β’ ((π β π β§ πΎ β π) β (πβπΎ) = πΎ) | ||
Theorem | pmtrdifel 19194* | A transposition of elements of a set without a special element corresponds to a transposition of elements of the set. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) β β’ βπ‘ β π βπ β π βπ₯ β (π β {πΎ})(π‘βπ₯) = (πβπ₯) | ||
Theorem | pmtrdifwrdellem1 19195* | Lemma 1 for pmtrdifwrdel 19199. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = (π₯ β (0..^(β―βπ)) β¦ ((pmTrspβπ)βdom ((πβπ₯) β I ))) β β’ (π β Word π β π β Word π ) | ||
Theorem | pmtrdifwrdellem2 19196* | Lemma 2 for pmtrdifwrdel 19199. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = (π₯ β (0..^(β―βπ)) β¦ ((pmTrspβπ)βdom ((πβπ₯) β I ))) β β’ (π β Word π β (β―βπ) = (β―βπ)) | ||
Theorem | pmtrdifwrdellem3 19197* | Lemma 3 for pmtrdifwrdel 19199. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = (π₯ β (0..^(β―βπ)) β¦ ((pmTrspβπ)βdom ((πβπ₯) β I ))) β β’ (π β Word π β βπ β (0..^(β―βπ))βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)) | ||
Theorem | pmtrdifwrdel2lem1 19198* | Lemma 1 for pmtrdifwrdel2 19200. (Contributed by AV, 31-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = (π₯ β (0..^(β―βπ)) β¦ ((pmTrspβπ)βdom ((πβπ₯) β I ))) β β’ ((π β Word π β§ πΎ β π) β βπ β (0..^(β―βπ))((πβπ)βπΎ) = πΎ) | ||
Theorem | pmtrdifwrdel 19199* | A sequence of transpositions of elements of a set without a special element corresponds to a sequence of transpositions of elements of the set. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) β β’ βπ€ β Word πβπ’ β Word π ((β―βπ€) = (β―βπ’) β§ βπ β (0..^(β―βπ€))βπ₯ β (π β {πΎ})((π€βπ)βπ₯) = ((π’βπ)βπ₯)) | ||
Theorem | pmtrdifwrdel2 19200* | A sequence of transpositions of elements of a set without a special element corresponds to a sequence of transpositions of elements of the set not moving the special element. (Contributed by AV, 31-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) β β’ (πΎ β π β βπ€ β Word πβπ’ β Word π ((β―βπ€) = (β―βπ’) β§ βπ β (0..^(β―βπ€))(((π’βπ)βπΎ) = πΎ β§ βπ₯ β (π β {πΎ})((π€βπ)βπ₯) = ((π’βπ)βπ₯)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |