HomeHome Intuitionistic Logic Explorer
Theorem List (p. 130 of 149)
< 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 - 12901-13000   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremgrpsgrp 12901 A group is a semigroup. (Contributed by AV, 28-Aug-2021.)
(๐บ โˆˆ Grp โ†’ ๐บ โˆˆ Smgrp)
 
Theoremdfgrp2 12902* 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 12880, 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 โˆง โˆƒ๐‘› โˆˆ ๐ต โˆ€๐‘ฅ โˆˆ ๐ต ((๐‘› + ๐‘ฅ) = ๐‘ฅ โˆง โˆƒ๐‘– โˆˆ ๐ต (๐‘– + ๐‘ฅ) = ๐‘›)))
 
Theoremdfgrp2e 12903* 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 โ†” (โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต ((๐‘ฅ + ๐‘ฆ) โˆˆ ๐ต โˆง โˆ€๐‘ง โˆˆ ๐ต ((๐‘ฅ + ๐‘ฆ) + ๐‘ง) = (๐‘ฅ + (๐‘ฆ + ๐‘ง))) โˆง โˆƒ๐‘› โˆˆ ๐ต โˆ€๐‘ฅ โˆˆ ๐ต ((๐‘› + ๐‘ฅ) = ๐‘ฅ โˆง โˆƒ๐‘– โˆˆ ๐ต (๐‘– + ๐‘ฅ) = ๐‘›)))
 
Theoremgrpidcl 12904 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 โˆˆ ๐ต)
 
Theoremgrpbn0 12905 The base set of a group is not empty. It is also inhabited (see grpidcl 12904). (Contributed by Szymon Jaroszewicz, 3-Apr-2007.)
๐ต = (Baseโ€˜๐บ)    โ‡’   (๐บ โˆˆ Grp โ†’ ๐ต โ‰  โˆ…)
 
Theoremgrplid 12906 The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &    0 = (0gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต) โ†’ ( 0 + ๐‘‹) = ๐‘‹)
 
Theoremgrprid 12907 The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &    0 = (0gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต) โ†’ (๐‘‹ + 0 ) = ๐‘‹)
 
Theoremgrpn0 12908 A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (Revised by Mario Carneiro, 2-Dec-2014.)
(๐บ โˆˆ Grp โ†’ ๐บ โ‰  โˆ…)
 
Theoremhashfingrpnn 12909 A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.)
๐ต = (Baseโ€˜๐บ)    &   (๐œ‘ โ†’ ๐บ โˆˆ Grp)    &   (๐œ‘ โ†’ ๐ต โˆˆ Fin)    โ‡’   (๐œ‘ โ†’ (โ™ฏโ€˜๐ต) โˆˆ โ„•)
 
Theoremgrprcan 12910 Right cancellation law for groups. (Contributed by NM, 24-Aug-2011.) (Proof shortened by Mario Carneiro, 6-Jan-2015.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐‘‹ + ๐‘) = (๐‘Œ + ๐‘) โ†” ๐‘‹ = ๐‘Œ))
 
Theoremgrpinveu 12911* 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 12912 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 12913 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 12914* Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 12899. (Contributed by Mario Carneiro, 14-Jun-2015.)
(๐œ‘ โ†’ ๐ต = (Baseโ€˜๐บ))    &   (๐œ‘ โ†’ + = (+gโ€˜๐บ))    &   (๐œ‘ โ†’ 0 โˆˆ ๐ต)    &   ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต) โ†’ ( 0 + ๐‘ฅ) = ๐‘ฅ)    &   (๐œ‘ โ†’ ๐บ โˆˆ Grp)    โ‡’   (๐œ‘ โ†’ 0 = (0gโ€˜๐บ))
 
Theoremgrpinvfvalg 12915* 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 12916* 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 12917 Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015.)
๐ต = (Baseโ€˜๐บ)    &   ๐‘ = (invgโ€˜๐บ)    โ‡’   (๐บ โˆˆ ๐‘‰ โ†’ ๐‘ Fn ๐ต)
 
Theoremgrpsubfvalg 12918* 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 12919 Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &   ๐ผ = (invgโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต) โ†’ (๐‘‹ โˆ’ ๐‘Œ) = (๐‘‹ + (๐ผโ€˜๐‘Œ)))
 
Theoremgrpinvf 12920 The group inversion operation is a function on the base set. (Contributed by Mario Carneiro, 4-May-2015.)
๐ต = (Baseโ€˜๐บ)    &   ๐‘ = (invgโ€˜๐บ)    โ‡’   (๐บ โˆˆ Grp โ†’ ๐‘:๐ตโŸถ๐ต)
 
Theoremgrpinvcl 12921 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 12922 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 12923 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 12924 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 12925 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 12926* 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 12927* 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 12928* 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 12929* 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 12930 The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011.)
0 = (0gโ€˜๐บ)    &   ๐‘ = (invgโ€˜๐บ)    โ‡’   (๐บ โˆˆ Grp โ†’ (๐‘โ€˜ 0 ) = 0 )
 
Theoremgrpressid 12931 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 12530. (Contributed by Jim Kingdon, 28-Feb-2025.)
๐ต = (Baseโ€˜๐บ)    โ‡’   (๐บ โˆˆ Grp โ†’ (๐บ โ†พs ๐ต) โˆˆ Grp)
 
Theoremgrplcan 12932 Left cancellation law for groups. (Contributed by NM, 25-Aug-2011.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐‘ + ๐‘‹) = (๐‘ + ๐‘Œ) โ†” ๐‘‹ = ๐‘Œ))
 
Theoremgrpasscan1 12933 An associative cancellation law for groups. (Contributed by Paul Chapman, 25-Feb-2008.) (Revised by AV, 30-Aug-2021.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &   ๐‘ = (invgโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต) โ†’ (๐‘‹ + ((๐‘โ€˜๐‘‹) + ๐‘Œ)) = ๐‘Œ)
 
Theoremgrpasscan2 12934 An associative cancellation law for groups. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &   ๐‘ = (invgโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต) โ†’ ((๐‘‹ + (๐‘โ€˜๐‘Œ)) + ๐‘Œ) = ๐‘‹)
 
Theoremgrpidrcan 12935 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 12936 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 12937 Double inverse law for groups. Lemma 2.2.1(c) of [Herstein] p. 55. (Contributed by NM, 31-Mar-2014.)
๐ต = (Baseโ€˜๐บ)    &   ๐‘ = (invgโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต) โ†’ (๐‘โ€˜(๐‘โ€˜๐‘‹)) = ๐‘‹)
 
Theoremgrpinvcnv 12938 The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015.)
๐ต = (Baseโ€˜๐บ)    &   ๐‘ = (invgโ€˜๐บ)    โ‡’   (๐บ โˆˆ Grp โ†’ โ—ก๐‘ = ๐‘)
 
Theoremgrpinv11 12939 The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015.)
๐ต = (Baseโ€˜๐บ)    &   ๐‘ = (invgโ€˜๐บ)    &   (๐œ‘ โ†’ ๐บ โˆˆ Grp)    &   (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)    &   (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต)    โ‡’   (๐œ‘ โ†’ ((๐‘โ€˜๐‘‹) = (๐‘โ€˜๐‘Œ) โ†” ๐‘‹ = ๐‘Œ))
 
Theoremgrpinvf1o 12940 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 12941 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 12942 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 12943 Subtraction of an inverse. (Contributed by NM, 7-Apr-2015.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    &   ๐‘ = (invgโ€˜๐บ)    &   (๐œ‘ โ†’ ๐บ โˆˆ Grp)    &   (๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ต)    &   (๐œ‘ โ†’ ๐‘Œ โˆˆ ๐ต)    โ‡’   (๐œ‘ โ†’ (๐‘‹ โˆ’ (๐‘โ€˜๐‘Œ)) = (๐‘‹ + ๐‘Œ))
 
Theoremgrplmulf1o 12944* 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 12945* 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 12946* 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 12947* 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 12948 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 12949 Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014.)
๐ต = (Baseโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   (๐บ โˆˆ Grp โ†’ โˆ’ :(๐ต ร— ๐ต)โŸถ๐ต)
 
Theoremgrpsubcl 12950 Closure of group subtraction. (Contributed by NM, 31-Mar-2014.)
๐ต = (Baseโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต) โ†’ (๐‘‹ โˆ’ ๐‘Œ) โˆˆ ๐ต)
 
Theoremgrpsubrcan 12951 Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014.)
๐ต = (Baseโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐‘‹ โˆ’ ๐‘) = (๐‘Œ โˆ’ ๐‘) โ†” ๐‘‹ = ๐‘Œ))
 
Theoremgrpinvsub 12952 Inverse of a group subtraction. (Contributed by NM, 9-Sep-2014.)
๐ต = (Baseโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    &   ๐‘ = (invgโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต) โ†’ (๐‘โ€˜(๐‘‹ โˆ’ ๐‘Œ)) = (๐‘Œ โˆ’ ๐‘‹))
 
Theoremgrpinvval2 12953 A df-neg 8131-like equation for inverse in terms of group subtraction. (Contributed by Mario Carneiro, 4-Oct-2015.)
๐ต = (Baseโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    &   ๐‘ = (invgโ€˜๐บ)    &    0 = (0gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต) โ†’ (๐‘โ€˜๐‘‹) = ( 0 โˆ’ ๐‘‹))
 
Theoremgrpsubid 12954 Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014.)
๐ต = (Baseโ€˜๐บ)    &    0 = (0gโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต) โ†’ (๐‘‹ โˆ’ ๐‘‹) = 0 )
 
Theoremgrpsubid1 12955 Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015.)
๐ต = (Baseโ€˜๐บ)    &    0 = (0gโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต) โ†’ (๐‘‹ โˆ’ 0 ) = ๐‘‹)
 
Theoremgrpsubeq0 12956 If the difference between two group elements is zero, they are equal. (subeq0 8183 analog.) (Contributed by NM, 31-Mar-2014.)
๐ต = (Baseโ€˜๐บ)    &    0 = (0gโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต) โ†’ ((๐‘‹ โˆ’ ๐‘Œ) = 0 โ†” ๐‘‹ = ๐‘Œ))
 
Theoremgrpsubadd0sub 12957 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 12958 Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐‘‹ โˆ’ ๐‘Œ) = ๐‘ โ†” (๐‘ + ๐‘Œ) = ๐‘‹))
 
Theoremgrpsubsub 12959 Double group subtraction. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ (๐‘‹ โˆ’ (๐‘Œ โˆ’ ๐‘)) = (๐‘‹ + (๐‘ โˆ’ ๐‘Œ)))
 
Theoremgrpaddsubass 12960 Associative-type law for group subtraction and addition. (Contributed by NM, 16-Apr-2014.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐‘‹ + ๐‘Œ) โˆ’ ๐‘) = (๐‘‹ + (๐‘Œ โˆ’ ๐‘)))
 
Theoremgrppncan 12961 Cancellation law for subtraction (pncan 8163 analog). (Contributed by NM, 16-Apr-2014.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต) โ†’ ((๐‘‹ + ๐‘Œ) โˆ’ ๐‘Œ) = ๐‘‹)
 
Theoremgrpnpcan 12962 Cancellation law for subtraction (npcan 8166 analog). (Contributed by NM, 19-Apr-2014.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต) โ†’ ((๐‘‹ โˆ’ ๐‘Œ) + ๐‘Œ) = ๐‘‹)
 
Theoremgrpsubsub4 12963 Double group subtraction (subsub4 8190 analog). (Contributed by Mario Carneiro, 2-Dec-2014.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐‘‹ โˆ’ ๐‘Œ) โˆ’ ๐‘) = (๐‘‹ โˆ’ (๐‘ + ๐‘Œ)))
 
Theoremgrppnpcan2 12964 Cancellation law for mixed addition and subtraction. (pnpcan2 8197 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐‘‹ + ๐‘) โˆ’ (๐‘Œ + ๐‘)) = (๐‘‹ โˆ’ ๐‘Œ))
 
Theoremgrpnpncan 12965 Cancellation law for group subtraction. (npncan 8178 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐‘‹ โˆ’ ๐‘Œ) + (๐‘Œ โˆ’ ๐‘)) = (๐‘‹ โˆ’ ๐‘))
 
Theoremgrpnpncan0 12966 Cancellation law for group subtraction (npncan2 8184 analog). (Contributed by AV, 24-Nov-2019.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    &    0 = (0gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต)) โ†’ ((๐‘‹ โˆ’ ๐‘Œ) + (๐‘Œ โˆ’ ๐‘‹)) = 0 )
 
Theoremgrpnnncan2 12967 Cancellation law for group subtraction. (nnncan2 8194 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.)
๐ต = (Baseโ€˜๐บ)    &    โˆ’ = (-gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง (๐‘‹ โˆˆ ๐ต โˆง ๐‘Œ โˆˆ ๐ต โˆง ๐‘ โˆˆ ๐ต)) โ†’ ((๐‘‹ โˆ’ ๐‘) โˆ’ (๐‘Œ โˆ’ ๐‘)) = (๐‘‹ โˆ’ ๐‘Œ))
 
Theoremdfgrp3mlem 12968* Lemma for dfgrp3m 12969. (Contributed by AV, 28-Aug-2021.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Smgrp โˆง โˆƒ๐‘ค ๐‘ค โˆˆ ๐ต โˆง โˆ€๐‘ฅ โˆˆ ๐ต โˆ€๐‘ฆ โˆˆ ๐ต (โˆƒ๐‘™ โˆˆ ๐ต (๐‘™ + ๐‘ฅ) = ๐‘ฆ โˆง โˆƒ๐‘Ÿ โˆˆ ๐ต (๐‘ฅ + ๐‘Ÿ) = ๐‘ฆ)) โ†’ โˆƒ๐‘ข โˆˆ ๐ต โˆ€๐‘Ž โˆˆ ๐ต ((๐‘ข + ๐‘Ž) = ๐‘Ž โˆง โˆƒ๐‘– โˆˆ ๐ต (๐‘– + ๐‘Ž) = ๐‘ข))
 
Theoremdfgrp3m 12969* 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 12970* 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 12971* The left group action of element ๐ด of group ๐บ. (Contributed by Paul Chapman, 18-Mar-2008.)
๐น = (๐‘” โˆˆ ๐‘‹ โ†ฆ (๐‘Ž โˆˆ ๐‘‹ โ†ฆ (๐‘” + ๐‘Ž)))    &   ๐‘‹ = (Baseโ€˜๐บ)    โ‡’   (๐ด โˆˆ ๐‘‹ โ†’ (๐นโ€˜๐ด) = (๐‘Ž โˆˆ ๐‘‹ โ†ฆ (๐ด + ๐‘Ž)))
 
Theoremgrplactcnv 12972* 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 12973* 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 12974 Weak property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 27-Mar-2015.)
(๐œ‘ โ†’ (Baseโ€˜๐บ) = (Baseโ€˜๐ป))    &   (๐œ‘ โ†’ (+gโ€˜๐บ) = (+gโ€˜๐ป))    &   (๐œ‘ โ†’ ๐บ โˆˆ ๐‘‰)    &   (๐œ‘ โ†’ ๐ป โˆˆ ๐‘Š)    โ‡’   (๐œ‘ โ†’ (-gโ€˜๐บ) = (-gโ€˜๐ป))
 
Theoremgrpsubpropd2 12975* Strong property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 4-Oct-2015.)
(๐œ‘ โ†’ ๐ต = (Baseโ€˜๐บ))    &   (๐œ‘ โ†’ ๐ต = (Baseโ€˜๐ป))    &   (๐œ‘ โ†’ ๐บ โˆˆ Grp)    &   ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ต โˆง ๐‘ฆ โˆˆ ๐ต)) โ†’ (๐‘ฅ(+gโ€˜๐บ)๐‘ฆ) = (๐‘ฅ(+gโ€˜๐ป)๐‘ฆ))    โ‡’   (๐œ‘ โ†’ (-gโ€˜๐บ) = (-gโ€˜๐ป))
 
Theoremgrp1 12976 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 12977 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 12978* Lemma for mhmmnd 12980 and ghmgrp 12982. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 25-Jan-2020.)
((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ ๐‘‹) โ†’ (๐นโ€˜(๐‘ฅ + ๐‘ฆ)) = ((๐นโ€˜๐‘ฅ) โจฃ (๐นโ€˜๐‘ฆ)))    &   (๐œ‘ โ†’ ๐ด โˆˆ ๐‘‹)    &   (๐œ‘ โ†’ ๐ต โˆˆ ๐‘‹)    โ‡’   (๐œ‘ โ†’ (๐นโ€˜(๐ด + ๐ต)) = ((๐นโ€˜๐ด) โจฃ (๐นโ€˜๐ต)))
 
Theoremmhmid 12979* 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 12980* 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 12981* The function fulfilling the conditions of mhmmnd 12980 is a monoid homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020.)
((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ โˆง ๐‘ฆ โˆˆ ๐‘‹) โ†’ (๐นโ€˜(๐‘ฅ + ๐‘ฆ)) = ((๐นโ€˜๐‘ฅ) โจฃ (๐นโ€˜๐‘ฆ)))    &   ๐‘‹ = (Baseโ€˜๐บ)    &   ๐‘Œ = (Baseโ€˜๐ป)    &    + = (+gโ€˜๐บ)    &    โจฃ = (+gโ€˜๐ป)    &   (๐œ‘ โ†’ ๐น:๐‘‹โ€“ontoโ†’๐‘Œ)    &   (๐œ‘ โ†’ ๐บ โˆˆ Mnd)    โ‡’   (๐œ‘ โ†’ ๐น โˆˆ (๐บ MndHom ๐ป))
 
Theoremghmgrp 12982* 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 12984, however, defines the group multiple for arbitrary (i.e. also negative) integers. This is meaningful for groups only, and requires Definition df-minusg 12881 of the inverse operation invg.

 
Syntaxcmg 12983 Extend class notation with a function mapping a group operation to the multiple/power operation for the magma/group.
class .g
 
Definitiondf-mulg 12984* 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 12985* 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 12986 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 12987 Functionality of the group multiple operation. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
๐ต = (Baseโ€˜๐บ)    &    ยท = (.gโ€˜๐บ)    โ‡’   (๐บ โˆˆ ๐‘‰ โ†’ ยท Fn (โ„ค ร— ๐ต))
 
Theoremmulg0 12988 Group multiple (exponentiation) operation at zero. (Contributed by Mario Carneiro, 11-Dec-2014.)
๐ต = (Baseโ€˜๐บ)    &    0 = (0gโ€˜๐บ)    &    ยท = (.gโ€˜๐บ)    โ‡’   (๐‘‹ โˆˆ ๐ต โ†’ (0 ยท ๐‘‹) = 0 )
 
Theoremmulgnn 12989 Group multiple (exponentiation) operation at a positive integer. (Contributed by Mario Carneiro, 11-Dec-2014.)
๐ต = (Baseโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &    ยท = (.gโ€˜๐บ)    &   ๐‘† = seq1( + , (โ„• ร— {๐‘‹}))    โ‡’   ((๐‘ โˆˆ โ„• โˆง ๐‘‹ โˆˆ ๐ต) โ†’ (๐‘ ยท ๐‘‹) = (๐‘†โ€˜๐‘))
 
Theoremmulg1 12990 Group multiple (exponentiation) operation at one. (Contributed by Mario Carneiro, 11-Dec-2014.)
๐ต = (Baseโ€˜๐บ)    &    ยท = (.gโ€˜๐บ)    โ‡’   (๐‘‹ โˆˆ ๐ต โ†’ (1 ยท ๐‘‹) = ๐‘‹)
 
Theoremmulgnnp1 12991 Group multiple (exponentiation) operation at a successor. (Contributed by Mario Carneiro, 11-Dec-2014.)
๐ต = (Baseโ€˜๐บ)    &    ยท = (.gโ€˜๐บ)    &    + = (+gโ€˜๐บ)    โ‡’   ((๐‘ โˆˆ โ„• โˆง ๐‘‹ โˆˆ ๐ต) โ†’ ((๐‘ + 1) ยท ๐‘‹) = ((๐‘ ยท ๐‘‹) + ๐‘‹))
 
Theoremmulg2 12992 Group multiple (exponentiation) operation at two. (Contributed by Mario Carneiro, 15-Oct-2015.)
๐ต = (Baseโ€˜๐บ)    &    ยท = (.gโ€˜๐บ)    &    + = (+gโ€˜๐บ)    โ‡’   (๐‘‹ โˆˆ ๐ต โ†’ (2 ยท ๐‘‹) = (๐‘‹ + ๐‘‹))
 
Theoremmulgnegnn 12993 Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 11-Dec-2014.)
๐ต = (Baseโ€˜๐บ)    &    ยท = (.gโ€˜๐บ)    &   ๐ผ = (invgโ€˜๐บ)    โ‡’   ((๐‘ โˆˆ โ„• โˆง ๐‘‹ โˆˆ ๐ต) โ†’ (-๐‘ ยท ๐‘‹) = (๐ผโ€˜(๐‘ ยท ๐‘‹)))
 
Theoremmulgnn0p1 12994 Group multiple (exponentiation) operation at a successor, extended to โ„•0. (Contributed by Mario Carneiro, 11-Dec-2014.)
๐ต = (Baseโ€˜๐บ)    &    ยท = (.gโ€˜๐บ)    &    + = (+gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Mnd โˆง ๐‘ โˆˆ โ„•0 โˆง ๐‘‹ โˆˆ ๐ต) โ†’ ((๐‘ + 1) ยท ๐‘‹) = ((๐‘ ยท ๐‘‹) + ๐‘‹))
 
Theoremmulgnnsubcl 12995* Closure of the group multiple (exponentiation) operation in a subsemigroup. (Contributed by Mario Carneiro, 10-Jan-2015.)
๐ต = (Baseโ€˜๐บ)    &    ยท = (.gโ€˜๐บ)    &    + = (+gโ€˜๐บ)    &   (๐œ‘ โ†’ ๐บ โˆˆ ๐‘‰)    &   (๐œ‘ โ†’ ๐‘† โŠ† ๐ต)    &   ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘† โˆง ๐‘ฆ โˆˆ ๐‘†) โ†’ (๐‘ฅ + ๐‘ฆ) โˆˆ ๐‘†)    โ‡’   ((๐œ‘ โˆง ๐‘ โˆˆ โ„• โˆง ๐‘‹ โˆˆ ๐‘†) โ†’ (๐‘ ยท ๐‘‹) โˆˆ ๐‘†)
 
Theoremmulgnn0subcl 12996* 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 12997* 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 12998 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 12999 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 13000 Closure of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.)
๐ต = (Baseโ€˜๐บ)    &    ยท = (.gโ€˜๐บ)    โ‡’   ((๐บ โˆˆ Grp โˆง ๐‘ โˆˆ โ„ค โˆง ๐‘‹ โˆˆ ๐ต) โ†’ (๐‘ ยท ๐‘‹) โˆˆ ๐ต)
    < 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-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14834
  Copyright terms: Public domain < Previous  Next >