![]() |
Metamath
Proof Explorer Theorem List (p. 194 of 481) | < 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-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | symg2hash 19301 | The symmetric group on a (proper) pair has cardinality 2. (Contributed by AV, 9-Dec-2018.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ, π½} β β’ ((πΌ β π β§ π½ β π β§ πΌ β π½) β (β―βπ΅) = 2) | ||
Theorem | symg2bas 19302 | 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 19300. (Contributed by AV, 9-Dec-2018.) (Proof shortened by AV, 16-Jun-2022.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ, π½} β β’ ((πΌ β π β§ π½ β π) β π΅ = {{β¨πΌ, πΌβ©, β¨π½, π½β©}, {β¨πΌ, π½β©, β¨π½, πΌβ©}}) | ||
Theorem | 0symgefmndeq 19303 | 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 19304 | The symmetric group on a singleton π΄ is identical with the monoid of endofunctions on π΄. (Contributed by AV, 31-Mar-2024.) |
β’ (π΄ = {π} β (EndoFMndβπ΄) = (SymGrpβπ΄)) | ||
Theorem | symgpssefmnd 19305 | 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 19306* | 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 19307* | Obsolete proof of symgvalstruct 19306 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 19308 | 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 19309 | 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 19310 | 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 19311 | 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 19312 | 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 19313 | The symmetric group on a set π΄ is a submonoid of the monoid of endofunctions on π΄. Alternate proof based on issubmndb 18720 and not on injsubmefmnd 18812 and sursubmefmnd 18811. (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 19314* | 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 19315* | The converse of galactghm 19314. 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 19316 | The topology of the symmetric group on π΄. (Contributed by Mario Carneiro, 29-Aug-2015.) |
β’ πΊ = (SymGrpβπ) & β’ π΅ = (BaseβπΊ) β β’ (π β π β ((βtβ(π Γ {π« π})) βΎt π΅) = (TopOpenβπΊ)) | ||
Theorem | symgga 19317* | The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015.) |
β’ πΊ = (SymGrpβπ) & β’ π΅ = (BaseβπΊ) & β’ πΉ = (π β π΅, π₯ β π β¦ (πβπ₯)) β β’ (π β π β πΉ β (πΊ GrpAct π)) | ||
Theorem | pgrpsubgsymgbi 19318 | Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β (π β (SubGrpβπΊ) β (π β π΅ β§ (πΊ βΎs π) β Grp))) | ||
Theorem | pgrpsubgsymg 19319* | 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 19320 | 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 19321 | 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 19322* | Lemma for cayley 19324. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) & β’ π» = (SymGrpβπ) & β’ π = (Baseβπ») & β’ πΉ = (π β π β¦ (π β π β¦ (π + π))) β β’ (πΊ β Grp β πΉ β (πΊ GrpHom π»)) | ||
Theorem | cayleylem2 19323* | Lemma for cayley 19324. (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 19324* | 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 19325* | 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 19326* | 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 19327* | The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019.) |
β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((πΎ β π β§ π β π) β πΈ:πβΆπ) | ||
Theorem | symgextfv 19328* | 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 19329* | 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 19330* | Lemma for symgextf1 19331. (Contributed by AV, 6-Jan-2019.) |
β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((πΎ β π β§ π β π) β ((π β (π β {πΎ}) β§ π β {πΎ}) β (πΈβπ) β (πΈβπ))) | ||
Theorem | symgextf1 19331* | 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 19332* | 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 19333* | 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 19334* | 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 19335* | 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 19336 | Homomorphic property of composites of permutations with a singleton. (Contributed by AV, 20-Jan-2019.) |
β’ πΊ = (SymGrpβπ΄) & β’ π΅ = (BaseβπΊ) β β’ ((π΄ β π β§ π β Word π΅ β§ π β π΅) β (πΊ Ξ£g (π ++ β¨βπββ©)) = ((πΊ Ξ£g π) β π)) | ||
Theorem | gsmsymgrfixlem1 19337* | Lemma 1 for gsmsymgrfix 19338. (Contributed by AV, 20-Jan-2019.) |
β’ π = (SymGrpβπ) & β’ π΅ = (Baseβπ) β β’ (((π β Word π΅ β§ π β π΅) β§ (π β Fin β§ πΎ β π) β§ (βπ β (0..^(β―βπ))((πβπ)βπΎ) = πΎ β ((π Ξ£g π)βπΎ) = πΎ)) β (βπ β (0..^((β―βπ) + 1))(((π ++ β¨βπββ©)βπ)βπΎ) = πΎ β ((π Ξ£g (π ++ β¨βπββ©))βπΎ) = πΎ)) | ||
Theorem | gsmsymgrfix 19338* | 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 19339* | 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 19340* | Lemma 1 for gsmsymgreq 19342. (Contributed by AV, 26-Jan-2019.) |
β’ π = (SymGrpβπ) & β’ π΅ = (Baseβπ) & β’ π = (SymGrpβπ) & β’ π = (Baseβπ) & β’ πΌ = (π β© π) β β’ (((π β Fin β§ π β Fin β§ π½ β πΌ) β§ ((π β Word π΅ β§ πΆ β π΅) β§ (π β Word π β§ π β π) β§ (β―βπ) = (β―βπ))) β ((βπ β πΌ ((π Ξ£g π)βπ) = ((π Ξ£g π)βπ) β§ (πΆβπ½) = (π βπ½)) β ((π Ξ£g (π ++ β¨βπΆββ©))βπ½) = ((π Ξ£g (π ++ β¨βπ ββ©))βπ½))) | ||
Theorem | gsmsymgreqlem2 19341* | Lemma 2 for gsmsymgreq 19342. (Contributed by AV, 26-Jan-2019.) |
β’ π = (SymGrpβπ) & β’ π΅ = (Baseβπ) & β’ π = (SymGrpβπ) & β’ π = (Baseβπ) & β’ πΌ = (π β© π) β β’ (((π β Fin β§ π β Fin) β§ ((π β Word π΅ β§ πΆ β π΅) β§ (π β Word π β§ π β π) β§ (β―βπ) = (β―βπ))) β ((βπ β (0..^(β―βπ))βπ β πΌ ((πβπ)βπ) = ((πβπ)βπ) β βπ β πΌ ((π Ξ£g π)βπ) = ((π Ξ£g π)βπ)) β (βπ β (0..^(β―β(π ++ β¨βπΆββ©)))βπ β πΌ (((π ++ β¨βπΆββ©)βπ)βπ) = (((π ++ β¨βπ ββ©)βπ)βπ) β βπ β πΌ ((π Ξ£g (π ++ β¨βπΆββ©))βπ) = ((π Ξ£g (π ++ β¨βπ ββ©))βπ)))) | ||
Theorem | gsmsymgreq 19342* | 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 19343* | A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = {π β π β£ (πβπΎ) = πΎ} β β’ (πΉ β π β (πΉ β π β (πΉ:πβ1-1-ontoβπ β§ (πΉβπΎ) = πΎ))) | ||
Theorem | symgfixels 19344* | 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 19345* | 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 19346* | 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 19347* | 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 19348* | Lemma 1 for symgfixfo 19349. (Contributed by AV, 7-Jan-2019.) |
β’ π = (Baseβ(SymGrpβπ)) & β’ π = {π β π β£ (πβπΎ) = πΎ} & β’ π = (Baseβ(SymGrpβ(π β {πΎ}))) & β’ π» = (π β π β¦ (π βΎ (π β {πΎ}))) & β’ πΈ = (π₯ β π β¦ if(π₯ = πΎ, πΎ, (πβπ₯))) β β’ ((π β π β§ πΎ β π β§ π β π) β πΈ β π) | ||
Theorem | symgfixfo 19349* | 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 19350* | 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 19351 | Syntax for the transposition generator function. |
class pmTrsp | ||
Definition | df-pmtr 19352* | Define a function that generates the transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ pmTrsp = (π β V β¦ (π β {π¦ β π« π β£ π¦ β 2o} β¦ (π§ β π β¦ if(π§ β π, βͺ (π β {π§}), π§)))) | ||
Theorem | f1omvdmvd 19353 | 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 19354 | 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 19355 | 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 19356 | 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 19357 | 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 19358 | 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 19359 | 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 19360* | The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ (π· β π β π = (π β {π¦ β π« π· β£ π¦ β 2o} β¦ (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§)))) | ||
Theorem | pmtrval 19361* | A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ π β π· β§ π β 2o) β (πβπ) = (π§ β π· β¦ if(π§ β π, βͺ (π β {π§}), π§))) | ||
Theorem | pmtrfv 19362 | General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ (((π· β π β§ π β π· β§ π β 2o) β§ π β π·) β ((πβπ)βπ) = if(π β π, βͺ (π β {π}), π)) | ||
Theorem | pmtrprfv 19363 | In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ (π β π· β§ π β π· β§ π β π)) β ((πβ{π, π})βπ) = π) | ||
Theorem | pmtrprfv3 19364 | In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ (π β π· β§ π β π· β§ π β π·) β§ (π β π β§ π β π β§ π β π)) β ((πβ{π, π})βπ) = π) | ||
Theorem | pmtrf 19365 | Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ π β π· β§ π β 2o) β (πβπ):π·βΆπ·) | ||
Theorem | pmtrmvd 19366 | A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π = (pmTrspβπ·) β β’ ((π· β π β§ π β π· β§ π β 2o) β dom ((πβπ) β I ) = π) | ||
Theorem | pmtrrn 19367 | Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ ((π· β π β§ π β π· β§ π β 2o) β (πβπ) β π ) | ||
Theorem | pmtrfrn 19368 | 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 19369 | Mapping of a point under a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π & β’ π = dom (πΉ β I ) β β’ ((πΉ β π β§ π β π·) β (πΉβπ) = if(π β π, βͺ (π β {π}), π)) | ||
Theorem | pmtrrn2 19370* | For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ (πΉ β π β βπ₯ β π· βπ¦ β π· (π₯ β π¦ β§ πΉ = (πβ{π₯, π¦}))) | ||
Theorem | pmtrfinv 19371 | A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ (πΉ β π β (πΉ β πΉ) = ( I βΎ π·)) | ||
Theorem | pmtrfmvdn0 19372 | A transposition moves at least one point. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ (πΉ β π β dom (πΉ β I ) β β ) | ||
Theorem | pmtrff1o 19373 | A transposition function is a permutation. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ (πΉ β π β πΉ:π·β1-1-ontoβπ·) | ||
Theorem | pmtrfcnv 19374 | A transposition function is its own inverse. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ (πΉ β π β β‘πΉ = πΉ) | ||
Theorem | pmtrfb 19375 | 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 19376 | Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π = (pmTrspβπ·) & β’ π = ran π β β’ ((πΉ β π β§ πΊ:π·β1-1-ontoβπ·) β ((πΊ β πΉ) β β‘πΊ) β π ) | ||
Theorem | symgsssg 19377* | 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 19378* | 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 19379 | Transpositions are elements of the symmetric group. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
β’ π = ran (pmTrspβπ·) & β’ πΊ = (SymGrpβπ·) & β’ π΅ = (BaseβπΊ) β β’ π β π΅ | ||
Theorem | symggen 19380* | 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 19381 | 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 19382 | 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 19383 | Lemma 1 for pmtr3ncom 19385. (Contributed by AV, 17-Mar-2018.) |
β’ π = (pmTrspβπ·) & β’ πΉ = (πβ{π, π}) & β’ πΊ = (πβ{π, π}) β β’ ((π· β π β§ (π β π· β§ π β π· β§ π β π·) β§ (π β π β§ π β π β§ π β π)) β ((πΊ β πΉ)βπ) β ((πΉ β πΊ)βπ)) | ||
Theorem | pmtr3ncomlem2 19384 | Lemma 2 for pmtr3ncom 19385. (Contributed by AV, 17-Mar-2018.) |
β’ π = (pmTrspβπ·) & β’ πΉ = (πβ{π, π}) & β’ πΊ = (πβ{π, π}) β β’ ((π· β π β§ (π β π· β§ π β π· β§ π β π·) β§ (π β π β§ π β π β§ π β π)) β (πΊ β πΉ) β (πΉ β πΊ)) | ||
Theorem | pmtr3ncom 19385* | 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 19386 | Lemma 1 for pmtrdifel 19390. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = ((pmTrspβπ)βdom (π β I )) β β’ (π β π β π β π ) | ||
Theorem | pmtrdifellem2 19387 | Lemma 2 for pmtrdifel 19390. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = ((pmTrspβπ)βdom (π β I )) β β’ (π β π β dom (π β I ) = dom (π β I )) | ||
Theorem | pmtrdifellem3 19388* | Lemma 3 for pmtrdifel 19390. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = ((pmTrspβπ)βdom (π β I )) β β’ (π β π β βπ₯ β (π β {πΎ})(πβπ₯) = (πβπ₯)) | ||
Theorem | pmtrdifellem4 19389 | Lemma 4 for pmtrdifel 19390. (Contributed by AV, 28-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = ((pmTrspβπ)βdom (π β I )) β β’ ((π β π β§ πΎ β π) β (πβπΎ) = πΎ) | ||
Theorem | pmtrdifel 19390* | 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 19391* | Lemma 1 for pmtrdifwrdel 19395. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = (π₯ β (0..^(β―βπ)) β¦ ((pmTrspβπ)βdom ((πβπ₯) β I ))) β β’ (π β Word π β π β Word π ) | ||
Theorem | pmtrdifwrdellem2 19392* | Lemma 2 for pmtrdifwrdel 19395. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = (π₯ β (0..^(β―βπ)) β¦ ((pmTrspβπ)βdom ((πβπ₯) β I ))) β β’ (π β Word π β (β―βπ) = (β―βπ)) | ||
Theorem | pmtrdifwrdellem3 19393* | Lemma 3 for pmtrdifwrdel 19395. (Contributed by AV, 15-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = (π₯ β (0..^(β―βπ)) β¦ ((pmTrspβπ)βdom ((πβπ₯) β I ))) β β’ (π β Word π β βπ β (0..^(β―βπ))βπ β (π β {πΎ})((πβπ)βπ) = ((πβπ)βπ)) | ||
Theorem | pmtrdifwrdel2lem1 19394* | Lemma 1 for pmtrdifwrdel2 19396. (Contributed by AV, 31-Jan-2019.) |
β’ π = ran (pmTrspβ(π β {πΎ})) & β’ π = ran (pmTrspβπ) & β’ π = (π₯ β (0..^(β―βπ)) β¦ ((pmTrspβπ)βdom ((πβπ₯) β I ))) β β’ ((π β Word π β§ πΎ β π) β βπ β (0..^(β―βπ))((πβπ)βπΎ) = πΎ) | ||
Theorem | pmtrdifwrdel 19395* | 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 19396* | 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..^(β―βπ€))(((π’βπ)βπΎ) = πΎ β§ βπ₯ β (π β {πΎ})((π€βπ)βπ₯) = ((π’βπ)βπ₯)))) | ||
Theorem | pmtrprfval 19397* | The transpositions on a pair. (Contributed by AV, 9-Dec-2018.) |
β’ (pmTrspβ{1, 2}) = (π β {{1, 2}} β¦ (π§ β {1, 2} β¦ if(π§ = 1, 2, 1))) | ||
Theorem | pmtrprfvalrn 19398 | The range of the transpositions on a pair is actually a singleton: the transposition of the two elements of the pair. (Contributed by AV, 9-Dec-2018.) |
β’ ran (pmTrspβ{1, 2}) = {{β¨1, 2β©, β¨2, 1β©}} | ||
Syntax | cpsgn 19399 | Syntax for the sign of a permutation. |
class pmSgn | ||
Syntax | cevpm 19400 | Syntax for even permutations. |
class pmEven |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |