P. 194 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19301-19400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oppgsubm 19301	Being a submonoid is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (SubMnd‘𝐺) = (SubMnd‘𝑂)
Theorem	oppgsubg 19302	Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (SubGrp‘𝐺) = (SubGrp‘𝑂)
Theorem	oppgcntz 19303	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 19304	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 19305	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‘𝑊)))
10.2.10  Symmetric groups
10.2.10.1  Definition and basic properties 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 19307. However, the set is allowed to be empty, see symgbas0 19326. Hint: The symmetric groups should not be confused with "symmetry groups" which is a different topic in group theory. In this context, the one-to-one onto functions are called permutations for short. Since the base set of symmetric groups on a set 𝐴 is the set of all permutations of 𝐴 (see symgbas 19309), we can formally say 𝑃 ∈ (SymGrp‘𝐴) expressing "𝑃 is a permutation of 𝐴" if we are not interested in the group (or topology) structure. In general, a permutation group "... is a group G whose elements are permutations of a given set M and whose group operation is the composition of permutations in G (which are thought of as bijective functions from the set M to itself)." (see Wikipedia "Permutation group", 17-Mar-2019, https://en.wikipedia.org/wiki/Permutation_group 19309). This means that a symmetric group is a permutation group, and each permutation group is a subgroup of a symmetric group (see pgrpsubgsymgbi 19345 and pgrpsubgsymg 19346). For example, the structure with the singleton containing only the identity function restricted to a set as base set and the function composition as group operation is a permutation group (group consisting of permutations), see idrespermg 19348, which is a (proper) subgroup of a symmetric group, see idressubgsymg 19347. As in [Rotman] p. 28 "Let 𝑥 ∈ 𝑋 and 𝑝 ∈ SymGrp(𝑋); we say 𝑝 fixes 𝑥 if (𝑝‘𝑥) = 𝑥; otherwise 𝑝 moves 𝑥.". The theorems starting with symgfix2 19353 are about fixed/moved elements.
Syntax	csymg 19306	Extend class notation to include the class of symmetric groups.
class SymGrp
Definition	df-symg 19307*	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 19308*	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 19309*	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 19310	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 19311	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 19312	Elements in the symmetric group are 1-1 onto functions. (Contributed by SO, 9-Jul-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴–1-1-onto→𝐴)
Theorem	symgbasf 19313	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 19314	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 19315	The symmetric group on 𝑛 objects has cardinality 𝑛!. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → (♯‘𝐵) = (!‘(♯‘𝐴)))
Theorem	symgbasfi 19316	The symmetric group on a finite index set is finite. (Contributed by SO, 9-Jul-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin)
Theorem	symgfv 19317	The function value of a permutation. (Contributed by AV, 1-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴)
Theorem	symgfvne 19318	The function values of a permutation for different arguments are different. (Contributed by AV, 8-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑍 → (𝑌 ≠ 𝑋 → (𝐹‘𝑌) ≠ 𝑍)))
Theorem	symgressbas 19319	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 19320*	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 19321	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 19322	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 19323	The identity function restricted to a set is a permutation of this set. (Contributed by AV, 17-Mar-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ (Base‘𝐺))
Theorem	symgmov1 19324*	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 19325*	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 19326	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 19327	The symmetric group on a singleton has cardinality 1. (Contributed by AV, 9-Dec-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (♯‘𝐵) = 1)
Theorem	symg1bas 19328	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 19329	The symmetric group on a (proper) pair has cardinality 2. (Contributed by AV, 9-Dec-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼, 𝐽}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 2)
Theorem	symg2bas 19330	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 19328. (Contributed by AV, 9-Dec-2018.) (Proof shortened by AV, 16-Jun-2022.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼, 𝐽}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 𝐵 = {{⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}, {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}})
Theorem	0symgefmndeq 19331	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 19332	The symmetric group on a singleton 𝐴 is identical with the monoid of endofunctions on 𝐴. (Contributed by AV, 31-Mar-2024.)
⊢ (𝐴 = {𝑋} → (EndoFMnd‘𝐴) = (SymGrp‘𝐴))
Theorem	symgpssefmnd 19333	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 19334*	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	symgsubmefmnd 19335	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 19336	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 19337	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 19338	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 19339	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 19340	The symmetric group on a set 𝐴 is a submonoid of the monoid of endofunctions on 𝐴. Alternate proof based on issubmndb 18739 and not on injsubmefmnd 18831 and sursubmefmnd 18830. (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 19341*	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 19342*	The converse of galactghm 19341. 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 19343	The topology of the symmetric group on 𝐴. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺))
Theorem	symgga 19344*	The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐹 = (𝑓 ∈ 𝐵, 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥))    ⇒   ⊢ (𝑋 ∈ 𝑉 → 𝐹 ∈ (𝐺 GrpAct 𝑋))
Theorem	pgrpsubgsymgbi 19345	Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝑃 ∈ (SubGrp‘𝐺) ↔ (𝑃 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑃) ∈ Grp)))
Theorem	pgrpsubgsymg 19346*	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 19347	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 19348	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‘𝐺)))
10.2.10.2  Cayley's theorem
Theorem	cayleylem1 19349*	Lemma for cayley 19351. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐻 = (SymGrp‘𝑋)    &   ⊢ 𝑆 = (Base‘𝐻)    &   ⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)))    ⇒   ⊢ (𝐺 ∈ Grp → 𝐹 ∈ (𝐺 GrpHom 𝐻))
Theorem	cayleylem2 19350*	Lemma for cayley 19351. (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 19351*	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 19352*	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→𝑠)
10.2.10.3  Permutations fixing one element
Theorem	symgfix2 19353*	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 19354*	The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019.)
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))    &   ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥)))    ⇒   ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸:𝑁⟶𝑁)
Theorem	symgextfv 19355*	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 19356*	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 19357*	Lemma for symgextf1 19358. (Contributed by AV, 6-Jan-2019.)
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))    &   ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥)))    ⇒   ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ((𝑋 ∈ (𝑁 ∖ {𝐾}) ∧ 𝑌 ∈ {𝐾}) → (𝐸‘𝑋) ≠ (𝐸‘𝑌)))
Theorem	symgextf1 19358*	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 19359*	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 19360*	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 19361*	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 19362*	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 19363	Homomorphic property of composites of permutations with a singleton. (Contributed by AV, 20-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ ⟨“𝑍”⟩)) = ((𝐺 Σg 𝑊) ∘ 𝑍))
Theorem	gsmsymgrfixlem1 19364*	Lemma 1 for gsmsymgrfix 19365. (Contributed by AV, 20-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(♯‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^((♯‘𝑊) + 1))(((𝑊 ++ ⟨“𝑃”⟩)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑊 ++ ⟨“𝑃”⟩))‘𝐾) = 𝐾))
Theorem	gsmsymgrfix 19365*	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 19366*	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 19367*	Lemma 1 for gsmsymgreq 19369. (Contributed by AV, 26-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑍 = (SymGrp‘𝑀)    &   ⊢ 𝑃 = (Base‘𝑍)    &   ⊢ 𝐼 = (𝑁 ∩ 𝑀)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) ∧ (𝐶‘𝐽) = (𝑅‘𝐽)) → ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝐽) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝐽)))
Theorem	gsmsymgreqlem2 19368*	Lemma 2 for gsmsymgreq 19369. (Contributed by AV, 26-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑍 = (SymGrp‘𝑀)    &   ⊢ 𝑃 = (Base‘𝑍)    &   ⊢ 𝐼 = (𝑁 ∩ 𝑀)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (∀𝑖 ∈ (0..^(♯‘(𝑋 ++ ⟨“𝐶”⟩)))∀𝑛 ∈ 𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛))))
Theorem	gsmsymgreq 19369*	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 19370*	A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}    ⇒   ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝑄 ↔ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)))
Theorem	symgfixels 19371*	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 19372*	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 19373*	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 19374*	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 19375*	Lemma 1 for symgfixfo 19376. (Contributed by AV, 7-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}    &   ⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))    &   ⊢ 𝐻 = (𝑞 ∈ 𝑄 ↦ (𝑞 ↾ (𝑁 ∖ {𝐾})))    &   ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥)))    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸 ∈ 𝑄)
Theorem	symgfixfo 19376*	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 19377*	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→𝑆)
10.2.10.4  Transpositions in the symmetric group 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.". We (currently) do not have/need a definition for cycles, so transpositions are explicitly defined in df-pmtr 19379.
Syntax	cpmtr 19378	Syntax for the transposition generator function.
class pmTrsp
Definition	df-pmtr 19379*	Define a function that generates the transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ pmTrsp = (𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))
Theorem	f1omvdmvd 19380	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 19381	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 19382	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 19383	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 19384	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 19385	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 19386	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 19387*	The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝑇 = (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))
Theorem	pmtrval 19388*	A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧)))
Theorem	pmtrfv 19389	General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) ∧ 𝑍 ∈ 𝐷) → ((𝑇‘𝑃)‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍))
Theorem	pmtrprfv 19390	In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑋) = 𝑌)
Theorem	pmtrprfv3 19391	In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝑇‘{𝑋, 𝑌})‘𝑍) = 𝑍)
Theorem	pmtrf 19392	Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃):𝐷⟶𝐷)
Theorem	pmtrmvd 19393	A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → dom ((𝑇‘𝑃) ∖ I ) = 𝑃)
Theorem	pmtrrn 19394	Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) ∈ 𝑅)
Theorem	pmtrfrn 19395	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 19396	Mapping of a point under a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    &   ⊢ 𝑃 = dom (𝐹 ∖ I )    ⇒   ⊢ ((𝐹 ∈ 𝑅 ∧ 𝑍 ∈ 𝐷) → (𝐹‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍))
Theorem	pmtrrn2 19397*	For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))
Theorem	pmtrfinv 19398	A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) = ( I ↾ 𝐷))
Theorem	pmtrfmvdn0 19399	A transposition moves at least one point. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≠ ∅)
Theorem	pmtrff1o 19400	A transposition function is a permutation. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → 𝐹:𝐷–1-1-onto→𝐷)