![]() |
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 |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | grpsgrp 12901 | A group is a semigroup. (Contributed by AV, 28-Aug-2021.) |
โข (๐บ โ Grp โ ๐บ โ Smgrp) | ||
Theorem | dfgrp2 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 โง โ๐ โ ๐ต โ๐ฅ โ ๐ต ((๐ + ๐ฅ) = ๐ฅ โง โ๐ โ ๐ต (๐ + ๐ฅ) = ๐))) | ||
Theorem | dfgrp2e 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 โ (โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ + ๐ฆ) โ ๐ต โง โ๐ง โ ๐ต ((๐ฅ + ๐ฆ) + ๐ง) = (๐ฅ + (๐ฆ + ๐ง))) โง โ๐ โ ๐ต โ๐ฅ โ ๐ต ((๐ + ๐ฅ) = ๐ฅ โง โ๐ โ ๐ต (๐ + ๐ฅ) = ๐))) | ||
Theorem | grpidcl 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 โ ๐ต) | ||
Theorem | grpbn0 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 โ ๐ต โ โ ) | ||
Theorem | grplid 12906 | The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข 0 = (0gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ต) โ ( 0 + ๐) = ๐) | ||
Theorem | grprid 12907 | The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข 0 = (0gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ต) โ (๐ + 0 ) = ๐) | ||
Theorem | grpn0 12908 | A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (Revised by Mario Carneiro, 2-Dec-2014.) |
โข (๐บ โ Grp โ ๐บ โ โ ) | ||
Theorem | hashfingrpnn 12909 | A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ต โ Fin) โ โข (๐ โ (โฏโ๐ต) โ โ) | ||
Theorem | grprcan 12910 | Right cancellation law for groups. (Contributed by NM, 24-Aug-2011.) (Proof shortened by Mario Carneiro, 6-Jan-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) = (๐ + ๐) โ ๐ = ๐)) | ||
Theorem | grpinveu 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 ) | ||
Theorem | grpid 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 = ๐)) | ||
Theorem | isgrpid2 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 = ๐)) | ||
Theorem | grpidd2 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โ๐บ)) | ||
Theorem | grpinvfvalg 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 ))) | ||
Theorem | grpinvval 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 )) | ||
Theorem | grpinvfng 12917 | Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (invgโ๐บ) โ โข (๐บ โ ๐ โ ๐ Fn ๐ต) | ||
Theorem | grpsubfvalg 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โ๐บ) โ โข (๐บ โ ๐ โ โ = (๐ฅ โ ๐ต, ๐ฆ โ ๐ต โฆ (๐ฅ + (๐ผโ๐ฆ)))) | ||
Theorem | grpsubval 12919 | Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข ๐ผ = (invgโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ ๐) = (๐ + (๐ผโ๐))) | ||
Theorem | grpinvf 12920 | The group inversion operation is a function on the base set. (Contributed by Mario Carneiro, 4-May-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (invgโ๐บ) โ โข (๐บ โ Grp โ ๐:๐ตโถ๐ต) | ||
Theorem | grpinvcl 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 โง ๐ โ ๐ต) โ (๐โ๐) โ ๐ต) | ||
Theorem | grplinv 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 ) | ||
Theorem | grprinv 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 ) | ||
Theorem | grpinvid1 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 )) | ||
Theorem | grpinvid2 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 )) | ||
Theorem | isgrpinv 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 ) โ ๐ = ๐)) | ||
Theorem | grplrinv 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 )) | ||
Theorem | grpidinv2 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 ))) | ||
Theorem | grpidinv 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 โ โ๐ข โ ๐ต โ๐ฅ โ ๐ต (((๐ข + ๐ฅ) = ๐ฅ โง (๐ฅ + ๐ข) = ๐ฅ) โง โ๐ฆ โ ๐ต ((๐ฆ + ๐ฅ) = ๐ข โง (๐ฅ + ๐ฆ) = ๐ข))) | ||
Theorem | grpinvid 12930 | The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011.) |
โข 0 = (0gโ๐บ) & โข ๐ = (invgโ๐บ) โ โข (๐บ โ Grp โ (๐โ 0 ) = 0 ) | ||
Theorem | grpressid 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) | ||
Theorem | grplcan 12932 | Left cancellation law for groups. (Contributed by NM, 25-Aug-2011.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) = (๐ + ๐) โ ๐ = ๐)) | ||
Theorem | grpasscan1 12933 | 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 12934 | 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 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 )) | ||
Theorem | grpidlcan 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 )) | ||
Theorem | grpinvinv 12937 | 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 12938 | The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (invgโ๐บ) โ โข (๐บ โ Grp โ โก๐ = ๐) | ||
Theorem | grpinv11 12939 | The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (invgโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐โ๐) = (๐โ๐) โ ๐ = ๐)) | ||
Theorem | grpinvf1o 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โ๐ต) | ||
Theorem | grpinvnz 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 ) | ||
Theorem | grpinvnzcl 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 })) | ||
Theorem | grpsubinv 12943 | Subtraction of an inverse. (Contributed by NM, 7-Apr-2015.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) & โข ๐ = (invgโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐ โ (๐โ๐)) = (๐ + ๐)) | ||
Theorem | grplmulf1o 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โ๐ต) | ||
Theorem | grpinvpropdg 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โ๐ฟ)) | ||
Theorem | grpidssd 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โ๐)) | ||
Theorem | grpinvssd 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โ๐)โ๐))) | ||
Theorem | grpinvadd 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 โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐โ(๐ + ๐)) = ((๐โ๐) + (๐โ๐))) | ||
Theorem | grpsubf 12949 | Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) โ โข (๐บ โ Grp โ โ :(๐ต ร ๐ต)โถ๐ต) | ||
Theorem | grpsubcl 12950 | Closure of group subtraction. (Contributed by NM, 31-Mar-2014.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ ๐) โ ๐ต) | ||
Theorem | grpsubrcan 12951 | Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ ๐) = (๐ โ ๐) โ ๐ = ๐)) | ||
Theorem | grpinvsub 12952 | Inverse of a group subtraction. (Contributed by NM, 9-Sep-2014.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) & โข ๐ = (invgโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐โ(๐ โ ๐)) = (๐ โ ๐)) | ||
Theorem | grpinvval2 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 โ ๐)) | ||
Theorem | grpsubid 12954 | Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ต) โ (๐ โ ๐) = 0 ) | ||
Theorem | grpsubid1 12955 | Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ต) โ (๐ โ 0 ) = ๐) | ||
Theorem | grpsubeq0 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 โ ๐ = ๐)) | ||
Theorem | grpsubadd0sub 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 โ ๐))) | ||
Theorem | grpsubadd 12958 | Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ ๐) = ๐ โ (๐ + ๐) = ๐)) | ||
Theorem | grpsubsub 12959 | Double group subtraction. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ โ (๐ โ ๐)) = (๐ + (๐ โ ๐))) | ||
Theorem | grpaddsubass 12960 | Associative-type law for group subtraction and addition. (Contributed by NM, 16-Apr-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) โ ๐) = (๐ + (๐ โ ๐))) | ||
Theorem | grppncan 12961 | Cancellation law for subtraction (pncan 8163 analog). (Contributed by NM, 16-Apr-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ + ๐) โ ๐) = ๐) | ||
Theorem | grpnpcan 12962 | Cancellation law for subtraction (npcan 8166 analog). (Contributed by NM, 19-Apr-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ โ ๐) + ๐) = ๐) | ||
Theorem | grpsubsub4 12963 | Double group subtraction (subsub4 8190 analog). (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ ๐) โ ๐) = (๐ โ (๐ + ๐))) | ||
Theorem | grppnpcan2 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 โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) โ (๐ + ๐)) = (๐ โ ๐)) | ||
Theorem | grpnpncan 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 โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ ๐) + (๐ โ ๐)) = (๐ โ ๐)) | ||
Theorem | grpnpncan0 12966 | Cancellation law for group subtraction (npncan2 8184 analog). (Contributed by AV, 24-Nov-2019.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) & โข 0 = (0gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ ๐) + (๐ โ ๐)) = 0 ) | ||
Theorem | grpnnncan2 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 โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ โ ๐) โ (๐ โ ๐)) = (๐ โ ๐)) | ||
Theorem | dfgrp3mlem 12968* | Lemma for dfgrp3m 12969. (Contributed by AV, 28-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Smgrp โง โ๐ค ๐ค โ ๐ต โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (โ๐ โ ๐ต (๐ + ๐ฅ) = ๐ฆ โง โ๐ โ ๐ต (๐ฅ + ๐) = ๐ฆ)) โ โ๐ข โ ๐ต โ๐ โ ๐ต ((๐ข + ๐) = ๐ โง โ๐ โ ๐ต (๐ + ๐) = ๐ข)) | ||
Theorem | dfgrp3m 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 โง โ๐ค ๐ค โ ๐ต โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต (โ๐ โ ๐ต (๐ + ๐ฅ) = ๐ฆ โง โ๐ โ ๐ต (๐ฅ + ๐) = ๐ฆ))) | ||
Theorem | dfgrp3me 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 โ (โ๐ค ๐ค โ ๐ต โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต ((๐ฅ + ๐ฆ) โ ๐ต โง โ๐ง โ ๐ต ((๐ฅ + ๐ฆ) + ๐ง) = (๐ฅ + (๐ฆ + ๐ง)) โง (โ๐ โ ๐ต (๐ + ๐ฅ) = ๐ฆ โง โ๐ โ ๐ต (๐ฅ + ๐) = ๐ฆ)))) | ||
Theorem | grplactfval 12971* | The left group action of element ๐ด of group ๐บ. (Contributed by Paul Chapman, 18-Mar-2008.) |
โข ๐น = (๐ โ ๐ โฆ (๐ โ ๐ โฆ (๐ + ๐))) & โข ๐ = (Baseโ๐บ) โ โข (๐ด โ ๐ โ (๐นโ๐ด) = (๐ โ ๐ โฆ (๐ด + ๐))) | ||
Theorem | grplactcnv 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โ๐ โง โก(๐นโ๐ด) = (๐นโ(๐ผโ๐ด)))) | ||
Theorem | grplactf1o 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โ๐) | ||
Theorem | grpsubpropdg 12974 | Weak property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 27-Mar-2015.) |
โข (๐ โ (Baseโ๐บ) = (Baseโ๐ป)) & โข (๐ โ (+gโ๐บ) = (+gโ๐ป)) & โข (๐ โ ๐บ โ ๐) & โข (๐ โ ๐ป โ ๐) โ โข (๐ โ (-gโ๐บ) = (-gโ๐ป)) | ||
Theorem | grpsubpropd2 12975* | Strong property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 4-Oct-2015.) |
โข (๐ โ ๐ต = (Baseโ๐บ)) & โข (๐ โ ๐ต = (Baseโ๐ป)) & โข (๐ โ ๐บ โ Grp) & โข ((๐ โง (๐ฅ โ ๐ต โง ๐ฆ โ ๐ต)) โ (๐ฅ(+gโ๐บ)๐ฆ) = (๐ฅ(+gโ๐ป)๐ฆ)) โ โข (๐ โ (-gโ๐บ) = (-gโ๐ป)) | ||
Theorem | grp1 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) | ||
Theorem | grp1inv 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 โพ {๐ผ})) | ||
Theorem | mhmlem 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.) |
โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐นโ(๐ฅ + ๐ฆ)) = ((๐นโ๐ฅ) โจฃ (๐นโ๐ฆ))) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ต โ ๐) โ โข (๐ โ (๐นโ(๐ด + ๐ต)) = ((๐นโ๐ด) โจฃ (๐นโ๐ต))) | ||
Theorem | mhmid 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โ๐ป)) | ||
Theorem | mhmmnd 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) | ||
Theorem | mhmfmhm 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 ๐ป)) | ||
Theorem | ghmgrp 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) | ||
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. | ||
Syntax | cmg 12983 | Extend class notation with a function mapping a group operation to the multiple/power operation for the magma/group. |
class .g | ||
Definition | df-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โ๐)โ(๐ โ-๐)))))) | ||
Theorem | mulgfvalg 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( + , (โ ร {๐ฅ}))โ-๐)))))) | ||
Theorem | mulgval 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 < ๐, (๐โ๐), (๐ผโ(๐โ-๐))))) | ||
Theorem | mulgfng 12987 | Functionality of the group multiple operation. (Contributed by Mario Carneiro, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข (๐บ โ ๐ โ ยท Fn (โค ร ๐ต)) | ||
Theorem | mulg0 12988 | Group multiple (exponentiation) operation at zero. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข ยท = (.gโ๐บ) โ โข (๐ โ ๐ต โ (0 ยท ๐) = 0 ) | ||
Theorem | mulgnn 12989 | Group multiple (exponentiation) operation at a positive integer. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ = seq1( + , (โ ร {๐})) โ โข ((๐ โ โ โง ๐ โ ๐ต) โ (๐ ยท ๐) = (๐โ๐)) | ||
Theorem | mulg1 12990 | Group multiple (exponentiation) operation at one. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข (๐ โ ๐ต โ (1 ยท ๐) = ๐) | ||
Theorem | mulgnnp1 12991 | Group multiple (exponentiation) operation at a successor. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐ โ โ โง ๐ โ ๐ต) โ ((๐ + 1) ยท ๐) = ((๐ ยท ๐) + ๐)) | ||
Theorem | mulg2 12992 | Group multiple (exponentiation) operation at two. (Contributed by Mario Carneiro, 15-Oct-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข (๐ โ ๐ต โ (2 ยท ๐) = (๐ + ๐)) | ||
Theorem | mulgnegnn 12993 | Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ผ = (invgโ๐บ) โ โข ((๐ โ โ โง ๐ โ ๐ต) โ (-๐ ยท ๐) = (๐ผโ(๐ ยท ๐))) | ||
Theorem | mulgnn0p1 12994 | 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 12995* | Closure of the group multiple (exponentiation) operation in a subsemigroup. (Contributed by Mario Carneiro, 10-Jan-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) & โข (๐ โ ๐บ โ ๐) & โข (๐ โ ๐ โ ๐ต) & โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ฅ + ๐ฆ) โ ๐) โ โข ((๐ โง ๐ โ โ โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐) | ||
Theorem | mulgnn0subcl 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 โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐) | ||
Theorem | mulgsubcl 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โ๐บ) & โข ((๐ โง ๐ฅ โ ๐) โ (๐ผโ๐ฅ) โ ๐) โ โข ((๐ โง ๐ โ โค โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐) | ||
Theorem | mulgnncl 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 โง ๐ โ โ โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) | ||
Theorem | mulgnn0cl 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 โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) | ||
Theorem | mulgcl 13000 | Closure of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |