Home | Metamath
Proof Explorer Theorem List (p. 188 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | grpprop 18701 | If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by NM, 11-Oct-2013.) |
β’ (BaseβπΎ) = (BaseβπΏ) & β’ (+gβπΎ) = (+gβπΏ) β β’ (πΎ β Grp β πΏ β Grp) | ||
Theorem | grppropstr 18702 | Generalize a specific 2-element group πΏ to show that any set πΎ with the same (relevant) properties is also a group. (Contributed by NM, 28-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ (BaseβπΎ) = π΅ & β’ (+gβπΎ) = + & β’ πΏ = {β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©} β β’ (πΎ β Grp β πΏ β Grp) | ||
Theorem | grpss 18703 | Show that a structure extending a constructed group (e.g., a ring) is also a group. This allows to prove that a constructed potential ring π is a group before we know that it is also a ring. (Theorem ringgrp 19893, on the other hand, requires that we know in advance that π is a ring.) (Contributed by NM, 11-Oct-2013.) |
β’ πΊ = {β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©} & β’ π β V & β’ πΊ β π & β’ Fun π β β’ (πΊ β Grp β π β Grp) | ||
Theorem | isgrpd2e 18704* | Deduce a group from its properties. In this version of isgrpd2 18705, we don't assume there is an expression for the inverse of π₯. (Contributed by NM, 10-Aug-2013.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β + = (+gβπΊ)) & β’ (π β 0 = (0gβπΊ)) & β’ (π β πΊ β Mnd) & β’ ((π β§ π₯ β π΅) β βπ¦ β π΅ (π¦ + π₯) = 0 ) β β’ (π β πΊ β Grp) | ||
Theorem | isgrpd2 18705* | Deduce a group from its properties. π (negative) is normally dependent on π₯ i.e. read it as π(π₯). Note: normally we don't use a π antecedent on hypotheses that name structure components, since they can be eliminated with eqid 2738, but we make an exception for theorems such as isgrpd2 18705, ismndd 18513, and islmodd 20251 since theorems using them often rewrite the structure components. (Contributed by NM, 10-Aug-2013.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β + = (+gβπΊ)) & β’ (π β 0 = (0gβπΊ)) & β’ (π β πΊ β Mnd) & β’ ((π β§ π₯ β π΅) β π β π΅) & β’ ((π β§ π₯ β π΅) β (π + π₯) = 0 ) β β’ (π β πΊ β Grp) | ||
Theorem | isgrpde 18706* | Deduce a group from its properties. In this version of isgrpd 18707, we don't assume there is an expression for the inverse of π₯. (Contributed by NM, 6-Jan-2015.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β + = (+gβπΊ)) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β 0 β π΅) & β’ ((π β§ π₯ β π΅) β ( 0 + π₯) = π₯) & β’ ((π β§ π₯ β π΅) β βπ¦ β π΅ (π¦ + π₯) = 0 ) β β’ (π β πΊ β Grp) | ||
Theorem | isgrpd 18707* | Deduce a group from its properties. Unlike isgrpd2 18705, this one goes straight from the base properties rather than going through Mnd. π (negative) is normally dependent on π₯ i.e. read it as π(π₯). (Contributed by NM, 6-Jun-2013.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β + = (+gβπΊ)) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β 0 β π΅) & β’ ((π β§ π₯ β π΅) β ( 0 + π₯) = π₯) & β’ ((π β§ π₯ β π΅) β π β π΅) & β’ ((π β§ π₯ β π΅) β (π + π₯) = 0 ) β β’ (π β πΊ β Grp) | ||
Theorem | isgrpi 18708* | Properties that determine a group. π (negative) is normally dependent on π₯ i.e. read it as π(π₯). (Contributed by NM, 3-Sep-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) & β’ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ 0 β π΅ & β’ (π₯ β π΅ β ( 0 + π₯) = π₯) & β’ (π₯ β π΅ β π β π΅) & β’ (π₯ β π΅ β (π + π₯) = 0 ) β β’ πΊ β Grp | ||
Theorem | grpsgrp 18709 | A group is a semigroup. (Contributed by AV, 28-Aug-2021.) |
β’ (πΊ β Grp β πΊ β Smgrp) | ||
Theorem | dfgrp2 18710* | 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 18686, 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 18711* | Alternate definition of a group as a set with a closed, associative operation, a left identity and a left inverse for each element. Alternate definition in [Lang] p. 7. (Contributed by NM, 10-Oct-2006.) (Revised by AV, 28-Aug-2021.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (πΊ β Grp β (βπ₯ β π΅ βπ¦ β π΅ ((π₯ + π¦) β π΅ β§ βπ§ β π΅ ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) β§ βπ β π΅ βπ₯ β π΅ ((π + π₯) = π₯ β§ βπ β π΅ (π + π₯) = π))) | ||
Theorem | isgrpix 18712* | Properties that determine a group. Read π as π(π₯). Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011.) |
β’ π΅ β V & β’ + β V & β’ πΊ = {β¨1, π΅β©, β¨2, + β©} & β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) & β’ ((π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ 0 β π΅ & β’ (π₯ β π΅ β ( 0 + π₯) = π₯) & β’ (π₯ β π΅ β π β π΅) & β’ (π₯ β π΅ β (π + π₯) = 0 ) β β’ πΊ β Grp | ||
Theorem | grpidcl 18713 | 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 18714 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β π΅ β β ) | ||
Theorem | grplid 18715 | The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ π β π΅) β ( 0 + π) = π) | ||
Theorem | grprid 18716 | The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ π β π΅) β (π + 0 ) = π) | ||
Theorem | grpn0 18717 | A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ (πΊ β Grp β πΊ β β ) | ||
Theorem | hashfingrpnn 18718 | A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π΅ β Fin) β β’ (π β (β―βπ΅) β β) | ||
Theorem | grprcan 18719 | Right cancellation law for groups. (Contributed by NM, 24-Aug-2011.) (Proof shortened by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) = (π + π) β π = π)) | ||
Theorem | grpinveu 18720* | 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 18721 | 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 18722 | 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 18723* | Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 18707. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β + = (+gβπΊ)) & β’ (π β 0 β π΅) & β’ ((π β§ π₯ β π΅) β ( 0 + π₯) = π₯) & β’ (π β πΊ β Grp) β β’ (π β 0 = (0gβπΊ)) | ||
Theorem | grpinvfval 18724* | The inverse function of a group. For a shorter proof using ax-rep 5241, see grpinvfvalALT 18725. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) Remove dependency on ax-rep 5241. (Revised by Rohan Ridenour, 13-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (invgβπΊ) β β’ π = (π₯ β π΅ β¦ (β©π¦ β π΅ (π¦ + π₯) = 0 )) | ||
Theorem | grpinvfvalALT 18725* | Shorter proof of grpinvfval 18724 using ax-rep 5241. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (invgβπΊ) β β’ π = (π₯ β π΅ β¦ (β©π¦ β π΅ (π¦ + π₯) = 0 )) | ||
Theorem | grpinvval 18726* | The inverse of a group element. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (invgβπΊ) β β’ (π β π΅ β (πβπ) = (β©π¦ β π΅ (π¦ + π) = 0 )) | ||
Theorem | grpinvfn 18727 | Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π = (invgβπΊ) β β’ π Fn π΅ | ||
Theorem | grpinvfvi 18728 | The group inverse function is compatible with identity-function protection. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
β’ π = (invgβπΊ) β β’ π = (invgβ( I βπΊ)) | ||
Theorem | grpsubfval 18729* | Group subtraction (division) operation. For a shorter proof using ax-rep 5241, see grpsubfvalALT 18730. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) Remove dependency on ax-rep 5241. (Revised by Rohan Ridenour, 17-Aug-2023.) (Proof shortened by AV, 19-Feb-2024.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ πΌ = (invgβπΊ) & β’ β = (-gβπΊ) β β’ β = (π₯ β π΅, π¦ β π΅ β¦ (π₯ + (πΌβπ¦))) | ||
Theorem | grpsubfvalALT 18730* | Shorter proof of grpsubfval 18729 using ax-rep 5241. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) (Proof shortened by AV, 19-Feb-2024.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ πΌ = (invgβπΊ) & β’ β = (-gβπΊ) β β’ β = (π₯ β π΅, π¦ β π΅ β¦ (π₯ + (πΌβπ¦))) | ||
Theorem | grpsubval 18731 | Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ πΌ = (invgβπΊ) & β’ β = (-gβπΊ) β β’ ((π β π΅ β§ π β π΅) β (π β π) = (π + (πΌβπ))) | ||
Theorem | grpinvf 18732 | The group inversion operation is a function on the base set. (Contributed by Mario Carneiro, 4-May-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π = (invgβπΊ) β β’ (πΊ β Grp β π:π΅βΆπ΅) | ||
Theorem | grpinvcl 18733 | 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 18734 | 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 18735 | 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 18736 | 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 18737 | 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 18738* | 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 18739* | 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 18740* | 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 18741* | 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 18742 | The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011.) |
β’ 0 = (0gβπΊ) & β’ π = (invgβπΊ) β β’ (πΊ β Grp β (πβ 0 ) = 0 ) | ||
Theorem | grplcan 18743 | Left cancellation law for groups. (Contributed by NM, 25-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) = (π + π) β π = π)) | ||
Theorem | grpasscan1 18744 | 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 18745 | 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 18746 | 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 18747 | 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 18748 | 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 18749 | The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π = (invgβπΊ) β β’ (πΊ β Grp β β‘π = π) | ||
Theorem | grpinv11 18750 | The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π = (invgβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πβπ) = (πβπ) β π = π)) | ||
Theorem | grpinvf1o 18751 | 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 18752 | 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 18753 | 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 18754 | Subtraction of an inverse. (Contributed by NM, 7-Apr-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ π = (invgβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β (πβπ)) = (π + π)) | ||
Theorem | grplmulf1o 18755* | Left multiplication by a group element is a bijection on any group. (Contributed by Mario Carneiro, 17-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ πΉ = (π₯ β π΅ β¦ (π + π₯)) β β’ ((πΊ β Grp β§ π β π΅) β πΉ:π΅β1-1-ontoβπ΅) | ||
Theorem | grpinvpropd 18756* | 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 18757* | 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 18758* | 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 18759 | 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 18760 | Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) β β’ (πΊ β Grp β β :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | grpsubcl 18761 | Closure of group subtraction. (Contributed by NM, 31-Mar-2014.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β (π β π) β π΅) | ||
Theorem | grpsubrcan 18762 | Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β π) = (π β π) β π = π)) | ||
Theorem | grpinvsub 18763 | Inverse of a group subtraction. (Contributed by NM, 9-Sep-2014.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ π = (invgβπΊ) β β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β (πβ(π β π)) = (π β π)) | ||
Theorem | grpinvval2 18764 | A df-neg 11322-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 18765 | Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ π β π΅) β (π β π) = 0 ) | ||
Theorem | grpsubid1 18766 | Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ π β π΅) β (π β 0 ) = π) | ||
Theorem | grpsubeq0 18767 | If the difference between two group elements is zero, they are equal. (subeq0 11361 analog.) (Contributed by NM, 31-Mar-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β ((π β π) = 0 β π = π)) | ||
Theorem | grpsubadd0sub 18768 | 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 18769 | Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β π) = π β (π + π) = π)) | ||
Theorem | grpsubsub 18770 | Double group subtraction. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β (π β π)) = (π + (π β π))) | ||
Theorem | grpaddsubass 18771 | Associative-type law for group subtraction and addition. (Contributed by NM, 16-Apr-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) β π) = (π + (π β π))) | ||
Theorem | grppncan 18772 | Cancellation law for subtraction (pncan 11341 analog). (Contributed by NM, 16-Apr-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β ((π + π) β π) = π) | ||
Theorem | grpnpcan 18773 | Cancellation law for subtraction (npcan 11344 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β ((π β π) + π) = π) | ||
Theorem | grpsubsub4 18774 | Double group subtraction (subsub4 11368 analog). (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β π) β π) = (π β (π + π))) | ||
Theorem | grppnpcan2 18775 | Cancellation law for mixed addition and subtraction. (pnpcan2 11375 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) β (π + π)) = (π β π)) | ||
Theorem | grpnpncan 18776 | Cancellation law for group subtraction. (npncan 11356 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β π) + (π β π)) = (π β π)) | ||
Theorem | grpnpncan0 18777 | Cancellation law for group subtraction (npncan2 11362 analog). (Contributed by AV, 24-Nov-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅)) β ((π β π) + (π β π)) = 0 ) | ||
Theorem | grpnnncan2 18778 | Cancellation law for group subtraction. (nnncan2 11372 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β π) β (π β π)) = (π β π)) | ||
Theorem | dfgrp3lem 18779* | Lemma for dfgrp3 18780. (Contributed by AV, 28-Aug-2021.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Smgrp β§ π΅ β β β§ βπ₯ β π΅ βπ¦ β π΅ (βπ β π΅ (π + π₯) = π¦ β§ βπ β π΅ (π₯ + π) = π¦)) β βπ’ β π΅ βπ β π΅ ((π’ + π) = π β§ βπ β π΅ (π + π) = π’)) | ||
Theorem | dfgrp3 18780* | Alternate definition of a group as semigroup (with at least one element) which is also a quasigroup, i.e. a magma in which solutions π₯ and π¦ of the equations (π + π₯) = π and (π₯ + π) = π exist. Theorem 3.2 of [Bruck] p. 28. (Contributed by AV, 28-Aug-2021.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (πΊ β Grp β (πΊ β Smgrp β§ π΅ β β β§ βπ₯ β π΅ βπ¦ β π΅ (βπ β π΅ (π + π₯) = π¦ β§ βπ β π΅ (π₯ + π) = π¦))) | ||
Theorem | dfgrp3e 18781* | 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 18782* | The left group action of element π΄ of group πΊ. (Contributed by Paul Chapman, 18-Mar-2008.) |
β’ πΉ = (π β π β¦ (π β π β¦ (π + π))) & β’ π = (BaseβπΊ) β β’ (π΄ β π β (πΉβπ΄) = (π β π β¦ (π΄ + π))) | ||
Theorem | grplactval 18783* | The value of the left group action of element π΄ of group πΊ at π΅. (Contributed by Paul Chapman, 18-Mar-2008.) |
β’ πΉ = (π β π β¦ (π β π β¦ (π + π))) & β’ π = (BaseβπΊ) β β’ ((π΄ β π β§ π΅ β π) β ((πΉβπ΄)βπ΅) = (π΄ + π΅)) | ||
Theorem | grplactcnv 18784* | 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 18785* | The left group action of element π΄ of group πΊ maps the underlying set π of πΊ one-to-one onto itself. (Contributed by Paul Chapman, 18-Mar-2008.) (Proof shortened by Mario Carneiro, 14-Aug-2015.) |
β’ πΉ = (π β π β¦ (π β π β¦ (π + π))) & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Grp β§ π΄ β π) β (πΉβπ΄):πβ1-1-ontoβπ) | ||
Theorem | grpsubpropd 18786 | Weak property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 27-Mar-2015.) |
β’ (π β (BaseβπΊ) = (Baseβπ»)) & β’ (π β (+gβπΊ) = (+gβπ»)) β β’ (π β (-gβπΊ) = (-gβπ»)) | ||
Theorem | grpsubpropd2 18787* | Strong property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β π΅ = (Baseβπ»)) & β’ (π β πΊ β Grp) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΊ)π¦) = (π₯(+gβπ»)π¦)) β β’ (π β (-gβπΊ) = (-gβπ»)) | ||
Theorem | grp1 18788 | 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 18789 | The inverse function of the trivial group. (Contributed by FL, 21-Jun-2010.) (Revised by AV, 26-Aug-2021.) |
β’ π = {β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©} β β’ (πΌ β π β (invgβπ) = ( I βΎ {πΌ})) | ||
Theorem | prdsinvlem 18790* | Characterization of inverses in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π :πΌβΆGrp) & β’ (π β πΉ β π΅) & β’ 0 = (0g β π ) & β’ π = (π¦ β πΌ β¦ ((invgβ(π βπ¦))β(πΉβπ¦))) β β’ (π β (π β π΅ β§ (π + πΉ) = 0 )) | ||
Theorem | prdsgrpd 18791 | The product of a family of groups is a group. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆGrp) β β’ (π β π β Grp) | ||
Theorem | prdsinvgd 18792* | Negation in a product of groups. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆGrp) & β’ π΅ = (Baseβπ) & β’ π = (invgβπ) & β’ (π β π β π΅) β β’ (π β (πβπ) = (π₯ β πΌ β¦ ((invgβ(π βπ₯))β(πβπ₯)))) | ||
Theorem | pwsgrp 18793 | A structure power of a group is a group. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β Grp β§ πΌ β π) β π β Grp) | ||
Theorem | pwsinvg 18794 | Negation in a group power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (invgβπ ) & β’ π = (invgβπ) β β’ ((π β Grp β§ πΌ β π β§ π β π΅) β (πβπ) = (π β π)) | ||
Theorem | pwssub 18795 | Subtraction in a group power. (Contributed by Mario Carneiro, 12-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (-gβπ ) & β’ β = (-gβπ) β β’ (((π β Grp β§ πΌ β π) β§ (πΉ β π΅ β§ πΊ β π΅)) β (πΉ β πΊ) = (πΉ βf ππΊ)) | ||
Theorem | imasgrp2 18796* | The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β + = (+gβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ (π β π β π) & β’ ((π β§ π₯ β π β§ π¦ β π) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (πΉβ((π₯ + π¦) + π§)) = (πΉβ(π₯ + (π¦ + π§)))) & β’ (π β 0 β π) & β’ ((π β§ π₯ β π) β (πΉβ( 0 + π₯)) = (πΉβπ₯)) & β’ ((π β§ π₯ β π) β π β π) & β’ ((π β§ π₯ β π) β (πΉβ(π + π₯)) = (πΉβ 0 )) β β’ (π β (π β Grp β§ (πΉβ 0 ) = (0gβπ))) | ||
Theorem | imasgrp 18797* | The image structure of a group is a group. (Contributed by Mario Carneiro, 24-Feb-2015.) (Revised by Mario Carneiro, 5-Sep-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β + = (+gβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ (π β π β Grp) & β’ 0 = (0gβπ ) β β’ (π β (π β Grp β§ (πΉβ 0 ) = (0gβπ))) | ||
Theorem | imasgrpf1 18798 | The image of a group under an injection is a group. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ π = (πΉ βs π ) & β’ π = (Baseβπ ) β β’ ((πΉ:πβ1-1βπ΅ β§ π β Grp) β π β Grp) | ||
Theorem | qusgrp2 18799* | Prove that a quotient structure is a group. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) |
β’ (π β π = (π /s βΌ )) & β’ (π β π = (Baseβπ )) & β’ (π β + = (+gβπ )) & β’ (π β βΌ Er π) & β’ (π β π β π) & β’ (π β ((π βΌ π β§ π βΌ π) β (π + π) βΌ (π + π))) & β’ ((π β§ π₯ β π β§ π¦ β π) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π₯ + π¦) + π§) βΌ (π₯ + (π¦ + π§))) & β’ (π β 0 β π) & β’ ((π β§ π₯ β π) β ( 0 + π₯) βΌ π₯) & β’ ((π β§ π₯ β π) β π β π) & β’ ((π β§ π₯ β π) β (π + π₯) βΌ 0 ) β β’ (π β (π β Grp β§ [ 0 ] βΌ = (0gβπ))) | ||
Theorem | xpsgrp 18800 | The binary product of groups is a group. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ π = (π Γs π) β β’ ((π β Grp β§ π β Grp) β π β Grp) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |