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	ghmnsgima 19301	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 19302	The inverse image of a normal subgroup under a homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑉 ∈ (NrmSGrp‘𝑇)) → (◡𝐹 “ 𝑉) ∈ (NrmSGrp‘𝑆))
Theorem	ghmker 19303	The kernel of a homomorphism is a normal subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 0 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (◡𝐹 “ { 0 }) ∈ (NrmSGrp‘𝑆))
Theorem	ghmeqker 19304	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 19305*	Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 GrpHom 𝑌))
Theorem	f1ghm0to0 19306	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 19307*	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 19308	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 19309	A bijective group homomorphism is an isomorphism. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 GrpHom 𝑆)))
Theorem	conjghm 19310*	Conjugation is an automorphism of the group. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ (𝐺 GrpHom 𝐺) ∧ 𝐹:𝑋–1-1-onto→𝑋))
Theorem	conjsubg 19311*	A conjugated subgroup is also a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → ran 𝐹 ∈ (SubGrp‘𝐺))
Theorem	conjsubgen 19312*	A conjugated subgroup is equinumerous to the original subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → 𝑆 ≈ ran 𝐹)
Theorem	conjnmz 19313*	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 19314*	Alternative condition for elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    &   ⊢ 𝑁 = {𝑦 ∈ 𝑋 ∣ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)}    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)))
Theorem	conjnsg 19315*	A normal subgroup is unchanged under conjugation. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → 𝑆 = ran 𝐹)
Theorem	qusghm 19316*	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 19317*	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 19318	The class of group isomorphism sets.
class GrpIso
Syntax	cgic 19319	The class of the group isomorphism relation.
class ≃𝑔
Definition	df-gim 19320*	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 19321	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 19322	The group isomorphism function is a well-defined function. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ GrpIso Fn (Grp × Grp)
Theorem	isgim 19323	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 19324	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 19325	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 19326	A group isomorphism is a homomorphism whose converse is also a homomorphism. Characterization of isomorphisms similar to ishmeo 23877. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) ↔ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 GrpHom 𝑅)))
Theorem	subggim 19327	Behavior of subgroups under isomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝐹 ∈ (𝑅 GrpIso 𝑆) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝐹 “ 𝐴) ∈ (SubGrp‘𝑆)))
Theorem	gimcnv 19328	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 19329	The composition of group isomorphisms is a group isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ((𝐹 ∈ (𝑇 GrpIso 𝑈) ∧ 𝐺 ∈ (𝑆 GrpIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GrpIso 𝑈))
Theorem	gim0to0 19330	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 19331	The relation "is isomorphic to" for groups. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑔 𝑆 ↔ (𝑅 GrpIso 𝑆) ≠ ∅)
Theorem	brgici 19332	Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) → 𝑅 ≃𝑔 𝑆)
Theorem	gicref 19333	Isomorphism is reflexive. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ (𝑅 ∈ Grp → 𝑅 ≃𝑔 𝑅)
Theorem	giclcl 19334	Isomorphism implies the left side is a group. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑔 𝑆 → 𝑅 ∈ Grp)
Theorem	gicrcl 19335	Isomorphism implies the right side is a group. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝑅 ≃𝑔 𝑆 → 𝑆 ∈ Grp)
Theorem	gicsym 19336	Isomorphism is symmetric. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ (𝑅 ≃𝑔 𝑆 → 𝑆 ≃𝑔 𝑅)
Theorem	gictr 19337	Isomorphism is transitive. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ((𝑅 ≃𝑔 𝑆 ∧ 𝑆 ≃𝑔 𝑇) → 𝑅 ≃𝑔 𝑇)
Theorem	gicer 19338	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 19339	Isomorphic groups have equinumerous base sets. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐶 = (Base‘𝑆)    ⇒   ⊢ (𝑅 ≃𝑔 𝑆 → 𝐵 ≈ 𝐶)
Theorem	gicsubgen 19340	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 19341*	Lemma for ghmqusnsg 19343. (Contributed by Thierry Arnoux, 13-May-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    &   ⊢ (𝜑 → 𝑁 ⊆ 𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐺))    ⇒   ⊢ (𝜑 → (𝐽‘[𝑋](𝐺 ~QG 𝑁)) = (𝐹‘𝑋))
Theorem	ghmqusnsglem2 19342*	Lemma for ghmqusnsg 19343. (Contributed by Thierry Arnoux, 13-May-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝑁))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    &   ⊢ (𝜑 → 𝑁 ⊆ 𝐾)    &   ⊢ (𝜑 → 𝑁 ∈ (NrmSGrp‘𝐺))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑄))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 (𝐽‘𝑌) = (𝐹‘𝑥))
Theorem	ghmqusnsg 19343*	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 19344*	Lemma for ghmqusker 19348. (Contributed by Thierry Arnoux, 14-Feb-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐺))    ⇒   ⊢ (𝜑 → (𝐽‘[𝑋](𝐺 ~QG 𝐾)) = (𝐹‘𝑋))
Theorem	ghmquskerco 19345*	In the case of theorem ghmqusker 19348, 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 19346*	Lemma for ghmqusker 19348. (Contributed by Thierry Arnoux, 14-Feb-2025.)
⊢ 0 = (0g‘𝐻)    &   ⊢ (𝜑 → 𝐹 ∈ (𝐺 GrpHom 𝐻))    &   ⊢ 𝐾 = (◡𝐹 “ { 0 })    &   ⊢ 𝑄 = (𝐺 /s (𝐺 ~QG 𝐾))    &   ⊢ 𝐽 = (𝑞 ∈ (Base‘𝑄) ↦ ∪ (𝐹 “ 𝑞))    &   ⊢ (𝜑 → 𝑌 ∈ (Base‘𝑄))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 (𝐽‘𝑌) = (𝐹‘𝑥))
Theorem	ghmquskerlem3 19347*	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 19348*	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 19349	The image 𝐻 of a group homomorphism 𝐹 is isomorphic with the quotient group 𝑄 over 𝐹's kernel 𝐾. Together with ghmker 19303 and ghmima 19298, 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 19350	Extend class definition to include the class of group actions.
class GrpAct
Definition	df-ga 19351*	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 19352*	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 19367). 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 19353	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 19354	The right argument of a group action is a set. (Contributed by Mario Carneiro, 30-Apr-2015.)
⊢ ( ⊕ ∈ (𝐺 GrpAct 𝑌) → 𝑌 ∈ V)
Theorem	gagrpid 19355	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 19356	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 19357	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 19358	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 19359	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 19360	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 19361*	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 19362*	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 19363	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 19364*	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 19365	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 19366	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 19367*	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 19368*	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 19369*	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 19370*	The stabilizer subgroup in a group action. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → 𝐻 ∈ (SubGrp‘𝐺))
Theorem	gastacos 19371*	Write the coset relation for the stabilizer subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    &   ⊢ ∼ = (𝐺 ~QG 𝐻)    ⇒   ⊢ ((( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) ∧ (𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐵 ∼ 𝐶 ↔ (𝐵 ⊕ 𝐴) = (𝐶 ⊕ 𝐴)))
Theorem	orbstafun 19372*	Existence and uniqueness for the function of orbsta 19374. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐴) = 𝐴}    &   ⊢ ∼ = (𝐺 ~QG 𝐻)    &   ⊢ 𝐹 = ran (𝑘 ∈ 𝑋 ↦ ⟨[𝑘] ∼ , (𝑘 ⊕ 𝐴)⟩)    ⇒   ⊢ (( ⊕ ∈ (𝐺 GrpAct 𝑌) ∧ 𝐴 ∈ 𝑌) → Fun 𝐹)
Theorem	orbstaval 19373*	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 19374*	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 19375*	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 19376	Syntax for the centralizer of a set in a monoid.
class Cntz
Syntax	ccntr 19377	Syntax for the centralizer of a monoid.
class Cntr
Definition	df-cntz 19378*	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 19379	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 19380	Substitute definition of the center. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑍‘𝐵) = (Cntr‘𝑀)
Theorem	cntzfval 19381*	First level substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑀 ∈ 𝑉 → 𝑍 = (𝑠 ∈ 𝒫 𝐵 ↦ {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑠 (𝑥 + 𝑦) = (𝑦 + 𝑥)}))
Theorem	cntzval 19382*	Definition substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) = (𝑦 + 𝑥)})
Theorem	elcntz 19383*	Elementhood in the centralizer. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑆 ⊆ 𝐵 → (𝐴 ∈ (𝑍‘𝑆) ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝑆 (𝐴 + 𝑦) = (𝑦 + 𝐴))))
Theorem	cntzel 19384*	Membership in a centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ (𝑍‘𝑆) ↔ ∀𝑦 ∈ 𝑆 (𝑋 + 𝑦) = (𝑦 + 𝑋)))
Theorem	cntzsnval 19385*	Special substitution for the centralizer of a singleton. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑌 ∈ 𝐵 → (𝑍‘{𝑌}) = {𝑥 ∈ 𝐵 ∣ (𝑥 + 𝑌) = (𝑌 + 𝑥)})
Theorem	elcntzsn 19386	Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑌 ∈ 𝐵 → (𝑋 ∈ (𝑍‘{𝑌}) ↔ (𝑋 ∈ 𝐵 ∧ (𝑋 + 𝑌) = (𝑌 + 𝑋))))
Theorem	sscntz 19387*	A centralizer expression for two sets elementwise commuting. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑆 ⊆ (𝑍‘𝑇) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑇 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
Theorem	cntzrcl 19388	Reverse closure for elements of the centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑋 ∈ (𝑍‘𝑆) → (𝑀 ∈ V ∧ 𝑆 ⊆ 𝐵))
Theorem	cntzssv 19389	The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑍‘𝑆) ⊆ 𝐵
Theorem	cntzi 19390	Membership in a centralizer (inference). (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑋 ∈ (𝑍‘𝑆) ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	elcntr 19391*	Elementhood in the center of a magma. (Contributed by SN, 21-Mar-2025.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntr‘𝑀)    ⇒   ⊢ (𝐴 ∈ 𝑍 ↔ (𝐴 ∈ 𝐵 ∧ ∀𝑦 ∈ 𝐵 (𝐴 + 𝑦) = (𝑦 + 𝐴)))
Theorem	cntrss 19392	The center is a subset of the base field. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ (Cntr‘𝑀) ⊆ 𝐵
Theorem	cntri 19393	Defining property of the center of a group. (Contributed by Mario Carneiro, 22-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ + = (+g‘𝑀)    &   ⊢ 𝑍 = (Cntr‘𝑀)    ⇒   ⊢ ((𝑋 ∈ 𝑍 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	resscntz 19394	Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝑍 = (Cntz‘𝐺)    &   ⊢ 𝑌 = (Cntz‘𝐻)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑆 ⊆ 𝐴) → (𝑌‘𝑆) = ((𝑍‘𝑆) ∩ 𝐴))
Theorem	cntzsgrpcl 19395*	Centralizers are closed under the semigroup operation. (Contributed by AV, 17-Feb-2025.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    &   ⊢ 𝐶 = (𝑍‘𝑆)    ⇒   ⊢ ((𝑀 ∈ Smgrp ∧ 𝑆 ⊆ 𝐵) → ∀𝑦 ∈ 𝐶 ∀𝑧 ∈ 𝐶 (𝑦(+g‘𝑀)𝑧) ∈ 𝐶)
Theorem	cntz2ss 19396	Centralizers reverse the subset relation. (Contributed by Mario Carneiro, 3-Oct-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝑆) → (𝑍‘𝑆) ⊆ (𝑍‘𝑇))
Theorem	cntzrec 19397	Reciprocity relationship for centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑆 ⊆ 𝐵 ∧ 𝑇 ⊆ 𝐵) → (𝑆 ⊆ (𝑍‘𝑇) ↔ 𝑇 ⊆ (𝑍‘𝑆)))
Theorem	cntziinsn 19398*	Express any centralizer as an intersection of singleton centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ (𝑆 ⊆ 𝐵 → (𝑍‘𝑆) = (𝐵 ∩ ∩ 𝑥 ∈ 𝑆 (𝑍‘{𝑥})))
Theorem	cntzsubm 19399	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 19400	Centralizers in a group are subgroups. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → (𝑍‘𝑆) ∈ (SubGrp‘𝑀))