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	mulgnn0p1 19101	Group multiple (exponentiation) operation at a successor, extended to ℕ0. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → ((𝑁 + 1) · 𝑋) = ((𝑁 · 𝑋) + 𝑋))
Theorem	mulgnnsubcl 19102*	Closure of the group multiple (exponentiation) operation in a submagma. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆)
Theorem	mulgnn0subcl 19103*	Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 0 ∈ 𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆)
Theorem	mulgsubcl 19104*	Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 0 ∈ 𝑆)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (𝐼‘𝑥) ∈ 𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆)
Theorem	mulgnncl 19105	Closure of the group multiple (exponentiation) operation for a positive multiplier in a magma. (Contributed by Mario Carneiro, 11-Dec-2014.) (Revised by AV, 29-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mgm ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵)
Theorem	mulgnn0cl 19106	Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵)
Theorem	mulgcl 19107	Closure of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵)
Theorem	mulgneg 19108	Group multiple (exponentiation) operation at a negative integer. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = (𝐼‘(𝑁 · 𝑋)))
Theorem	mulgnegneg 19109	The inverse of a negative group multiple is the positive group multiple. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝐼‘(-𝑁 · 𝑋)) = (𝑁 · 𝑋))
Theorem	mulgm1 19110	Group multiple (exponentiation) operation at negative one. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by Mario Carneiro, 20-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (-1 · 𝑋) = (𝐼‘𝑋))
Theorem	mulgnn0cld 19111	Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 19106. (Contributed by SN, 1-Feb-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁 · 𝑋) ∈ 𝐵)
Theorem	mulgcld 19112	Deduction associated with mulgcl 19107. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁 · 𝑋) ∈ 𝐵)
Theorem	mulgaddcomlem 19113	Lemma for mulgaddcom 19114. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ ((𝑦 · 𝑋) + 𝑋) = (𝑋 + (𝑦 · 𝑋))) → ((-𝑦 · 𝑋) + 𝑋) = (𝑋 + (-𝑦 · 𝑋)))
Theorem	mulgaddcom 19114	The group multiple operator commutes with the group operation. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑁 · 𝑋) + 𝑋) = (𝑋 + (𝑁 · 𝑋)))
Theorem	mulginvcom 19115	The group multiple operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · (𝐼‘𝑋)) = (𝐼‘(𝑁 · 𝑋)))
Theorem	mulginvinv 19116	The group multiple operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝐼‘(𝑁 · (𝐼‘𝑋))) = (𝑁 · 𝑋))
Theorem	mulgnn0z 19117	A group multiple of the identity, for nonnegative multiple. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0) → (𝑁 · 0 ) = 0 )
Theorem	mulgz 19118	A group multiple of the identity, for integer multiple. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → (𝑁 · 0 ) = 0 )
Theorem	mulgnndir 19119	Sum of group multiples, for positive multiples. (Contributed by Mario Carneiro, 11-Dec-2014.) (Revised by AV, 29-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
Theorem	mulgnn0dir 19120	Sum of group multiples, generalized to ℕ0. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
Theorem	mulgdirlem 19121	Lemma for mulgdir 19122. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
Theorem	mulgdir 19122	Sum of group multiples, generalized to ℤ. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
Theorem	mulgp1 19123	Group multiple (exponentiation) operation at a successor, extended to ℤ. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑁 + 1) · 𝑋) = ((𝑁 · 𝑋) + 𝑋))
Theorem	mulgneg2 19124	Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = (𝑁 · (𝐼‘𝑋)))
Theorem	mulgnnass 19125	Product of group multiples, for positive multiples in a semigroup. (Contributed by Mario Carneiro, 13-Dec-2014.) (Revised by AV, 29-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
Theorem	mulgnn0ass 19126	Product of group multiples, generalized to ℕ0. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
Theorem	mulgass 19127	Product of group multiples, generalized to ℤ. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
Theorem	mulgassr 19128	Reversed product of group multiples. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑁 · 𝑀) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
Theorem	mulgmodid 19129	Casting out multiples of the identity element leaves the group multiple unchanged. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑁 ∈ ℤ ∧ 𝑀 ∈ ℕ) ∧ (𝑋 ∈ 𝐵 ∧ (𝑀 · 𝑋) = 0 )) → ((𝑁 mod 𝑀) · 𝑋) = (𝑁 · 𝑋))
Theorem	mulgsubdir 19130	Distribution of group multiples over subtraction for group elements, subdir 11705 analog. (Contributed by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 − 𝑁) · 𝑋) = ((𝑀 · 𝑋) − (𝑁 · 𝑋)))
Theorem	mhmmulg 19131	A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ × = (.g‘𝐻)    ⇒   ⊢ ((𝐹 ∈ (𝐺 MndHom 𝐻) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝐹‘(𝑁 · 𝑋)) = (𝑁 × (𝐹‘𝑋)))
Theorem	mulgpropd 19132*	Two structures with the same group-nature have the same group multiple function. 𝐾 is expected to either be V (when strong equality is available) or 𝐵 (when closure is available). (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ · = (.g‘𝐺)    &   ⊢ × = (.g‘𝐻)    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐻))    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐾)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) ∈ 𝐾)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦))    ⇒   ⊢ (𝜑 → · = × )
Theorem	submmulgcl 19133	Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ ∙ = (.g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆) → (𝑁 ∙ 𝑋) ∈ 𝑆)
Theorem	submmulg 19134	A group multiple is the same if evaluated in a submonoid. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ ∙ = (.g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ · = (.g‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (SubMnd‘𝐺) ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑆) → (𝑁 ∙ 𝑋) = (𝑁 · 𝑋))
Theorem	pwsmulg 19135	Value of a group multiple in a structure power. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ ∙ = (.g‘𝑌)    &   ⊢ · = (.g‘𝑅)    ⇒   ⊢ (((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) ∧ (𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵 ∧ 𝐴 ∈ 𝐼)) → ((𝑁 ∙ 𝑋)‘𝐴) = (𝑁 · (𝑋‘𝐴)))
10.2.3  Subgroups and Quotient groups
Syntax	csubg 19136	Extend class notation with all subgroups of a group.
class SubGrp
Syntax	cnsg 19137	Extend class notation with all normal subgroups of a group.
class NrmSGrp
Syntax	cqg 19138	Quotient group equivalence class.
class ~QG
Definition	df-subg 19139*	Define a subgroup of a group as a set of elements that is a group in its own right. Equivalently (issubg2 19157), a subgroup is a subset of the group that is closed for the group internal operation (see subgcl 19152), contains the neutral element of the group (see subg0 19148) and contains the inverses for all of its elements (see subginvcl 19151). (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ SubGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ 𝒫 (Base‘𝑤) ∣ (𝑤 ↾s 𝑠) ∈ Grp})
Definition	df-nsg 19140*	Define the equivalence relation in a quotient ring or quotient group (where 𝑖 is a two-sided ideal or a normal subgroup). For non-normal subgroups this generates the left cosets. (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ NrmSGrp = (𝑤 ∈ Grp ↦ {𝑠 ∈ (SubGrp‘𝑤) ∣ [(Base‘𝑤) / 𝑏][(+g‘𝑤) / 𝑝]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ((𝑥𝑝𝑦) ∈ 𝑠 ↔ (𝑦𝑝𝑥) ∈ 𝑠)})
Definition	df-eqg 19141*	Define the equivalence relation in a group generated by a subgroup. More precisely, if 𝐺 is a group and 𝐻 is a subgroup, then 𝐺 ~QG 𝐻 is the equivalence relation on 𝐺 associated with the left cosets of 𝐻. A typical application of this definition is the construction of the quotient group (resp. ring) of a group (resp. ring) by a normal subgroup (resp. two-sided ideal). (Contributed by Mario Carneiro, 15-Jun-2015.)
⊢ ~QG = (𝑟 ∈ V, 𝑖 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ (Base‘𝑟) ∧ (((invg‘𝑟)‘𝑥)(+g‘𝑟)𝑦) ∈ 𝑖)})
Theorem	issubg 19142	The subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝐺 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ∧ (𝐺 ↾s 𝑆) ∈ Grp))
Theorem	subgss 19143	A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝐵)
Theorem	subgid 19144	A group is a subgroup of itself. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐵 ∈ (SubGrp‘𝐺))
Theorem	subggrp 19145	A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐻 ∈ Grp)
Theorem	subgbas 19146	The base of the restricted group in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 = (Base‘𝐻))
Theorem	subgrcl 19147	Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝐺 ∈ Grp)
Theorem	subg0 19148	A subgroup of a group must have the same identity as the group. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 = (0g‘𝐻))
Theorem	subginv 19149	The inverse of an element in a subgroup is the same as the inverse in the larger group. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ 𝐽 = (invg‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆) → (𝐼‘𝑋) = (𝐽‘𝑋))
Theorem	subg0cl 19150	The group identity is an element of any subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 0 ∈ 𝑆)
Theorem	subginvcl 19151	The inverse of an element is closed in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆) → (𝐼‘𝑋) ∈ 𝑆)
Theorem	subgcl 19152	A subgroup is closed under group operation. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆)
Theorem	subgsubcl 19153	A subgroup is closed under group subtraction. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 − 𝑌) ∈ 𝑆)
Theorem	subgsub 19154	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 19155	Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆)
Theorem	subgmulg 19156	A group multiple is the same if evaluated in a subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ · = (.g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ ∙ = (.g‘𝐻)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) = (𝑁 ∙ 𝑋))
Theorem	issubg2 19157*	Characterize the subgroups of a group by closure properties. (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀𝑥 ∈ 𝑆 (∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆 ∧ (𝐼‘𝑥) ∈ 𝑆))))
Theorem	issubgrpd2 19158*	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 19159*	Prove a subgroup by closure. (Contributed by Stefan O'Rear, 7-Dec-2014.)
⊢ (𝜑 → 𝑆 = (𝐼 ↾s 𝐷))    &   ⊢ (𝜑 → 0 = (0g‘𝐼))    &   ⊢ (𝜑 → + = (+g‘𝐼))    &   ⊢ (𝜑 → 𝐷 ⊆ (Base‘𝐼))    &   ⊢ (𝜑 → 0 ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷) → (𝑥 + 𝑦) ∈ 𝐷)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → ((invg‘𝐼)‘𝑥) ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝑆 ∈ Grp)
Theorem	issubg3 19160*	A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝑆 ∈ (SubGrp‘𝐺) ↔ (𝑆 ∈ (SubMnd‘𝐺) ∧ ∀𝑥 ∈ 𝑆 (𝐼‘𝑥) ∈ 𝑆)))
Theorem	issubg4 19161*	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 19162	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 19163	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 19164	A subgroup is a submonoid. (Contributed by Mario Carneiro, 18-Jun-2015.)
⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (SubMnd‘𝐺))
Theorem	subsubg 19165	A subgroup of a subgroup is a subgroup. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑆)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → (𝐴 ∈ (SubGrp‘𝐻) ↔ (𝐴 ∈ (SubGrp‘𝐺) ∧ 𝐴 ⊆ 𝑆)))
Theorem	subgint 19166	The intersection of a nonempty collection of subgroups is a subgroup. (Contributed by Mario Carneiro, 7-Dec-2014.)
⊢ ((𝑆 ⊆ (SubGrp‘𝐺) ∧ 𝑆 ≠ ∅) → ∩ 𝑆 ∈ (SubGrp‘𝐺))
Theorem	0subg 19167	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	0subgOLD 19168	Obsolete version of 0subg 19167 as of 31-Jan-2025. (Contributed by Stefan O'Rear, 10-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → { 0 } ∈ (SubGrp‘𝐺))
Theorem	trivsubgd 19169	The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    &   ⊢ (𝜑 → 𝐴 ∈ (SubGrp‘𝐺))    ⇒   ⊢ (𝜑 → 𝐴 = 𝐵)
Theorem	trivsubgsnd 19170	The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    ⇒   ⊢ (𝜑 → (SubGrp‘𝐺) = {𝐵})
Theorem	isnsg 19171*	Property of being a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)))
Theorem	isnsg2 19172*	Weaken the condition of isnsg 19171 to only one side of the implication. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 → (𝑦 + 𝑥) ∈ 𝑆)))
Theorem	nsgbi 19173	Defining property of a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (NrmSGrp‘𝐺) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) ∈ 𝑆 ↔ (𝐵 + 𝐴) ∈ 𝑆))
Theorem	nsgsubg 19174	A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ (𝑆 ∈ (NrmSGrp‘𝐺) → 𝑆 ∈ (SubGrp‘𝐺))
Theorem	nsgconj 19175	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 19176*	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 19177	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 19178	Normal subgroups form an algebraic closure system. (Contributed by Stefan O'Rear, 4-Sep-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (NrmSGrp‘𝐺) ∈ (ACS‘𝐵))
Theorem	elnmz 19179*	Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    ⇒   ⊢ (𝐴 ∈ 𝑁 ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑧 ∈ 𝑋 ((𝐴 + 𝑧) ∈ 𝑆 ↔ (𝑧 + 𝐴) ∈ 𝑆)))
Theorem	nmzbi 19180*	Defining property of the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    ⇒   ⊢ ((𝐴 ∈ 𝑁 ∧ 𝐵 ∈ 𝑋) → ((𝐴 + 𝐵) ∈ 𝑆 ↔ (𝐵 + 𝐴) ∈ 𝑆))
Theorem	nmzsubg 19181*	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 19182*	A subgroup is a subset of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ⊆ 𝑁)
Theorem	isnsg4 19183*	A subgroup is normal iff its normalizer is the entire group. (Contributed by Mario Carneiro, 18-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑆 ∈ (NrmSGrp‘𝐺) ↔ (𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑁 = 𝑋))
Theorem	nmznsg 19184*	Any subgroup is a normal subgroup of its normalizer. (Contributed by Mario Carneiro, 19-Jan-2015.)
⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑆 ↔ (𝑦 + 𝑥) ∈ 𝑆)}    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑁)    ⇒   ⊢ (𝑆 ∈ (SubGrp‘𝐺) → 𝑆 ∈ (NrmSGrp‘𝐻))
Theorem	0nsg 19185	The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → { 0 } ∈ (NrmSGrp‘𝐺))
Theorem	nsgid 19186	The whole group is a normal subgroup of itself. (Contributed by Mario Carneiro, 4-Feb-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐵 ∈ (NrmSGrp‘𝐺))
Theorem	0idnsgd 19187	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 19188	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 19189	A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 = { 0 })    ⇒   ⊢ (𝜑 → (NrmSGrp‘𝐺) ≈ 1o)
Theorem	1nsgtrivd 19190	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 19191	The left coset equivalence relation is a relation. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ 𝑅 = (𝐺 ~QG 𝑆)    ⇒   ⊢ Rel 𝑅
Theorem	eqgfval 19192*	Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑅 = (𝐺 ~QG 𝑆)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑆 ⊆ 𝑋) → 𝑅 = {⟨𝑥, 𝑦⟩ ∣ ({𝑥, 𝑦} ⊆ 𝑋 ∧ ((𝑁‘𝑥) + 𝑦) ∈ 𝑆)})
Theorem	eqgval 19193	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 19194	The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ ∼ = (𝐺 ~QG 𝑌)    ⇒   ⊢ (𝑌 ∈ (SubGrp‘𝐺) → ∼ Er 𝑋)
Theorem	eqglact 19195*	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 19196	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 19197	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 19198	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 19199	Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.)
⊢ ∼ = (𝐺 ~QG 𝐻)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐻 ∈ (SubGrp‘𝐺)) → ([𝑋] ∼ = 𝐻 ↔ 𝑋 ∈ 𝐻))
Theorem	quselbas 19200*	Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025.)
⊢ ∼ = (𝐺 ~QG 𝑆)    &   ⊢ 𝑈 = (𝐺 /s ∼ )    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑋 ∈ 𝑊) → (𝑋 ∈ (Base‘𝑈) ↔ ∃𝑥 ∈ 𝐵 𝑋 = [𝑥] ∼ ))