P. 191 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19001-19100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	symgcl 19001	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 19002	The identity function restricted to a set is a permutation of this set. (Contributed by AV, 17-Mar-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ (Base‘𝐺))
Theorem	symgmov1 19003*	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 19004*	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 19005	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 19006	The symmetric group on a singleton has cardinality 1. (Contributed by AV, 9-Dec-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (♯‘𝐵) = 1)
Theorem	symg1bas 19007	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 19008	The symmetric group on a (proper) pair has cardinality 2. (Contributed by AV, 9-Dec-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼, 𝐽}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 2)
Theorem	symg2bas 19009	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 19007. (Contributed by AV, 9-Dec-2018.) (Proof shortened by AV, 16-Jun-2022.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼, 𝐽}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 𝐵 = {{⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}, {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}})
Theorem	0symgefmndeq 19010	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 19011	The symmetric group on a singleton 𝐴 is identical with the monoid of endofunctions on 𝐴. (Contributed by AV, 31-Mar-2024.)
⊢ (𝐴 = {𝑋} → (EndoFMnd‘𝐴) = (SymGrp‘𝐴))
Theorem	symgpssefmnd 19012	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 19013*	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 19014*	Obsolete proof of symgvalstruct 19013 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 19015	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 19016	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 19017	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 19018	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 19019	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 19020	The symmetric group on a set 𝐴 is a submonoid of the monoid of endofunctions on 𝐴. Alternate proof based on issubmndb 18453 and not on injsubmefmnd 18545 and sursubmefmnd 18544. (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 19021*	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 19022*	The converse of galactghm 19021. 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 19023	The topology of the symmetric group on 𝐴. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺))
Theorem	symgga 19024*	The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐹 = (𝑓 ∈ 𝐵, 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥))    ⇒   ⊢ (𝑋 ∈ 𝑉 → 𝐹 ∈ (𝐺 GrpAct 𝑋))
Theorem	pgrpsubgsymgbi 19025	Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝑃 ∈ (SubGrp‘𝐺) ↔ (𝑃 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑃) ∈ Grp)))
Theorem	pgrpsubgsymg 19026*	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 19027	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 19028	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 19029*	Lemma for cayley 19031. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐻 = (SymGrp‘𝑋)    &   ⊢ 𝑆 = (Base‘𝐻)    &   ⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)))    ⇒   ⊢ (𝐺 ∈ Grp → 𝐹 ∈ (𝐺 GrpHom 𝐻))
Theorem	cayleylem2 19030*	Lemma for cayley 19031. (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 19031*	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 19032*	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 19033*	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 19034*	The extension of a permutation, fixing the additional element, is a function. (Contributed by AV, 6-Jan-2019.)
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))    &   ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥)))    ⇒   ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸:𝑁⟶𝑁)
Theorem	symgextfv 19035*	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 19036*	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 19037*	Lemma for symgextf1 19038. (Contributed by AV, 6-Jan-2019.)
⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))    &   ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥)))    ⇒   ⊢ ((𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → ((𝑋 ∈ (𝑁 ∖ {𝐾}) ∧ 𝑌 ∈ {𝐾}) → (𝐸‘𝑋) ≠ (𝐸‘𝑌)))
Theorem	symgextf1 19038*	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 19039*	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 19040*	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 19041*	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 19042*	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 19043	Homomorphic property of composites of permutations with a singleton. (Contributed by AV, 20-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ ⟨“𝑍”⟩)) = ((𝐺 Σg 𝑊) ∘ 𝑍))
Theorem	gsmsymgrfixlem1 19044*	Lemma 1 for gsmsymgrfix 19045. (Contributed by AV, 20-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (((𝑊 ∈ Word 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ (𝑁 ∈ Fin ∧ 𝐾 ∈ 𝑁) ∧ (∀𝑖 ∈ (0..^(♯‘𝑊))((𝑊‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg 𝑊)‘𝐾) = 𝐾)) → (∀𝑖 ∈ (0..^((♯‘𝑊) + 1))(((𝑊 ++ ⟨“𝑃”⟩)‘𝑖)‘𝐾) = 𝐾 → ((𝑆 Σg (𝑊 ++ ⟨“𝑃”⟩))‘𝐾) = 𝐾))
Theorem	gsmsymgrfix 19045*	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 19046*	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 19047*	Lemma 1 for gsmsymgreq 19049. (Contributed by AV, 26-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑍 = (SymGrp‘𝑀)    &   ⊢ 𝑃 = (Base‘𝑍)    &   ⊢ 𝐼 = (𝑁 ∩ 𝑀)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin ∧ 𝐽 ∈ 𝐼) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛) ∧ (𝐶‘𝐽) = (𝑅‘𝐽)) → ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝐽) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝐽)))
Theorem	gsmsymgreqlem2 19048*	Lemma 2 for gsmsymgreq 19049. (Contributed by AV, 26-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑍 = (SymGrp‘𝑀)    &   ⊢ 𝑃 = (Base‘𝑍)    &   ⊢ 𝐼 = (𝑁 ∩ 𝑀)    ⇒   ⊢ (((𝑁 ∈ Fin ∧ 𝑀 ∈ Fin) ∧ ((𝑋 ∈ Word 𝐵 ∧ 𝐶 ∈ 𝐵) ∧ (𝑌 ∈ Word 𝑃 ∧ 𝑅 ∈ 𝑃) ∧ (♯‘𝑋) = (♯‘𝑌))) → ((∀𝑖 ∈ (0..^(♯‘𝑋))∀𝑛 ∈ 𝐼 ((𝑋‘𝑖)‘𝑛) = ((𝑌‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg 𝑋)‘𝑛) = ((𝑍 Σg 𝑌)‘𝑛)) → (∀𝑖 ∈ (0..^(♯‘(𝑋 ++ ⟨“𝐶”⟩)))∀𝑛 ∈ 𝐼 (((𝑋 ++ ⟨“𝐶”⟩)‘𝑖)‘𝑛) = (((𝑌 ++ ⟨“𝑅”⟩)‘𝑖)‘𝑛) → ∀𝑛 ∈ 𝐼 ((𝑆 Σg (𝑋 ++ ⟨“𝐶”⟩))‘𝑛) = ((𝑍 Σg (𝑌 ++ ⟨“𝑅”⟩))‘𝑛))))
Theorem	gsmsymgreq 19049*	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 19050*	A permutation of a set fixing an element of the set. (Contributed by AV, 4-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}    ⇒   ⊢ (𝐹 ∈ 𝑉 → (𝐹 ∈ 𝑄 ↔ (𝐹:𝑁–1-1-onto→𝑁 ∧ (𝐹‘𝐾) = 𝐾)))
Theorem	symgfixels 19051*	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 19052*	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 19053*	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 19054*	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 19055*	Lemma 1 for symgfixfo 19056. (Contributed by AV, 7-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑄 = {𝑞 ∈ 𝑃 ∣ (𝑞‘𝐾) = 𝐾}    &   ⊢ 𝑆 = (Base‘(SymGrp‘(𝑁 ∖ {𝐾})))    &   ⊢ 𝐻 = (𝑞 ∈ 𝑄 ↦ (𝑞 ↾ (𝑁 ∖ {𝐾})))    &   ⊢ 𝐸 = (𝑥 ∈ 𝑁 ↦ if(𝑥 = 𝐾, 𝐾, (𝑍‘𝑥)))    ⇒   ⊢ ((𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆) → 𝐸 ∈ 𝑄)
Theorem	symgfixfo 19056*	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 19057*	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 19059.
Syntax	cpmtr 19058	Syntax for the transposition generator function.
class pmTrsp
Definition	df-pmtr 19059*	Define a function that generates the transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ pmTrsp = (𝑑 ∈ V ↦ (𝑝 ∈ {𝑦 ∈ 𝒫 𝑑 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝑑 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))
Theorem	f1omvdmvd 19060	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 19061	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 19062	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 19063	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 19064	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 19065	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 19066	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 19067*	The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝑇 = (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))
Theorem	pmtrval 19068*	A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧)))
Theorem	pmtrfv 19069	General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) ∧ 𝑍 ∈ 𝐷) → ((𝑇‘𝑃)‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍))
Theorem	pmtrprfv 19070	In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑋) = 𝑌)
Theorem	pmtrprfv3 19071	In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝑇‘{𝑋, 𝑌})‘𝑍) = 𝑍)
Theorem	pmtrf 19072	Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃):𝐷⟶𝐷)
Theorem	pmtrmvd 19073	A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → dom ((𝑇‘𝑃) ∖ I ) = 𝑃)
Theorem	pmtrrn 19074	Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) ∈ 𝑅)
Theorem	pmtrfrn 19075	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 19076	Mapping of a point under a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    &   ⊢ 𝑃 = dom (𝐹 ∖ I )    ⇒   ⊢ ((𝐹 ∈ 𝑅 ∧ 𝑍 ∈ 𝐷) → (𝐹‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍))
Theorem	pmtrrn2 19077*	For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))
Theorem	pmtrfinv 19078	A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) = ( I ↾ 𝐷))
Theorem	pmtrfmvdn0 19079	A transposition moves at least one point. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≠ ∅)
Theorem	pmtrff1o 19080	A transposition function is a permutation. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → 𝐹:𝐷–1-1-onto→𝐷)
Theorem	pmtrfcnv 19081	A transposition function is its own inverse. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → ◡𝐹 = 𝐹)
Theorem	pmtrfb 19082	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 19083	Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ ((𝐹 ∈ 𝑅 ∧ 𝐺:𝐷–1-1-onto→𝐷) → ((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∈ 𝑅)
Theorem	symgsssg 19084*	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 19085*	The symmetric group has a subgroup of permutations that move finitely many points. (Contributed by Stefan O'Rear, 24-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐷 ∈ 𝑉 → {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin} ∈ (SubGrp‘𝐺))
Theorem	symgtrf 19086	Transpositions are elements of the symmetric group. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝑇 ⊆ 𝐵
Theorem	symggen 19087*	The span of the transpositions is the subgroup that moves finitely many points. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubMnd‘𝐺))    ⇒   ⊢ (𝐷 ∈ 𝑉 → (𝐾‘𝑇) = {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin})
Theorem	symggen2 19088	A finite permutation group is generated by the transpositions, see also Theorem 3.4 in [Rotman] p. 31. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubMnd‘𝐺))    ⇒   ⊢ (𝐷 ∈ Fin → (𝐾‘𝑇) = 𝐵)
Theorem	symgtrinv 19089	To invert a permutation represented as a sequence of transpositions, reverse the sequence. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → (𝐼‘(𝐺 Σg 𝑊)) = (𝐺 Σg (reverse‘𝑊)))
Theorem	pmtr3ncomlem1 19090	Lemma 1 for pmtr3ncom 19092. (Contributed by AV, 17-Mar-2018.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌})    &   ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍})    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝐺 ∘ 𝐹)‘𝑋) ≠ ((𝐹 ∘ 𝐺)‘𝑋))
Theorem	pmtr3ncomlem2 19091	Lemma 2 for pmtr3ncom 19092. (Contributed by AV, 17-Mar-2018.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌})    &   ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍})    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐺 ∘ 𝐹) ≠ (𝐹 ∘ 𝐺))
Theorem	pmtr3ncom 19092*	Transpositions over sets with at least 3 elements are not commutative, see also the remark in [Rotman] p. 28. (Contributed by AV, 21-Mar-2019.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 3 ≤ (♯‘𝐷)) → ∃𝑓 ∈ ran 𝑇∃𝑔 ∈ ran 𝑇(𝑔 ∘ 𝑓) ≠ (𝑓 ∘ 𝑔))
Theorem	pmtrdifellem1 19093	Lemma 1 for pmtrdifel 19097. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ (𝑄 ∈ 𝑇 → 𝑆 ∈ 𝑅)
Theorem	pmtrdifellem2 19094	Lemma 2 for pmtrdifel 19097. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ (𝑄 ∈ 𝑇 → dom (𝑆 ∖ I ) = dom (𝑄 ∖ I ))
Theorem	pmtrdifellem3 19095*	Lemma 3 for pmtrdifel 19097. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ (𝑄 ∈ 𝑇 → ∀𝑥 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑥) = (𝑆‘𝑥))
Theorem	pmtrdifellem4 19096	Lemma 4 for pmtrdifel 19097. (Contributed by AV, 28-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → (𝑆‘𝐾) = 𝐾)
Theorem	pmtrdifel 19097*	A transposition of elements of a set without a special element corresponds to a transposition of elements of the set. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    ⇒   ⊢ ∀𝑡 ∈ 𝑇 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ (𝑁 ∖ {𝐾})(𝑡‘𝑥) = (𝑟‘𝑥)
Theorem	pmtrdifwrdellem1 19098*	Lemma 1 for pmtrdifwrdel 19102. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → 𝑈 ∈ Word 𝑅)
Theorem	pmtrdifwrdellem2 19099*	Lemma 2 for pmtrdifwrdel 19102. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → (♯‘𝑊) = (♯‘𝑈))
Theorem	pmtrdifwrdellem3 19100*	Lemma 3 for pmtrdifwrdel 19102. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → ∀𝑖 ∈ (0..^(♯‘𝑊))∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))