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	grplinv 19201	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 19202	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 19203	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 19204	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 19205*	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 19206	The left inverse of a group element. Deduction associated with grplinv 19201. (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘𝑋) + 𝑋) = 0 )
Theorem	grprinvd 19207	The right inverse of a group element. Deduction associated with grprinv 19202. (Contributed by SN, 29-Jan-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 + (𝑁‘𝑋)) = 0 )
Theorem	grplrinv 19208*	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 19209*	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 19210*	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 19211	The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011.)
⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝑁‘ 0 ) = 0 )
Theorem	grplcan 19212	Left cancellation law for groups. (Contributed by NM, 25-Aug-2011.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑍 + 𝑋) = (𝑍 + 𝑌) ↔ 𝑋 = 𝑌))
Theorem	grpasscan1 19213	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 19214	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 19215	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 19216	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 19217	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 19218	The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → ◡𝑁 = 𝑁)
Theorem	grpinv11 19219	The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015.) (Proof shortened by SN, 8-Jul-2025.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → ((𝑁‘𝑋) = (𝑁‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	grpinvf1o 19220	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 19221	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 19222	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 19223	Subtraction of an inverse. (Contributed by NM, 7-Apr-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑋 − (𝑁‘𝑌)) = (𝑋 + 𝑌))
Theorem	grplmulf1o 19224*	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	grpraddf1o 19225*	Right addition by a group element is a bijection on any group. (Contributed by SN, 28-Apr-2012.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝑥 + 𝑋))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → 𝐹:𝐵–1-1-onto→𝐵)
Theorem	grpinvpropd 19226*	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 19227*	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 19228*	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 19229	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 19230	Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → − :(𝐵 × 𝐵)⟶𝐵)
Theorem	grpsubcl 19231	Closure of group subtraction. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) ∈ 𝐵)
Theorem	grpsubrcan 19232	Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑍) = (𝑌 − 𝑍) ↔ 𝑋 = 𝑌))
Theorem	grpinvsub 19233	Inverse of a group subtraction. (Contributed by NM, 9-Sep-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 𝑁 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑁‘(𝑋 − 𝑌)) = (𝑌 − 𝑋))
Theorem	grpinvval2 19234	A df-neg 11545-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 19235	Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 − 𝑋) = 0 )
Theorem	grpsubid1 19236	Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵) → (𝑋 − 0 ) = 𝑋)
Theorem	grpsubeq0 19237	If the difference between two group elements is zero, they are equal. (subeq0 11585 analog.) (Contributed by Jeff Madsen, 6-Jan-2011.) (Revised by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 − 𝑌) = 0 ↔ 𝑋 = 𝑌))
Theorem	grpsubadd0sub 19238	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 19239	Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) = 𝑍 ↔ (𝑍 + 𝑌) = 𝑋))
Theorem	grpsubsub 19240	Double group subtraction. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 − (𝑌 − 𝑍)) = (𝑋 + (𝑍 − 𝑌)))
Theorem	grpaddsubass 19241	Associative-type law for group subtraction and addition. (Contributed by NM, 16-Apr-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) − 𝑍) = (𝑋 + (𝑌 − 𝑍)))
Theorem	grppncan 19242	Cancellation law for subtraction (pncan 11564 analog). (Contributed by NM, 16-Apr-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 + 𝑌) − 𝑌) = 𝑋)
Theorem	grpnpcan 19243	Cancellation law for subtraction (npcan 11567 analog). (Contributed by NM, 19-Apr-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 − 𝑌) + 𝑌) = 𝑋)
Theorem	grpsubsub4 19244	Double group subtraction (subsub4 11592 analog). (Contributed by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) − 𝑍) = (𝑋 − (𝑍 + 𝑌)))
Theorem	grppnpcan2 19245	Cancellation law for mixed addition and subtraction. (pnpcan2 11599 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑍) − (𝑌 + 𝑍)) = (𝑋 − 𝑌))
Theorem	grpnpncan 19246	Cancellation law for group subtraction. (npncan 11580 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑌) + (𝑌 − 𝑍)) = (𝑋 − 𝑍))
Theorem	grpnpncan0 19247	Cancellation law for group subtraction (npncan2 11586 analog). (Contributed by AV, 24-Nov-2019.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ − = (-g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝑋 − 𝑌) + (𝑌 − 𝑋)) = 0 )
Theorem	grpnnncan2 19248	Cancellation law for group subtraction. (nnncan2 11596 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 − 𝑍) − (𝑌 − 𝑍)) = (𝑋 − 𝑌))
Theorem	dfgrp3lem 19249*	Lemma for dfgrp3 19250. (Contributed by AV, 28-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)) → ∃𝑢 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑢 + 𝑎) = 𝑎 ∧ ∃𝑖 ∈ 𝐵 (𝑖 + 𝑎) = 𝑢))
Theorem	dfgrp3 19250*	Alternate definition of a group as semigroup (with at least one element) which is also a quasigroup, i.e. a magma in which solutions 𝑥 and 𝑦 of the equations (𝑎 + 𝑥) = 𝑏 and (𝑥 + 𝑎) = 𝑏 exist. Theorem 3.2 of [Bruck] p. 28. (Contributed by AV, 28-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp ↔ (𝐺 ∈ Smgrp ∧ 𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦)))
Theorem	dfgrp3e 19251*	Alternate definition of a group as a set with a closed, associative operation, for which solutions 𝑥 and 𝑦 of the equations (𝑎 + 𝑥) = 𝑏 and (𝑥 + 𝑎) = 𝑏 exist. Exercise 1 of [Herstein] p. 57. (Contributed by NM, 5-Dec-2006.) (Revised by AV, 28-Aug-2021.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp ↔ (𝐵 ≠ ∅ ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙 ∈ 𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟 ∈ 𝐵 (𝑥 + 𝑟) = 𝑦))))
Theorem	grplactfval 19252*	The left group action of element 𝐴 of group 𝐺. (Contributed by Paul Chapman, 18-Mar-2008.)
⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)))    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑋 → (𝐹‘𝐴) = (𝑎 ∈ 𝑋 ↦ (𝐴 + 𝑎)))
Theorem	grplactval 19253*	The value of the left group action of element 𝐴 of group 𝐺 at 𝐵. (Contributed by Paul Chapman, 18-Mar-2008.)
⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)))    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝐹‘𝐴)‘𝐵) = (𝐴 + 𝐵))
Theorem	grplactcnv 19254*	The left group action of element 𝐴 of group 𝐺 maps the underlying set 𝑋 of 𝐺 one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ((𝐹‘𝐴):𝑋–1-1-onto→𝑋 ∧ ◡(𝐹‘𝐴) = (𝐹‘(𝐼‘𝐴))))
Theorem	grplactf1o 19255*	The left group action of element 𝐴 of group 𝐺 maps the underlying set 𝑋 of 𝐺 one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008.) (Proof shortened by Mario Carneiro, 14-Aug-2015.)
⊢ 𝐹 = (𝑔 ∈ 𝑋 ↦ (𝑎 ∈ 𝑋 ↦ (𝑔 + 𝑎)))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝐹‘𝐴):𝑋–1-1-onto→𝑋)
Theorem	grpsubpropd 19256	Weak property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 27-Mar-2015.)
⊢ (𝜑 → (Base‘𝐺) = (Base‘𝐻))    &   ⊢ (𝜑 → (+g‘𝐺) = (+g‘𝐻))    ⇒   ⊢ (𝜑 → (-g‘𝐺) = (-g‘𝐻))
Theorem	grpsubpropd2 19257*	Strong property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 4-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐺))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐻))    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐺)𝑦) = (𝑥(+g‘𝐻)𝑦))    ⇒   ⊢ (𝜑 → (-g‘𝐺) = (-g‘𝐻))
Theorem	grp1 19258	The (smallest) structure representing a trivial group. According to Wikipedia ("Trivial group", 28-Apr-2019, https://en.wikipedia.org/wiki/Trivial_group) "In mathematics, a trivial group is a group consisting of a single element. All such groups are isomorphic, so one often speaks of the trivial group. The single element of the trivial group is the identity element". (Contributed by NM, 4-Nov-2006.) (Revised by AV, 28-Apr-2019.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩}    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Grp)
Theorem	grp1inv 19259	The inverse function of the trivial group. (Contributed by FL, 21-Jun-2010.) (Revised by AV, 26-Aug-2021.)
⊢ 𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩}    ⇒   ⊢ (𝐼 ∈ 𝑉 → (invg‘𝑀) = ( I ↾ {𝐼}))
Theorem	prdsinvlem 19260*	Characterization of inverses in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ + = (+g‘𝑌)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Grp)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ 0 = (0g ∘ 𝑅)    &   ⊢ 𝑁 = (𝑦 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑦))‘(𝐹‘𝑦)))    ⇒   ⊢ (𝜑 → (𝑁 ∈ 𝐵 ∧ (𝑁 + 𝐹) = 0 ))
Theorem	prdsgrpd 19261	The product of a family of groups is a group. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Grp)    ⇒   ⊢ (𝜑 → 𝑌 ∈ Grp)
Theorem	prdsinvgd 19262*	Negation in a product of groups. (Contributed by Stefan O'Rear, 10-Jan-2015.)
⊢ 𝑌 = (𝑆Xs𝑅)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑊)    &   ⊢ (𝜑 → 𝑆 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑅:𝐼⟶Grp)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑁 = (invg‘𝑌)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑁‘𝑋) = (𝑥 ∈ 𝐼 ↦ ((invg‘(𝑅‘𝑥))‘(𝑋‘𝑥))))
Theorem	pwsgrp 19263	A structure power of a group is a group. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    ⇒   ⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Grp)
Theorem	pwsinvg 19264	Negation in a structure power. (Contributed by Mario Carneiro, 11-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑀 = (invg‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑌)    ⇒   ⊢ ((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = (𝑀 ∘ 𝑋))
Theorem	pwssub 19265	Subtraction in a structure power. (Contributed by Mario Carneiro, 12-Jan-2015.)
⊢ 𝑌 = (𝑅 ↑s 𝐼)    &   ⊢ 𝐵 = (Base‘𝑌)    &   ⊢ 𝑀 = (-g‘𝑅)    &   ⊢ − = (-g‘𝑌)    ⇒   ⊢ (((𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑉) ∧ (𝐹 ∈ 𝐵 ∧ 𝐺 ∈ 𝐵)) → (𝐹 − 𝐺) = (𝐹 ∘f 𝑀𝐺))
Theorem	imasgrp2 19266*	The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ (𝜑 → 𝑅 ∈ 𝑊)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → (𝐹‘((𝑥 + 𝑦) + 𝑧)) = (𝐹‘(𝑥 + (𝑦 + 𝑧))))    &   ⊢ (𝜑 → 0 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘( 0 + 𝑥)) = (𝐹‘𝑥))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝐹‘(𝑁 + 𝑥)) = (𝐹‘ 0 ))    ⇒   ⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) = (0g‘𝑈)))
Theorem	imasgrp 19267*	The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.)
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → 𝐹:𝑉–onto→𝐵)    &   ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉) ∧ (𝑝 ∈ 𝑉 ∧ 𝑞 ∈ 𝑉)) → (((𝐹‘𝑎) = (𝐹‘𝑝) ∧ (𝐹‘𝑏) = (𝐹‘𝑞)) → (𝐹‘(𝑎 + 𝑏)) = (𝐹‘(𝑝 + 𝑞))))    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ 0 = (0g‘𝑅)    ⇒   ⊢ (𝜑 → (𝑈 ∈ Grp ∧ (𝐹‘ 0 ) = (0g‘𝑈)))
Theorem	imasgrpf1 19268	The image of a group under an injection is a group. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑈 = (𝐹 “s 𝑅)    &   ⊢ 𝑉 = (Base‘𝑅)    ⇒   ⊢ ((𝐹:𝑉–1-1→𝐵 ∧ 𝑅 ∈ Grp) → 𝑈 ∈ Grp)
Theorem	qusgrp2 19269*	Prove that a quotient structure is a group. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 12-Aug-2015.)
⊢ (𝜑 → 𝑈 = (𝑅 /s ∼ ))    &   ⊢ (𝜑 → 𝑉 = (Base‘𝑅))    &   ⊢ (𝜑 → + = (+g‘𝑅))    &   ⊢ (𝜑 → ∼ Er 𝑉)    &   ⊢ (𝜑 → 𝑅 ∈ 𝑋)    &   ⊢ (𝜑 → ((𝑎 ∼ 𝑝 ∧ 𝑏 ∼ 𝑞) → (𝑎 + 𝑏) ∼ (𝑝 + 𝑞)))    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉) → (𝑥 + 𝑦) ∈ 𝑉)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉 ∧ 𝑧 ∈ 𝑉)) → ((𝑥 + 𝑦) + 𝑧) ∼ (𝑥 + (𝑦 + 𝑧)))    &   ⊢ (𝜑 → 0 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → ( 0 + 𝑥) ∼ 𝑥)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 𝑁 ∈ 𝑉)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → (𝑁 + 𝑥) ∼ 0 )    ⇒   ⊢ (𝜑 → (𝑈 ∈ Grp ∧ [ 0 ] ∼ = (0g‘𝑈)))
Theorem	xpsgrp 19270	The binary product of groups is a group. (Contributed by Mario Carneiro, 20-Aug-2015.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    ⇒   ⊢ ((𝑅 ∈ Grp ∧ 𝑆 ∈ Grp) → 𝑇 ∈ Grp)
Theorem	xpsinv 19271	Value of the negation operation in a binary structure product. (Contributed by AV, 18-Mar-2025.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ 𝑀 = (invg‘𝑅)    &   ⊢ 𝑁 = (invg‘𝑆)    &   ⊢ 𝐼 = (invg‘𝑇)    ⇒   ⊢ (𝜑 → (𝐼‘⟨𝐴, 𝐵⟩) = ⟨(𝑀‘𝐴), (𝑁‘𝐵)⟩)
Theorem	xpsgrpsub 19272	Value of the subtraction operation in a binary structure product of groups. (Contributed by AV, 24-Mar-2025.)
⊢ 𝑇 = (𝑅 ×s 𝑆)    &   ⊢ 𝑋 = (Base‘𝑅)    &   ⊢ 𝑌 = (Base‘𝑆)    &   ⊢ (𝜑 → 𝑅 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑌)    &   ⊢ · = (-g‘𝑅)    &   ⊢ × = (-g‘𝑆)    &   ⊢ − = (-g‘𝑇)    ⇒   ⊢ (𝜑 → (⟨𝐴, 𝐵⟩ − ⟨𝐶, 𝐷⟩) = ⟨(𝐴 · 𝐶), (𝐵 × 𝐷)⟩)
Theorem	mhmlem 19273*	Lemma for mhmmnd 19275 and ghmgrp 19277. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 25-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐴 + 𝐵)) = ((𝐹‘𝐴) ⨣ (𝐹‘𝐵)))
Theorem	mhmid 19274*	A surjective monoid morphism preserves identity element. (Contributed by Thierry Arnoux, 25-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑌 = (Base‘𝐻)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+g‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝜑 → (𝐹‘ 0 ) = (0g‘𝐻))
Theorem	mhmmnd 19275*	The image of a monoid 𝐺 under a monoid homomorphism 𝐹 is a monoid. (Contributed by Thierry Arnoux, 25-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑌 = (Base‘𝐻)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+g‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    ⇒   ⊢ (𝜑 → 𝐻 ∈ Mnd)
Theorem	mhmfmhm 19276*	The function fulfilling the conditions of mhmmnd 19275 is a monoid homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑌 = (Base‘𝐻)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+g‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    ⇒   ⊢ (𝜑 → 𝐹 ∈ (𝐺 MndHom 𝐻))
Theorem	ghmgrp 19277*	The image of a group 𝐺 under a group homomorphism 𝐹 is a group. This is a stronger result than that usually found in the literature, since the target of the homomorphism (operator 𝑂 in our model) need not have any of the properties of a group as a prerequisite. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 25-Jan-2020.)
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)))    &   ⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑌 = (Base‘𝐻)    &   ⊢ + = (+g‘𝐺)    &   ⊢ ⨣ = (+g‘𝐻)    &   ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    ⇒   ⊢ (𝜑 → 𝐻 ∈ Grp)
10.2.2  Group multiple operation The "group multiple" operation (if the group is multiplicative, also called "group power" or "group exponentiation" operation), can be defined for arbitrary magmas, if the multiplier/exponent is a nonnegative integer. See also the definition in [Lang] p. 6, where an element 𝑥(of a monoid) to the power of a nonnegative integer 𝑛 is defined and denoted by 𝑥↑𝑛. Definition df-mulg 19279, however, defines the group multiple for arbitrary (i.e. also negative) integers. This is meaningful for groups only, and requires Definition df-minusg 19149 of the inverse operation invg.
Syntax	cmg 19278	Extend class notation with a function mapping a group operation to the multiple/power operation for the magma/group.
class .g
Definition	df-mulg 19279*	Define the group multiple function, also known as group exponentiation when viewed multiplicatively. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ .g = (𝑔 ∈ V ↦ (𝑛 ∈ ℤ, 𝑥 ∈ (Base‘𝑔) ↦ if(𝑛 = 0, (0g‘𝑔), ⦋seq1((+g‘𝑔), (ℕ × {𝑥})) / 𝑠⦌if(0 < 𝑛, (𝑠‘𝑛), ((invg‘𝑔)‘(𝑠‘ -𝑛))))))
Theorem	mulgfval 19280*	Group multiple (exponentiation) operation. For a shorter proof using ax-rep 5231, see mulgfvalALT 19281. (Contributed by Mario Carneiro, 11-Dec-2014.) Remove dependency on ax-rep 5231. (Revised by Rohan Ridenour, 17-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ · = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘ -𝑛)))))
Theorem	mulgfvalALT 19281*	Shorter proof of mulgfval 19280 using ax-rep 5231. (Contributed by Mario Carneiro, 11-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ · = (𝑛 ∈ ℤ, 𝑥 ∈ 𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘ -𝑛)))))
Theorem	mulgval 19282	Value of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝑆 = seq1( + , (ℕ × {𝑋}))    ⇒   ⊢ ((𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = if(𝑁 = 0, 0 , if(0 < 𝑁, (𝑆‘𝑁), (𝐼‘(𝑆‘ -𝑁)))))
Theorem	mulgfn 19283	Functionality of the group multiple operation. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ · Fn (ℤ × 𝐵)
Theorem	mulgfvi 19284	The group multiple operation is compatible with identity-function protection. (Contributed by Mario Carneiro, 21-Mar-2015.)
⊢ · = (.g‘𝐺)    ⇒   ⊢ · = (.g‘( I ‘𝐺))
Theorem	mulg0 19285	Group multiple (exponentiation) operation at zero. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (0 · 𝑋) = 0 )
Theorem	mulgnn 19286	Group multiple (exponentiation) operation at a positive integer. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝑆 = seq1( + , (ℕ × {𝑋}))    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = (𝑆‘𝑁))
Theorem	ressmulgnn 19287	Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 12-Jun-2017.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐴 ⊆ (Base‘𝐺)    &   ⊢ ∗ = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐴) → (𝑁(.g‘𝐻)𝑋) = (𝑁 ∗ 𝑋))
Theorem	ressmulgnn0 19288	Values for the group multiple function in a restricted structure. (Contributed by Thierry Arnoux, 14-Jun-2017.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ 𝐴 ⊆ (Base‘𝐺)    &   ⊢ ∗ = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ (0g‘𝐺) = (0g‘𝐻)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐴) → (𝑁(.g‘𝐻)𝑋) = (𝑁 ∗ 𝑋))
Theorem	ressmulgnnd 19289	Values for the group multiple function in a restricted structure, a deduction version. (Contributed by metakunt, 14-May-2025.)
⊢ 𝐻 = (𝐺 ↾s 𝐴)    &   ⊢ (𝜑 → 𝐴 ⊆ (Base‘𝐺))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ (𝜑 → (𝑁(.g‘𝐻)𝑋) = (𝑁(.g‘𝐺)𝑋))
Theorem	mulgnngsum 19290*	Group multiple (exponentiation) operation at a positive integer expressed by a group sum. (Contributed by AV, 28-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ (1...𝑁) ↦ 𝑋)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = (𝐺 Σg 𝐹))
Theorem	mulgnn0gsum 19291*	Group multiple (exponentiation) operation at a nonnegative integer expressed by a group sum. This corresponds to the definition in [Lang] p. 6, second formula. (Contributed by AV, 28-Dec-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ (1...𝑁) ↦ 𝑋)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = (𝐺 Σg 𝐹))
Theorem	mulg1 19292	Group multiple (exponentiation) operation at one. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (1 · 𝑋) = 𝑋)
Theorem	mulgnnp1 19293	Group multiple (exponentiation) operation at a successor. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → ((𝑁 + 1) · 𝑋) = ((𝑁 · 𝑋) + 𝑋))
Theorem	mulg2 19294	Group multiple (exponentiation) operation at two. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (2 · 𝑋) = (𝑋 + 𝑋))
Theorem	mulgnegnn 19295	Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 11-Dec-2014.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → ( -𝑁 · 𝑋) = (𝐼‘(𝑁 · 𝑋)))
Theorem	mulgnn0p1 19296	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 19297*	Closure of the group multiple (exponentiation) operation in a submagma. (Contributed by Mario Carneiro, 10-Jan-2015.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ + = (+g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑆 ⊆ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    ⇒   ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝑆) → (𝑁 · 𝑋) ∈ 𝑆)
Theorem	mulgnn0subcl 19298*	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 19299*	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 19300	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 ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵)