Home | Metamath
Proof Explorer Theorem List (p. 179 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | elsymgbas2 17801 | 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 17802 | 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 17803 | Elements in the symmetric group are 1-1 onto functions. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴–1-1-onto→𝐴) | ||
Theorem | symgbasf 17804 | A permutation (element of the symmetric group) is a function of a set into itself. (Contributed by AV, 1-Jan-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴⟶𝐴) | ||
Theorem | symghash 17805 | The symmetric group on 𝑛 objects has cardinality 𝑛!. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ Fin → (#‘𝐵) = (!‘(#‘𝐴))) | ||
Theorem | symgbasfi 17806 | The symmetric group on a finite index set is finite. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin) | ||
Theorem | symgfv 17807 | The function value of a permutation. (Contributed by AV, 1-Jan-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴) | ||
Theorem | symgfvne 17808 | The function values of a permutation for different arguments are different. (Contributed by AV, 8-Jan-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑍 → (𝑌 ≠ 𝑋 → (𝐹‘𝑌) ≠ 𝑍))) | ||
Theorem | symgplusg 17809* | 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.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔)) | ||
Theorem | symgov 17810 | 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.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌)) | ||
Theorem | symgcl 17811 | 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 | symgmov1 17812* | 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 17813* | 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 17814 | 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 17815 | The symmetric group on a singleton has cardinality 1. (Contributed by AV, 9-Dec-2018.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼} ⇒ ⊢ (𝐼 ∈ 𝑉 → (#‘𝐵) = 1) | ||
Theorem | symg1bas 17816 | 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 17817 | The symmetric group on a (proper) pair has cardinality 2. (Contributed by AV, 9-Dec-2018.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼, 𝐽} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (#‘𝐵) = 2) | ||
Theorem | symg2bas 17818 | The symmetric group on a pair is the symmetric group S2 consisting of the identity and the transposition. This theorem is also valid if the elements are identical: then it collapses to theorem symg1bas 17816. (Contributed by AV, 9-Dec-2018.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼, 𝐽} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) | ||
Theorem | symgtset 17819 | 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.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → (∏t‘(𝐴 × {𝒫 𝐴})) = (TopSet‘𝐺)) | ||
Theorem | symggrp 17820 | The symmetric group on a set 𝐴 is a group. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Grp) | ||
Theorem | symgid 17821 | 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.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) = (0g‘𝐺)) | ||
Theorem | symginv 17822 | 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 | galactghm 17823* | 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 17824* | The converse of galactghm 17823. 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 17825 | The topology of the symmetric group on 𝐴. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐺 = (SymGrp‘𝑋) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺)) | ||
Theorem | symgga 17826* | The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ 𝐺 = (SymGrp‘𝑋) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐹 = (𝑓 ∈ 𝐵, 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥)) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐹 ∈ (𝐺 GrpAct 𝑋)) | ||
Theorem | pgrpsubgsymgbi 17827 | Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑃 ∈ (SubGrp‘𝐺) ↔ (𝑃 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑃) ∈ Grp))) | ||
Theorem | pgrpsubgsymg 17828* | Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐹 = (Base‘𝑃) ⇒ ⊢ (𝐴 ∈ 𝑉 → ((𝑃 ∈ Grp ∧ 𝐹 ⊆ 𝐵 ∧ (+g‘𝑃) = (𝑓 ∈ 𝐹, 𝑔 ∈ 𝐹 ↦ (𝑓 ∘ 𝑔))) → 𝐹 ∈ (SubGrp‘𝐺))) | ||
Theorem | idresperm 17829 | The identity function restricted to a set is a permutation of this set. (Contributed by AV, 17-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ (Base‘𝐺)) | ||
Theorem | idressubgsymg 17830 | 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 17831 | 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 17832* | Lemma for cayley 17834. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐻 = (SymGrp‘𝑋) & ⊢ 𝑆 = (Base‘𝐻) & ⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎))) ⇒ ⊢ (𝐺 ∈ Grp → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | ||
Theorem | cayleylem2 17833* | Lemma for cayley 17834. (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 17834* | 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 17835* | 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 17836* | 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 17837* | The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019.) |
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) ⇒ ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸:𝑁⟶𝑁) | ||
Theorem | symgextfv 17838* | 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 17839* | 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 17840* | Lemma for symgextf1 17841. (Contributed by AV, 6-Jan-2019.) |
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) ⇒ ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ((𝑋 ∈ (𝑁 ∖ {𝐾}) ∧ 𝑌 ∈ {𝐾}) → (𝐸‘𝑋) ≠ (𝐸‘𝑌))) | ||
Theorem | symgextf1 17841* | 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 17842* | 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 17843* | 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 17844* | 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 17845* | 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 17846 | Homomorphic property of composites of permutations with a singleton. (Contributed by AV, 20-Jan-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ 〈“𝑍”〉)) = ((𝐺 Σg 𝑊) ∘ 𝑍)) | ||
Theorem | gsmsymgrfixlem1 17847* | Lemma 1 for gsmsymgrfix 17848. (Contributed by AV, 20-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(#‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^((#‘𝑊) + 1))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑊 ++ 〈“𝑃”〉))‘𝐾) = 𝐾)) | ||
Theorem | gsmsymgrfix 17848* | 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 17849* | 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 17850* | Lemma 1 for gsmsymgreq 17852. (Contributed by AV, 26-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑍 = (SymGrp‘𝑀) & ⊢ 𝑃 = (Base‘𝑍) & ⊢ 𝐼 = (𝑁 ∩ 𝑀) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ((∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) ∧ (𝐶‘𝐽) = (𝑅‘𝐽)) → ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝐽) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝐽))) | ||
Theorem | gsmsymgreqlem2 17851* | Lemma 2 for gsmsymgreq 17852. (Contributed by AV, 26-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑍 = (SymGrp‘𝑀) & ⊢ 𝑃 = (Base‘𝑍) & ⊢ 𝐼 = (𝑁 ∩ 𝑀) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (#‘𝑋) = (#‘𝑌))) → ((∀𝑖 ∈ (0..^(#‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (∀𝑖 ∈ (0..^(#‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) | ||
Theorem | gsmsymgreq 17852* | 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 17853* | A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ⇒ ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝑄 ↔ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾))) | ||
Theorem | symgfixels 17854* | 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 17855* | 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 17856* | 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 17857* | 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 17858* | Lemma 1 for symgfixfo 17859. (Contributed by AV, 7-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} & ⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝐻 = (𝑞 ∈ 𝑄 ↦ (𝑞 ↾ (𝑁 ∖ {𝐾}))) & ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) ⇒ ⊢ ((𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸 ∈ 𝑄) | ||
Theorem | symgfixfo 17859* | 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 17860* | 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 17861 | Syntax for the transposition generator function. |
class pmTrsp | ||
Definition | df-pmtr 17862* | Define a function that generates the transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ pmTrsp = (𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2𝑜} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) | ||
Theorem | f1omvdmvd 17863 | 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 17864 | 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 17865 | 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 17866 | 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 17867 | 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 ) ≈ 2𝑜 ∧ dom (𝐺 ∖ I ) = dom (𝐹 ∖ I ))) → 𝐹 = 𝐺) | ||
Theorem | f1omvdco2 17868 | 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 17869 | 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 17870* | The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ (𝐷 ∈ 𝑉 → 𝑇 = (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2𝑜} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) | ||
Theorem | pmtrval 17871* | A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → (𝑇‘𝑃) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧))) | ||
Theorem | pmtrfv 17872 | General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝑍 ∈ 𝐷) → ((𝑇‘𝑃)‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍)) | ||
Theorem | pmtrprfv 17873 | In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑋) = 𝑌) | ||
Theorem | pmtrprfv3 17874 | In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝑇‘{𝑋, 𝑌})‘𝑍) = 𝑍) | ||
Theorem | pmtrf 17875 | Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → (𝑇‘𝑃):𝐷⟶𝐷) | ||
Theorem | pmtrmvd 17876 | A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → dom ((𝑇‘𝑃) ∖ I ) = 𝑃) | ||
Theorem | pmtrrn 17877 | Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) → (𝑇‘𝑃) ∈ 𝑅) | ||
Theorem | pmtrfrn 17878 | 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 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2𝑜) ∧ 𝐹 = (𝑇‘𝑃))) | ||
Theorem | pmtrffv 17879 | Mapping of a point under a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 & ⊢ 𝑃 = dom (𝐹 ∖ I ) ⇒ ⊢ ((𝐹 ∈ 𝑅 ∧ 𝑍 ∈ 𝐷) → (𝐹‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍)) | ||
Theorem | pmtrrn2 17880* | For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))) | ||
Theorem | pmtrfinv 17881 | A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) = ( I ↾ 𝐷)) | ||
Theorem | pmtrfmvdn0 17882 | A transposition moves at least one point. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≠ ∅) | ||
Theorem | pmtrff1o 17883 | A transposition function is a permutation. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → 𝐹:𝐷–1-1-onto→𝐷) | ||
Theorem | pmtrfcnv 17884 | A transposition function is its own inverse. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → ◡𝐹 = 𝐹) | ||
Theorem | pmtrfb 17885 | An intrinsic characterization of the transposition permutations. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 ↔ (𝐷 ∈ V ∧ 𝐹:𝐷–1-1-onto→𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2𝑜)) | ||
Theorem | pmtrfconj 17886 | Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ ((𝐹 ∈ 𝑅 ∧ 𝐺:𝐷–1-1-onto→𝐷) → ((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∈ 𝑅) | ||
Theorem | symgsssg 17887* | 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 17888* | 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 17889 | Transpositions are elements of the symmetric group. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ 𝑇 = ran (pmTrsp‘𝐷) & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝑇 ⊆ 𝐵 | ||
Theorem | symggen 17890* | 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 17891 | 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 17892 | 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 17893 | Lemma 1 for pmtr3ncom 17895. (Contributed by AV, 17-Mar-2018.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌}) & ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍}) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝐺 ∘ 𝐹)‘𝑋) ≠ ((𝐹 ∘ 𝐺)‘𝑋)) | ||
Theorem | pmtr3ncomlem2 17894 | Lemma 2 for pmtr3ncom 17895. (Contributed by AV, 17-Mar-2018.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌}) & ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍}) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐺 ∘ 𝐹) ≠ (𝐹 ∘ 𝐺)) | ||
Theorem | pmtr3ncom 17895* | 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 17896 | Lemma 1 for pmtrdifel 17900. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ (𝑄 ∈ 𝑇 → 𝑆 ∈ 𝑅) | ||
Theorem | pmtrdifellem2 17897 | Lemma 2 for pmtrdifel 17900. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ (𝑄 ∈ 𝑇 → dom (𝑆 ∖ I ) = dom (𝑄 ∖ I )) | ||
Theorem | pmtrdifellem3 17898* | Lemma 3 for pmtrdifel 17900. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ (𝑄 ∈ 𝑇 → ∀𝑥 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑥) = (𝑆‘𝑥)) | ||
Theorem | pmtrdifellem4 17899 | Lemma 4 for pmtrdifel 17900. (Contributed by AV, 28-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → (𝑆‘𝐾) = 𝐾) | ||
Theorem | pmtrdifel 17900* | 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‘𝑁) ⇒ ⊢ ∀𝑡 ∈ 𝑇 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ (𝑁 ∖ {𝐾})(𝑡‘𝑥) = (𝑟‘𝑥) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |