P. 138 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13701-13800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subgintm 13701*	The intersection of an inhabited collection of subgroups is a subgroup. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ ∃𝑤 𝑤 ∈ 𝑆) → ∩ 𝑆 ∈ (SubGrp‘𝐺))
Theorem	0subg 13702	The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014.) (Proof shortened by SN, 31-Jan-2025.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → { 0 } ∈ (SubGrp‘𝐺))
Theorem	trivsubgd 13703	The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    &   ⊢ (𝜑 → 𝐴 ∈ (SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	trivsubgsnd 13704	The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    ⇒   ⊢ (𝜑 → (SubGrp‘𝐺) = {𝐵})
Theorem	isnsg 13705*	Property of being a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)))
Theorem	isnsg2 13706*	Weaken the condition of isnsg 13705 to only one side of the implication. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 → (𝑦 + 𝑥) ∈ 𝑆)))
Theorem	nsgbi 13707	Defining property of a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) ∈ 𝑆 ↔ (𝐵 + 𝐴) ∈ 𝑆))
Theorem	nsgsubg 13708	A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝑆 ∈ (SubGrp‘𝐺))
Theorem	nsgconj 13709	The conjugation of an element of a normal subgroup is in the subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆) → ((𝐴 + 𝐵) − 𝐴) ∈ 𝑆)
Theorem	isnsg3 13710*	A subgroup is normal iff the conjugation of all the elements of the subgroup is in the subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑆 ((𝑥 + 𝑦) − 𝑥) ∈ 𝑆))
Theorem	elnmz 13711*	Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    ⇒   ⊢ (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑧 ∈ 𝑋 ((𝐴 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝐴) ∈ 𝑆)))
Theorem	nmzbi 13712*	Defining property of the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    ⇒   ⊢ ((𝐴 ∈ 𝑁 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) ∈ 𝑆 ↔ (𝐵 + 𝐴) ∈ 𝑆))
Theorem	nmzsubg 13713*	The normalizer NG(S) of a subset 𝑆 of the group is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝑁 ∈ (SubGrp‘𝐺))
Theorem	ssnmz 13714*	A subgroup is a subset of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝑁)
Theorem	isnsg4 13715*	A subgroup is normal iff its normalizer is the entire group. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 = 𝑋))
Theorem	nmznsg 13716*	Any subgroup is a normal subgroup of its normalizer. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑁)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (NrmSGrp‘𝐻))
Theorem	0nsg 13717	The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → { 0 } ∈ (NrmSGrp‘𝐺))
Theorem	nsgid 13718	The whole group is a normal subgroup of itself. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐵 ∈ (NrmSGrp‘𝐺))
Theorem	0idnsgd 13719	The whole group and the zero subgroup are normal subgroups of a group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    ⇒   ⊢ (𝜑 → {{ 0 }, 𝐵} ⊆ (NrmSGrp‘𝐺))
Theorem	trivnsgd 13720	The only normal subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    ⇒   ⊢ (𝜑 → (NrmSGrp‘𝐺) = {𝐵})
Theorem	triv1nsgd 13721	A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    ⇒   ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 1o)
Theorem	1nsgtrivd 13722	A group with exactly one normal subgroup is trivial. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 1o)    ⇒   ⊢ (𝜑 → 𝐵 = { 0 })
Theorem	releqgg 13723	The left coset equivalence relation is a relation. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑅 = (𝐺 ~QG 𝑆)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → Rel 𝑅)
Theorem	eqgex 13724	The left coset equivalence relation exists. (Contributed by Jim Kingdon, 25-Apr-2025.)
⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊) → (𝐺 ~QG 𝑆) ∈ V)
Theorem	eqgfval 13725*	Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑅 = (𝐺 ~QG 𝑆)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)})
Theorem	eqgval 13726	Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.) (Revised by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑅 = (𝐺 ~QG 𝑆)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → (𝐴𝑅𝐵 ↔ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ((𝑁‘𝐴) + 𝐵) ∈ 𝑆)))
Theorem	eqger 13727	The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ ∼ = (𝐺 ~QG 𝑌)    ⇒   ⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋)
Theorem	eqglact 13728*	A left coset can be expressed as the image of a left action. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ ∼ = (𝐺 ~QG 𝑌)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑌 ⊆ 𝑋 ∧ 𝐴 ∈ 𝑋) → [𝐴] ∼ = ((𝑥 ∈ 𝑋 ↦ (𝐴 + 𝑥)) “ 𝑌))
Theorem	eqgid 13729	The left coset containing the identity is the original subgroup. (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ ∼ = (𝐺 ~QG 𝑌)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝑌 ∈ (SubGrp‘𝐺) → [ 0 ] ∼ = 𝑌)
Theorem	eqgen 13730	Each coset is equipotent to the subgroup itself (which is also the coset containing the identity). (Contributed by Mario Carneiro, 20-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ ∼ = (𝐺 ~QG 𝑌)    ⇒   ⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ (𝑋 / ∼ )) → 𝑌 ≈ 𝐴)
Theorem	eqgcpbl 13731	The subgroup coset equivalence relation is compatible with addition when the subgroup is normal. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ ∼ = (𝐺 ~QG 𝑌)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑌 ∈ (NrmSGrp‘𝐺) → ((𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷) → (𝐴 + 𝐵) ∼ (𝐶 + 𝐷)))
Theorem	eqg0el 13732	Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ ∼ = (𝐺 ~QG 𝐻)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ (SubGrp‘𝐺)) → ([𝑋] ∼ = 𝐻 ↔ 𝑋 ∈ 𝐻))
Theorem	quselbasg 13733*	Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025.)
⊢ ∼ = (𝐺 ~QG 𝑆)    &   ⊢ 𝑈 = (𝐺 /s ∼ )    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊 ∧ 𝑆 ∈ 𝑍) → (𝑋 ∈ (Base‘𝑈) ↔ ∃𝑥 ∈ 𝐵 𝑋 = [𝑥] ∼ ))
Theorem	quseccl0g 13734	Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) Generalization of quseccl 13736 for arbitrary sets 𝐺. (Revised by AV, 24-Feb-2025.)
⊢ ∼ = (𝐺 ~QG 𝑆)    &   ⊢ 𝐻 = (𝐺 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶 ∧ 𝑆 ∈ 𝑍) → [𝑋] ∼ ∈ 𝐵)
Theorem	qusgrp 13735	If 𝑌 is a normal subgroup of 𝐺, then 𝐻 = 𝐺 / 𝑌 is a group, called the quotient of 𝐺 by 𝑌. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆))    ⇒   ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝐻 ∈ Grp)
Theorem	quseccl 13736	Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) (Proof shortened by AV, 9-Mar-2025.)
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆))    &   ⊢ 𝑉 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑋 ∈ 𝑉) → [𝑋](𝐺 ~QG 𝑆) ∈ 𝐵)
Theorem	qusadd 13737	Value of the group operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆))    &   ⊢ 𝑉 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ✚ = (+g‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋](𝐺 ~QG 𝑆) ✚ [𝑌](𝐺 ~QG 𝑆)) = [(𝑋 + 𝑌)](𝐺 ~QG 𝑆))
Theorem	qus0 13738	Value of the group identity operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆))    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → [ 0 ](𝐺 ~QG 𝑆) = (0g‘𝐻))
Theorem	qusinv 13739	Value of the group inverse operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆))    &   ⊢ 𝑉 = (Base‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑋 ∈ 𝑉) → (𝑁‘[𝑋](𝐺 ~QG 𝑆)) = [(𝐼‘𝑋)](𝐺 ~QG 𝑆))
Theorem	qussub 13740	Value of the group subtraction operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.)
⊢ 𝐻 = (𝐺 /s (𝐺 ~QG 𝑆))    &   ⊢ 𝑉 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝑁 = (-g‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ([𝑋](𝐺 ~QG 𝑆)𝑁[𝑌](𝐺 ~QG 𝑆)) = [(𝑋 − 𝑌)](𝐺 ~QG 𝑆))
Theorem	ecqusaddd 13741	Addition of equivalence classes in a quotient group. (Contributed by AV, 25-Feb-2025.)
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → [(𝐴(+g‘𝑅)𝐶)] ∼ = ([𝐴] ∼ (+g‘𝑄)[𝐶] ∼ ))
Theorem	ecqusaddcl 13742	Closure of the addition in a quotient group. (Contributed by AV, 24-Feb-2025.)
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → ([𝐴] ∼ (+g‘𝑄)[𝐶] ∼ ) ∈ (Base‘𝑄))
7.2.4  Elementary theory of group homomorphisms
Syntax	cghm 13743	Extend class notation with the generator of group hom-sets.
class GrpHom
Definition	df-ghm 13744*	A homomorphism of groups is a map between two structures which preserves the group operation. Requiring both sides to be groups simplifies most theorems at the cost of complicating the theorem which pushes forward a group structure. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ GrpHom = (𝑠 ∈ Grp, 𝑡 ∈ Grp ↦ {𝑔 ∣ [(Base‘𝑠) / 𝑤](𝑔:𝑤⟶(Base‘𝑡) ∧ ∀𝑥 ∈ 𝑤 ∀𝑦 ∈ 𝑤 (𝑔‘(𝑥(+g‘𝑠)𝑦)) = ((𝑔‘𝑥)(+g‘𝑡)(𝑔‘𝑦)))})
Theorem	reldmghm 13745	Lemma for group homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ Rel dom GrpHom
Theorem	isghm 13746*	Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))))
Theorem	isghm3 13747*	Property of a group homomorphism, similar to ismhm 13460. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))))
Theorem	ghmgrp1 13748	A group homomorphism is only defined when the domain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp)
Theorem	ghmgrp2 13749	A group homomorphism is only defined when the codomain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp)
Theorem	ghmf 13750	A group homomorphism is a function. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝑋⟶𝑌)
Theorem	ghmlin 13751	A homomorphism of groups is linear. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉)))
Theorem	ghmid 13752	A homomorphism of groups preserves the identity. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑌 = (0g‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘𝑌) = 0 )
Theorem	ghminv 13753	A homomorphism of groups preserves inverses. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑀 = (invg‘𝑆)    &   ⊢ 𝑁 = (invg‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑀‘𝑋)) = (𝑁‘(𝐹‘𝑋)))
Theorem	ghmsub 13754	Linearity of subtraction through a group homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ − = (-g‘𝑆)    &   ⊢ 𝑁 = (-g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘(𝑈 − 𝑉)) = ((𝐹‘𝑈)𝑁(𝐹‘𝑉)))
Theorem	isghmd 13755*	Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    &   ⊢ (𝜑 → 𝑆 ∈ Grp)    &   ⊢ (𝜑 → 𝑇 ∈ Grp)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	ghmmhm 13756	A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 ∈ (𝑆 MndHom 𝑇))
Theorem	ghmmhmb 13757	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	ghmex 13758	The set of group homomorphisms exists. (Contributed by Jim Kingdon, 15-May-2025.)
⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝑆 GrpHom 𝑇) ∈ V)
Theorem	ghmmulg 13759	A group homomorphism preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ × = (.g‘𝐻)    ⇒   ⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋)))
Theorem	ghmrn 13760	The range of a homomorphism is a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ∈ (SubGrp‘𝑇))
Theorem	0ghm 13761	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 13762	The identity homomorphism on a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ( I ↾ 𝐵) ∈ (𝐺 GrpHom 𝐺))
Theorem	resghm 13763	Restriction of a homomorphism to a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ (SubGrp‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 GrpHom 𝑇))
Theorem	resghm2 13764	One direction of resghm2b 13765. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑈) ∧ 𝑋 ∈ (SubGrp‘𝑇)) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	resghm2b 13765	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 13766	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 13767	The composition of group homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐹 ∈ (𝑇 GrpHom 𝑈) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GrpHom 𝑈))
Theorem	ghmima 13768	The image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ (SubGrp‘𝑆)) → (𝐹 “ 𝑈) ∈ (SubGrp‘𝑇))
Theorem	ghmpreima 13769	The inverse image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑉 ∈ (SubGrp‘𝑇)) → (◡𝐹 “ 𝑉) ∈ (SubGrp‘𝑆))
Theorem	ghmeql 13770	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 13771	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 13772	The inverse image of a normal subgroup under a homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑉 ∈ (NrmSGrp‘𝑇)) → (◡𝐹 “ 𝑉) ∈ (NrmSGrp‘𝑆))
Theorem	ghmker 13773	The kernel of a homomorphism is a normal subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 0 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (◡𝐹 “ { 0 }) ∈ (NrmSGrp‘𝑆))
Theorem	ghmeqker 13774	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	f1ghm0to0 13775	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 13776*	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 13777	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 13778	A bijective group homomorphism is an isomorphism. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 GrpHom 𝑆)))
Theorem	conjghm 13779*	Conjugation is an automorphism of the group. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ (𝐺 GrpHom 𝐺) ∧ 𝐹:𝑋–1-1-onto→𝑋))
Theorem	conjsubg 13780*	A conjugated subgroup is also a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → ran 𝐹 ∈ (SubGrp‘𝐺))
Theorem	conjsubgen 13781*	A conjugated subgroup is equinumerous to the original subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → 𝑆 ≈ ran 𝐹)
Theorem	conjnmz 13782*	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 13783*	Alternative condition for elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    &   ⊢ 𝑁 = {𝑦 ∈ 𝑋 ∣ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)}    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)))
Theorem	conjnsg 13784*	A normal subgroup is unchanged under conjugation. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → 𝑆 = ran 𝐹)
Theorem	qusghm 13785*	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 13786*	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 𝑀))
7.2.5  Abelian groups
7.2.5.1  Definition and basic properties
Syntax	ccmn 13787	Extend class notation with class of all commutative monoids.
class CMnd
Syntax	cabl 13788	Extend class notation with class of all Abelian groups.
class Abel
Definition	df-cmn 13789*	Define class of all commutative monoids. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ CMnd = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∀𝑏 ∈ (Base‘𝑔)(𝑎(+g‘𝑔)𝑏) = (𝑏(+g‘𝑔)𝑎)}
Definition	df-abl 13790	Define class of all Abelian groups. (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ Abel = (Grp ∩ CMnd)
Theorem	isabl 13791	The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.)
⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ CMnd))
Theorem	ablgrp 13792	An Abelian group is a group. (Contributed by NM, 26-Aug-2011.)
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp)
Theorem	ablgrpd 13793	An Abelian group is a group, deduction form of ablgrp 13792. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ (𝜑 → 𝐺 ∈ Abel)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	ablcmn 13794	An Abelian group is a commutative monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝐺 ∈ Abel → 𝐺 ∈ CMnd)
Theorem	ablcmnd 13795	An Abelian group is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝐺 ∈ Abel)    ⇒   ⊢ (𝜑 → 𝐺 ∈ CMnd)
Theorem	iscmn 13796*	The predicate "is a commutative monoid". (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ CMnd ↔ (𝐺 ∈ Mnd ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
Theorem	isabl2 13797*	The predicate "is an Abelian (commutative) group". (Contributed by NM, 17-Oct-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Abel ↔ (𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 + 𝑦) = (𝑦 + 𝑥)))
Theorem	cmnpropd 13798*	If two structures have the same group components (properties), one is a commutative monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ CMnd ↔ 𝐿 ∈ CMnd))
Theorem	ablpropd 13799*	If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 6-Dec-2014.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel))
Theorem	ablprop 13800	If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 11-Oct-2013.)
⊢ (Base‘𝐾) = (Base‘𝐿)    &   ⊢ (+g‘𝐾) = (+g‘𝐿)    ⇒   ⊢ (𝐾 ∈ Abel ↔ 𝐿 ∈ Abel)