P. 193 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19201-19300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ghmf 19201	A group homomorphism is a function. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝑋⟶𝑌)
Theorem	ghmlin 19202	A homomorphism of groups is linear. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉)))
Theorem	ghmid 19203	A homomorphism of groups preserves the identity. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑌 = (0g‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘𝑌) = 0 )
Theorem	ghminv 19204	A homomorphism of groups preserves inverses. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑀 = (invg‘𝑆)    &   ⊢ 𝑁 = (invg‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑀‘𝑋)) = (𝑁‘(𝐹‘𝑋)))
Theorem	ghmsub 19205	Linearity of subtraction through a group homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ − = (-g‘𝑆)    &   ⊢ 𝑁 = (-g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘(𝑈 − 𝑉)) = ((𝐹‘𝑈)𝑁(𝐹‘𝑉)))
Theorem	isghmd 19206*	Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    &   ⊢ (𝜑 → 𝑆 ∈ Grp)    &   ⊢ (𝜑 → 𝑇 ∈ Grp)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	ghmmhm 19207	A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 ∈ (𝑆 MndHom 𝑇))
Theorem	ghmmhmb 19208	Group homomorphisms and monoid homomorphisms coincide. (Thus, GrpHom is somewhat redundant, although its stronger reverse closure properties are sometimes useful.) (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝑆 GrpHom 𝑇) = (𝑆 MndHom 𝑇))
Theorem	ghmmulg 19209	A group homomorphism preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ × = (.g‘𝐻)    ⇒   ⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋)))
Theorem	ghmrn 19210	The range of a homomorphism is a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ∈ (SubGrp‘𝑇))
Theorem	0ghm 19211	The constant zero linear function between two groups. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 0 = (0g‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Grp ∧ 𝑁 ∈ Grp) → (𝐵 × { 0 }) ∈ (𝑀 GrpHom 𝑁))
Theorem	idghm 19212	The identity homomorphism on a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ( I ↾ 𝐵) ∈ (𝐺 GrpHom 𝐺))
Theorem	resghm 19213	Restriction of a homomorphism to a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ (SubGrp‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 GrpHom 𝑇))
Theorem	resghm2 19214	One direction of resghm2b 19215. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑈) ∧ 𝑋 ∈ (SubGrp‘𝑇)) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	resghm2b 19215	Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝑋 ∈ (SubGrp‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ 𝐹 ∈ (𝑆 GrpHom 𝑈)))
Theorem	ghmghmrn 19216	A group homomorphism from 𝐺 to 𝐻 is also a group homomorphism from 𝐺 to its image in 𝐻. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by AV, 26-Aug-2021.)
⊢ 𝑈 = (𝑇 ↾s ran 𝐹)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 ∈ (𝑆 GrpHom 𝑈))
Theorem	ghmco 19217	The composition of group homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐹 ∈ (𝑇 GrpHom 𝑈) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GrpHom 𝑈))
Theorem	ghmima 19218	The image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ (SubGrp‘𝑆)) → (𝐹 “ 𝑈) ∈ (SubGrp‘𝑇))
Theorem	ghmpreima 19219	The inverse image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑉 ∈ (SubGrp‘𝑇)) → (◡𝐹 “ 𝑉) ∈ (SubGrp‘𝑆))
Theorem	ghmeql 19220	The equalizer of two group homomorphisms is a subgroup. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → dom (𝐹 ∩ 𝐺) ∈ (SubGrp‘𝑆))
Theorem	ghmnsgima 19221	The image of a normal subgroup under a surjective homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝑌 = (Base‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ (NrmSGrp‘𝑆) ∧ ran 𝐹 = 𝑌) → (𝐹 “ 𝑈) ∈ (NrmSGrp‘𝑇))
Theorem	ghmnsgpreima 19222	The inverse image of a normal subgroup under a homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑉 ∈ (NrmSGrp‘𝑇)) → (◡𝐹 “ 𝑉) ∈ (NrmSGrp‘𝑆))
Theorem	ghmker 19223	The kernel of a homomorphism is a normal subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 0 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (◡𝐹 “ { 0 }) ∈ (NrmSGrp‘𝑆))
Theorem	ghmeqker 19224	Two source points map to the same destination point under a group homomorphism iff their difference belongs to the kernel. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ − = (-g‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → ((𝐹‘𝑈) = (𝐹‘𝑉) ↔ (𝑈 − 𝑉) ∈ 𝐾))
Theorem	pwsdiagghm 19225*	Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 GrpHom 𝑌))
Theorem	f1ghm0to0 19226	If a group homomorphism 𝐹 is injective, it maps the zero of one group (and only the zero) to the zero of the other group. (Contributed by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 13-May-2023.)
⊢ 𝐴 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑁 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴–1-1→𝐵 ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) = 0 ↔ 𝑋 = 𝑁))
Theorem	ghmf1 19227*	Two ways of saying a group homomorphism is 1-1 into its codomain. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) (Proof shortened by AV, 4-Apr-2025.)
⊢ 𝐴 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑁 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹:𝐴–1-1→𝐵 ↔ ∀𝑥 ∈ 𝐴 ((𝐹‘𝑥) = 0 → 𝑥 = 𝑁)))
Theorem	kerf1ghm 19228	A group homomorphism 𝐹 is injective if and only if its kernel is the singleton {𝑁}. (Contributed by Thierry Arnoux, 27-Oct-2017.) (Proof shortened by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 13-May-2023.)
⊢ 𝐴 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑁 = (0g‘𝑅)    &   ⊢ 0 = (0g‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹:𝐴–1-1→𝐵 ↔ (◡𝐹 “ { 0 }) = {𝑁}))
Theorem	ghmf1o 19229	A bijective group homomorphism is an isomorphism. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 GrpHom 𝑆)))
Theorem	conjghm 19230*	Conjugation is an automorphism of the group. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ (𝐺 GrpHom 𝐺) ∧ 𝐹:𝑋–1-1-onto→𝑋))
Theorem	conjsubg 19231*	A conjugated subgroup is also a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → ran 𝐹 ∈ (SubGrp‘𝐺))
Theorem	conjsubgen 19232*	A conjugated subgroup is equinumerous to the original subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → 𝑆 ≈ ran 𝐹)
Theorem	conjnmz 19233*	A subgroup is unchanged under conjugation by an element of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    &   ⊢ 𝑁 = {𝑦 ∈ 𝑋 ∣ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)}    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑁) → 𝑆 = ran 𝐹)
Theorem	conjnmzb 19234*	Alternative condition for elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    &   ⊢ 𝑁 = {𝑦 ∈ 𝑋 ∣ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)}    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)))
Theorem	conjnsg 19235*	A normal subgroup is unchanged under conjugation. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → 𝑆 = ran 𝐹)
Theorem	qusghm 19236*	If 𝑌 is a normal subgroup of 𝐺, then the "natural map" from elements to their cosets is a group homomorphism from 𝐺 to 𝐺 / 𝑌. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 18-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑌))    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ [𝑥](𝐺 ~QG 𝑌))    ⇒   ⊢ (𝑌 ∈ (NrmSGrp‘𝐺) → 𝐹 ∈ (𝐺 GrpHom 𝐻))
Theorem	ghmpropd 19237*	Group homomorphism depends only on the group attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐽))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐶 = (Base‘𝑀))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐽)𝑦) = (𝑥(+g‘𝐿)𝑦))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐶 ∧ 𝑦 ∈ 𝐶)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝑀)𝑦))    ⇒   ⊢ (𝜑 → (𝐽 GrpHom 𝐾) = (𝐿 GrpHom 𝑀))
10.2.6  Isomorphisms of groups
Syntax	cgim 19238	The class of group isomorphism sets.
class GrpIso
Syntax	cgic 19239	The class of the group isomorphism relation.
class ≃𝑔
Definition	df-gim 19240*	An isomorphism of groups is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group operation. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ GrpIso = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∈ (𝑠 GrpHom 𝑡) ∣ 𝑔:(Base‘𝑠)–1-1-onto→(Base‘𝑡)})
Definition	df-gic 19241	Two groups are said to be isomorphic iff they are connected by at least one isomorphism. Isomorphic groups share all global group properties, but to relate local properties requires knowledge of a specific isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ ≃𝑔 = (◡ GrpIso “ (V ∖ 1o))
Theorem	gimfn 19242	The group isomorphism function is a well-defined function. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ GrpIso Fn (Grp × Grp)
Theorem	isgim 19243	An isomorphism of groups is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) ↔ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐵–1-1-onto→𝐶))
Theorem	gimf1o 19244	An isomorphism of groups is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) → 𝐹:𝐵–1-1-onto→𝐶)
Theorem	gimghm 19245	An isomorphism of groups is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
Theorem	isgim2 19246	A group isomorphism is a homomorphism whose converse is also a homomorphism. Characterization of isomorphisms similar to ishmeo 23695. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) ↔ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 GrpHom 𝑅)))
Theorem	subggim 19247	Behavior of subgroups under isomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝐹 ∈ (𝑅 GrpIso 𝑆) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝐹 “ 𝐴) ∈ (SubGrp‘𝑆)))
Theorem	gimcnv 19248	The converse of a group isomorphism is a group isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
⊢ (𝐹 ∈ (𝑆 GrpIso 𝑇) → ◡𝐹 ∈ (𝑇 GrpIso 𝑆))
Theorem	gimco 19249	The composition of group isomorphisms is a group isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ((𝐹 ∈ (𝑇 GrpIso 𝑈) ∧ 𝐺 ∈ (𝑆 GrpIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GrpIso 𝑈))
Theorem	gim0to0 19250	A group isomorphism maps the zero of one group (and only the zero) to the zero of the other group. (Contributed by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 23-May-2023.)
⊢ 𝐴 = (Base‘𝑅)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑁 = (0g‘𝑆)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ ((𝐹 ∈ (𝑅 GrpIso 𝑆) ∧ 𝑋 ∈ 𝐴) → ((𝐹‘𝑋) = 𝑁 ↔ 𝑋 = 0 ))
Theorem	brgic 19251	The relation "is isomorphic to" for groups. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑔 𝑆 ↔ (𝑅 GrpIso 𝑆) ≠ ∅)
Theorem	brgici 19252	Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) → 𝑅 ≃𝑔 𝑆)
Theorem	gicref 19253	Isomorphism is reflexive. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ (𝑅 ∈ Grp → 𝑅 ≃𝑔 𝑅)
Theorem	giclcl 19254	Isomorphism implies the left side is a group. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑔 𝑆 → 𝑅 ∈ Grp)
Theorem	gicrcl 19255	Isomorphism implies the right side is a group. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝑅 ≃𝑔 𝑆 → 𝑆 ∈ Grp)
Theorem	gicsym 19256	Isomorphism is symmetric. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ (𝑅 ≃𝑔 𝑆 → 𝑆 ≃𝑔 𝑅)
Theorem	gictr 19257	Isomorphism is transitive. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ((𝑅 ≃𝑔 𝑆 ∧ 𝑆 ≃𝑔 𝑇) → 𝑅 ≃𝑔 𝑇)
Theorem	gicer 19258	Isomorphism is an equivalence relation on groups. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 1-May-2021.)
⊢ ≃𝑔 Er Grp
Theorem	gicen 19259	Isomorphic groups have equinumerous base sets. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝑅 ≃𝑔 𝑆 → 𝐵 ≈ 𝐶)
Theorem	gicsubgen 19260	A less trivial example of a group invariant: cardinality of the subgroup lattice. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑔 𝑆 → (SubGrp‘𝑅) ≈ (SubGrp‘𝑆))
10.2.6.1  The first isomorphism theorem of groups
Theorem	ghmqusnsglem1 19261*	Lemma for ghmqusnsg 19263. (Contributed by Thierry Arnoux, 13-May-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    &   ⊢ (𝜑 → 𝑁 ⊆ 𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐺))    ⇒   ⊢ (𝜑 → (𝐽‘[𝑋](𝐺 ~QG 𝑁)) = (𝐹‘𝑋))
Theorem	ghmqusnsglem2 19262*	Lemma for ghmqusnsg 19263. (Contributed by Thierry Arnoux, 13-May-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    &   ⊢ (𝜑 → 𝑁 ⊆ 𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑄))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 (𝐽‘𝑌) = (𝐹‘𝑥))
Theorem	ghmqusnsg 19263*	The mapping 𝐻 induced by a surjective group homomorphism 𝐹 from the quotient group 𝑄 over a normal subgroup 𝑁 of 𝐹's kernel 𝐾 is a group isomorphism. In this case, one says that 𝐹 factors through 𝑄, which is also called the factor group. (Contributed by Thierry Arnoux, 13-May-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    &   ⊢ (𝜑 → 𝑁 ⊆ 𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    ⇒   ⊢ (𝜑 → 𝐽 ∈ (𝑄 GrpHom 𝐻))
Theorem	ghmquskerlem1 19264*	Lemma for ghmqusker 19268. (Contributed by Thierry Arnoux, 14-Feb-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐺))    ⇒   ⊢ (𝜑 → (𝐽‘[𝑋](𝐺 ~QG 𝐾)) = (𝐹‘𝑋))
Theorem	ghmquskerco 19265*	In the case of theorem ghmqusker 19268, the composition of the natural homomorphism 𝐿 with the constructed homomorphism 𝐽 equals the original homomorphism 𝐹. One says that 𝐹 factors through 𝑄. (Proposed by Saveliy Skresanov, 15-Feb-2025.) (Contributed by Thierry Arnoux, 15-Feb-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐿 = (𝑥 ∈ 𝐵 ↦ [𝑥](𝐺 ~QG 𝐾))    ⇒   ⊢ (𝜑 → 𝐹 = (𝐽 ∘ 𝐿))
Theorem	ghmquskerlem2 19266*	Lemma for ghmqusker 19268. (Contributed by Thierry Arnoux, 14-Feb-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑄))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 (𝐽‘𝑌) = (𝐹‘𝑥))
Theorem	ghmquskerlem3 19267*	The mapping 𝐻 induced by a surjective group homomorphism 𝐹 from the quotient group 𝑄 over 𝐹's kernel 𝐾 is a group isomorphism. In this case, one says that 𝐹 factors through 𝑄, which is also called the factor group. (Contributed by Thierry Arnoux, 22-Mar-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    ⇒   ⊢ (𝜑 → 𝐽 ∈ (𝑄 GrpHom 𝐻))
Theorem	ghmqusker 19268*	A surjective group homomorphism 𝐹 from 𝐺 to 𝐻 induces an isomorphism 𝐽 from 𝑄 to 𝐻, where 𝑄 is the factor group of 𝐺 by 𝐹's kernel 𝐾. (Contributed by Thierry Arnoux, 15-Feb-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    &   ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻))    ⇒   ⊢ (𝜑 → 𝐽 ∈ (𝑄 GrpIso 𝐻))
Theorem	gicqusker 19269	The image 𝐻 of a group homomorphism 𝐹 is isomorphic with the quotient group 𝑄 over 𝐹's kernel 𝐾. Together with ghmker 19223 and ghmima 19218, this is sometimes called the first isomorphism theorem for groups. (Contributed by Thierry Arnoux, 10-Mar-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))    &   ⊢ (𝜑 → ran 𝐹 = (Base‘𝐻))    ⇒   ⊢ (𝜑 → 𝑄 ≃𝑔 𝐻)
10.2.7  Group actions
Syntax	cga 19270	Extend class definition to include the class of group actions.
class GrpAct
Definition	df-ga 19271*	Define the class of all group actions. A group 𝐺 acts on a set 𝑆 if a permutation on 𝑆 is associated with every element of 𝐺 in such a way that the identity permutation on 𝑆 is associated with the neutral element of 𝐺, and the composition of the permutations associated with two elements of 𝐺 is identical with the permutation associated with the composition of these two elements (in the same order) in the group 𝐺. (Contributed by Jeff Hankins, 10-Aug-2009.)
⊢ GrpAct = (𝑔 ∈ Grp, 𝑠 ∈ V ↦ ⦋(Base‘𝑔) / 𝑏⦌{𝑚 ∈ (𝑠 ↑m (𝑏 × 𝑠)) ∣ ∀𝑥 ∈ 𝑠 (((0g‘𝑔)𝑚𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑦(+g‘𝑔)𝑧)𝑚𝑥) = (𝑦𝑚(𝑧𝑚𝑥)))})
Theorem	isga 19272*	The predicate "is a (left) group action". The group 𝐺 is said to act on the base set 𝑌 of the action, which is not assumed to have any special properties. There is a related notion of right group action, but as the Wikipedia article explains, it is not mathematically interesting. The way actions are usually thought of is that each element 𝑔 of 𝐺 is a permutation of the elements of 𝑌 (see gapm 19287). Since group theory was classically about symmetry groups, it is therefore likely that the notion of group action was useful even in early group theory. (Contributed by Jeff Hankins, 10-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) ↔ ((𝐺 ∈ Grp ∧ 𝑌 ∈ V) ∧ ( ⊕ :(𝑋 × 𝑌)⟶𝑌 ∧ ∀𝑥 ∈ 𝑌 (( 0 ⊕ 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ⊕ 𝑥) = (𝑦 ⊕ (𝑧 ⊕ 𝑥))))))
Theorem	gagrp 19273	The left argument of a group action is a group. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → 𝐺 ∈ Grp)
Theorem	gaset 19274	The right argument of a group action is a set. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → 𝑌 ∈ V)
Theorem	gagrpid 19275	The identity of the group does not alter the base set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → ( 0 ⊕ 𝐴) = 𝐴)
Theorem	gaf 19276	The mapping of the group action operation. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → ⊕ :(𝑋 × 𝑌)⟶𝑌)
Theorem	gafo 19277	A group action is onto its base set. (Contributed by Jeff Hankins, 10-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → ⊕ :(𝑋 × 𝑌)–onto→𝑌)
Theorem	gaass 19278	An "associative" property for group actions. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑌)) → ((𝐴 + 𝐵) ⊕ 𝐶) = (𝐴 ⊕ (𝐵 ⊕ 𝐶)))
Theorem	ga0 19279	The action of a group on the empty set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ (𝐺 ∈ Grp → ∅ ∈ (𝐺 GrpAct ∅))
Theorem	gaid 19280	The trivial action of a group on any set. Each group element corresponds to the identity permutation. (Contributed by Jeff Hankins, 11-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑆 ∈ 𝑉) → (2nd ↾ (𝑋 × 𝑆)) ∈ (𝐺 GrpAct 𝑆))
Theorem	subgga 19281*	A subgroup acts on its parent group. (Contributed by Jeff Hankins, 13-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑌)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑌, 𝑦 ∈ 𝑋 ↦ (𝑥 + 𝑦))    ⇒   ⊢ (𝑌 ∈ (SubGrp‘𝐺) → 𝐹 ∈ (𝐻 GrpAct 𝑋))
Theorem	gass 19282*	A subset of a group action is a group action iff it is closed under the group action operation. (Contributed by Mario Carneiro, 17-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑍 ⊆ 𝑌) → (( ⊕ ↾ (𝑋 × 𝑍)) ∈ (𝐺 GrpAct 𝑍) ↔ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑍 (𝑥 ⊕ 𝑦) ∈ 𝑍))
Theorem	gasubg 19283	The restriction of a group action to a subgroup is a group action. (Contributed by Mario Carneiro, 17-Jan-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝑆 ∈ (SubGrp‘𝐺)) → ( ⊕ ↾ (𝑆 × 𝑌)) ∈ (𝐻 GrpAct 𝑌))
Theorem	gaid2 19284*	A group operation is a left group action of the group on itself. (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ (𝑥 + 𝑦))    ⇒   ⊢ (𝐺 ∈ Grp → 𝐹 ∈ (𝐺 GrpAct 𝑋))
Theorem	galcan 19285	The action of a particular group element is left-cancelable. (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((𝐴 ⊕ 𝐵) = (𝐴 ⊕ 𝐶) ↔ 𝐵 = 𝐶))
Theorem	gacan 19286	Group inverses cancel in a group action. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝐶 ∈ 𝑌)) → ((𝐴 ⊕ 𝐵) = 𝐶 ↔ ((𝑁‘𝐴) ⊕ 𝐶) = 𝐵))
Theorem	gapm 19287*	The action of a particular group element is a permutation of the base set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑌 ↦ (𝐴 ⊕ 𝑥))    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑋) → 𝐹:𝑌–1-1-onto→𝑌)
Theorem	gaorb 19288*	The orbit equivalence relation puts two points in the group action in the same equivalence class iff there is a group element that takes one element to the other. (Contributed by Mario Carneiro, 14-Jan-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}    ⇒   ⊢ (𝐴 ∼ 𝐵 ↔ (𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ∧ ∃ℎ ∈ 𝑋 (ℎ ⊕ 𝐴) = 𝐵))
Theorem	gaorber 19289*	The orbit equivalence relation is an equivalence relation on the target set of the group action. (Contributed by NM, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.)
⊢ ∼ = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → ∼ Er 𝑌)
Theorem	gastacl 19290*	The stabilizer subgroup in a group action. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐻 ∈ (SubGrp‘𝐺))
Theorem	gastacos 19291*	Write the coset relation for the stabilizer subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    &   ⊢ ∼ = (𝐺 ~QG 𝐻)    ⇒   ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵 ∼ 𝐶 ↔ (𝐵 ⊕ 𝐴) = (𝐶 ⊕ 𝐴)))
Theorem	orbstafun 19292*	Existence and uniqueness for the function of orbsta 19294. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    &   ⊢ ∼ = (𝐺 ~QG 𝐻)    &   ⊢ 𝐹 = ran (𝑘 ∈ 𝑋 ↦ ⟨[𝑘] ∼ , (𝑘 ⊕ 𝐴)⟩)    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → Fun 𝐹)
Theorem	orbstaval 19293*	Value of the function at a given equivalence class element. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    &   ⊢ ∼ = (𝐺 ~QG 𝐻)    &   ⊢ 𝐹 = ran (𝑘 ∈ 𝑋 ↦ ⟨[𝑘] ∼ , (𝑘 ⊕ 𝐴)⟩)    ⇒   ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ 𝐵 ∈ 𝑋) → (𝐹‘[𝐵] ∼ ) = (𝐵 ⊕ 𝐴))
Theorem	orbsta 19294*	The Orbit-Stabilizer theorem. The mapping 𝐹 is a bijection from the cosets of the stabilizer subgroup of 𝐴 to the orbit of 𝐴. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    &   ⊢ ∼ = (𝐺 ~QG 𝐻)    &   ⊢ 𝐹 = ran (𝑘 ∈ 𝑋 ↦ ⟨[𝑘] ∼ , (𝑘 ⊕ 𝐴)⟩)    &   ⊢ 𝑂 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)}    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐹:(𝑋 / ∼ )–1-1-onto→[𝐴]𝑂)
Theorem	orbsta2 19295*	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 19296	Syntax for the centralizer of a set in a monoid.
class Cntz
Syntax	ccntr 19297	Syntax for the centralizer of a monoid.
class Cntr
Definition	df-cntz 19298*	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 19299	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 19300	Substitute definition of the center. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑍‘𝐵) = (Cntr‘𝑀)