P. 192 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19101-19200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	subg0cl 19101	The group identity is an element of any subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆)
Theorem	subginvcl 19102	The inverse of an element is closed in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆) → (𝐼‘𝑋) ∈ 𝑆)
Theorem	subgcl 19103	A subgroup is closed under group operation. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆)
Theorem	subgsubcl 19104	A subgroup is closed under group subtraction. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 − 𝑌) ∈ 𝑆)
Theorem	subgsub 19105	The subtraction of elements in a subgroup is the same as subtraction in the group. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ − = (-g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ 𝑁 = (-g‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 − 𝑌) = (𝑋𝑁𝑌))
Theorem	subgmulgcl 19106	Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆)
Theorem	subgmulg 19107	A group multiple is the same if evaluated in a subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ · = (.g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ ∙ = (.g‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) = (𝑁 ∙ 𝑋))
Theorem	issubg2 19108*	Characterize the subgroups of a group by closure properties. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))))
Theorem	issubgrpd2 19109*	Prove a subgroup by closure (definition version). (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ (𝜑 → 𝑆 = (𝐼 ↾s 𝐷))    &   ⊢ (𝜑 → 0 = (0g‘𝐼))    &   ⊢ (𝜑 → + = (+g‘𝐼))    &   ⊢ (𝜑 → 𝐷 ⊆ (Base‘𝐼))    &   ⊢ (𝜑 → 0 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 + 𝑦) ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((invg‘𝐼)‘𝑥) ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (SubGrp‘𝐼))
Theorem	issubgrpd 19110*	Prove a subgroup by closure. (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ (𝜑 → 𝑆 = (𝐼 ↾s 𝐷))    &   ⊢ (𝜑 → 0 = (0g‘𝐼))    &   ⊢ (𝜑 → + = (+g‘𝐼))    &   ⊢ (𝜑 → 𝐷 ⊆ (Base‘𝐼))    &   ⊢ (𝜑 → 0 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 + 𝑦) ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((invg‘𝐼)‘𝑥) ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝑆 ∈ Grp)
Theorem	issubg3 19111*	A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)))
Theorem	issubg4 19112*	A subgroup is a nonempty subset of the group closed under subtraction. (Contributed by Mario Carneiro, 17-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 − 𝑦) ∈ 𝑆)))
Theorem	grpissubg 19113	If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then the (base set of the) group is subgroup of the other group. (Contributed by AV, 14-Mar-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = (Base‘𝐻)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) → ((𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → 𝑆 ∈ (SubGrp‘𝐺)))
Theorem	resgrpisgrp 19114	If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then the other group restricted to the base set of the group is a group. (Contributed by AV, 14-Mar-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑆 = (Base‘𝐻)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ Grp) → ((𝑆 ⊆ 𝐵 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → (𝐺 ↾s 𝑆) ∈ Grp))
Theorem	subgsubm 19115	A subgroup is a submonoid. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (SubMnd‘𝐺))
Theorem	subsubg 19116	A subgroup of a subgroup is a subgroup. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐴 ∈ (SubGrp‘𝐻) ↔ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴 ⊆ 𝑆)))
Theorem	subgint 19117	The intersection of a nonempty collection of subgroups is a subgroup. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubGrp‘𝐺))
Theorem	0subg 19118	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 19119	The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    &   ⊢ (𝜑 → 𝐴 ∈ (SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	trivsubgsnd 19120	The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    ⇒   ⊢ (𝜑 → (SubGrp‘𝐺) = {𝐵})
Theorem	isnsg 19121*	Property of being a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)))
Theorem	isnsg2 19122*	Weaken the condition of isnsg 19121 to only one side of the implication. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 → (𝑦 + 𝑥) ∈ 𝑆)))
Theorem	nsgbi 19123	Defining property of a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) ∈ 𝑆 ↔ (𝐵 + 𝐴) ∈ 𝑆))
Theorem	nsgsubg 19124	A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝑆 ∈ (SubGrp‘𝐺))
Theorem	nsgconj 19125	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 19126*	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	subgacs 19127	Subgroups are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) (Revised by Mario Carneiro, 22-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (SubGrp‘𝐺) ∈ (ACS‘𝐵))
Theorem	nsgacs 19128	Normal subgroups form an algebraic closure system. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (NrmSGrp‘𝐺) ∈ (ACS‘𝐵))
Theorem	elnmz 19129*	Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    ⇒   ⊢ (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑧 ∈ 𝑋 ((𝐴 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝐴) ∈ 𝑆)))
Theorem	nmzbi 19130*	Defining property of the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    ⇒   ⊢ ((𝐴 ∈ 𝑁 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) ∈ 𝑆 ↔ (𝐵 + 𝐴) ∈ 𝑆))
Theorem	nmzsubg 19131*	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 19132*	A subgroup is a subset of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝑁)
Theorem	isnsg4 19133*	A subgroup is normal iff its normalizer is the entire group. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 = 𝑋))
Theorem	nmznsg 19134*	Any subgroup is a normal subgroup of its normalizer. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑁)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (NrmSGrp‘𝐻))
Theorem	0nsg 19135	The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → { 0 } ∈ (NrmSGrp‘𝐺))
Theorem	nsgid 19136	The whole group is a normal subgroup of itself. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐵 ∈ (NrmSGrp‘𝐺))
Theorem	0idnsgd 19137	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 19138	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 19139	A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    ⇒   ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 1o)
Theorem	1nsgtrivd 19140	A group with exactly one normal subgroup is trivial. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 1o)    ⇒   ⊢ (𝜑 → 𝐵 = { 0 })
Theorem	releqg 19141	The left coset equivalence relation is a relation. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑅 = (𝐺 ~QG 𝑆)    ⇒   ⊢ Rel 𝑅
Theorem	eqgfval 19142*	Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑅 = (𝐺 ~QG 𝑆)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)})
Theorem	eqgval 19143	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 19144	The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ ∼ = (𝐺 ~QG 𝑌)    ⇒   ⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋)
Theorem	eqglact 19145*	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 19146	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 19147	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 19148	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 19149	Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ ∼ = (𝐺 ~QG 𝐻)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ (SubGrp‘𝐺)) → ([𝑋] ∼ = 𝐻 ↔ 𝑋 ∈ 𝐻))
Theorem	quselbas 19150*	Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025.)
⊢ ∼ = (𝐺 ~QG 𝑆)    &   ⊢ 𝑈 = (𝐺 /s ∼ )    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (𝑋 ∈ (Base‘𝑈) ↔ ∃𝑥 ∈ 𝐵 𝑋 = [𝑥] ∼ ))
Theorem	quseccl0 19151	Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) Generalization of quseccl 19153 for arbitrary sets 𝐺. (Revised by AV, 24-Feb-2025.)
⊢ ∼ = (𝐺 ~QG 𝑆)    &   ⊢ 𝐻 = (𝐺 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶) → [𝑋] ∼ ∈ 𝐵)
Theorem	qusgrp 19152	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 19153	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 19154	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 19155	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 19156	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 19157	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 19158	Addition of equivalence classes in a quotient group. (Contributed by AV, 25-Feb-2025.)
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → [(𝐴(+g‘𝑅)𝐶)] ∼ = ([𝐴] ∼ (+g‘𝑄)[𝐶] ∼ ))
Theorem	ecqusaddcl 19159	Closure of the addition in a quotient group. (Contributed by AV, 24-Feb-2025.)
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → ([𝐴] ∼ (+g‘𝑄)[𝐶] ∼ ) ∈ (Base‘𝑄))
Theorem	lagsubg2 19160	Lagrange's theorem for finite groups. Call the "order" of a group the cardinal number of the basic set of the group, and "index of a subgroup" the cardinal number of the set of left (or right, this is the same) cosets of this subgroup. Then the order of the group is the (cardinal) product of the order of any of its subgroups by the index of this subgroup. (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ ∼ = (𝐺 ~QG 𝑌)    &   ⊢ (𝜑 → 𝑌 ∈ (SubGrp‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ Fin)    ⇒   ⊢ (𝜑 → (♯‘𝑋) = ((♯‘(𝑋 / ∼ )) · (♯‘𝑌)))
Theorem	lagsubg 19161	Lagrange's theorem for Groups: the order of any subgroup of a finite group is a divisor of the order of the group. This is Metamath 100 proof #71. (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin) → (♯‘𝑌) ∥ (♯‘𝑋))
Theorem	eqg0subg 19162	The coset equivalence relation for the trivial (zero) subgroup of a group is the identity relation restricted to the base set of the group. (Contributed by AV, 25-Feb-2025.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑆 = { 0 }    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑅 = (𝐺 ~QG 𝑆)    ⇒   ⊢ (𝐺 ∈ Grp → 𝑅 = ( I ↾ 𝐵))
Theorem	eqg0subgecsn 19163	The equivalence classes modulo the coset equivalence relation for the trivial (zero) subgroup of a group are singletons. (Contributed by AV, 26-Feb-2025.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑆 = { 0 }    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑅 = (𝐺 ~QG 𝑆)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → [𝑋]𝑅 = {𝑋})
Theorem	qus0subgbas 19164*	The base set of a quotient of a group by the trivial (zero) subgroup. (Contributed by AV, 26-Feb-2025.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑆 = { 0 }    &   ⊢ ∼ = (𝐺 ~QG 𝑆)    &   ⊢ 𝑈 = (𝐺 /s ∼ )    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (Base‘𝑈) = {𝑢 ∣ ∃𝑥 ∈ 𝐵 𝑢 = {𝑥}})
Theorem	qus0subgadd 19165*	The addition in a quotient of a group by the trivial (zero) subgroup. (Contributed by AV, 26-Feb-2025.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑆 = { 0 }    &   ⊢ ∼ = (𝐺 ~QG 𝑆)    &   ⊢ 𝑈 = (𝐺 /s ∼ )    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ({𝑎} (+g‘𝑈){𝑏}) = {(𝑎(+g‘𝐺)𝑏)})
10.2.4  Cyclic monoids and groups This section contains some preliminary results about cyclic monoids and groups before the class CycGrp of cyclic groups (see df-cyg 19844) is defined in the context of Abelian groups.
Theorem	cycsubmel 19166*	Characterization of an element of the set of nonnegative integer powers of an element 𝐴. Although this theorem holds for any class 𝐺, the definition of 𝐹 is only meaningful if 𝐺 is a monoid or at least a unital magma. (Contributed by AV, 28-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴))    &   ⊢ 𝐶 = ran 𝐹    ⇒   ⊢ (𝑋 ∈ 𝐶 ↔ ∃𝑖 ∈ ℕ0 𝑋 = (𝑖 · 𝐴))
Theorem	cycsubmcl 19167*	The set of nonnegative integer powers of an element 𝐴 contains 𝐴. Although this theorem holds for any class 𝐺, the definition of 𝐹 is only meaningful if 𝐺 is a monoid or at least a unital magma. (Contributed by AV, 28-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴))    &   ⊢ 𝐶 = ran 𝐹    ⇒   ⊢ (𝐴 ∈ 𝐵 → 𝐴 ∈ 𝐶)
Theorem	cycsubm 19168*	The set of nonnegative integer powers of an element 𝐴 of a monoid forms a submonoid containing 𝐴 (see cycsubmcl 19167), called the cyclic monoid generated by the element 𝐴. This corresponds to the statement in [Lang] p. 6. (Contributed by AV, 28-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴))    &   ⊢ 𝐶 = ran 𝐹    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) → 𝐶 ∈ (SubMnd‘𝐺))
Theorem	cyccom 19169*	Condition for an operation to be commutative. Lemma for cycsubmcom 19170 and cygabl 19857. Formerly part of proof for cygabl 19857. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 20-Jan-2024.)
⊢ (𝜑 → ∀𝑐 ∈ 𝐶 ∃𝑥 ∈ 𝑍 𝑐 = (𝑥 · 𝐴))    &   ⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∀𝑛 ∈ 𝑍 ((𝑚 + 𝑛) · 𝐴) = ((𝑚 · 𝐴) + (𝑛 · 𝐴)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑍 ⊆ ℂ)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	cycsubmcom 19170*	The operation of a monoid is commutative over the set of nonnegative integer powers of an element 𝐴 of the monoid. (Contributed by AV, 20-Jan-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ ℕ0 ↦ (𝑥 · 𝐴))    &   ⊢ 𝐶 = ran 𝐹    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝐵) ∧ (𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶)) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	cycsubggend 19171*	The cyclic subgroup generated by 𝐴 includes its generator. Although this theorem holds for any class 𝐺, the definition of 𝐹 is only meaningful if 𝐺 is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴))    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → 𝐴 ∈ ran 𝐹)
Theorem	cycsubgcl 19172*	The set of integer powers of an element 𝐴 of a group forms a subgroup containing 𝐴, called the cyclic group generated by the element 𝐴. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (ran 𝐹 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ ran 𝐹))
Theorem	cycsubgss 19173*	The cyclic subgroup generated by an element 𝐴 is a subset of any subgroup containing 𝐴. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴))    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑆) → ran 𝐹 ⊆ 𝑆)
Theorem	cycsubg 19174*	The cyclic group generated by 𝐴 is the smallest subgroup containing 𝐴. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ran 𝐹 = ∩ {𝑠 ∈ (SubGrp‘𝐺) ∣ 𝐴 ∈ 𝑠})
Theorem	cycsubgcld 19175*	The cyclic subgroup generated by 𝐴 is a subgroup. Deduction related to cycsubgcl 19172. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ (SubGrp‘𝐺))
Theorem	cycsubg2 19176*	The subgroup generated by an element is exhausted by its multiples. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴))    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐾‘{𝐴}) = ran 𝐹)
Theorem	cycsubg2cl 19177	Any multiple of an element is contained in the generated cyclic subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ) → (𝑁 · 𝐴) ∈ (𝐾‘{𝐴}))
10.2.5  Elementary theory of group homomorphisms
Syntax	cghm 19178	Extend class notation with the generator of group hom-sets.
class GrpHom
Definition	df-ghm 19179*	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 19180	Lemma for group homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ Rel dom GrpHom
Theorem	isghm 19181*	Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014.) (Proof shortened by SN, 5-Jun-2025.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))))
Theorem	isghmOLD 19182*	Obsolete version of isghm 19181 as of 5-Jun-2025. (Contributed by Stefan O'Rear, 31-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))))
Theorem	isghm3 19183*	Property of a group homomorphism, similar to ismhm 18744. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))))
Theorem	ghmgrp1 19184	A group homomorphism is only defined when the domain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp)
Theorem	ghmgrp2 19185	A group homomorphism is only defined when the codomain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp)
Theorem	ghmf 19186	A group homomorphism is a function. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝑋⟶𝑌)
Theorem	ghmlin 19187	A homomorphism of groups is linear. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉)))
Theorem	ghmid 19188	A homomorphism of groups preserves the identity. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑌 = (0g‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘𝑌) = 0 )
Theorem	ghminv 19189	A homomorphism of groups preserves inverses. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑀 = (invg‘𝑆)    &   ⊢ 𝑁 = (invg‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑀‘𝑋)) = (𝑁‘(𝐹‘𝑋)))
Theorem	ghmsub 19190	Linearity of subtraction through a group homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ − = (-g‘𝑆)    &   ⊢ 𝑁 = (-g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘(𝑈 − 𝑉)) = ((𝐹‘𝑈)𝑁(𝐹‘𝑉)))
Theorem	isghmd 19191*	Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    &   ⊢ (𝜑 → 𝑆 ∈ Grp)    &   ⊢ (𝜑 → 𝑇 ∈ Grp)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	ghmmhm 19192	A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 ∈ (𝑆 MndHom 𝑇))
Theorem	ghmmhmb 19193	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 19194	A group homomorphism preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ × = (.g‘𝐻)    ⇒   ⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋)))
Theorem	ghmrn 19195	The range of a homomorphism is a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ∈ (SubGrp‘𝑇))
Theorem	0ghm 19196	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 19197	The identity homomorphism on a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ( I ↾ 𝐵) ∈ (𝐺 GrpHom 𝐺))
Theorem	resghm 19198	Restriction of a homomorphism to a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ (SubGrp‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 GrpHom 𝑇))
Theorem	resghm2 19199	One direction of resghm2b 19200. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑈) ∧ 𝑋 ∈ (SubGrp‘𝑇)) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	resghm2b 19200	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 𝑈)))