P. 133 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13201-13300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gsumwcl 13201	Closure of the composite of a word in a structure 𝐺. (Contributed by Stefan O'Rear, 15-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵)
Theorem	gsumwmhm 13202	Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ 𝐵 = (Base‘𝑀)    ⇒   ⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊)))
Theorem	gsumfzcl 13203	Closure of a finite group sum. (Contributed by Mario Carneiro, 15-Dec-2014.) (Revised by AV, 3-Jun-2019.) (Revised by Jim Kingdon, 16-Aug-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝑁 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵)    ⇒   ⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵)
7.2  Groups
7.2.1  Definition and basic properties
Syntax	cgrp 13204	Extend class notation with class of all groups.
class Grp
Syntax	cminusg 13205	Extend class notation with inverse of group element.
class invg
Syntax	csg 13206	Extend class notation with group subtraction (or division) operation.
class -g
Definition	df-grp 13207*	Define class of all groups. A group is a monoid (df-mnd 13121) whose internal operation is such that every element admits a left inverse (which can be proven to be a two-sided inverse). Thus, a group 𝐺 is an algebraic structure formed from a base set of elements (notated (Base‘𝐺) per df-base 12711) and an internal group operation (notated (+g‘𝐺) per df-plusg 12795). The operation combines any two elements of the group base set and must satisfy the 4 group axioms: closure (the result of the group operation must always be a member of the base set, see grpcl 13212), associativity (so ((𝑎+g𝑏)+g𝑐) = (𝑎+g(𝑏+g𝑐)) for any a, b, c, see grpass 13213), identity (there must be an element 𝑒 = (0g‘𝐺) such that 𝑒+g𝑎 = 𝑎+g𝑒 = 𝑎 for any a), and inverse (for each element a in the base set, there must be an element 𝑏 = invg𝑎 in the base set such that 𝑎+g𝑏 = 𝑏+g𝑎 = 𝑒). It can be proven that the identity element is unique (grpideu 13215). Groups need not be commutative; a commutative group is an Abelian group. Subgroups can often be formed from groups. An example of an (Abelian) group is the set of complex numbers ℂ over the group operation + (addition). Other structures include groups, including unital rings and fields. (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)}
Definition	df-minusg 13208*	Define inverse of group element. (Contributed by NM, 24-Aug-2011.)
⊢ invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))))
Definition	df-sbg 13209*	Define group subtraction (also called division for multiplicative groups). (Contributed by NM, 31-Mar-2014.)
⊢ -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))))
Theorem	isgrp 13210*	The predicate "is a group". (This theorem demonstrates the use of symbols as variable names, first proposed by FL in 2010.) (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Mnd ∧ ∀𝑎 ∈ 𝐵 ∃𝑚 ∈ 𝐵 (𝑚 + 𝑎) = 0 ))
Theorem	grpmnd 13211	A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
Theorem	grpcl 13212	Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	grpass 13213	A group operation is associative. (Contributed by NM, 14-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	grpinvex 13214*	Every member of a group has a left inverse. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 0 )
Theorem	grpideu 13215*	The two-sided identity element of a group is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 8-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ∃!𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥))
Theorem	grpassd 13216	A group operation is associative. (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	grpmndd 13217	A group is a monoid. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝐺 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Mnd)
Theorem	grpcld 13218	Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	grpplusf 13219	The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐹 = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐹:(𝐵 × 𝐵)⟶𝐵)
Theorem	grpplusfo 13220	The group addition operation is a function onto the base set/set of group elements. (Contributed by NM, 30-Oct-2006.) (Revised by AV, 30-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐹 = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐹:(𝐵 × 𝐵)–onto→𝐵)
Theorem	grppropd 13221*	If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp))
Theorem	grpprop 13222	If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by NM, 11-Oct-2013.)
⊢ (Base‘𝐾) = (Base‘𝐿)    &   ⊢ (+g‘𝐾) = (+g‘𝐿)    ⇒   ⊢ (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp)
Theorem	grppropstrg 13223	Generalize a specific 2-element group 𝐿 to show that any set 𝐾 with the same (relevant) properties is also a group. (Contributed by NM, 28-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ (Base‘𝐾) = 𝐵    &   ⊢ (+g‘𝐾) = +    &   ⊢ 𝐿 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}    ⇒   ⊢ (𝐾 ∈ 𝑉 → (𝐾 ∈ Grp ↔ 𝐿 ∈ Grp))
Theorem	isgrpd2e 13224*	Deduce a group from its properties. In this version of isgrpd2 13225, we don't assume there is an expression for the inverse of 𝑥. (Contributed by NM, 10-Aug-2013.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 0 = (0g‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	isgrpd2 13225*	Deduce a group from its properties. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). Note: normally we don't use a 𝜑 antecedent on hypotheses that name structure components, since they can be eliminated with eqid 2196, but we make an exception for theorems such as isgrpd2 13225 and ismndd 13141 since theorems using them often rewrite the structure components. (Contributed by NM, 10-Aug-2013.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 0 = (0g‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁 + 𝑥) = 0 )    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	isgrpde 13226*	Deduce a group from its properties. In this version of isgrpd 13227, we don't assume there is an expression for the inverse of 𝑥. (Contributed by NM, 6-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 0 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∃𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	isgrpd 13227*	Deduce a group from its properties. Unlike isgrpd2 13225, this one goes straight from the base properties rather than going through Mnd. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). (Contributed by NM, 6-Jun-2013.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 0 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁 + 𝑥) = 0 )    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	isgrpi 13228*	Properties that determine a group. 𝑁 (negative) is normally dependent on 𝑥 i.e. read it as 𝑁(𝑥). (Contributed by NM, 3-Sep-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ 0 ∈ 𝐵    &   ⊢ (𝑥 ∈ 𝐵 → ( 0 + 𝑥) = 𝑥)    &   ⊢ (𝑥 ∈ 𝐵 → 𝑁 ∈ 𝐵)    &   ⊢ (𝑥 ∈ 𝐵 → (𝑁 + 𝑥) = 0 )    ⇒   ⊢ 𝐺 ∈ Grp
Theorem	grpsgrp 13229	A group is a semigroup. (Contributed by AV, 28-Aug-2021.)
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Smgrp)
Theorem	grpmgmd 13230	A group is a magma, deduction form. (Contributed by SN, 14-Apr-2025.)
⊢ (𝜑 → 𝐺 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Mgm)
Theorem	dfgrp2 13231*	Alternate definition of a group as semigroup with a left identity and a left inverse for each element. This "definition" is weaker than df-grp 13207, based on the definition of a monoid which provides a left and a right identity. (Contributed by AV, 28-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Smgrp ∧ ∃𝑛 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖 ∈ 𝐵 (𝑖 + 𝑥) = 𝑛)))
Theorem	dfgrp2e 13232*	Alternate definition of a group as a set with a closed, associative operation, a left identity and a left inverse for each element. Alternate definition in [Lang] p. 7. (Contributed by NM, 10-Oct-2006.) (Revised by AV, 28-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp ↔ (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) ∧ ∃𝑛 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑛 + 𝑥) = 𝑥 ∧ ∃𝑖 ∈ 𝐵 (𝑖 + 𝑥) = 𝑛)))
Theorem	grpidcl 13233	The identity element of a group belongs to the group. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 0 ∈ 𝐵)
Theorem	grpbn0 13234	The base set of a group is not empty. It is also inhabited (see grpidcl 13233). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
Theorem	grplid 13235	The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
Theorem	grprid 13236	The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)
Theorem	grplidd 13237	The identity element of a group is a left identity. Deduction associated with grplid 13235. (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ( 0 + 𝑋) = 𝑋)
Theorem	grpridd 13238	The identity element of a group is a right identity. Deduction associated with grprid 13236. (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 + 0 ) = 𝑋)
Theorem	grpn0 13239	A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ (𝐺 ∈ Grp → 𝐺 ≠ ∅)
Theorem	hashfingrpnn 13240	A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ)
Theorem	grprcan 13241	Right cancellation law for groups. (Contributed by NM, 24-Aug-2011.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑍) = (𝑌 + 𝑍) ↔ 𝑋 = 𝑌))
Theorem	grpinveu 13242*	The left inverse element of a group is unique. Lemma 2.2.1(b) of [Herstein] p. 55. (Contributed by NM, 24-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ∃!𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 0 )
Theorem	grpid 13243	Two ways of saying that an element of a group is the identity element. Provides a convenient way to compute the value of the identity element. (Contributed by NM, 24-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝑋 + 𝑋) = 𝑋 ↔ 0 = 𝑋))
Theorem	isgrpid2 13244	Properties showing that an element 𝑍 is the identity element of a group. (Contributed by NM, 7-Aug-2013.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ((𝑍 ∈ 𝐵 ∧ (𝑍 + 𝑍) = 𝑍) ↔ 0 = 𝑍))
Theorem	grpidd2 13245*	Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 13227. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 0 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    ⇒   ⊢ (𝜑 → 0 = (0g‘𝐺))
Theorem	grpinvfvalg 13246*	The inverse function of a group. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) (Revised by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝑁 = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 )))
Theorem	grpinvval 13247*	The inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (𝑁‘𝑋) = (℩𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 0 ))
Theorem	grpinvfng 13248	Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝑁 Fn 𝐵)
Theorem	grpsubfvalg 13249*	Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 19-Feb-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦))))
Theorem	grpsubval 13250	Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌)))
Theorem	grpinvf 13251	The group inversion operation is a function on the base set. (Contributed by Mario Carneiro, 4-May-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝑁:𝐵⟶𝐵)
Theorem	grpinvcl 13252	A group element's inverse is a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 4-May-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) ∈ 𝐵)
Theorem	grpinvcld 13253	A group element's inverse is a group element. (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) ∈ 𝐵)
Theorem	grplinv 13254	The left inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ((𝑁‘𝑋) + 𝑋) = 0 )
Theorem	grprinv 13255	The right inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + (𝑁‘𝑋)) = 0 )
Theorem	grpinvid1 13256	The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑁‘𝑋) = 𝑌 ↔ (𝑋 + 𝑌) = 0 ))
Theorem	grpinvid2 13257	The inverse of a group element expressed in terms of the identity element. (Contributed by NM, 24-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑁‘𝑋) = 𝑌 ↔ (𝑌 + 𝑋) = 0 ))
Theorem	isgrpinv 13258*	Properties showing that a function 𝑀 is the inverse function of a group. (Contributed by NM, 7-Aug-2013.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ((𝑀:𝐵⟶𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑀‘𝑥) + 𝑥) = 0 ) ↔ 𝑁 = 𝑀))
Theorem	grplinvd 13259	The left inverse of a group element. Deduction associated with grplinv 13254. (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘𝑋) + 𝑋) = 0 )
Theorem	grprinvd 13260	The right inverse of a group element. Deduction associated with grprinv 13255. (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 + (𝑁‘𝑋)) = 0 )
Theorem	grplrinv 13261*	In a group, every member has a left and right inverse. (Contributed by AV, 1-Sep-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ∀𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ((𝑦 + 𝑥) = 0 ∧ (𝑥 + 𝑦) = 0 ))
Theorem	grpidinv2 13262*	A group's properties using the explicit identity element. (Contributed by NM, 5-Feb-2010.) (Revised by AV, 1-Sep-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝐵) → ((( 0 + 𝐴) = 𝐴 ∧ (𝐴 + 0 ) = 𝐴) ∧ ∃𝑦 ∈ 𝐵 ((𝑦 + 𝐴) = 0 ∧ (𝐴 + 𝑦) = 0 )))
Theorem	grpidinv 13263*	A group has a left and right identity element, and every member has a left and right inverse. (Contributed by NM, 14-Oct-2006.) (Revised by AV, 1-Sep-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ∃𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 (((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥) ∧ ∃𝑦 ∈ 𝐵 ((𝑦 + 𝑥) = 𝑢 ∧ (𝑥 + 𝑦) = 𝑢)))
Theorem	grpinvid 13264	The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝑁‘ 0 ) = 0 )
Theorem	grpressid 13265	A group restricted to its base set is a group. It will usually be the original group exactly, of course, but to show that needs additional conditions such as those in strressid 12776. (Contributed by Jim Kingdon, 28-Feb-2025.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝐺 ↾s 𝐵) ∈ Grp)
Theorem	grplcan 13266	Left cancellation law for groups. (Contributed by NM, 25-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑍 + 𝑋) = (𝑍 + 𝑌) ↔ 𝑋 = 𝑌))
Theorem	grpasscan1 13267	An associative cancellation law for groups. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by AV, 30-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + ((𝑁‘𝑋) + 𝑌)) = 𝑌)
Theorem	grpasscan2 13268	An associative cancellation law for groups. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + (𝑁‘𝑌)) + 𝑌) = 𝑋)
Theorem	grpidrcan 13269	If right adding an element of a group to an arbitrary element of the group results in this element, the added element is the identity element and vice versa. (Contributed by AV, 15-Mar-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑍) = 𝑋 ↔ 𝑍 = 0 ))
Theorem	grpidlcan 13270	If left adding an element of a group to an arbitrary element of the group results in this element, the added element is the identity element and vice versa. (Contributed by AV, 15-Mar-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑍 + 𝑋) = 𝑋 ↔ 𝑍 = 0 ))
Theorem	grpinvinv 13271	Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘(𝑁‘𝑋)) = 𝑋)
Theorem	grpinvcnv 13272	The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ◡𝑁 = 𝑁)
Theorem	grpinv11 13273	The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘𝑋) = (𝑁‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	grpinvf1o 13274	The group inverse is a one-to-one onto function. (Contributed by NM, 22-Oct-2014.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝑁:𝐵–1-1-onto→𝐵)
Theorem	grpinvnz 13275	The inverse of a nonzero group element is not zero. (Contributed by Stefan O'Rear, 27-Feb-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → (𝑁‘𝑋) ≠ 0 )
Theorem	grpinvnzcl 13276	The inverse of a nonzero group element is a nonzero group element. (Contributed by Stefan O'Rear, 27-Feb-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ (𝐵 ∖ { 0 })) → (𝑁‘𝑋) ∈ (𝐵 ∖ { 0 }))
Theorem	grpsubinv 13277	Subtraction of an inverse. (Contributed by NM, 7-Apr-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 − (𝑁‘𝑌)) = (𝑋 + 𝑌))
Theorem	grplmulf1o 13278*	Left multiplication by a group element is a bijection on any group. (Contributed by Mario Carneiro, 17-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑋 + 𝑥))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	grpinvpropdg 13279*	If two structures have the same group components (properties), they have the same group inversion function. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Stefan O'Rear, 21-Mar-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → 𝐾 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦))    ⇒   ⊢ (𝜑 → (invg‘𝐾) = (invg‘𝐿))
Theorem	grpidssd 13280*	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 both groups have the same identity element. (Contributed by AV, 15-Mar-2019.)
⊢ (𝜑 → 𝑀 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ Grp)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝑀))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥(+g‘𝑀)𝑦) = (𝑥(+g‘𝑆)𝑦))    ⇒   ⊢ (𝜑 → (0g‘𝑀) = (0g‘𝑆))
Theorem	grpinvssd 13281*	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 elements of the first group have the same inverses in both groups. (Contributed by AV, 15-Mar-2019.)
⊢ (𝜑 → 𝑀 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ Grp)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝑀))    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥(+g‘𝑀)𝑦) = (𝑥(+g‘𝑆)𝑦))    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝐵 → ((invg‘𝑆)‘𝑋) = ((invg‘𝑀)‘𝑋)))
Theorem	grpinvadd 13282	The inverse of the group operation reverses the arguments. Lemma 2.2.1(d) of [Herstein] p. 55. (Contributed by NM, 27-Oct-2006.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁‘(𝑋 + 𝑌)) = ((𝑁‘𝑌) + (𝑁‘𝑋)))
Theorem	grpsubf 13283	Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → − :(𝐵 × 𝐵)⟶𝐵)
Theorem	grpsubcl 13284	Closure of group subtraction. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵)
Theorem	grpsubrcan 13285	Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑍) = (𝑌 − 𝑍) ↔ 𝑋 = 𝑌))
Theorem	grpinvsub 13286	Inverse of a group subtraction. (Contributed by NM, 9-Sep-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁‘(𝑋 − 𝑌)) = (𝑌 − 𝑋))
Theorem	grpinvval2 13287	A df-neg 8219-like equation for inverse in terms of group subtraction. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = ( 0 − 𝑋))
Theorem	grpsubid 13288	Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 − 𝑋) = 0 )
Theorem	grpsubid1 13289	Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 − 0 ) = 𝑋)
Theorem	grpsubeq0 13290	If the difference between two group elements is zero, they are equal. (subeq0 8271 analog.) (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 − 𝑌) = 0 ↔ 𝑋 = 𝑌))
Theorem	grpsubadd0sub 13291	Subtraction expressed as addition of the difference of the identity element and the subtrahend. (Contributed by AV, 9-Nov-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + ( 0 − 𝑌)))
Theorem	grpsubadd 13292	Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) = 𝑍 ↔ (𝑍 + 𝑌) = 𝑋))
Theorem	grpsubsub 13293	Double group subtraction. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 − (𝑌 − 𝑍)) = (𝑋 + (𝑍 − 𝑌)))
Theorem	grpaddsubass 13294	Associative-type law for group subtraction and addition. (Contributed by NM, 16-Apr-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) − 𝑍) = (𝑋 + (𝑌 − 𝑍)))
Theorem	grppncan 13295	Cancellation law for subtraction (pncan 8251 analog). (Contributed by NM, 16-Apr-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + 𝑌) − 𝑌) = 𝑋)
Theorem	grpnpcan 13296	Cancellation law for subtraction (npcan 8254 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 − 𝑌) + 𝑌) = 𝑋)
Theorem	grpsubsub4 13297	Double group subtraction (subsub4 8278 analog). (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑍 + 𝑌)))
Theorem	grppnpcan2 13298	Cancellation law for mixed addition and subtraction. (pnpcan2 8285 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑍) − (𝑌 + 𝑍)) = (𝑋 − 𝑌))
Theorem	grpnpncan 13299	Cancellation law for group subtraction. (npncan 8266 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) + (𝑌 − 𝑍)) = (𝑋 − 𝑍))
Theorem	grpnpncan0 13300	Cancellation law for group subtraction (npncan2 8272 analog). (Contributed by AV, 24-Nov-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑋 − 𝑌) + (𝑌 − 𝑋)) = 0 )