HomeHome Intuitionistic Logic Explorer
Theorem List (p. 129 of 145)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 12801-12900   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremgrpinveu 12801* 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 )
 
Theoremgrpid 12802 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 = 𝑋))
 
Theoremisgrpid2 12803 Properties showing that an element 𝑍 is the identity element of a group. (Contributed by NM, 7-Aug-2013.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    0 = (0g𝐺)       (𝐺 ∈ Grp → ((𝑍𝐵 ∧ (𝑍 + 𝑍) = 𝑍) ↔ 0 = 𝑍))
 
Theoremgrpidd2 12804* Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 12789. (Contributed by Mario Carneiro, 14-Jun-2015.)
(𝜑𝐵 = (Base‘𝐺))    &   (𝜑+ = (+g𝐺))    &   (𝜑0𝐵)    &   ((𝜑𝑥𝐵) → ( 0 + 𝑥) = 𝑥)    &   (𝜑𝐺 ∈ Grp)       (𝜑0 = (0g𝐺))
 
Theoremgrpinvfvalg 12805* 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 )))
 
Theoremgrpinvval 12806* 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 ))
 
Theoremgrpinvfng 12807 Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015.)
𝐵 = (Base‘𝐺)    &   𝑁 = (invg𝐺)       (𝐺𝑉𝑁 Fn 𝐵)
 
Theoremgrpsubfvalg 12808* 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𝐺)       (𝐺𝑉 = (𝑥𝐵, 𝑦𝐵 ↦ (𝑥 + (𝐼𝑦))))
 
Theoremgrpsubval 12809 Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &   𝐼 = (invg𝐺)    &    = (-g𝐺)       ((𝑋𝐵𝑌𝐵) → (𝑋 𝑌) = (𝑋 + (𝐼𝑌)))
 
Theoremgrpinvf 12810 The group inversion operation is a function on the base set. (Contributed by Mario Carneiro, 4-May-2015.)
𝐵 = (Base‘𝐺)    &   𝑁 = (invg𝐺)       (𝐺 ∈ Grp → 𝑁:𝐵𝐵)
 
Theoremgrpinvcl 12811 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 ∧ 𝑋𝐵) → (𝑁𝑋) ∈ 𝐵)
 
Theoremgrplinv 12812 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 )
 
Theoremgrprinv 12813 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 )
 
Theoremgrpinvid1 12814 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 ))
 
Theoremgrpinvid2 12815 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 ))
 
Theoremisgrpinv 12816* 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 ) ↔ 𝑁 = 𝑀))
 
Theoremgrplrinv 12817* In a group, every member has a left and right inverse. (Contributed by AV, 1-Sep-2021.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    0 = (0g𝐺)       (𝐺 ∈ Grp → ∀𝑥𝐵𝑦𝐵 ((𝑦 + 𝑥) = 0 ∧ (𝑥 + 𝑦) = 0 ))
 
Theoremgrpidinv2 12818* 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 )))
 
Theoremgrpidinv 12819* 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 → ∃𝑢𝐵𝑥𝐵 (((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥) ∧ ∃𝑦𝐵 ((𝑦 + 𝑥) = 𝑢 ∧ (𝑥 + 𝑦) = 𝑢)))
 
Theoremgrpinvid 12820 The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011.)
0 = (0g𝐺)    &   𝑁 = (invg𝐺)       (𝐺 ∈ Grp → (𝑁0 ) = 0 )
 
Theoremgrplcan 12821 Left cancellation law for groups. (Contributed by NM, 25-Aug-2011.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)       ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑍 + 𝑋) = (𝑍 + 𝑌) ↔ 𝑋 = 𝑌))
 
Theoremgrpasscan1 12822 An associative cancellation law for groups. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by AV, 30-Aug-2021.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &   𝑁 = (invg𝐺)       ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 + ((𝑁𝑋) + 𝑌)) = 𝑌)
 
Theoremgrpasscan2 12823 An associative cancellation law for groups. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &   𝑁 = (invg𝐺)       ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 + (𝑁𝑌)) + 𝑌) = 𝑋)
 
Theoremgrpidrcan 12824 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 ))
 
Theoremgrpidlcan 12825 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 ))
 
Theoremgrpinvinv 12826 Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55. (Contributed by NM, 31-Mar-2014.)
𝐵 = (Base‘𝐺)    &   𝑁 = (invg𝐺)       ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑁‘(𝑁𝑋)) = 𝑋)
 
Theoremgrpinvcnv 12827 The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015.)
𝐵 = (Base‘𝐺)    &   𝑁 = (invg𝐺)       (𝐺 ∈ Grp → 𝑁 = 𝑁)
 
Theoremgrpinv11 12828 The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015.)
𝐵 = (Base‘𝐺)    &   𝑁 = (invg𝐺)    &   (𝜑𝐺 ∈ Grp)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)       (𝜑 → ((𝑁𝑋) = (𝑁𝑌) ↔ 𝑋 = 𝑌))
 
Theoremgrpinvf1o 12829 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𝐵)
 
Theoremgrpinvnz 12830 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 )
 
Theoremgrpinvnzcl 12831 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 }))
 
Theoremgrpsubinv 12832 Subtraction of an inverse. (Contributed by NM, 7-Apr-2015.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)    &   𝑁 = (invg𝐺)    &   (𝜑𝐺 ∈ Grp)    &   (𝜑𝑋𝐵)    &   (𝜑𝑌𝐵)       (𝜑 → (𝑋 (𝑁𝑌)) = (𝑋 + 𝑌))
 
Theoremgrplmulf1o 12833* 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𝐵)
 
Theoremgrpinvpropdg 12834* 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𝐿))
 
Theoremgrpidssd 12835* 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𝑆))
 
Theoremgrpinvssd 12836* 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𝑀)‘𝑋)))
 
Theoremgrpinvadd 12837 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 ∧ 𝑋𝐵𝑌𝐵) → (𝑁‘(𝑋 + 𝑌)) = ((𝑁𝑌) + (𝑁𝑋)))
 
Theoremgrpsubf 12838 Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014.)
𝐵 = (Base‘𝐺)    &    = (-g𝐺)       (𝐺 ∈ Grp → :(𝐵 × 𝐵)⟶𝐵)
 
Theoremgrpsubcl 12839 Closure of group subtraction. (Contributed by NM, 31-Mar-2014.)
𝐵 = (Base‘𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑋 𝑌) ∈ 𝐵)
 
Theoremgrpsubrcan 12840 Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014.)
𝐵 = (Base‘𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑍) = (𝑌 𝑍) ↔ 𝑋 = 𝑌))
 
Theoremgrpinvsub 12841 Inverse of a group subtraction. (Contributed by NM, 9-Sep-2014.)
𝐵 = (Base‘𝐺)    &    = (-g𝐺)    &   𝑁 = (invg𝐺)       ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → (𝑁‘(𝑋 𝑌)) = (𝑌 𝑋))
 
Theoremgrpinvval2 12842 A df-neg 8121-like equation for inverse in terms of group subtraction. (Contributed by Mario Carneiro, 4-Oct-2015.)
𝐵 = (Base‘𝐺)    &    = (-g𝐺)    &   𝑁 = (invg𝐺)    &    0 = (0g𝐺)       ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑁𝑋) = ( 0 𝑋))
 
Theoremgrpsubid 12843 Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014.)
𝐵 = (Base‘𝐺)    &    0 = (0g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑋 𝑋) = 0 )
 
Theoremgrpsubid1 12844 Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015.)
𝐵 = (Base‘𝐺)    &    0 = (0g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ 𝑋𝐵) → (𝑋 0 ) = 𝑋)
 
Theoremgrpsubeq0 12845 If the difference between two group elements is zero, they are equal. (subeq0 8173 analog.) (Contributed by NM, 31-Mar-2014.)
𝐵 = (Base‘𝐺)    &    0 = (0g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌) = 0𝑋 = 𝑌))
 
Theoremgrpsubadd0sub 12846 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 𝑌)))
 
Theoremgrpsubadd 12847 Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) = 𝑍 ↔ (𝑍 + 𝑌) = 𝑋))
 
Theoremgrpsubsub 12848 Double group subtraction. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → (𝑋 (𝑌 𝑍)) = (𝑋 + (𝑍 𝑌)))
 
Theoremgrpaddsubass 12849 Associative-type law for group subtraction and addition. (Contributed by NM, 16-Apr-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑌) 𝑍) = (𝑋 + (𝑌 𝑍)))
 
Theoremgrppncan 12850 Cancellation law for subtraction (pncan 8153 analog). (Contributed by NM, 16-Apr-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 + 𝑌) 𝑌) = 𝑋)
 
Theoremgrpnpcan 12851 Cancellation law for subtraction (npcan 8156 analog). (Contributed by NM, 19-Apr-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ 𝑋𝐵𝑌𝐵) → ((𝑋 𝑌) + 𝑌) = 𝑋)
 
Theoremgrpsubsub4 12852 Double group subtraction (subsub4 8180 analog). (Contributed by Mario Carneiro, 2-Dec-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) 𝑍) = (𝑋 (𝑍 + 𝑌)))
 
Theoremgrppnpcan2 12853 Cancellation law for mixed addition and subtraction. (pnpcan2 8187 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 + 𝑍) (𝑌 + 𝑍)) = (𝑋 𝑌))
 
Theoremgrpnpncan 12854 Cancellation law for group subtraction. (npncan 8168 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑌) + (𝑌 𝑍)) = (𝑋 𝑍))
 
Theoremgrpnpncan0 12855 Cancellation law for group subtraction (npncan2 8174 analog). (Contributed by AV, 24-Nov-2019.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    = (-g𝐺)    &    0 = (0g𝐺)       ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵)) → ((𝑋 𝑌) + (𝑌 𝑋)) = 0 )
 
Theoremgrpnnncan2 12856 Cancellation law for group subtraction. (nnncan2 8184 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
𝐵 = (Base‘𝐺)    &    = (-g𝐺)       ((𝐺 ∈ Grp ∧ (𝑋𝐵𝑌𝐵𝑍𝐵)) → ((𝑋 𝑍) (𝑌 𝑍)) = (𝑋 𝑌))
 
Theoremdfgrp3mlem 12857* Lemma for dfgrp3m 12858. (Contributed by AV, 28-Aug-2021.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)       ((𝐺 ∈ Smgrp ∧ ∃𝑤 𝑤𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (∃𝑙𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟𝐵 (𝑥 + 𝑟) = 𝑦)) → ∃𝑢𝐵𝑎𝐵 ((𝑢 + 𝑎) = 𝑎 ∧ ∃𝑖𝐵 (𝑖 + 𝑎) = 𝑢))
 
Theoremdfgrp3m 12858* 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 ∧ ∃𝑤 𝑤𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (∃𝑙𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟𝐵 (𝑥 + 𝑟) = 𝑦)))
 
Theoremdfgrp3me 12859* 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 ↔ (∃𝑤 𝑤𝐵 ∧ ∀𝑥𝐵𝑦𝐵 ((𝑥 + 𝑦) ∈ 𝐵 ∧ ∀𝑧𝐵 ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)) ∧ (∃𝑙𝐵 (𝑙 + 𝑥) = 𝑦 ∧ ∃𝑟𝐵 (𝑥 + 𝑟) = 𝑦))))
 
Theoremgrplactfval 12860* The left group action of element 𝐴 of group 𝐺. (Contributed by Paul Chapman, 18-Mar-2008.)
𝐹 = (𝑔𝑋 ↦ (𝑎𝑋 ↦ (𝑔 + 𝑎)))    &   𝑋 = (Base‘𝐺)       (𝐴𝑋 → (𝐹𝐴) = (𝑎𝑋 ↦ (𝐴 + 𝑎)))
 
Theoremgrplactcnv 12861* 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𝑋(𝐹𝐴) = (𝐹‘(𝐼𝐴))))
 
Theoremgrplactf1o 12862* 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𝑋)
 
Theoremgrpsubpropdg 12863 Weak property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 27-Mar-2015.)
(𝜑 → (Base‘𝐺) = (Base‘𝐻))    &   (𝜑 → (+g𝐺) = (+g𝐻))    &   (𝜑𝐺𝑉)    &   (𝜑𝐻𝑊)       (𝜑 → (-g𝐺) = (-g𝐻))
 
Theoremgrpsubpropd2 12864* Strong property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 4-Oct-2015.)
(𝜑𝐵 = (Base‘𝐺))    &   (𝜑𝐵 = (Base‘𝐻))    &   (𝜑𝐺 ∈ Grp)    &   ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(+g𝐺)𝑦) = (𝑥(+g𝐻)𝑦))       (𝜑 → (-g𝐺) = (-g𝐻))
 
Theoremgrp1 12865 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 AV, 28-Apr-2019.)
𝑀 = {⟨(Base‘ndx), {𝐼}⟩, ⟨(+g‘ndx), {⟨⟨𝐼, 𝐼⟩, 𝐼⟩}⟩}       (𝐼𝑉𝑀 ∈ Grp)
 
Theoremgrp1inv 12866 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 ↾ {𝐼}))
 
Theoremmhmlem 12867* Lemma for mhmmnd 12869 and ghmgrp 12871. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 25-Jan-2020.)
((𝜑𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))    &   (𝜑𝐴𝑋)    &   (𝜑𝐵𝑋)       (𝜑 → (𝐹‘(𝐴 + 𝐵)) = ((𝐹𝐴) (𝐹𝐵)))
 
Theoremmhmid 12868* A surjective monoid morphism preserves identity element. (Contributed by Thierry Arnoux, 25-Jan-2020.)
((𝜑𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))    &   𝑋 = (Base‘𝐺)    &   𝑌 = (Base‘𝐻)    &    + = (+g𝐺)    &    = (+g𝐻)    &   (𝜑𝐹:𝑋onto𝑌)    &   (𝜑𝐺 ∈ Mnd)    &    0 = (0g𝐺)       (𝜑 → (𝐹0 ) = (0g𝐻))
 
Theoremmhmmnd 12869* 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)
 
Theoremmhmfmhm 12870* The function fulfilling the conditions of mhmmnd 12869 is a monoid homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.)
((𝜑𝑥𝑋𝑦𝑋) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹𝑥) (𝐹𝑦)))    &   𝑋 = (Base‘𝐺)    &   𝑌 = (Base‘𝐻)    &    + = (+g𝐺)    &    = (+g𝐻)    &   (𝜑𝐹:𝑋onto𝑌)    &   (𝜑𝐺 ∈ Mnd)       (𝜑𝐹 ∈ (𝐺 MndHom 𝐻))
 
Theoremghmgrp 12871* 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)
 
7.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 12873, however, defines the group multiple for arbitrary (i.e. also negative) integers. This is meaningful for groups only, and requires Definition df-minusg 12771 of the inverse operation invg.

 
Syntaxcmg 12872 Extend class notation with a function mapping a group operation to the multiple/power operation for the magma/group.
class .g
 
Definitiondf-mulg 12873* 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𝑔)‘(𝑠‘-𝑛))))))
 
Theoremmulgfvalg 12874* Group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    0 = (0g𝐺)    &   𝐼 = (invg𝐺)    &    · = (.g𝐺)       (𝐺𝑉· = (𝑛 ∈ ℤ, 𝑥𝐵 ↦ if(𝑛 = 0, 0 , if(0 < 𝑛, (seq1( + , (ℕ × {𝑥}))‘𝑛), (𝐼‘(seq1( + , (ℕ × {𝑥}))‘-𝑛))))))
 
Theoremmulgval 12875 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 < 𝑁, (𝑆𝑁), (𝐼‘(𝑆‘-𝑁)))))
 
Theoremmulgfng 12876 Functionality of the group multiple operation. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)       (𝐺𝑉· Fn (ℤ × 𝐵))
 
Theoremmulg0 12877 Group multiple (exponentiation) operation at zero. (Contributed by Mario Carneiro, 11-Dec-2014.)
𝐵 = (Base‘𝐺)    &    0 = (0g𝐺)    &    · = (.g𝐺)       (𝑋𝐵 → (0 · 𝑋) = 0 )
 
Theoremmulgnn 12878 Group multiple (exponentiation) operation at a positive integer. (Contributed by Mario Carneiro, 11-Dec-2014.)
𝐵 = (Base‘𝐺)    &    + = (+g𝐺)    &    · = (.g𝐺)    &   𝑆 = seq1( + , (ℕ × {𝑋}))       ((𝑁 ∈ ℕ ∧ 𝑋𝐵) → (𝑁 · 𝑋) = (𝑆𝑁))
 
Theoremmulg1 12879 Group multiple (exponentiation) operation at one. (Contributed by Mario Carneiro, 11-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)       (𝑋𝐵 → (1 · 𝑋) = 𝑋)
 
Theoremmulgnnp1 12880 Group multiple (exponentiation) operation at a successor. (Contributed by Mario Carneiro, 11-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    + = (+g𝐺)       ((𝑁 ∈ ℕ ∧ 𝑋𝐵) → ((𝑁 + 1) · 𝑋) = ((𝑁 · 𝑋) + 𝑋))
 
Theoremmulg2 12881 Group multiple (exponentiation) operation at two. (Contributed by Mario Carneiro, 15-Oct-2015.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    + = (+g𝐺)       (𝑋𝐵 → (2 · 𝑋) = (𝑋 + 𝑋))
 
Theoremmulgnegnn 12882 Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 11-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &   𝐼 = (invg𝐺)       ((𝑁 ∈ ℕ ∧ 𝑋𝐵) → (-𝑁 · 𝑋) = (𝐼‘(𝑁 · 𝑋)))
 
Theoremmulgnn0p1 12883 Group multiple (exponentiation) operation at a successor, extended to 0. (Contributed by Mario Carneiro, 11-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    + = (+g𝐺)       ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0𝑋𝐵) → ((𝑁 + 1) · 𝑋) = ((𝑁 · 𝑋) + 𝑋))
 
Theoremmulgnnsubcl 12884* Closure of the group multiple (exponentiation) operation in a subsemigroup. (Contributed by Mario Carneiro, 10-Jan-2015.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    + = (+g𝐺)    &   (𝜑𝐺𝑉)    &   (𝜑𝑆𝐵)    &   ((𝜑𝑥𝑆𝑦𝑆) → (𝑥 + 𝑦) ∈ 𝑆)       ((𝜑𝑁 ∈ ℕ ∧ 𝑋𝑆) → (𝑁 · 𝑋) ∈ 𝑆)
 
Theoremmulgnn0subcl 12885* Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    + = (+g𝐺)    &   (𝜑𝐺𝑉)    &   (𝜑𝑆𝐵)    &   ((𝜑𝑥𝑆𝑦𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    &    0 = (0g𝐺)    &   (𝜑0𝑆)       ((𝜑𝑁 ∈ ℕ0𝑋𝑆) → (𝑁 · 𝑋) ∈ 𝑆)
 
Theoremmulgsubcl 12886* Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 10-Jan-2015.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    + = (+g𝐺)    &   (𝜑𝐺𝑉)    &   (𝜑𝑆𝐵)    &   ((𝜑𝑥𝑆𝑦𝑆) → (𝑥 + 𝑦) ∈ 𝑆)    &    0 = (0g𝐺)    &   (𝜑0𝑆)    &   𝐼 = (invg𝐺)    &   ((𝜑𝑥𝑆) → (𝐼𝑥) ∈ 𝑆)       ((𝜑𝑁 ∈ ℤ ∧ 𝑋𝑆) → (𝑁 · 𝑋) ∈ 𝑆)
 
Theoremmulgnncl 12887 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 ∧ 𝑁 ∈ ℕ ∧ 𝑋𝐵) → (𝑁 · 𝑋) ∈ 𝐵)
 
Theoremmulgnn0cl 12888 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𝑋𝐵) → (𝑁 · 𝑋) ∈ 𝐵)
 
Theoremmulgcl 12889 Closure of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)       ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵) → (𝑁 · 𝑋) ∈ 𝐵)
 
Theoremmulgneg 12890 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 ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵) → (-𝑁 · 𝑋) = (𝐼‘(𝑁 · 𝑋)))
 
Theoremmulgnegneg 12891 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 ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵) → (𝐼‘(-𝑁 · 𝑋)) = (𝑁 · 𝑋))
 
Theoremmulgm1 12892 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 · 𝑋) = (𝐼𝑋))
 
Theoremmulgcld 12893 Deduction associated with mulgcl 12889. (Contributed by Rohan Ridenour, 3-Aug-2023.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &   (𝜑𝐺 ∈ Grp)    &   (𝜑𝑁 ∈ ℤ)    &   (𝜑𝑋𝐵)       (𝜑 → (𝑁 · 𝑋) ∈ 𝐵)
 
Theoremmulgaddcomlem 12894 Lemma for mulgaddcom 12895. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    + = (+g𝐺)       (((𝐺 ∈ Grp ∧ 𝑦 ∈ ℤ ∧ 𝑋𝐵) ∧ ((𝑦 · 𝑋) + 𝑋) = (𝑋 + (𝑦 · 𝑋))) → ((-𝑦 · 𝑋) + 𝑋) = (𝑋 + (-𝑦 · 𝑋)))
 
Theoremmulgaddcom 12895 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 ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵) → ((𝑁 · 𝑋) + 𝑋) = (𝑋 + (𝑁 · 𝑋)))
 
Theoremmulginvcom 12896 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 ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵) → (𝑁 · (𝐼𝑋)) = (𝐼‘(𝑁 · 𝑋)))
 
Theoremmulginvinv 12897 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 ∧ 𝑁 ∈ ℤ ∧ 𝑋𝐵) → (𝐼‘(𝑁 · (𝐼𝑋))) = (𝑁 · 𝑋))
 
Theoremmulgnn0z 12898 A group multiple of the identity, for nonnegative multiple. (Contributed by Mario Carneiro, 13-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    0 = (0g𝐺)       ((𝐺 ∈ Mnd ∧ 𝑁 ∈ ℕ0) → (𝑁 · 0 ) = 0 )
 
Theoremmulgz 12899 A group multiple of the identity, for integer multiple. (Contributed by Mario Carneiro, 13-Dec-2014.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    0 = (0g𝐺)       ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → (𝑁 · 0 ) = 0 )
 
Theoremmulgnndir 12900 Sum of group multiples, for positive multiples. (Contributed by Mario Carneiro, 11-Dec-2014.) (Revised by AV, 29-Aug-2021.)
𝐵 = (Base‘𝐺)    &    · = (.g𝐺)    &    + = (+g𝐺)       ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14485
  Copyright terms: Public domain < Previous  Next >