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	0idnsgd 19201	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 19202	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 19203	A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    ⇒   ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 1o)
Theorem	1nsgtrivd 19204	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 19205	The left coset equivalence relation is a relation. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑅 = (𝐺 ~QG 𝑆)    ⇒   ⊢ Rel 𝑅
Theorem	eqgfval 19206*	Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑅 = (𝐺 ~QG 𝑆)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)})
Theorem	eqgval 19207	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 19208	The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ ∼ = (𝐺 ~QG 𝑌)    ⇒   ⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋)
Theorem	eqglact 19209*	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 19210	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 19211	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 19212	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 19213	Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ ∼ = (𝐺 ~QG 𝐻)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ (SubGrp‘𝐺)) → ([𝑋] ∼ = 𝐻 ↔ 𝑋 ∈ 𝐻))
Theorem	quselbas 19214*	Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025.)
⊢ ∼ = (𝐺 ~QG 𝑆)    &   ⊢ 𝑈 = (𝐺 /s ∼ )    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (𝑋 ∈ (Base‘𝑈) ↔ ∃𝑥 ∈ 𝐵 𝑋 = [𝑥] ∼ ))
Theorem	quseccl0 19215	Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) Generalization of quseccl 19217 for arbitrary sets 𝐺. (Revised by AV, 24-Feb-2025.)
⊢ ∼ = (𝐺 ~QG 𝑆)    &   ⊢ 𝐻 = (𝐺 /s ∼ )    &   ⊢ 𝐶 = (Base‘𝐺)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝐶) → [𝑋] ∼ ∈ 𝐵)
Theorem	qusgrp 19216	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 19217	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 19218	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 19219	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 19220	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 19221	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 19222	Addition of equivalence classes in a quotient group. (Contributed by AV, 25-Feb-2025.)
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → [(𝐴(+g‘𝑅)𝐶)] ∼ = ([𝐴] ∼ (+g‘𝑄)[𝐶] ∼ ))
Theorem	ecqusaddcl 19223	Closure of the addition in a quotient group. (Contributed by AV, 24-Feb-2025.)
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅))    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ ∼ = (𝑅 ~QG 𝐼)    &   ⊢ 𝑄 = (𝑅 /s ∼ )    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ 𝐵 ∧ 𝐶 ∈ 𝐵)) → ([𝐴] ∼ (+g‘𝑄)[𝐶] ∼ ) ∈ (Base‘𝑄))
Theorem	lagsubg2 19224	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 19225	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 19226	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 19227	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 19228*	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 19229*	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 19910) is defined in the context of Abelian groups.
Theorem	cycsubmel 19230*	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 19231*	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 19232*	The set of nonnegative integer powers of an element 𝐴 of a monoid forms a submonoid containing 𝐴 (see cycsubmcl 19231), 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 19233*	Condition for an operation to be commutative. Lemma for cycsubmcom 19234 and cygabl 19923. Formerly part of proof for cygabl 19923. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 20-Jan-2024.)
⊢ (𝜑 → ∀𝑐 ∈ 𝐶 ∃𝑥 ∈ 𝑍 𝑐 = (𝑥 · 𝐴))    &   ⊢ (𝜑 → ∀𝑚 ∈ 𝑍 ∀𝑛 ∈ 𝑍 ((𝑚 + 𝑛) · 𝐴) = ((𝑚 · 𝐴) + (𝑛 · 𝐴)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑍 ⊆ ℂ)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	cycsubmcom 19234*	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 19235*	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 19236*	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 19237*	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 19238*	The cyclic group generated by 𝐴 is the smallest subgroup containing 𝐴. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ran 𝐹 = ∩ {𝑠 ∈ (SubGrp‘𝐺) ∣ 𝐴 ∈ 𝑠})
Theorem	cycsubgcld 19239*	The cyclic subgroup generated by 𝐴 is a subgroup. Deduction related to cycsubgcl 19236. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑛 ∈ ℤ ↦ (𝑛 · 𝐴))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ran 𝐹 ∈ (SubGrp‘𝐺))
Theorem	cycsubg2 19240*	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 19241	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 19242	Extend class notation with the generator of group hom-sets.
class GrpHom
Definition	df-ghm 19243*	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 19244	Lemma for group homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ Rel dom GrpHom
Theorem	isghm 19245*	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 19246*	Obsolete version of isghm 19245 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 19247*	Property of a group homomorphism, similar to ismhm 18810. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) → (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑢 ∈ 𝑋 ∀𝑣 ∈ 𝑋 (𝐹‘(𝑢 + 𝑣)) = ((𝐹‘𝑢) ⨣ (𝐹‘𝑣)))))
Theorem	ghmgrp1 19248	A group homomorphism is only defined when the domain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑆 ∈ Grp)
Theorem	ghmgrp2 19249	A group homomorphism is only defined when the codomain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝑇 ∈ Grp)
Theorem	ghmf 19250	A group homomorphism is a function. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝑋⟶𝑌)
Theorem	ghmlin 19251	A homomorphism of groups is linear. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ∈ 𝑋) → (𝐹‘(𝑈 + 𝑉)) = ((𝐹‘𝑈) ⨣ (𝐹‘𝑉)))
Theorem	ghmid 19252	A homomorphism of groups preserves the identity. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑌 = (0g‘𝑆)    &   ⊢ 0 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹‘𝑌) = 0 )
Theorem	ghminv 19253	A homomorphism of groups preserves inverses. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑀 = (invg‘𝑆)    &   ⊢ 𝑁 = (invg‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑀‘𝑋)) = (𝑁‘(𝐹‘𝑋)))
Theorem	ghmsub 19254	Linearity of subtraction through a group homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝐵 = (Base‘𝑆)    &   ⊢ − = (-g‘𝑆)    &   ⊢ 𝑁 = (-g‘𝑇)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵) → (𝐹‘(𝑈 − 𝑉)) = ((𝐹‘𝑈)𝑁(𝐹‘𝑉)))
Theorem	isghmd 19255*	Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    &   ⊢ + = (+g‘𝑆)    &   ⊢ ⨣ = (+g‘𝑇)    &   ⊢ (𝜑 → 𝑆 ∈ Grp)    &   ⊢ (𝜑 → 𝑇 ∈ Grp)    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	ghmmhm 19256	A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹 ∈ (𝑆 MndHom 𝑇))
Theorem	ghmmhmb 19257	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 19258	A group homomorphism preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ × = (.g‘𝐻)    ⇒   ⊢ ((𝐹 ∈ (𝐺 GrpHom 𝐻) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋)))
Theorem	ghmrn 19259	The range of a homomorphism is a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → ran 𝐹 ∈ (SubGrp‘𝑇))
Theorem	0ghm 19260	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 19261	The identity homomorphism on a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ( I ↾ 𝐵) ∈ (𝐺 GrpHom 𝐺))
Theorem	resghm 19262	Restriction of a homomorphism to a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ 𝑈 = (𝑆 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑋 ∈ (SubGrp‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 GrpHom 𝑇))
Theorem	resghm2 19263	One direction of resghm2b 19264. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.)
⊢ 𝑈 = (𝑇 ↾s 𝑋)    ⇒   ⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑈) ∧ 𝑋 ∈ (SubGrp‘𝑇)) → 𝐹 ∈ (𝑆 GrpHom 𝑇))
Theorem	resghm2b 19264	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 19265	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 19266	The composition of group homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
⊢ ((𝐹 ∈ (𝑇 GrpHom 𝑈) ∧ 𝐺 ∈ (𝑆 GrpHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GrpHom 𝑈))
Theorem	ghmima 19267	The image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑈 ∈ (SubGrp‘𝑆)) → (𝐹 “ 𝑈) ∈ (SubGrp‘𝑇))
Theorem	ghmpreima 19268	The inverse image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.)
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑉 ∈ (SubGrp‘𝑇)) → (◡𝐹 “ 𝑉) ∈ (SubGrp‘𝑆))
Theorem	ghmeql 19269	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 19270	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 19271	The inverse image of a normal subgroup under a homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ ((𝐹 ∈ (𝑆 GrpHom 𝑇) ∧ 𝑉 ∈ (NrmSGrp‘𝑇)) → (◡𝐹 “ 𝑉) ∈ (NrmSGrp‘𝑆))
Theorem	ghmker 19272	The kernel of a homomorphism is a normal subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 0 = (0g‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (◡𝐹 “ { 0 }) ∈ (NrmSGrp‘𝑆))
Theorem	ghmeqker 19273	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 19274*	Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥}))    ⇒   ⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 GrpHom 𝑌))
Theorem	f1ghm0to0 19275	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 19276*	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 19277	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 19278	A bijective group homomorphism is an isomorphism. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝑆)    &   ⊢ 𝑌 = (Base‘𝑇)    ⇒   ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋–1-1-onto→𝑌 ↔ ◡𝐹 ∈ (𝑇 GrpHom 𝑆)))
Theorem	conjghm 19279*	Conjugation is an automorphism of the group. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐹 ∈ (𝐺 GrpHom 𝐺) ∧ 𝐹:𝑋–1-1-onto→𝑋))
Theorem	conjsubg 19280*	A conjugated subgroup is also a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → ran 𝐹 ∈ (SubGrp‘𝐺))
Theorem	conjsubgen 19281*	A conjugated subgroup is equinumerous to the original subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → 𝑆 ≈ ran 𝐹)
Theorem	conjnmz 19282*	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 19283*	Alternative condition for elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    &   ⊢ 𝑁 = {𝑦 ∈ 𝑋 ∣ ∀𝑧 ∈ 𝑋 ((𝑦 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝑦) ∈ 𝑆)}    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹)))
Theorem	conjnsg 19284*	A normal subgroup is unchanged under conjugation. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ ((𝐴 + 𝑥) − 𝐴))    ⇒   ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋) → 𝑆 = ran 𝐹)
Theorem	qusghm 19285*	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 19286*	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 19287	The class of group isomorphism sets.
class GrpIso
Syntax	cgic 19288	The class of the group isomorphism relation.
class ≃𝑔
Definition	df-gim 19289*	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 19290	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 19291	The group isomorphism function is a well-defined function. (Contributed by Mario Carneiro, 23-Aug-2015.)
⊢ GrpIso Fn (Grp × Grp)
Theorem	isgim 19292	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 19293	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 19294	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 19295	A group isomorphism is a homomorphism whose converse is also a homomorphism. Characterization of isomorphisms similar to ishmeo 23782. (Contributed by Mario Carneiro, 6-May-2015.)
⊢ (𝐹 ∈ (𝑅 GrpIso 𝑆) ↔ (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ◡𝐹 ∈ (𝑆 GrpHom 𝑅)))
Theorem	subggim 19296	Behavior of subgroups under isomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.)
⊢ 𝐵 = (Base‘𝑅)    ⇒   ⊢ ((𝐹 ∈ (𝑅 GrpIso 𝑆) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∈ (SubGrp‘𝑅) ↔ (𝐹 “ 𝐴) ∈ (SubGrp‘𝑆)))
Theorem	gimcnv 19297	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 19298	The composition of group isomorphisms is a group isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.)
⊢ ((𝐹 ∈ (𝑇 GrpIso 𝑈) ∧ 𝐺 ∈ (𝑆 GrpIso 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 GrpIso 𝑈))
Theorem	gim0to0 19299	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 19300	The relation "is isomorphic to" for groups. (Contributed by Stefan O'Rear, 25-Jan-2015.)
⊢ (𝑅 ≃𝑔 𝑆 ↔ (𝑅 GrpIso 𝑆) ≠ ∅)