Home | Metamath
Proof Explorer Theorem List (p. 185 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cntri 18401 | Defining property of the center of a group. (Contributed by Mario Carneiro, 22-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝑍 = (Cntr‘𝑀) ⇒ ⊢ ((𝑋 ∈ 𝑍 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋)) | ||
Theorem | resscntz 18402 | Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝐴) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝑌 = (Cntz‘𝐻) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑌‘𝑆) = ((𝑍‘𝑆) ∩ 𝐴)) | ||
Theorem | cntz2ss 18403 | Centralizers reverse the subset relation. (Contributed by Mario Carneiro, 3-Oct-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆) → (𝑍‘𝑆) ⊆ (𝑍‘𝑇)) | ||
Theorem | cntzrec 18404 | Reciprocity relationship for centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑆 ⊆ (𝑍‘𝑇) ↔ 𝑇 ⊆ (𝑍‘𝑆))) | ||
Theorem | cntziinsn 18405* | Express any centralizer as an intersection of singleton centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = (𝐵 ∩ ∩ 𝑥 ∈ 𝑆 (𝑍‘{𝑥}))) | ||
Theorem | cntzsubm 18406 | Centralizers in a monoid are submonoids. (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubMnd‘𝑀)) | ||
Theorem | cntzsubg 18407 | Centralizers in a group are subgroups. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubGrp‘𝑀)) | ||
Theorem | cntzidss 18408 | If the elements of 𝑆 commute, the elements of a subset 𝑇 also commute. (Contributed by Mario Carneiro, 25-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ 𝑇 ⊆ 𝑆) → 𝑇 ⊆ (𝑍‘𝑇)) | ||
Theorem | cntzmhm 18409 | Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝑌 = (Cntz‘𝐻) ⇒ ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → (𝐹‘𝐴) ∈ (𝑌‘(𝐹 “ 𝑆))) | ||
Theorem | cntzmhm2 18410 | Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝑌 = (Cntz‘𝐻) ⇒ ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑆 ⊆ (𝑍‘𝑇)) → (𝐹 “ 𝑆) ⊆ (𝑌‘(𝐹 “ 𝑇))) | ||
Theorem | cntrsubgnsg 18411 | A central subgroup is normal. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝑍 = (Cntr‘𝑀) ⇒ ⊢ ((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) → 𝑋 ∈ (NrmSGrp‘𝑀)) | ||
Theorem | cntrnsg 18412 | The center of a group is a normal subgroup. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
⊢ 𝑍 = (Cntr‘𝑀) ⇒ ⊢ (𝑀 ∈ Grp → 𝑍 ∈ (NrmSGrp‘𝑀)) | ||
Syntax | coppg 18413 | The opposite group operation. |
class oppg | ||
Definition | df-oppg 18414 | Define an opposite group, which is the same as the original group but with addition written the other way around. df-oppr 19304 does the same thing for multiplication. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
⊢ oppg = (𝑤 ∈ V ↦ (𝑤 sSet 〈(+g‘ndx), tpos (+g‘𝑤)〉)) | ||
Theorem | oppgval 18415 | Value of the opposite group. (Contributed by Stefan O'Rear, 25-Aug-2015.) (Revised by Mario Carneiro, 16-Sep-2015.) (Revised by Fan Zheng, 26-Jun-2016.) |
⊢ + = (+g‘𝑅) & ⊢ 𝑂 = (oppg‘𝑅) ⇒ ⊢ 𝑂 = (𝑅 sSet 〈(+g‘ndx), tpos + 〉) | ||
Theorem | oppgplusfval 18416 | Value of the addition operation of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Fan Zheng, 26-Jun-2016.) |
⊢ + = (+g‘𝑅) & ⊢ 𝑂 = (oppg‘𝑅) & ⊢ ✚ = (+g‘𝑂) ⇒ ⊢ ✚ = tpos + | ||
Theorem | oppgplus 18417 | Value of the addition operation of an opposite ring. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Fan Zheng, 26-Jun-2016.) |
⊢ + = (+g‘𝑅) & ⊢ 𝑂 = (oppg‘𝑅) & ⊢ ✚ = (+g‘𝑂) ⇒ ⊢ (𝑋 ✚ 𝑌) = (𝑌 + 𝑋) | ||
Theorem | oppglem 18418 | Lemma for oppgbas 18419. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐸 = Slot 𝑁 & ⊢ 𝑁 ∈ ℕ & ⊢ 𝑁 ≠ 2 ⇒ ⊢ (𝐸‘𝑅) = (𝐸‘𝑂) | ||
Theorem | oppgbas 18419 | Base set of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ 𝐵 = (Base‘𝑂) | ||
Theorem | oppgtset 18420 | Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐽 = (TopSet‘𝑅) ⇒ ⊢ 𝐽 = (TopSet‘𝑂) | ||
Theorem | oppgtopn 18421 | Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐽 = (TopOpen‘𝑅) ⇒ ⊢ 𝐽 = (TopOpen‘𝑂) | ||
Theorem | oppgmnd 18422 | The opposite of a monoid is a monoid. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 16-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝑅) ⇒ ⊢ (𝑅 ∈ Mnd → 𝑂 ∈ Mnd) | ||
Theorem | oppgmndb 18423 | Bidirectional form of oppgmnd 18422. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) ⇒ ⊢ (𝑅 ∈ Mnd ↔ 𝑂 ∈ Mnd) | ||
Theorem | oppgid 18424 | Zero in a monoid is a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.) (Revised by Mario Carneiro, 16-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ 0 = (0g‘𝑂) | ||
Theorem | oppggrp 18425 | The opposite of a group is a group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) ⇒ ⊢ (𝑅 ∈ Grp → 𝑂 ∈ Grp) | ||
Theorem | oppggrpb 18426 | Bidirectional form of oppggrp 18425. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) ⇒ ⊢ (𝑅 ∈ Grp ↔ 𝑂 ∈ Grp) | ||
Theorem | oppginv 18427 | Inverses in a group are a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝑅) & ⊢ 𝐼 = (invg‘𝑅) ⇒ ⊢ (𝑅 ∈ Grp → 𝐼 = (invg‘𝑂)) | ||
Theorem | invoppggim 18428 | The inverse is an antiautomorphism on any group. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐼 ∈ (𝐺 GrpIso 𝑂)) | ||
Theorem | oppggic 18429 | Every group is (naturally) isomorphic to its opposite. (Contributed by Stefan O'Rear, 26-Aug-2015.) |
⊢ 𝑂 = (oppg‘𝐺) ⇒ ⊢ (𝐺 ∈ Grp → 𝐺 ≃𝑔 𝑂) | ||
Theorem | oppgsubm 18430 | Being a submonoid is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝐺) ⇒ ⊢ (SubMnd‘𝐺) = (SubMnd‘𝑂) | ||
Theorem | oppgsubg 18431 | Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.) |
⊢ 𝑂 = (oppg‘𝐺) ⇒ ⊢ (SubGrp‘𝐺) = (SubGrp‘𝑂) | ||
Theorem | oppgcntz 18432 | A centralizer in a group is the same as the centralizer in the opposite group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝑂 = (oppg‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝑍‘𝐴) = ((Cntz‘𝑂)‘𝐴) | ||
Theorem | oppgcntr 18433 | The center of a group is the same as the center of the opposite group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝑂 = (oppg‘𝐺) & ⊢ 𝑍 = (Cntr‘𝐺) ⇒ ⊢ 𝑍 = (Cntr‘𝑂) | ||
Theorem | gsumwrev 18434 | A sum in an opposite monoid is the regular sum of a reversed word. (Contributed by Stefan O'Rear, 27-Aug-2015.) (Proof shortened by Mario Carneiro, 28-Feb-2016.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑂 = (oppg‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝑂 Σg 𝑊) = (𝑀 Σg (reverse‘𝑊))) | ||
According to Wikipedia ("Symmetric group", 09-Mar-2019,
https://en.wikipedia.org/wiki/symmetric_group) "In abstract algebra, the
symmetric group defined over any set is the group whose elements are all the
bijections from the set to itself, and whose group operation is the composition
of functions." and according to Encyclopedia of Mathematics ("Symmetric group",
09-Mar-2019, https://www.encyclopediaofmath.org/index.php/Symmetric_group)
"The group of all permutations (self-bijections) of a set with the operation of
composition (see Permutation group).". In [Rotman] p. 27 "If X is a nonempty
set, a permutation of X is a function a : X -> X that is a one-to-one
correspondence." and "If X is a nonempty set, the symmetric group on X, denoted
SX, is the group whose elements are the permutations of X and whose
binary operation is composition of functions.". Therefore, we define the
symmetric group on a set 𝐴 as the set of one-to-one onto functions
from 𝐴 to itself under function composition, see df-symg 18436. However, the
set is allowed to be empty, see symgbas0 18453. Hint: The symmetric groups
should not be confused with "symmetry groups" which is a different topic in
group theory.
| ||
Syntax | csymg 18435 | Extend class notation to include the class of symmetric groups. |
class SymGrp | ||
Definition | df-symg 18436* | 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. (Contributed by Paul Chapman, 25-Feb-2008.) |
⊢ SymGrp = (𝑥 ∈ V ↦ ⦋{ℎ ∣ ℎ:𝑥–1-1-onto→𝑥} / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))〉, 〈(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))〉}) | ||
Theorem | symgval 18437* | The value of the symmetric group function at 𝐴. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by Mario Carneiro, 12-Jan-2015.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} & ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔)) & ⊢ 𝐽 = (∏t‘(𝐴 × {𝒫 𝐴})) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉}) | ||
Theorem | symgbas 18438* | The base set of the symmetric group. (Contributed by Mario Carneiro, 12-Jan-2015.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 = {𝑥 ∣ 𝑥:𝐴–1-1-onto→𝐴} | ||
Theorem | elsymgbas2 18439 | 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 18440 | 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 18441 | Elements in the symmetric group are 1-1 onto functions. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴–1-1-onto→𝐴) | ||
Theorem | symgbasf 18442 | A permutation (element of the symmetric group) is a function from a set into itself. (Contributed by AV, 1-Jan-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴⟶𝐴) | ||
Theorem | symghash 18443 | The symmetric group on 𝑛 objects has cardinality 𝑛!. (Contributed by Mario Carneiro, 22-Jan-2015.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ Fin → (♯‘𝐵) = (!‘(♯‘𝐴))) | ||
Theorem | symgbasfi 18444 | The symmetric group on a finite index set is finite. (Contributed by SO, 9-Jul-2018.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin) | ||
Theorem | symgfv 18445 | The function value of a permutation. (Contributed by AV, 1-Jan-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴) | ||
Theorem | symgfvne 18446 | The function values of a permutation for different arguments are different. (Contributed by AV, 8-Jan-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑍 → (𝑌 ≠ 𝑋 → (𝐹‘𝑌) ≠ 𝑍))) | ||
Theorem | symgplusg 18447* | 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.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔)) | ||
Theorem | symgov 18448 | 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 18449 | 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 18450 | The identity function restricted to a set is a permutation of this set. (Contributed by AV, 17-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ (Base‘𝐺)) | ||
Theorem | symgmov1 18451* | 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 18452* | 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 18453 | 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 18454 | The symmetric group on a singleton has cardinality 1. (Contributed by AV, 9-Dec-2018.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼} ⇒ ⊢ (𝐼 ∈ 𝑉 → (♯‘𝐵) = 1) | ||
Theorem | symg1bas 18455 | 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 18456 | The symmetric group on a (proper) pair has cardinality 2. (Contributed by AV, 9-Dec-2018.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼, 𝐽} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 2) | ||
Theorem | symg2bas 18457 | 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 18455. (Contributed by AV, 9-Dec-2018.) (Proof shortened by AV, 16-Jun-2022.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼, 𝐽} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 𝐵 = {{〈𝐼, 𝐼〉, 〈𝐽, 𝐽〉}, {〈𝐼, 𝐽〉, 〈𝐽, 𝐼〉}}) | ||
Theorem | symggrplem 18458* | Lemma for symggrp 18460 and efmndsgrp 43953. Conditions for an operation to be associative. Formerly part of proof for symggrp 18460. (Contributed by AV, 28-Jan-2024.) |
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑥 ∘ 𝑦)) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | symgtset 18459 | 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 18460 | 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 18461 | 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 18462 | 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 18463* | 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 18464* | The converse of galactghm 18463. 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 18465 | The topology of the symmetric group on 𝐴. (Contributed by Mario Carneiro, 29-Aug-2015.) |
⊢ 𝐺 = (SymGrp‘𝑋) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺)) | ||
Theorem | symgga 18466* | The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015.) |
⊢ 𝐺 = (SymGrp‘𝑋) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐹 = (𝑓 ∈ 𝐵, 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥)) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝐹 ∈ (𝐺 GrpAct 𝑋)) | ||
Theorem | pgrpsubgsymgbi 18467 | Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝑃 ∈ (SubGrp‘𝐺) ↔ (𝑃 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑃) ∈ Grp))) | ||
Theorem | pgrpsubgsymg 18468* | Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐹 = (Base‘𝑃) ⇒ ⊢ (𝐴 ∈ 𝑉 → ((𝑃 ∈ Grp ∧ 𝐹 ⊆ 𝐵 ∧ (+g‘𝑃) = (𝑓 ∈ 𝐹, 𝑔 ∈ 𝐹 ↦ (𝑓 ∘ 𝑔))) → 𝐹 ∈ (SubGrp‘𝐺))) | ||
Theorem | idressubgsymg 18469 | 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 18470 | 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 18471* | Lemma for cayley 18473. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐻 = (SymGrp‘𝑋) & ⊢ 𝑆 = (Base‘𝐻) & ⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎))) ⇒ ⊢ (𝐺 ∈ Grp → 𝐹 ∈ (𝐺 GrpHom 𝐻)) | ||
Theorem | cayleylem2 18472* | Lemma for cayley 18473. (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 18473* | 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 18474* | 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 18475* | 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 18476* | The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019.) |
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) ⇒ ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸:𝑁⟶𝑁) | ||
Theorem | symgextfv 18477* | 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 18478* | 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 18479* | Lemma for symgextf1 18480. (Contributed by AV, 6-Jan-2019.) |
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) ⇒ ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ((𝑋 ∈ (𝑁 ∖ {𝐾}) ∧ 𝑌 ∈ {𝐾}) → (𝐸‘𝑋) ≠ (𝐸‘𝑌))) | ||
Theorem | symgextf1 18480* | 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 18481* | 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 18482* | 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 18483* | 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 18484* | 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 18485 | Homomorphic property of composites of permutations with a singleton. (Contributed by AV, 20-Jan-2019.) |
⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ 〈“𝑍”〉)) = ((𝐺 Σg 𝑊) ∘ 𝑍)) | ||
Theorem | gsmsymgrfixlem1 18486* | Lemma 1 for gsmsymgrfix 18487. (Contributed by AV, 20-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(♯‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^((♯‘𝑊) + 1))(((𝑊 ++ 〈“𝑃”〉)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑊 ++ 〈“𝑃”〉))‘𝐾) = 𝐾)) | ||
Theorem | gsmsymgrfix 18487* | 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 18488* | 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 18489* | Lemma 1 for gsmsymgreq 18491. (Contributed by AV, 26-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑍 = (SymGrp‘𝑀) & ⊢ 𝑃 = (Base‘𝑍) & ⊢ 𝐼 = (𝑁 ∩ 𝑀) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) ∧ (𝐶‘𝐽) = (𝑅‘𝐽)) → ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝐽) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝐽))) | ||
Theorem | gsmsymgreqlem2 18490* | Lemma 2 for gsmsymgreq 18491. (Contributed by AV, 26-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑍 = (SymGrp‘𝑀) & ⊢ 𝑃 = (Base‘𝑍) & ⊢ 𝐼 = (𝑁 ∩ 𝑀) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (∀𝑖 ∈ (0..^(♯‘(𝑋 ++ 〈“𝐶”〉)))∀𝑛 ∈ 𝐼 (((𝑋 ++ 〈“𝐶”〉)‘𝑖)‘𝑛) = (((𝑌 ++ 〈“𝑅”〉)‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ 〈“𝐶”〉))‘𝑛) = ((𝑍 Σg (𝑌 ++ 〈“𝑅”〉))‘𝑛)))) | ||
Theorem | gsmsymgreq 18491* | 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 18492* | A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} ⇒ ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝑄 ↔ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾))) | ||
Theorem | symgfixels 18493* | 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 18494* | 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 18495* | 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 18496* | 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 18497* | Lemma 1 for symgfixfo 18498. (Contributed by AV, 7-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾} & ⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾}))) & ⊢ 𝐻 = (𝑞 ∈ 𝑄 ↦ (𝑞 ↾ (𝑁 ∖ {𝐾}))) & ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥))) ⇒ ⊢ ((𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸 ∈ 𝑄) | ||
Theorem | symgfixfo 18498* | 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 18499* | 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 18500 | Syntax for the transposition generator function. |
class pmTrsp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |