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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | grppropstr 18701 | 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 18702 | 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 18703* | Deduce a group from its properties. In this version of isgrpd2 18704, 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 18704* | 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 2737, but we make an exception for theorems such as isgrpd2 18704, ismndd 18512, 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 18705* | Deduce a group from its properties. In this version of isgrpd 18706, 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 18706* | Deduce a group from its properties. Unlike isgrpd2 18704, 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 18707* | 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 18708 | A group is a semigroup. (Contributed by AV, 28-Aug-2021.) |
β’ (πΊ β Grp β πΊ β Smgrp) | ||
Theorem | dfgrp2 18709* | 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 18685, 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 18710* | 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 18711* | 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 18712 | 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 18713 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β π΅ β β ) | ||
Theorem | grplid 18714 | The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ π β π΅) β ( 0 + π) = π) | ||
Theorem | grprid 18715 | The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ π β π΅) β (π + 0 ) = π) | ||
Theorem | grpn0 18716 | A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ (πΊ β Grp β πΊ β β ) | ||
Theorem | hashfingrpnn 18717 | A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π΅ β Fin) β β’ (π β (β―βπ΅) β β) | ||
Theorem | grprcan 18718 | Right cancellation law for groups. (Contributed by NM, 24-Aug-2011.) (Proof shortened by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) = (π + π) β π = π)) | ||
Theorem | grpinveu 18719* | 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 18720 | 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 18721 | 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 18722* | Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 18706. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β + = (+gβπΊ)) & β’ (π β 0 β π΅) & β’ ((π β§ π₯ β π΅) β ( 0 + π₯) = π₯) & β’ (π β πΊ β Grp) β β’ (π β 0 = (0gβπΊ)) | ||
Theorem | grpinvfval 18723* | The inverse function of a group. For a shorter proof using ax-rep 5240, see grpinvfvalALT 18724. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) Remove dependency on ax-rep 5240. (Revised by Rohan Ridenour, 13-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (invgβπΊ) β β’ π = (π₯ β π΅ β¦ (β©π¦ β π΅ (π¦ + π₯) = 0 )) | ||
Theorem | grpinvfvalALT 18724* | Shorter proof of grpinvfval 18723 using ax-rep 5240. (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 18725* | 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 18726 | Functionality of the group inverse function. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π = (invgβπΊ) β β’ π Fn π΅ | ||
Theorem | grpinvfvi 18727 | The group inverse function is compatible with identity-function protection. (Contributed by Stefan O'Rear, 21-Mar-2015.) |
β’ π = (invgβπΊ) β β’ π = (invgβ( I βπΊ)) | ||
Theorem | grpsubfval 18728* | Group subtraction (division) operation. For a shorter proof using ax-rep 5240, see grpsubfvalALT 18729. (Contributed by NM, 31-Mar-2014.) (Revised by Stefan O'Rear, 27-Mar-2015.) Remove dependency on ax-rep 5240. (Revised by Rohan Ridenour, 17-Aug-2023.) (Proof shortened by AV, 19-Feb-2024.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ πΌ = (invgβπΊ) & β’ β = (-gβπΊ) β β’ β = (π₯ β π΅, π¦ β π΅ β¦ (π₯ + (πΌβπ¦))) | ||
Theorem | grpsubfvalALT 18729* | Shorter proof of grpsubfval 18728 using ax-rep 5240. (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 18730 | Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014.) (Revised by Mario Carneiro, 13-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ πΌ = (invgβπΊ) & β’ β = (-gβπΊ) β β’ ((π β π΅ β§ π β π΅) β (π β π) = (π + (πΌβπ))) | ||
Theorem | grpinvf 18731 | The group inversion operation is a function on the base set. (Contributed by Mario Carneiro, 4-May-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π = (invgβπΊ) β β’ (πΊ β Grp β π:π΅βΆπ΅) | ||
Theorem | grpinvcl 18732 | 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 18733 | 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 18734 | 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 18735 | 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 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 | isgrpinv 18737* | 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 18738* | 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 18739* | 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 18740* | 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 18741 | The inverse of the identity element of a group. (Contributed by NM, 24-Aug-2011.) |
β’ 0 = (0gβπΊ) & β’ π = (invgβπΊ) β β’ (πΊ β Grp β (πβ 0 ) = 0 ) | ||
Theorem | grplcan 18742 | Left cancellation law for groups. (Contributed by NM, 25-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) = (π + π) β π = π)) | ||
Theorem | grpasscan1 18743 | 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 18744 | 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 18745 | 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 18746 | 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 18747 | 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 18748 | The group inverse is its own inverse function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π = (invgβπΊ) β β’ (πΊ β Grp β β‘π = π) | ||
Theorem | grpinv11 18749 | The group inverse is one-to-one. (Contributed by NM, 22-Mar-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π = (invgβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πβπ) = (πβπ) β π = π)) | ||
Theorem | grpinvf1o 18750 | 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 18751 | 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 18752 | 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 18753 | Subtraction of an inverse. (Contributed by NM, 7-Apr-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ π = (invgβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π β (πβπ)) = (π + π)) | ||
Theorem | grplmulf1o 18754* | 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 18755* | 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 18756* | 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 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 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 18758 | 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 18759 | Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) β β’ (πΊ β Grp β β :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | grpsubcl 18760 | Closure of group subtraction. (Contributed by NM, 31-Mar-2014.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β (π β π) β π΅) | ||
Theorem | grpsubrcan 18761 | Right cancellation law for group subtraction. (Contributed by NM, 31-Mar-2014.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β π) = (π β π) β π = π)) | ||
Theorem | grpinvsub 18762 | Inverse of a group subtraction. (Contributed by NM, 9-Sep-2014.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ π = (invgβπΊ) β β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β (πβ(π β π)) = (π β π)) | ||
Theorem | grpinvval2 18763 | A df-neg 11321-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 18764 | Subtraction of a group element from itself. (Contributed by NM, 31-Mar-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ π β π΅) β (π β π) = 0 ) | ||
Theorem | grpsubid1 18765 | Subtraction of the identity from a group element. (Contributed by Mario Carneiro, 14-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ π β π΅) β (π β 0 ) = π) | ||
Theorem | grpsubeq0 18766 | If the difference between two group elements is zero, they are equal. (subeq0 11360 analog.) (Contributed by NM, 31-Mar-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β ((π β π) = 0 β π = π)) | ||
Theorem | grpsubadd0sub 18767 | 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 18768 | Relationship between group subtraction and addition. (Contributed by NM, 31-Mar-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β π) = π β (π + π) = π)) | ||
Theorem | grpsubsub 18769 | Double group subtraction. (Contributed by NM, 24-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β (π β π)) = (π + (π β π))) | ||
Theorem | grpaddsubass 18770 | Associative-type law for group subtraction and addition. (Contributed by NM, 16-Apr-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) β π) = (π + (π β π))) | ||
Theorem | grppncan 18771 | Cancellation law for subtraction (pncan 11340 analog). (Contributed by NM, 16-Apr-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β ((π + π) β π) = π) | ||
Theorem | grpnpcan 18772 | Cancellation law for subtraction (npcan 11343 analog). (Contributed by NM, 19-Apr-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β ((π β π) + π) = π) | ||
Theorem | grpsubsub4 18773 | Double group subtraction (subsub4 11367 analog). (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β π) β π) = (π β (π + π))) | ||
Theorem | grppnpcan2 18774 | Cancellation law for mixed addition and subtraction. (pnpcan2 11374 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) β (π + π)) = (π β π)) | ||
Theorem | grpnpncan 18775 | Cancellation law for group subtraction. (npncan 11355 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β π) + (π β π)) = (π β π)) | ||
Theorem | grpnpncan0 18776 | Cancellation law for group subtraction (npncan2 11361 analog). (Contributed by AV, 24-Nov-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅)) β ((π β π) + (π β π)) = 0 ) | ||
Theorem | grpnnncan2 18777 | Cancellation law for group subtraction. (nnncan2 11371 analog.) (Contributed by NM, 15-Feb-2008.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ β = (-gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β π) β (π β π)) = (π β π)) | ||
Theorem | dfgrp3lem 18778* | Lemma for dfgrp3 18779. (Contributed by AV, 28-Aug-2021.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Smgrp β§ π΅ β β β§ βπ₯ β π΅ βπ¦ β π΅ (βπ β π΅ (π + π₯) = π¦ β§ βπ β π΅ (π₯ + π) = π¦)) β βπ’ β π΅ βπ β π΅ ((π’ + π) = π β§ βπ β π΅ (π + π) = π’)) | ||
Theorem | dfgrp3 18779* | 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 18780* | 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 18781* | The left group action of element π΄ of group πΊ. (Contributed by Paul Chapman, 18-Mar-2008.) |
β’ πΉ = (π β π β¦ (π β π β¦ (π + π))) & β’ π = (BaseβπΊ) β β’ (π΄ β π β (πΉβπ΄) = (π β π β¦ (π΄ + π))) | ||
Theorem | grplactval 18782* | The value of the left group action of element π΄ of group πΊ at π΅. (Contributed by Paul Chapman, 18-Mar-2008.) |
β’ πΉ = (π β π β¦ (π β π β¦ (π + π))) & β’ π = (BaseβπΊ) β β’ ((π΄ β π β§ π΅ β π) β ((πΉβπ΄)βπ΅) = (π΄ + π΅)) | ||
Theorem | grplactcnv 18783* | 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 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βπΊ) β β’ ((πΊ β Grp β§ π΄ β π) β (πΉβπ΄):πβ1-1-ontoβπ) | ||
Theorem | grpsubpropd 18785 | Weak property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 27-Mar-2015.) |
β’ (π β (BaseβπΊ) = (Baseβπ»)) & β’ (π β (+gβπΊ) = (+gβπ»)) β β’ (π β (-gβπΊ) = (-gβπ»)) | ||
Theorem | grpsubpropd2 18786* | Strong property deduction for the group subtraction operation. (Contributed by Mario Carneiro, 4-Oct-2015.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β π΅ = (Baseβπ»)) & β’ (π β πΊ β Grp) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΊ)π¦) = (π₯(+gβπ»)π¦)) β β’ (π β (-gβπΊ) = (-gβπ»)) | ||
Theorem | grp1 18787 | 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 18788 | 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 18789* | Characterization of inverses in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π :πΌβΆGrp) & β’ (π β πΉ β π΅) & β’ 0 = (0g β π ) & β’ π = (π¦ β πΌ β¦ ((invgβ(π βπ¦))β(πΉβπ¦))) β β’ (π β (π β π΅ β§ (π + πΉ) = 0 )) | ||
Theorem | prdsgrpd 18790 | The product of a family of groups is a group. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆGrp) β β’ (π β π β Grp) | ||
Theorem | prdsinvgd 18791* | Negation in a product of groups. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆGrp) & β’ π΅ = (Baseβπ) & β’ π = (invgβπ) & β’ (π β π β π΅) β β’ (π β (πβπ) = (π₯ β πΌ β¦ ((invgβ(π βπ₯))β(πβπ₯)))) | ||
Theorem | pwsgrp 18792 | A structure power of a group is a group. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β Grp β§ πΌ β π) β π β Grp) | ||
Theorem | pwsinvg 18793 | Negation in a group power. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (invgβπ ) & β’ π = (invgβπ) β β’ ((π β Grp β§ πΌ β π β§ π β π΅) β (πβπ) = (π β π)) | ||
Theorem | pwssub 18794 | Subtraction in a group power. (Contributed by Mario Carneiro, 12-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) & β’ π = (-gβπ ) & β’ β = (-gβπ) β β’ (((π β Grp β§ πΌ β π) β§ (πΉ β π΅ β§ πΊ β π΅)) β (πΉ β πΊ) = (πΉ βf ππΊ)) | ||
Theorem | imasgrp2 18795* | 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 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βπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ (π β π β Grp) & β’ 0 = (0gβπ ) β β’ (π β (π β Grp β§ (πΉβ 0 ) = (0gβπ))) | ||
Theorem | imasgrpf1 18797 | 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 18798* | 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 18799 | The binary product of groups is a group. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ π = (π Γs π) β β’ ((π β Grp β§ π β Grp) β π β Grp) | ||
Theorem | mhmlem 18800* | Lemma for mhmmnd 18802 and ghmgrp 18804. (Contributed by Paul Chapman, 25-Apr-2008.) (Revised by Mario Carneiro, 12-May-2014.) (Revised by Thierry Arnoux, 25-Jan-2020.) |
β’ ((π β§ π₯ β π β§ π¦ β π) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) ⨣ (πΉβπ¦))) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (πΉβ(π΄ + π΅)) = ((πΉβπ΄) ⨣ (πΉβπ΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |