![]() |
Metamath
Proof Explorer Theorem List (p. 195 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-symg 19401* | Define the symmetric group on set 𝑥. We represent the group as the set of one-to-one onto functions from 𝑥 to itself under function composition, and topologize it as a function space assuming the set is discrete. This definition is based on the fact that a symmetric group is a restriction of the monoid of endofunctions. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by AV, 28-Mar-2024.) |
⊢ SymGrp = (𝑥 ∈ V ↦ ((EndoFMnd‘𝑥) ↾s {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥})) | ||
Theorem | symgval 19402* | The value of the symmetric group function at 𝐴. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 12-Jan-2015.) (Revised by AV, 28-Mar-2024.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} ⇒ ⊢ 𝐺 = ((EndoFMnd‘𝐴) ↾s 𝐵) | ||
Theorem | symgbas 19403* | The base set of the symmetric group. (Contributed by Mario Carneiro, 12-Jan-2015.) (Proof shortened by AV, 29-Mar-2024.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} | ||
Theorem | elsymgbas2 19404 | 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 19405 | 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 19406 | Elements in the symmetric group are 1-1 onto functions. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴–1-1-onto→𝐴) | ||
Theorem | symgbasf 19407 | A permutation (element of the symmetric group) is a function from a set into itself. (Contributed by AV, 1-Jan-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴⟶𝐴) | ||
Theorem | symgbasmap 19408 | A permutation (element of the symmetric group) is a mapping (or set exponentiation) from a set into itself. (Contributed by AV, 30-Mar-2024.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹 ∈ (𝐴 ↑m 𝐴)) | ||
Theorem | symghash 19409 | The symmetric group on 𝑛 objects has cardinality 𝑛!. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ Fin → (♯‘𝐵) = (!‘(♯‘𝐴))) | ||
Theorem | symgbasfi 19410 | The symmetric group on a finite index set is finite. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin) | ||
Theorem | symgfv 19411 | The function value of a permutation. (Contributed by AV, 1-Jan-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴) | ||
Theorem | symgfvne 19412 | The function values of a permutation for different arguments are different. (Contributed by AV, 8-Jan-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑍 → (𝑌 ≠ 𝑋 → (𝐹‘𝑌) ≠ 𝑍))) | ||
Theorem | symgressbas 19413 | The symmetric group on 𝐴 characterized as structure restriction of the monoid of endofunctions on 𝐴 to its base set. (Contributed by AV, 30-Mar-2024.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑀 = (EndoFMnd‘𝐴) ⇒ ⊢ 𝐺 = (𝑀 ↾s 𝐵) | ||
Theorem | symgplusg 19414* | The group operation of a symmetric group is the function composition. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 28-Jan-2015.) (Proof shortened by AV, 19-Feb-2024.) (Revised by AV, 29-Mar-2024.) (Proof shortened by AV, 14-Aug-2024.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (𝐴 ↑m 𝐴) & ⊢ + = (+g‘𝐺) ⇒ ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔)) | ||
Theorem | symgov 19415 | The value of the group operation of the symmetric group on 𝐴. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 28-Jan-2015.) (Revised by AV, 30-Mar-2024.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌)) | ||
Theorem | symgcl 19416 | The group operation of the symmetric group on 𝐴 is closed, i.e. a magma. (Contributed by Mario Carneiro, 12-Jan-2015.) (Revised by Mario Carneiro, 28-Jan-2015.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) | ||
Theorem | idresperm 19417 | The identity function restricted to a set is a permutation of this set. (Contributed by AV, 17-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ (Base‘𝐺)) | ||
Theorem | symgmov1 19418* | 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 19419* | 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 19420 | 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 19421 | The symmetric group on a singleton has cardinality 1. (Contributed by AV, 9-Dec-2018.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼} ⇒ ⊢ (𝐼 ∈ 𝑉 → (♯‘𝐵) = 1) | ||
Theorem | symg1bas 19422 | 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 19423 | The symmetric group on a (proper) pair has cardinality 2. (Contributed by AV, 9-Dec-2018.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼, 𝐽} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 2) | ||
Theorem | symg2bas 19424 | 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 19422. (Contributed by AV, 9-Dec-2018.) (Proof shortened by AV, 16-Jun-2022.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼, 𝐽} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) | ||
Theorem | 0symgefmndeq 19425 | 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 19426 | The symmetric group on a singleton 𝐴 is identical with the monoid of endofunctions on 𝐴. (Contributed by AV, 31-Mar-2024.) |
⊢ (𝐴 = {𝑋} → (EndoFMnd‘𝐴) = (SymGrp‘𝐴)) | ||
Theorem | symgpssefmnd 19427 | 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 19428* | 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 19429* | Obsolete version of symgvalstruct 19428 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 19430 | 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 19431 | 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 19432 | 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 19433 | 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 19434 | 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 19435 | The symmetric group on a set 𝐴 is a submonoid of the monoid of endofunctions on 𝐴. Alternate proof based on issubmndb 18830 and not on injsubmefmnd 18922 and sursubmefmnd 18921. (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 19436* | 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 19437* | The converse of galactghm 19436. 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 19438 | The topology of the symmetric group on 𝐴. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐺 = (SymGrp‘𝑋) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺)) | ||
Theorem | symgga 19439* | The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ 𝐺 = (SymGrp‘𝑋) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐹 = (𝑓 ∈ 𝐵, 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥)) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐹 ∈ (𝐺 GrpAct 𝑋)) | ||
Theorem | pgrpsubgsymgbi 19440 | Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑃 ∈ (SubGrp‘𝐺) ↔ (𝑃 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑃) ∈ Grp))) | ||
Theorem | pgrpsubgsymg 19441* | 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 19442 | 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 19443 | 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 19444* | Lemma for cayley 19446. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐻 = (SymGrp‘𝑋) & ⊢ 𝑆 = (Base‘𝐻) & ⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎))) ⇒ ⊢ (𝐺 ∈ Grp → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | ||
Theorem | cayleylem2 19445* | Lemma for cayley 19446. (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 19446* | 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 19447* | 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 19448* | 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 19449* | The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019.) |
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) ⇒ ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸:𝑁⟶𝑁) | ||
Theorem | symgextfv 19450* | 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 19451* | 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 19452* | Lemma for symgextf1 19453. (Contributed by AV, 6-Jan-2019.) |
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) ⇒ ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ((𝑋 ∈ (𝑁 ∖ {𝐾}) ∧ 𝑌 ∈ {𝐾}) → (𝐸‘𝑋) ≠ (𝐸‘𝑌))) | ||
Theorem | symgextf1 19453* | 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 19454* | 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 19455* | 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 19456* | 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 19457* | 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 19458 | Homomorphic property of composites of permutations with a singleton. (Contributed by AV, 20-Jan-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ 〈“𝑍”〉)) = ((𝐺 Σg 𝑊) ∘ 𝑍)) | ||
Theorem | gsmsymgrfixlem1 19459* | Lemma 1 for gsmsymgrfix 19460. (Contributed by AV, 20-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(♯‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^((♯‘𝑊) + 1))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑊 ++ 〈“𝑃”〉))‘𝐾) = 𝐾)) | ||
Theorem | gsmsymgrfix 19460* | 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 19461* | 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 19462* | Lemma 1 for gsmsymgreq 19464. (Contributed by AV, 26-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑍 = (SymGrp‘𝑀) & ⊢ 𝑃 = (Base‘𝑍) & ⊢ 𝐼 = (𝑁 ∩ 𝑀) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) ∧ (𝐶‘𝐽) = (𝑅‘𝐽)) → ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝐽) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝐽))) | ||
Theorem | gsmsymgreqlem2 19463* | Lemma 2 for gsmsymgreq 19464. (Contributed by AV, 26-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑍 = (SymGrp‘𝑀) & ⊢ 𝑃 = (Base‘𝑍) & ⊢ 𝐼 = (𝑁 ∩ 𝑀) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (∀𝑖 ∈ (0..^(♯‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) | ||
Theorem | gsmsymgreq 19464* | 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 19465* | A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ⇒ ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝑄 ↔ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾))) | ||
Theorem | symgfixels 19466* | 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 19467* | 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 19468* | 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 19469* | 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 19470* | Lemma 1 for symgfixfo 19471. (Contributed by AV, 7-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} & ⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝐻 = (𝑞 ∈ 𝑄 ↦ (𝑞 ↾ (𝑁 ∖ {𝐾}))) & ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) ⇒ ⊢ ((𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸 ∈ 𝑄) | ||
Theorem | symgfixfo 19471* | 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 19472* | 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 19473 | Syntax for the transposition generator function. |
class pmTrsp | ||
Definition | df-pmtr 19474* | Define a function that generates the transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ pmTrsp = (𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) | ||
Theorem | f1omvdmvd 19475 | 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 19476 | 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 19477 | 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 19478 | 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 19479 | 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 19480 | 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 19481 | 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 19482* | The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ (𝐷 ∈ 𝑉 → 𝑇 = (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) | ||
Theorem | pmtrval 19483* | A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧))) | ||
Theorem | pmtrfv 19484 | General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) ∧ 𝑍 ∈ 𝐷) → ((𝑇‘𝑃)‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍)) | ||
Theorem | pmtrprfv 19485 | In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑋) = 𝑌) | ||
Theorem | pmtrprfv3 19486 | In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝑇‘{𝑋, 𝑌})‘𝑍) = 𝑍) | ||
Theorem | pmtrf 19487 | Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃):𝐷⟶𝐷) | ||
Theorem | pmtrmvd 19488 | A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → dom ((𝑇‘𝑃) ∖ I ) = 𝑃) | ||
Theorem | pmtrrn 19489 | Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) ∈ 𝑅) | ||
Theorem | pmtrfrn 19490 | 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 19491 | Mapping of a point under a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 & ⊢ 𝑃 = dom (𝐹 ∖ I ) ⇒ ⊢ ((𝐹 ∈ 𝑅 ∧ 𝑍 ∈ 𝐷) → (𝐹‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍)) | ||
Theorem | pmtrrn2 19492* | For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))) | ||
Theorem | pmtrfinv 19493 | A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) = ( I ↾ 𝐷)) | ||
Theorem | pmtrfmvdn0 19494 | A transposition moves at least one point. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≠ ∅) | ||
Theorem | pmtrff1o 19495 | A transposition function is a permutation. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → 𝐹:𝐷–1-1-onto→𝐷) | ||
Theorem | pmtrfcnv 19496 | A transposition function is its own inverse. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → ◡𝐹 = 𝐹) | ||
Theorem | pmtrfb 19497 | 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 19498 | Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ ((𝐹 ∈ 𝑅 ∧ 𝐺:𝐷–1-1-onto→𝐷) → ((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∈ 𝑅) | ||
Theorem | symgsssg 19499* | 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 19500* | 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‘𝐺)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |