![]() |
Metamath
Proof Explorer Theorem List (p. 183 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43657) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | symg2bas 18201 | 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 18199. (Contributed by AV, 9-Dec-2018.) (Proof shortened by AV, 16-Jun-2022.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼, 𝐽} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) | ||
Theorem | symgtset 18202 | 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 18203 | 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 18204 | 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 18205 | 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 18206* | 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 18207* | The converse of galactghm 18206. 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 18208 | The topology of the symmetric group on 𝐴. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐺 = (SymGrp‘𝑋) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺)) | ||
Theorem | symgga 18209* | The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ 𝐺 = (SymGrp‘𝑋) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐹 = (𝑓 ∈ 𝐵, 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥)) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐹 ∈ (𝐺 GrpAct 𝑋)) | ||
Theorem | pgrpsubgsymgbi 18210 | Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑃 ∈ (SubGrp‘𝐺) ↔ (𝑃 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑃) ∈ Grp))) | ||
Theorem | pgrpsubgsymg 18211* | 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 18212 | The identity function restricted to a set is a permutation of this set. (Contributed by AV, 17-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ (Base‘𝐺)) | ||
Theorem | idressubgsymg 18213 | 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 18214 | 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 18215* | Lemma for cayley 18217. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐻 = (SymGrp‘𝑋) & ⊢ 𝑆 = (Base‘𝐻) & ⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎))) ⇒ ⊢ (𝐺 ∈ Grp → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | ||
Theorem | cayleylem2 18216* | Lemma for cayley 18217. (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 18217* | 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 18218* | 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 18219* | 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 18220* | The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019.) |
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) ⇒ ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸:𝑁⟶𝑁) | ||
Theorem | symgextfv 18221* | 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 18222* | 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 18223* | Lemma for symgextf1 18224. (Contributed by AV, 6-Jan-2019.) |
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) ⇒ ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ((𝑋 ∈ (𝑁 ∖ {𝐾}) ∧ 𝑌 ∈ {𝐾}) → (𝐸‘𝑋) ≠ (𝐸‘𝑌))) | ||
Theorem | symgextf1 18224* | 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 18225* | 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 18226* | 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 18227* | 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 18228* | 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 18229 | Homomorphic property of composites of permutations with a singleton. (Contributed by AV, 20-Jan-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ 〈“𝑍”〉)) = ((𝐺 Σg 𝑊) ∘ 𝑍)) | ||
Theorem | gsmsymgrfixlem1 18230* | Lemma 1 for gsmsymgrfix 18231. (Contributed by AV, 20-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(♯‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^((♯‘𝑊) + 1))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑊 ++ 〈“𝑃”〉))‘𝐾) = 𝐾)) | ||
Theorem | gsmsymgrfix 18231* | 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 18232* | 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 18233* | Lemma 1 for gsmsymgreq 18235. (Contributed by AV, 26-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑍 = (SymGrp‘𝑀) & ⊢ 𝑃 = (Base‘𝑍) & ⊢ 𝐼 = (𝑁 ∩ 𝑀) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) ∧ (𝐶‘𝐽) = (𝑅‘𝐽)) → ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝐽) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝐽))) | ||
Theorem | gsmsymgreqlem2 18234* | Lemma 2 for gsmsymgreq 18235. (Contributed by AV, 26-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑍 = (SymGrp‘𝑀) & ⊢ 𝑃 = (Base‘𝑍) & ⊢ 𝐼 = (𝑁 ∩ 𝑀) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (∀𝑖 ∈ (0..^(♯‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) | ||
Theorem | gsmsymgreq 18235* | 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 18236* | A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ⇒ ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝑄 ↔ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾))) | ||
Theorem | symgfixels 18237* | 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 18238* | 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 18239* | 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 18240* | 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 18241* | Lemma 1 for symgfixfo 18242. (Contributed by AV, 7-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} & ⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝐻 = (𝑞 ∈ 𝑄 ↦ (𝑞 ↾ (𝑁 ∖ {𝐾}))) & ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) ⇒ ⊢ ((𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸 ∈ 𝑄) | ||
Theorem | symgfixfo 18242* | 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 18243* | 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 18244 | Syntax for the transposition generator function. |
class pmTrsp | ||
Definition | df-pmtr 18245* | Define a function that generates the transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ pmTrsp = (𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) | ||
Theorem | f1omvdmvd 18246 | 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 18247 | 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 18248 | 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 18249 | 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 18250 | 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 18251 | 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 18252 | 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 18253* | The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ (𝐷 ∈ 𝑉 → 𝑇 = (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) | ||
Theorem | pmtrval 18254* | A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧))) | ||
Theorem | pmtrfv 18255 | General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) ∧ 𝑍 ∈ 𝐷) → ((𝑇‘𝑃)‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍)) | ||
Theorem | pmtrprfv 18256 | In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑋) = 𝑌) | ||
Theorem | pmtrprfv3 18257 | In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝑇‘{𝑋, 𝑌})‘𝑍) = 𝑍) | ||
Theorem | pmtrf 18258 | Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃):𝐷⟶𝐷) | ||
Theorem | pmtrmvd 18259 | A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → dom ((𝑇‘𝑃) ∖ I ) = 𝑃) | ||
Theorem | pmtrrn 18260 | Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) ∈ 𝑅) | ||
Theorem | pmtrfrn 18261 | 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 18262 | Mapping of a point under a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 & ⊢ 𝑃 = dom (𝐹 ∖ I ) ⇒ ⊢ ((𝐹 ∈ 𝑅 ∧ 𝑍 ∈ 𝐷) → (𝐹‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍)) | ||
Theorem | pmtrrn2 18263* | For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))) | ||
Theorem | pmtrfinv 18264 | A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) = ( I ↾ 𝐷)) | ||
Theorem | pmtrfmvdn0 18265 | A transposition moves at least one point. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≠ ∅) | ||
Theorem | pmtrff1o 18266 | A transposition function is a permutation. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → 𝐹:𝐷–1-1-onto→𝐷) | ||
Theorem | pmtrfcnv 18267 | A transposition function is its own inverse. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → ◡𝐹 = 𝐹) | ||
Theorem | pmtrfb 18268 | 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 18269 | Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ ((𝐹 ∈ 𝑅 ∧ 𝐺:𝐷–1-1-onto→𝐷) → ((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∈ 𝑅) | ||
Theorem | symgsssg 18270* | 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 18271* | 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 18272 | Transpositions are elements of the symmetric group. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ 𝑇 = ran (pmTrsp‘𝐷) & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝑇 ⊆ 𝐵 | ||
Theorem | symggen 18273* | 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 18274 | 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 18275 | 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 18276 | Lemma 1 for pmtr3ncom 18278. (Contributed by AV, 17-Mar-2018.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌}) & ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍}) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝐺 ∘ 𝐹)‘𝑋) ≠ ((𝐹 ∘ 𝐺)‘𝑋)) | ||
Theorem | pmtr3ncomlem2 18277 | Lemma 2 for pmtr3ncom 18278. (Contributed by AV, 17-Mar-2018.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌}) & ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍}) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐺 ∘ 𝐹) ≠ (𝐹 ∘ 𝐺)) | ||
Theorem | pmtr3ncom 18278* | 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 18279 | Lemma 1 for pmtrdifel 18283. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ (𝑄 ∈ 𝑇 → 𝑆 ∈ 𝑅) | ||
Theorem | pmtrdifellem2 18280 | Lemma 2 for pmtrdifel 18283. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ (𝑄 ∈ 𝑇 → dom (𝑆 ∖ I ) = dom (𝑄 ∖ I )) | ||
Theorem | pmtrdifellem3 18281* | Lemma 3 for pmtrdifel 18283. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ (𝑄 ∈ 𝑇 → ∀𝑥 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑥) = (𝑆‘𝑥)) | ||
Theorem | pmtrdifellem4 18282 | Lemma 4 for pmtrdifel 18283. (Contributed by AV, 28-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → (𝑆‘𝐾) = 𝐾) | ||
Theorem | pmtrdifel 18283* | 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 18284* | Lemma 1 for pmtrdifwrdel 18288. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I ))) ⇒ ⊢ (𝑊 ∈ Word 𝑇 → 𝑈 ∈ Word 𝑅) | ||
Theorem | pmtrdifwrdellem2 18285* | Lemma 2 for pmtrdifwrdel 18288. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I ))) ⇒ ⊢ (𝑊 ∈ Word 𝑇 → (♯‘𝑊) = (♯‘𝑈)) | ||
Theorem | pmtrdifwrdellem3 18286* | Lemma 3 for pmtrdifwrdel 18288. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I ))) ⇒ ⊢ (𝑊 ∈ Word 𝑇 → ∀𝑖 ∈ (0..^(♯‘𝑊))∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)) | ||
Theorem | pmtrdifwrdel2lem1 18287* | Lemma 1 for pmtrdifwrdel2 18289. (Contributed by AV, 31-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I ))) ⇒ ⊢ ((𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁) → ∀𝑖 ∈ (0..^(♯‘𝑊))((𝑈‘𝑖)‘𝐾) = 𝐾) | ||
Theorem | pmtrdifwrdel 18288* | 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 18289* | 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 18290* | The transpositions on a pair. (Contributed by AV, 9-Dec-2018.) |
⊢ (pmTrsp‘{1, 2}) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) | ||
Theorem | pmtrprfvalrn 18291 | 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 18292 | Syntax for the sign of a permutation. |
class pmSgn | ||
Syntax | cevpm 18293 | Syntax for even permutations. |
class pmEven | ||
Definition | df-psgn 18294* | Define a function which takes the value 1 for even permutations and -1 for odd. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
⊢ pmSgn = (𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))))) | ||
Definition | df-evpm 18295 | Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018.) |
⊢ pmEven = (𝑑 ∈ V ↦ (◡(pmSgn‘𝑑) “ {1})) | ||
Theorem | psgnunilem1 18296* | Lemma for psgnuni 18303. Given two consequtive transpositions in a representation of a permutation, either they are equal and therefore equivalent to the identity, or they are not and it is possible to commute them such that a chosen point in the left transposition is preserved in the right. By repeating this process, a point can be removed from a representation of the identity. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = ran (pmTrsp‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑃 ∈ 𝑇) & ⊢ (𝜑 → 𝑄 ∈ 𝑇) & ⊢ (𝜑 → 𝐴 ∈ dom (𝑃 ∖ I )) ⇒ ⊢ (𝜑 → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I )))) | ||
Theorem | psgnunilem5 18297* | Lemma for psgnuni 18303. It is impossible to shift a transposition off the end because if the active transposition is at the right end, it is the only transposition moving 𝐴 in contradiction to this being a representation of the identity. (Contributed by Stefan O'Rear, 25-Aug-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Proof shortened by AV, 12-Oct-2022.) |
⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝑇 = ran (pmTrsp‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑇) & ⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷)) & ⊢ (𝜑 → (♯‘𝑊) = 𝐿) & ⊢ (𝜑 → 𝐼 ∈ (0..^𝐿)) & ⊢ (𝜑 → 𝐴 ∈ dom ((𝑊‘𝐼) ∖ I )) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝐼) ¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I )) ⇒ ⊢ (𝜑 → (𝐼 + 1) ∈ (0..^𝐿)) | ||
Theorem | psgnunilem5OLD 18298* | Obsolete version of psgnunilem5 18297 as of 12-Oct-2022. (Contributed by Stefan O'Rear, 25-Aug-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝑇 = ran (pmTrsp‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑇) & ⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷)) & ⊢ (𝜑 → (♯‘𝑊) = 𝐿) & ⊢ (𝜑 → 𝐼 ∈ (0..^𝐿)) & ⊢ (𝜑 → 𝐴 ∈ dom ((𝑊‘𝐼) ∖ I )) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝐼) ¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I )) ⇒ ⊢ (𝜑 → (𝐼 + 1) ∈ (0..^𝐿)) | ||
Theorem | psgnunilem2 18299* | Lemma for psgnuni 18303. Induction step for moving a transposition as far to the right as possible. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝑇 = ran (pmTrsp‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑇) & ⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷)) & ⊢ (𝜑 → (♯‘𝑊) = 𝐿) & ⊢ (𝜑 → 𝐼 ∈ (0..^𝐿)) & ⊢ (𝜑 → 𝐴 ∈ dom ((𝑊‘𝐼) ∖ I )) & ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝐼) ¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I )) & ⊢ (𝜑 → ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) ⇒ ⊢ (𝜑 → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I )))) | ||
Theorem | psgnunilem3 18300* | Lemma for psgnuni 18303. Any nonempty representation of the identity can be incrementally transformed into a representation two shorter. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝑇 = ran (pmTrsp‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Word 𝑇) & ⊢ (𝜑 → (♯‘𝑊) = 𝐿) & ⊢ (𝜑 → (♯‘𝑊) ∈ ℕ) & ⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷)) & ⊢ (𝜑 → ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷))) ⇒ ⊢ ¬ 𝜑 |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |