P. 183 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 18201-18300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	sgrp2rid2ex 18201*	A small semigroup (with two elements) with two right identities which are different. (Contributed by AV, 10-Feb-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    &   ⊢ ⚬ = (+g‘𝑀)    ⇒   ⊢ ((♯‘𝑆) = 2 → ∃𝑥 ∈ 𝑆 ∃𝑧 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 ≠ 𝑧 ∧ (𝑦 ⚬ 𝑥) = 𝑦 ∧ (𝑦 ⚬ 𝑧) = 𝑦))
Theorem	sgrp2nmndlem4 18202*	Lemma 4 for sgrp2nmnd 18204: M is a semigroup. (Contributed by AV, 29-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    ⇒   ⊢ ((♯‘𝑆) = 2 → 𝑀 ∈ Smgrp)
Theorem	sgrp2nmndlem5 18203*	Lemma 5 for sgrp2nmnd 18204: M is not a monoid. (Contributed by AV, 29-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    ⇒   ⊢ ((♯‘𝑆) = 2 → 𝑀 ∉ Mnd)
Theorem	sgrp2nmnd 18204*	A small semigroup (with two elements) which is not a monoid. (Contributed by AV, 26-Jan-2020.)
⊢ 𝑆 = {𝐴, 𝐵}    &   ⊢ (Base‘𝑀) = 𝑆    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵))    ⇒   ⊢ ((♯‘𝑆) = 2 → (𝑀 ∈ Smgrp ∧ 𝑀 ∉ Mnd))
Theorem	mgmnsgrpex 18205	There is a magma which is not a semigroup. (Contributed by AV, 29-Jan-2020.)
⊢ ∃𝑚 ∈ Mgm 𝑚 ∉ Smgrp
Theorem	sgrpnmndex 18206	There is a semigroup which is not a monoid. (Contributed by AV, 29-Jan-2020.)
⊢ ∃𝑚 ∈ Smgrp 𝑚 ∉ Mnd
Theorem	sgrpssmgm 18207	The class of all semigroups is a proper subclass of the class of all magmas. (Contributed by AV, 29-Jan-2020.)
⊢ Smgrp ⊊ Mgm
Theorem	mndsssgrp 18208	The class of all monoids is a proper subclass of the class of all semigroups. (Contributed by AV, 29-Jan-2020.)
⊢ Mnd ⊊ Smgrp
Theorem	pwmndgplus 18209*	The operation of the monoid of the power set of a class 𝐴 under union. (Contributed by AV, 27-Feb-2024.)
⊢ (Base‘𝑀) = 𝒫 𝐴    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝒫 𝐴, 𝑦 ∈ 𝒫 𝐴 ↦ (𝑥 ∪ 𝑦))    ⇒   ⊢ ((𝑋 ∈ 𝒫 𝐴 ∧ 𝑌 ∈ 𝒫 𝐴) → (𝑋(+g‘𝑀)𝑌) = (𝑋 ∪ 𝑌))
Theorem	pwmndid 18210*	The identity of the monoid of the power set of a class 𝐴 under union is the empty set. (Contributed by AV, 27-Feb-2024.)
⊢ (Base‘𝑀) = 𝒫 𝐴    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝒫 𝐴, 𝑦 ∈ 𝒫 𝐴 ↦ (𝑥 ∪ 𝑦))    ⇒   ⊢ (0g‘𝑀) = ∅
Theorem	pwmnd 18211*	The power set of a class 𝐴 is a monoid under union. (Contributed by AV, 27-Feb-2024.)
⊢ (Base‘𝑀) = 𝒫 𝐴    &   ⊢ (+g‘𝑀) = (𝑥 ∈ 𝒫 𝐴, 𝑦 ∈ 𝒫 𝐴 ↦ (𝑥 ∪ 𝑦))    ⇒   ⊢ 𝑀 ∈ Mnd
10.2  Groups
10.2.1  Definition and basic properties
Syntax	cgrp 18212	Extend class notation with class of all groups.
class Grp
Syntax	cminusg 18213	Extend class notation with inverse of group element.
class invg
Syntax	csg 18214	Extend class notation with group subtraction (or division) operation.
class -g
Definition	df-grp 18215*	Define class of all groups. A group is a monoid (df-mnd 18021) 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 16585) and an internal group operation (notated (+g‘𝐺) per df-plusg 16674). 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 18220), associativity (so ((𝑎+g𝑏)+g𝑐) = (𝑎+g(𝑏+g𝑐)) for any a, b, c, see grpass 18221), 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 18223). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 19020). Subgroups can often be formed from groups, see df-subg 18387. An example of an (Abelian) group is the set of complex numbers ℂ over the group operation + (addition), as proven in cnaddablx 19100; an Abelian group is a group as proven in ablgrp 19022. Other structures include groups, including unital rings (df-ring 19411) and fields (df-field 19617). (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.)
⊢ Grp = {𝑔 ∈ Mnd ∣ ∀𝑎 ∈ (Base‘𝑔)∃𝑚 ∈ (Base‘𝑔)(𝑚(+g‘𝑔)𝑎) = (0g‘𝑔)}
Definition	df-minusg 18216*	Define inverse of group element. (Contributed by NM, 24-Aug-2011.)
⊢ invg = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ (℩𝑤 ∈ (Base‘𝑔)(𝑤(+g‘𝑔)𝑥) = (0g‘𝑔))))
Definition	df-sbg 18217*	Define group subtraction (also called division for multiplicative groups). (Contributed by NM, 31-Mar-2014.)
⊢ -g = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔), 𝑦 ∈ (Base‘𝑔) ↦ (𝑥(+g‘𝑔)((invg‘𝑔)‘𝑦))))
Theorem	isgrp 18218*	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 18219	A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.)
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
Theorem	grpcl 18220	Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	grpass 18221	A group operation is associative. (Contributed by NM, 14-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	grpinvex 18222*	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 18223*	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	grpmndd 18224	A group is a monoid. (Contributed by SN, 1-Jun-2024.)
⊢ (𝜑 → 𝐺 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝐺 ∈ Mnd)
Theorem	grpcld 18225	Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵)
Theorem	grpplusf 18226	The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐹 = (+𝑓‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐹:(𝐵 × 𝐵)⟶𝐵)
Theorem	grpplusfo 18227	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	resgrpplusfrn 18228	The underlying set of a group operation which is a restriction of a structure. (Contributed by Paul Chapman, 25-Mar-2008.) (Revised by AV, 30-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐻 = (𝐺 ↾s 𝑆)    &   ⊢ 𝐹 = (+𝑓‘𝐻)    ⇒   ⊢ ((𝐻 ∈ Grp ∧ 𝑆 ⊆ 𝐵) → 𝑆 = ran 𝐹)
Theorem	grppropd 18229*	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 18230	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	grppropstr 18231	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	grpss 18232	Show that a structure extending a constructed group (e.g., a ring) is also a group. This allows us to prove that a constructed potential ring 𝑅 is a group before we know that it is also a ring. (Theorem ringgrp 19414, on the other hand, requires that we know in advance that 𝑅 is a ring.) (Contributed by NM, 11-Oct-2013.)
⊢ 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}    &   ⊢ 𝑅 ∈ V    &   ⊢ 𝐺 ⊆ 𝑅    &   ⊢ Fun 𝑅    ⇒   ⊢ (𝐺 ∈ Grp ↔ 𝑅 ∈ Grp)
Theorem	isgrpd2e 18233*	Deduce a group from its properties. In this version of isgrpd2 18234, 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 18234*	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 2738, but we make an exception for theorems such as isgrpd2 18234, ismndd 18042, and islmodd 19752 since theorems using them often rewrite the structure components. (Contributed by NM, 10-Aug-2013.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 0 = (0g‘𝐺))    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑁 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁 + 𝑥) = 0 )    ⇒   ⊢ (𝜑 → 𝐺 ∈ Grp)
Theorem	isgrpde 18235*	Deduce a group from its properties. In this version of isgrpd 18236, 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 18236*	Deduce a group from its properties. Unlike isgrpd2 18234, 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 18237*	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 18238	A group is a semigroup. (Contributed by AV, 28-Aug-2021.)
⊢ (𝐺 ∈ Grp → 𝐺 ∈ Smgrp)
Theorem	dfgrp2 18239*	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 18215, 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 18240*	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	isgrpix 18241*	Properties that determine a group. Read 𝑁 as 𝑁(𝑥). Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.)
⊢ 𝐵 ∈ V    &   ⊢ + ∈ V    &   ⊢ 𝐺 = {⟨1, 𝐵⟩, ⟨2, + ⟩}    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)    &   ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))    &   ⊢ 0 ∈ 𝐵    &   ⊢ (𝑥 ∈ 𝐵 → ( 0 + 𝑥) = 𝑥)    &   ⊢ (𝑥 ∈ 𝐵 → 𝑁 ∈ 𝐵)    &   ⊢ (𝑥 ∈ 𝐵 → (𝑁 + 𝑥) = 0 )    ⇒   ⊢ 𝐺 ∈ Grp
Theorem	grpidcl 18242	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 18243	The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝐵 ≠ ∅)
Theorem	grplid 18244	The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋)
Theorem	grprid 18245	The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋)
Theorem	grpn0 18246	A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ (𝐺 ∈ Grp → 𝐺 ≠ ∅)
Theorem	hashfingrpnn 18247	A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐵 ∈ Fin)    ⇒   ⊢ (𝜑 → (♯‘𝐵) ∈ ℕ)
Theorem	grprcan 18248	Right cancellation law for groups. (Contributed by NM, 24-Aug-2011.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑍) = (𝑌 + 𝑍) ↔ 𝑋 = 𝑌))
Theorem	grpinveu 18249*	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 18250	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 18251	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 18252*	Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 18236. (Contributed by Mario Carneiro, 14-Jun-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → + = (+g‘𝐺))    &   ⊢ (𝜑 → 0 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    ⇒   ⊢ (𝜑 → 0 = (0g‘𝐺))
Theorem	grpinvfval 18253*	The inverse function of a group. For a shorter proof using ax-rep 5151, see grpinvfvalALT 18254. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) Remove dependency on ax-rep 5151. (Revised by Rohan Ridenour, 13-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ 𝑁 = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ))
Theorem	grpinvfvalALT 18254*	Shorter proof of grpinvfval 18253 using ax-rep 5151. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ 𝑁 = (𝑥 ∈ 𝐵 ↦ (℩𝑦 ∈ 𝐵 (𝑦 + 𝑥) = 0 ))
Theorem	grpinvval 18255*	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	grpinvfn 18256	Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ 𝑁 Fn 𝐵
Theorem	grpinvfvi 18257	The group inverse function is compatible with identity-function protection. (Contributed by Stefan O'Rear, 21-Mar-2015.)
⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ 𝑁 = (invg‘( I ‘𝐺))
Theorem	grpsubfval 18258*	Group subtraction (division) operation. For a shorter proof using ax-rep 5151, see grpsubfvalALT 18259. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) Remove dependency on ax-rep 5151. (Revised by Rohan Ridenour, 17-Aug-2023.) (Proof shortened by AV, 19-Feb-2024.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦)))
Theorem	grpsubfvalALT 18259*	Shorter proof of grpsubfval 18258 using ax-rep 5151. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 19-Feb-2024.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ − = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ (𝑥 + (𝐼‘𝑦)))
Theorem	grpsubval 18260	Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 + (𝐼‘𝑌)))
Theorem	grpinvf 18261	The group inversion operation is a function on the base set. (Contributed by Mario Carneiro, 4-May-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → 𝑁:𝐵⟶𝐵)
Theorem	grpinvcl 18262	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	grplinv 18263	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 18264	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 18265	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 18266	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 18267*	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	grplrinv 18268*	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 18269*	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 18270*	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 18271	The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝑁‘ 0 ) = 0 )
Theorem	grplcan 18272	Left cancellation law for groups. (Contributed by NM, 25-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑍 + 𝑋) = (𝑍 + 𝑌) ↔ 𝑋 = 𝑌))
Theorem	grpasscan1 18273	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 18274	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 18275	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 18276	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 18277	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 18278	The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ◡𝑁 = 𝑁)
Theorem	grpinv11 18279	The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘𝑋) = (𝑁‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	grpinvf1o 18280	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 18281	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 18282	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 18283	Subtraction of an inverse. (Contributed by NM, 7-Apr-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 − (𝑁‘𝑌)) = (𝑋 + 𝑌))
Theorem	grplmulf1o 18284*	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	grpinvpropd 18285*	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 18286*	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 18287*	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 18288	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 18289	Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → − :(𝐵 × 𝐵)⟶𝐵)
Theorem	grpsubcl 18290	Closure of group subtraction. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵)
Theorem	grpsubrcan 18291	Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑍) = (𝑌 − 𝑍) ↔ 𝑋 = 𝑌))
Theorem	grpinvsub 18292	Inverse of a group subtraction. (Contributed by NM, 9-Sep-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁‘(𝑋 − 𝑌)) = (𝑌 − 𝑋))
Theorem	grpinvval2 18293	A df-neg 10944-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 18294	Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 − 𝑋) = 0 )
Theorem	grpsubid1 18295	Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 − 0 ) = 𝑋)
Theorem	grpsubeq0 18296	If the difference between two group elements is zero, they are equal. (subeq0 10983 analog.) (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 − 𝑌) = 0 ↔ 𝑋 = 𝑌))
Theorem	grpsubadd0sub 18297	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 18298	Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) = 𝑍 ↔ (𝑍 + 𝑌) = 𝑋))
Theorem	grpsubsub 18299	Double group subtraction. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 − (𝑌 − 𝑍)) = (𝑋 + (𝑍 − 𝑌)))
Theorem	grpaddsubass 18300	Associative-type law for group subtraction and addition. (Contributed by NM, 16-Apr-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) − 𝑍) = (𝑋 + (𝑌 − 𝑍)))