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	orbsta2 19301*	Relation between the size of the orbit and the size of the stabilizer of a point in a finite group action. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    &   ⊢ ∼ = (𝐺 ~QG 𝐻)    &   ⊢ 𝑂 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}    ⇒   ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → (♯‘𝑋) = ((♯‘[𝐴]𝑂) · (♯‘𝐻)))
10.2.8  Centralizers and centers
Syntax	ccntz 19302	Syntax for the centralizer of a set in a monoid.
class Cntz
Syntax	ccntr 19303	Syntax for the centralizer of a monoid.
class Cntr
Definition	df-cntz 19304*	Define the centralizer of a subset of a magma, which is the set of elements each of which commutes with each element of the given subset. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ Cntz = (𝑚 ∈ V ↦ (𝑠 ∈ 𝒫 (Base‘𝑚) ↦ {𝑥 ∈ (Base‘𝑚) ∣ ∀𝑦 ∈ 𝑠 (𝑥(+g‘𝑚)𝑦) = (𝑦(+g‘𝑚)𝑥)}))
Definition	df-cntr 19305	Define the center of a magma, which is the elements that commute with all others. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ Cntr = (𝑚 ∈ V ↦ ((Cntz‘𝑚)‘(Base‘𝑚)))
Theorem	cntrval 19306	Substitute definition of the center. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑍‘𝐵) = (Cntr‘𝑀)
Theorem	cntzfval 19307*	First level substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑀 ∈ 𝑉 → 𝑍 = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)}))
Theorem	cntzval 19308*	Definition substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)})
Theorem	elcntz 19309*	Elementhood in the centralizer. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑆 ⊆ 𝐵 → (𝐴 ∈ (𝑍‘𝑆) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑆 (𝐴 + 𝑦) = (𝑦 + 𝐴))))
Theorem	cntzel 19310*	Membership in a centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ (𝑍‘𝑆) ↔ ∀𝑦 ∈ 𝑆 (𝑋 + 𝑦) = (𝑦 + 𝑋)))
Theorem	cntzsnval 19311*	Special substitution for the centralizer of a singleton. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑌 ∈ 𝐵 → (𝑍‘{𝑌}) = {𝑥 ∈ 𝐵 ∣ (𝑥 + 𝑌) = (𝑌 + 𝑥)})
Theorem	elcntzsn 19312	Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑌 ∈ 𝐵 → (𝑋 ∈ (𝑍‘{𝑌}) ↔ (𝑋 ∈ 𝐵 ∧ (𝑋 + 𝑌) = (𝑌 + 𝑋))))
Theorem	sscntz 19313*	A centralizer expression for two sets elementwise commuting. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑆 ⊆ (𝑍‘𝑇) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
Theorem	cntzrcl 19314	Reverse closure for elements of the centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑋 ∈ (𝑍‘𝑆) → (𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵))
Theorem	cntzssv 19315	The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑍‘𝑆) ⊆ 𝐵
Theorem	cntzi 19316	Membership in a centralizer (inference). (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑋 ∈ (𝑍‘𝑆) ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	elcntr 19317*	Elementhood in the center of a magma. (Contributed by SN, 21-Mar-2025.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntr‘𝑀)    ⇒   ⊢ (𝐴 ∈ 𝑍 ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐴 + 𝑦) = (𝑦 + 𝐴)))
Theorem	cntrss 19318	The center is a subset of the base field. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (Cntr‘𝑀) ⊆ 𝐵
Theorem	cntri 19319	Defining property of the center of a group. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntr‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝑍 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	resscntz 19320	Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝑌 = (Cntz‘𝐻)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑌‘𝑆) = ((𝑍‘𝑆) ∩ 𝐴))
Theorem	cntzsgrpcl 19321*	Centralizers are closed under the semigroup operation. (Contributed by AV, 17-Feb-2025.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    &   ⊢ 𝐶 = (𝑍‘𝑆)    ⇒   ⊢ ((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) → ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 (𝑦(+g‘𝑀)𝑧) ∈ 𝐶)
Theorem	cntz2ss 19322	Centralizers reverse the subset relation. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆) → (𝑍‘𝑆) ⊆ (𝑍‘𝑇))
Theorem	cntzrec 19323	Reciprocity relationship for centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑆 ⊆ (𝑍‘𝑇) ↔ 𝑇 ⊆ (𝑍‘𝑆)))
Theorem	cntziinsn 19324*	Express any centralizer as an intersection of singleton centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = (𝐵 ∩ ∩ 𝑥 ∈ 𝑆 (𝑍‘{𝑥})))
Theorem	cntzsubm 19325	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 19326	Centralizers in a group are subgroups. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubGrp‘𝑀))
Theorem	cntzidss 19327	If the elements of 𝑆 commute, the elements of a subset 𝑇 also commute. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ 𝑍 = (Cntz‘𝐺)    ⇒   ⊢ ((𝑆 ⊆ (𝑍‘𝑆) ∧ 𝑇 ⊆ 𝑆) → 𝑇 ⊆ (𝑍‘𝑇))
Theorem	cntzmhm 19328	Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝑌 = (Cntz‘𝐻)    ⇒   ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝐴 ∈ (𝑍‘𝑆)) → (𝐹‘𝐴) ∈ (𝑌‘(𝐹 “ 𝑆)))
Theorem	cntzmhm2 19329	Centralizers in a monoid are preserved by monoid homomorphisms. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝑌 = (Cntz‘𝐻)    ⇒   ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑆 ⊆ (𝑍‘𝑇)) → (𝐹 “ 𝑆) ⊆ (𝑌‘(𝐹 “ 𝑇)))
Theorem	cntrsubgnsg 19330	A central subgroup is normal. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑍 = (Cntr‘𝑀)    ⇒   ⊢ ((𝑋 ∈ (SubGrp‘𝑀) ∧ 𝑋 ⊆ 𝑍) → 𝑋 ∈ (NrmSGrp‘𝑀))
Theorem	cntrnsg 19331	The center of a group is a normal subgroup. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑍 = (Cntr‘𝑀)    ⇒   ⊢ (𝑀 ∈ Grp → 𝑍 ∈ (NrmSGrp‘𝑀))
10.2.9  The opposite group
Syntax	coppg 19332	The opposite group operation.
class oppg
Definition	df-oppg 19333	Define an opposite group, which is the same as the original group but with addition written the other way around. df-oppr 20302 does the same thing for multiplication. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ oppg = (𝑤 ∈ V ↦ (𝑤 sSet ⟨(+g‘ndx), tpos (+g‘𝑤)⟩))
Theorem	oppgval 19334	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 19335	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 19336	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	setsplusg 19337	The other components of an extensible structure remain unchanged if the +g component is set/substituted. (Contributed by Stefan O'Rear, 26-Aug-2015.) Generalisation of the former oppglem and mgplem. (Revised by AV, 18-Oct-2024.)
⊢ 𝑂 = (𝑅 sSet ⟨(+g‘ndx), 𝑆⟩)    &   ⊢ 𝐸 = Slot (𝐸‘ndx)    &   ⊢ (𝐸‘ndx) ≠ (+g‘ndx)    ⇒   ⊢ (𝐸‘𝑅) = (𝐸‘𝑂)
Theorem	oppgbas 19338	Base set of an opposite group. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ 𝐵 = (Base‘𝑂)
Theorem	oppgtset 19339	Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐽 = (TopSet‘𝑅)    ⇒   ⊢ 𝐽 = (TopSet‘𝑂)
Theorem	oppgtopn 19340	Topology of an opposite group. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐽 = (TopOpen‘𝑅)    ⇒   ⊢ 𝐽 = (TopOpen‘𝑂)
Theorem	oppgmnd 19341	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 19342	Bidirectional form of oppgmnd 19341. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Mnd ↔ 𝑂 ∈ Mnd)
Theorem	oppgid 19343	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 19344	The opposite of a group is a group. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Grp → 𝑂 ∈ Grp)
Theorem	oppggrpb 19345	Bidirectional form of oppggrp 19344. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Grp ↔ 𝑂 ∈ Grp)
Theorem	oppginv 19346	Inverses in a group are a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝑅)    &   ⊢ 𝐼 = (invg‘𝑅)    ⇒   ⊢ (𝑅 ∈ Grp → 𝐼 = (invg‘𝑂))
Theorem	invoppggim 19347	The inverse is an antiautomorphism on any group. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐼 ∈ (𝐺 GrpIso 𝑂))
Theorem	oppggic 19348	Every group is (naturally) isomorphic to its opposite. (Contributed by Stefan O'Rear, 26-Aug-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐺 ≃𝑔 𝑂)
Theorem	oppgsubm 19349	Being a submonoid is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (SubMnd‘𝐺) = (SubMnd‘𝑂)
Theorem	oppgsubg 19350	Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝑂 = (oppg‘𝐺)    ⇒   ⊢ (SubGrp‘𝐺) = (SubGrp‘𝑂)
Theorem	oppgcntz 19351	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 19352	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 19353	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 19355. However, the set is allowed to be empty, see symgbas0 19374. 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 19357), 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 19357). This means that a symmetric group is a permutation group, and each permutation group is a subgroup of a symmetric group (see pgrpsubgsymgbi 19394 and pgrpsubgsymg 19395). 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 19397, which is a (proper) subgroup of a symmetric group, see idressubgsymg 19396. As in [Rotman] p. 28 "Let 𝑥 ∈ 𝑋 and 𝑝 ∈ SymGrp(𝑋); we say 𝑝 fixes 𝑥 if (𝑝‘𝑥) = 𝑥; otherwise 𝑝 moves 𝑥.". The theorems starting with symgfix2 19402 are about fixed/moved elements.
Syntax	csymg 19354	Extend class notation to include the class of symmetric groups.
class SymGrp
Definition	df-symg 19355*	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 19356*	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 19357*	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 19358	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 19359	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 19360	Elements in the symmetric group are 1-1 onto functions. (Contributed by SO, 9-Jul-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴–1-1-onto→𝐴)
Theorem	symgbasf 19361	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 19362	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 19363	The symmetric group on 𝑛 objects has cardinality 𝑛!. (Contributed by Mario Carneiro, 22-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → (♯‘𝐵) = (!‘(♯‘𝐴)))
Theorem	symgbasfi 19364	The symmetric group on a finite index set is finite. (Contributed by SO, 9-Jul-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin)
Theorem	symgfv 19365	The function value of a permutation. (Contributed by AV, 1-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴)
Theorem	symgfvne 19366	The function values of a permutation for different arguments are different. (Contributed by AV, 8-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑍 → (𝑌 ≠ 𝑋 → (𝐹‘𝑌) ≠ 𝑍)))
Theorem	symgressbas 19367	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 19368*	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 19369	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 19370	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 19371	The identity function restricted to a set is a permutation of this set. (Contributed by AV, 17-Mar-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    ⇒   ⊢ (𝐴 ∈ 𝑉 → ( I ↾ 𝐴) ∈ (Base‘𝐺))
Theorem	symgmov1 19372*	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 19373*	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 19374	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 19375	The symmetric group on a singleton has cardinality 1. (Contributed by AV, 9-Dec-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (♯‘𝐵) = 1)
Theorem	symg1bas 19376	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 19377	The symmetric group on a (proper) pair has cardinality 2. (Contributed by AV, 9-Dec-2018.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼, 𝐽}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 2)
Theorem	symg2bas 19378	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 19376. (Contributed by AV, 9-Dec-2018.) (Proof shortened by AV, 16-Jun-2022.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐴 = {𝐼, 𝐽}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊) → 𝐵 = {{⟨𝐼, 𝐼⟩, ⟨𝐽, 𝐽⟩}, {⟨𝐼, 𝐽⟩, ⟨𝐽, 𝐼⟩}})
Theorem	0symgefmndeq 19379	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 19380	The symmetric group on a singleton 𝐴 is identical with the monoid of endofunctions on 𝐴. (Contributed by AV, 31-Mar-2024.)
⊢ (𝐴 = {𝑋} → (EndoFMnd‘𝐴) = (SymGrp‘𝐴))
Theorem	symgpssefmnd 19381	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 19382*	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 19383*	Obsolete version of symgvalstruct 19382 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 19384	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 19385	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 19386	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 19387	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 19388	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 19389	The symmetric group on a set 𝐴 is a submonoid of the monoid of endofunctions on 𝐴. Alternate proof based on issubmndb 18787 and not on injsubmefmnd 18879 and sursubmefmnd 18878. (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 19390*	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 19391*	The converse of galactghm 19390. 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 19392	The topology of the symmetric group on 𝐴. (Contributed by Mario Carneiro, 29-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺))
Theorem	symgga 19393*	The symmetric group induces a group action on its base set. (Contributed by Mario Carneiro, 24-Jan-2015.)
⊢ 𝐺 = (SymGrp‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐹 = (𝑓 ∈ 𝐵, 𝑥 ∈ 𝑋 ↦ (𝑓‘𝑥))    ⇒   ⊢ (𝑋 ∈ 𝑉 → 𝐹 ∈ (𝐺 GrpAct 𝑋))
Theorem	pgrpsubgsymgbi 19394	Every permutation group is a subgroup of the corresponding symmetric group. (Contributed by AV, 14-Mar-2019.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑉 → (𝑃 ∈ (SubGrp‘𝐺) ↔ (𝑃 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑃) ∈ Grp)))
Theorem	pgrpsubgsymg 19395*	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 19396	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 19397	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 19398*	Lemma for cayley 19400. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐻 = (SymGrp‘𝑋)    &   ⊢ 𝑆 = (Base‘𝐻)    &   ⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)))    ⇒   ⊢ (𝐺 ∈ Grp → 𝐹 ∈ (𝐺 GrpHom 𝐻))
Theorem	cayleylem2 19399*	Lemma for cayley 19400. (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 19400*	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→𝑆))