P. 196 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19501-19600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	oppglt 19501	less-than relation of an opposite group. (Contributed by Thierry Arnoux, 13-Apr-2018.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ < = (lt‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → < = (lt‘𝑂))
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 19503. However, the set is allowed to be empty, see symgbas0 19522. 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 19505), 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 19505). This means that a symmetric group is a permutation group, and each permutation group is a subgroup of a symmetric group (see pgrpsubgsymgbi 19541 and pgrpsubgsymg 19542). 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 19544, which is a (proper) subgroup of a symmetric group, see idressubgsymg 19543. As in [Rotman] p. 28 "Let 𝑥 ∈ 𝑋 and 𝑝 ∈ SymGrp(𝑋); we say 𝑝 fixes 𝑥 if (𝑝‘𝑥) = 𝑥; otherwise 𝑝 moves 𝑥.". The theorems starting with symgfix2 19549 are about fixed/moved elements.
Syntax	csymg 19502	Extend class notation to include the class of symmetric groups.
class SymGrp
Definition	df-symg 19503*	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 19504*	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 19505*	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 19506	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 19507	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 19508	Elements in the symmetric group are 1-1 onto functions. (Contributed by SO, 9-Jul-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴–1-1-onto→𝐴)
Theorem	symgbasf 19509	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 19510	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 19511	The symmetric group on 𝑛 objects has cardinality 𝑛!. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → (♯‘𝐵) = (!‘(♯‘𝐴)))
Theorem	symgbasfi 19512	The symmetric group on a finite index set is finite. (Contributed by SO, 9-Jul-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin)
Theorem	symgfv 19513	The function value of a permutation. (Contributed by AV, 1-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴)
Theorem	symgfvne 19514	The function values of a permutation for different arguments are different. (Contributed by AV, 8-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑍 → (𝑌 ≠ 𝑋 → (𝐹‘𝑌) ≠ 𝑍)))
Theorem	symgressbas 19515	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 19516*	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 19517	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 19518	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 19519	The identity function restricted to a set is a permutation of this set. (Contributed by AV, 17-Mar-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ (Base‘𝐺))
Theorem	symgmov1 19520*	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 19521*	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 19522	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 19523	The symmetric group on a singleton has cardinality 1. (Contributed by AV, 9-Dec-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (♯‘𝐵) = 1)
Theorem	symg1bas 19524	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 19525	The symmetric group on a (proper) pair has cardinality 2. (Contributed by AV, 9-Dec-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼, 𝐽}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 2)
Theorem	symg2bas 19526	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 19524. (Contributed by AV, 9-Dec-2018.) (Proof shortened by AV, 16-Jun-2022.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼, 𝐽}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 𝐵 = {{⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}, {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}})
Theorem	0symgefmndeq 19527	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 19528	The symmetric group on a singleton 𝐴 is identical with the monoid of endofunctions on 𝐴. (Contributed by AV, 31-Mar-2024.)
⊢ (𝐴 = {𝑋} → (EndoFMnd‘𝐴) = (SymGrp‘𝐴))
Theorem	symgpssefmnd 19529	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 19530*	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 19531	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 19532	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 19533	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 19534	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 19535	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 19536	The symmetric group on a set 𝐴 is a submonoid of the monoid of endofunctions on 𝐴. Alternate proof based on issubmndb 18919 and not on injsubmefmnd 19012 and sursubmefmnd 19011. (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 19537*	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 19538*	The converse of galactghm 19537. 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 19539	The topology of the symmetric group on 𝐴. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺))
Theorem	symgga 19540*	The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐹 = (𝑓 ∈ 𝐵, 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥))    ⇒   ⊢ (𝑋 ∈ 𝑉 → 𝐹 ∈ (𝐺 GrpAct 𝑋))
Theorem	pgrpsubgsymgbi 19541	Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝑃 ∈ (SubGrp‘𝐺) ↔ (𝑃 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑃) ∈ Grp)))
Theorem	pgrpsubgsymg 19542*	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 19543	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 19544	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 19545*	Lemma for cayley 19547. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐻 = (SymGrp‘𝑋)    &   ⊢ 𝑆 = (Base‘𝐻)    &   ⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)))    ⇒   ⊢ (𝐺 ∈ Grp → 𝐹 ∈ (𝐺 GrpHom 𝐻))
Theorem	cayleylem2 19546*	Lemma for cayley 19547. (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 19547*	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 19548*	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 19549*	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 19550*	The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019.)
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))    &   ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥)))    ⇒   ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸:𝑁⟶𝑁)
Theorem	symgextfv 19551*	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 19552*	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 19553*	Lemma for symgextf1 19554. (Contributed by AV, 6-Jan-2019.)
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))    &   ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥)))    ⇒   ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ((𝑋 ∈ (𝑁 ∖ {𝐾}) ∧ 𝑌 ∈ {𝐾}) → (𝐸‘𝑋) ≠ (𝐸‘𝑌)))
Theorem	symgextf1 19554*	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 19555*	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 19556*	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 19557*	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 19558*	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 19559	Homomorphic property of composites of permutations with a singleton. (Contributed by AV, 20-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ ⟨“𝑍”⟩)) = ((𝐺 Σg 𝑊) ∘ 𝑍))
Theorem	gsmsymgrfixlem1 19560*	Lemma 1 for gsmsymgrfix 19561. (Contributed by AV, 20-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(♯‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^((♯‘𝑊) + 1))(((𝑊 ++ ⟨“𝑃”⟩)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑊 ++ ⟨“𝑃”⟩))‘𝐾) = 𝐾))
Theorem	gsmsymgrfix 19561*	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 19562*	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 19563*	Lemma 1 for gsmsymgreq 19565. (Contributed by AV, 26-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑍 = (SymGrp‘𝑀)    &   ⊢ 𝑃 = (Base‘𝑍)    &   ⊢ 𝐼 = (𝑁 ∩ 𝑀)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) ∧ (𝐶‘𝐽) = (𝑅‘𝐽)) → ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝐽) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝐽)))
Theorem	gsmsymgreqlem2 19564*	Lemma 2 for gsmsymgreq 19565. (Contributed by AV, 26-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑍 = (SymGrp‘𝑀)    &   ⊢ 𝑃 = (Base‘𝑍)    &   ⊢ 𝐼 = (𝑁 ∩ 𝑀)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (∀𝑖 ∈ (0..^(♯‘(𝑋 ++ ⟨“𝐶”⟩)))∀𝑛 ∈ 𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛))))
Theorem	gsmsymgreq 19565*	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 19566*	A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}    ⇒   ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝑄 ↔ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)))
Theorem	symgfixels 19567*	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 19568*	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 19569*	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 19570*	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 19571*	Lemma 1 for symgfixfo 19572. (Contributed by AV, 7-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}    &   ⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))    &   ⊢ 𝐻 = (𝑞 ∈ 𝑄 ↦ (𝑞 ↾ (𝑁 ∖ {𝐾})))    &   ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥)))    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸 ∈ 𝑄)
Theorem	symgfixfo 19572*	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 19573*	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 19575.
Syntax	cpmtr 19574	Syntax for the transposition generator function.
class pmTrsp
Definition	df-pmtr 19575*	Define a function that generates the transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ pmTrsp = (𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))
Theorem	f1omvdmvd 19576	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 19577	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 19578	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 19579	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 19580	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 19581	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 19582	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 19583*	The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝑇 = (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))
Theorem	pmtrval 19584*	A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧)))
Theorem	pmtrfv 19585	General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) ∧ 𝑍 ∈ 𝐷) → ((𝑇‘𝑃)‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍))
Theorem	pmtrprfv 19586	In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑋) = 𝑌)
Theorem	pmtrprfv3 19587	In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝑇‘{𝑋, 𝑌})‘𝑍) = 𝑍)
Theorem	pmtrf 19588	Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃):𝐷⟶𝐷)
Theorem	pmtrmvd 19589	A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → dom ((𝑇‘𝑃) ∖ I ) = 𝑃)
Theorem	pmtrrn 19590	Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) ∈ 𝑅)
Theorem	pmtrfrn 19591	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 19592	Mapping of a point under a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    &   ⊢ 𝑃 = dom (𝐹 ∖ I )    ⇒   ⊢ ((𝐹 ∈ 𝑅 ∧ 𝑍 ∈ 𝐷) → (𝐹‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍))
Theorem	pmtrrn2 19593*	For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))
Theorem	pmtrfinv 19594	A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) = ( I ↾ 𝐷))
Theorem	pmtrfmvdn0 19595	A transposition moves at least one point. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≠ ∅)
Theorem	pmtrff1o 19596	A transposition function is a permutation. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → 𝐹:𝐷–1-1-onto→𝐷)
Theorem	pmtrfcnv 19597	A transposition function is its own inverse. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → ◡𝐹 = 𝐹)
Theorem	pmtrfb 19598	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 19599	Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ ((𝐹 ∈ 𝑅 ∧ 𝐺:𝐷–1-1-onto→𝐷) → ((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∈ 𝑅)
Theorem	symgsssg 19600*	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‘𝐺))