![]() |
Metamath
Proof Explorer Theorem List (p. 189 of 480) | < 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: | ![]() (1-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | symggrplem 18801* | Lemma for symggrp 19309 and efmndsgrp 18803. Conditions for an operation to be associative. Formerly part of proof for symggrp 19309. (Contributed by AV, 28-Jan-2024.) |
β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) & β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) = (π₯ β π¦)) β β’ ((π β π΅ β§ π β π΅ β§ π β π΅) β ((π + π) + π) = (π + (π + π))) | ||
Theorem | efmndmgm 18802 | The monoid of endofunctions on a class π΄ is a magma. (Contributed by AV, 28-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) β β’ πΊ β Mgm | ||
Theorem | efmndsgrp 18803 | The monoid of endofunctions on a class π΄ is a semigroup. (Contributed by AV, 28-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) β β’ πΊ β Smgrp | ||
Theorem | ielefmnd 18804 | The identity function restricted to a set π΄ is an element of the base set of the monoid of endofunctions on π΄. (Contributed by AV, 27-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) β β’ (π΄ β π β ( I βΎ π΄) β (BaseβπΊ)) | ||
Theorem | efmndid 18805 | The identity function restricted to a set π΄ is the identity element of the monoid of endofunctions on π΄. (Contributed by AV, 25-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) β β’ (π΄ β π β ( I βΎ π΄) = (0gβπΊ)) | ||
Theorem | efmndmnd 18806 | The monoid of endofunctions on a set π΄ is actually a monoid. (Contributed by AV, 31-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) β β’ (π΄ β π β πΊ β Mnd) | ||
Theorem | efmnd0nmnd 18807 | Even the monoid of endofunctions on the empty set is actually a monoid. (Contributed by AV, 31-Jan-2024.) |
β’ (EndoFMndββ ) β Mnd | ||
Theorem | efmndbas0 18808 | The base set of the monoid of endofunctions on the empty set is the singleton containing the empty set. (Contributed by AV, 27-Jan-2024.) (Proof shortened by AV, 31-Mar-2024.) |
β’ (Baseβ(EndoFMndββ )) = {β } | ||
Theorem | efmnd1hash 18809 | The monoid of endofunctions on a singleton has cardinality 1. (Contributed by AV, 27-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ} β β’ (πΌ β π β (β―βπ΅) = 1) | ||
Theorem | efmnd1bas 18810 | The monoid of endofunctions on a singleton consists of the identity only. (Contributed by AV, 31-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ} β β’ (πΌ β π β π΅ = {{β¨πΌ, πΌβ©}}) | ||
Theorem | efmnd2hash 18811 | The monoid of endofunctions on a (proper) pair has cardinality 4. (Contributed by AV, 18-Feb-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ, π½} β β’ ((πΌ β π β§ π½ β π β§ πΌ β π½) β (β―βπ΅) = 4) | ||
Theorem | submefmnd 18812* | If the base set of a monoid is contained in the base set of the monoid of endofunctions on a set π΄, contains the identity function and has the function composition as group operation, then its base set is a submonoid of the monoid of endofunctions on set π΄. Analogous to pgrpsubgsymg 19318. (Contributed by AV, 17-Feb-2024.) |
β’ π = (EndoFMndβπ΄) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (Baseβπ) β β’ (π΄ β π β (((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π))) β πΉ β (SubMndβπ))) | ||
Theorem | sursubmefmnd 18813* | The set of surjective endofunctions on a set π΄ is a submonoid of the monoid of endofunctions on π΄. (Contributed by AV, 25-Feb-2024.) |
β’ π = (EndoFMndβπ΄) β β’ (π΄ β π β {β β£ β:π΄βontoβπ΄} β (SubMndβπ)) | ||
Theorem | injsubmefmnd 18814* | The set of injective endofunctions on a set π΄ is a submonoid of the monoid of endofunctions on π΄. (Contributed by AV, 25-Feb-2024.) |
β’ π = (EndoFMndβπ΄) β β’ (π΄ β π β {β β£ β:π΄β1-1βπ΄} β (SubMndβπ)) | ||
Theorem | idressubmefmnd 18815 | The singleton containing only the identity function restricted to a set is a submonoid of the monoid of endofunctions on this set. (Contributed by AV, 17-Feb-2024.) |
β’ πΊ = (EndoFMndβπ΄) β β’ (π΄ β π β {( I βΎ π΄)} β (SubMndβπΊ)) | ||
Theorem | idresefmnd 18816 | The structure with the singleton containing only the identity function restricted to a set π΄ as base set and the function composition as group operation, constructed by (structure) restricting the monoid of endofunctions on π΄ to that singleton, is a monoid whose base set is a subset of the base set of the monoid of endofunctions on π΄. (Contributed by AV, 17-Feb-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ πΈ = (πΊ βΎs {( I βΎ π΄)}) β β’ (π΄ β π β (πΈ β Mnd β§ (BaseβπΈ) β (BaseβπΊ))) | ||
Theorem | smndex1ibas 18817 | The modulo function πΌ is an endofunction on β0. (Contributed by AV, 12-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) β β’ πΌ β (Baseβπ) | ||
Theorem | smndex1iidm 18818* | The modulo function πΌ is idempotent. (Contributed by AV, 12-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) β β’ (πΌ β πΌ) = πΌ | ||
Theorem | smndex1gbas 18819* | The constant functions (πΊβπΎ) are endofunctions on β0. (Contributed by AV, 12-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) β β’ (πΎ β (0..^π) β (πΊβπΎ) β (Baseβπ)) | ||
Theorem | smndex1gid 18820* | The composition of a constant function (πΊβπΎ) with another endofunction on β0 results in (πΊβπΎ) itself. (Contributed by AV, 14-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) β β’ ((πΉ β (Baseβπ) β§ πΎ β (0..^π)) β ((πΊβπΎ) β πΉ) = (πΊβπΎ)) | ||
Theorem | smndex1igid 18821* | The composition of the modulo function πΌ and a constant function (πΊβπΎ) results in (πΊβπΎ) itself. (Contributed by AV, 14-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) β β’ (πΎ β (0..^π) β (πΌ β (πΊβπΎ)) = (πΊβπΎ)) | ||
Theorem | smndex1basss 18822* | The modulo function πΌ and the constant functions (πΊβπΎ) are endofunctions on β0. (Contributed by AV, 12-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) & β’ π΅ = ({πΌ} βͺ βͺ π β (0..^π){(πΊβπ)}) β β’ π΅ β (Baseβπ) | ||
Theorem | smndex1bas 18823* | The base set of the monoid of endofunctions on β0 restricted to the modulo function πΌ and the constant functions (πΊβπΎ). (Contributed by AV, 12-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) & β’ π΅ = ({πΌ} βͺ βͺ π β (0..^π){(πΊβπ)}) & β’ π = (π βΎs π΅) β β’ (Baseβπ) = π΅ | ||
Theorem | smndex1mgm 18824* | The monoid of endofunctions on β0 restricted to the modulo function πΌ and the constant functions (πΊβπΎ) is a magma. (Contributed by AV, 14-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) & β’ π΅ = ({πΌ} βͺ βͺ π β (0..^π){(πΊβπ)}) & β’ π = (π βΎs π΅) β β’ π β Mgm | ||
Theorem | smndex1sgrp 18825* | The monoid of endofunctions on β0 restricted to the modulo function πΌ and the constant functions (πΊβπΎ) is a semigroup. (Contributed by AV, 14-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) & β’ π΅ = ({πΌ} βͺ βͺ π β (0..^π){(πΊβπ)}) & β’ π = (π βΎs π΅) β β’ π β Smgrp | ||
Theorem | smndex1mndlem 18826* | Lemma for smndex1mnd 18827 and smndex1id 18828. (Contributed by AV, 16-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) & β’ π΅ = ({πΌ} βͺ βͺ π β (0..^π){(πΊβπ)}) & β’ π = (π βΎs π΅) β β’ (π β π΅ β ((πΌ β π) = π β§ (π β πΌ) = π)) | ||
Theorem | smndex1mnd 18827* | The monoid of endofunctions on β0 restricted to the modulo function πΌ and the constant functions (πΊβπΎ) is a monoid. (Contributed by AV, 16-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) & β’ π΅ = ({πΌ} βͺ βͺ π β (0..^π){(πΊβπ)}) & β’ π = (π βΎs π΅) β β’ π β Mnd | ||
Theorem | smndex1id 18828* | The modulo function πΌ is the identity of the monoid of endofunctions on β0 restricted to the modulo function πΌ and the constant functions (πΊβπΎ). (Contributed by AV, 16-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) & β’ π΅ = ({πΌ} βͺ βͺ π β (0..^π){(πΊβπ)}) & β’ π = (π βΎs π΅) β β’ πΌ = (0gβπ) | ||
Theorem | smndex1n0mnd 18829* | The identity of the monoid π of endofunctions on set β0 is not contained in the base set of the constructed monoid π. (Contributed by AV, 17-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) & β’ π΅ = ({πΌ} βͺ βͺ π β (0..^π){(πΊβπ)}) & β’ π = (π βΎs π΅) β β’ (0gβπ) β π΅ | ||
Theorem | nsmndex1 18830* | The base set π΅ of the constructed monoid π is not a submonoid of the monoid π of endofunctions on set β0, although π β Mnd and π β Mnd and π΅ β (Baseβπ) hold. (Contributed by AV, 17-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) & β’ π΅ = ({πΌ} βͺ βͺ π β (0..^π){(πΊβπ)}) & β’ π = (π βΎs π΅) β β’ π΅ β (SubMndβπ) | ||
Theorem | smndex2dbas 18831 | The doubling function π· is an endofunction on β0. (Contributed by AV, 18-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (π₯ β β0 β¦ (2 Β· π₯)) β β’ π· β π΅ | ||
Theorem | smndex2dnrinv 18832 | The doubling function π· has no right inverse in the monoid of endofunctions on β0. (Contributed by AV, 18-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (π₯ β β0 β¦ (2 Β· π₯)) β β’ βπ β π΅ (π· β π) β 0 | ||
Theorem | smndex2hbas 18833 | The halving functions π» are endofunctions on β0. (Contributed by AV, 18-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (π₯ β β0 β¦ (2 Β· π₯)) & β’ π β β0 & β’ π» = (π₯ β β0 β¦ if(2 β₯ π₯, (π₯ / 2), π)) β β’ π» β π΅ | ||
Theorem | smndex2dlinvh 18834* | The halving functions π» are left inverses of the doubling function π·. (Contributed by AV, 18-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (π₯ β β0 β¦ (2 Β· π₯)) & β’ π β β0 & β’ π» = (π₯ β β0 β¦ if(2 β₯ π₯, (π₯ / 2), π)) β β’ (π» β π·) = 0 | ||
Theorem | mgm2nsgrplem1 18835* | Lemma 1 for mgm2nsgrp 18839: π is a magma, even if π΄ = π΅ (π is the trivial magma in this case, see mgmb1mgm1 18580). (Contributed by AV, 27-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if((π₯ = π΄ β§ π¦ = π΄), π΅, π΄)) β β’ ((π΄ β π β§ π΅ β π) β π β Mgm) | ||
Theorem | mgm2nsgrplem2 18836* | Lemma 2 for mgm2nsgrp 18839. (Contributed by AV, 27-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if((π₯ = π΄ β§ π¦ = π΄), π΅, π΄)) & β’ β¬ = (+gβπ) β β’ ((π΄ β π β§ π΅ β π) β ((π΄ β¬ π΄) β¬ π΅) = π΄) | ||
Theorem | mgm2nsgrplem3 18837* | Lemma 3 for mgm2nsgrp 18839. (Contributed by AV, 28-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if((π₯ = π΄ β§ π¦ = π΄), π΅, π΄)) & β’ β¬ = (+gβπ) β β’ ((π΄ β π β§ π΅ β π) β (π΄ β¬ (π΄ β¬ π΅)) = π΅) | ||
Theorem | mgm2nsgrplem4 18838* | Lemma 4 for mgm2nsgrp 18839: M is not a semigroup. (Contributed by AV, 28-Jan-2020.) (Proof shortened by AV, 31-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if((π₯ = π΄ β§ π¦ = π΄), π΅, π΄)) β β’ ((β―βπ) = 2 β π β Smgrp) | ||
Theorem | mgm2nsgrp 18839* | A small magma (with two elements) which is not a semigroup. (Contributed by AV, 28-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if((π₯ = π΄ β§ π¦ = π΄), π΅, π΄)) β β’ ((β―βπ) = 2 β (π β Mgm β§ π β Smgrp)) | ||
Theorem | sgrp2nmndlem1 18840* | Lemma 1 for sgrp2nmnd 18847: π is a magma, even if π΄ = π΅ (π is the trivial magma in this case, see mgmb1mgm1 18580). (Contributed by AV, 29-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if(π₯ = π΄, π΄, π΅)) β β’ ((π΄ β π β§ π΅ β π) β π β Mgm) | ||
Theorem | sgrp2nmndlem2 18841* | Lemma 2 for sgrp2nmnd 18847. (Contributed by AV, 29-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if(π₯ = π΄, π΄, π΅)) & β’ β¬ = (+gβπ) β β’ ((π΄ β π β§ πΆ β π) β (π΄ β¬ πΆ) = π΄) | ||
Theorem | sgrp2nmndlem3 18842* | Lemma 3 for sgrp2nmnd 18847. (Contributed by AV, 29-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if(π₯ = π΄, π΄, π΅)) & β’ β¬ = (+gβπ) β β’ ((πΆ β π β§ π΅ β π β§ π΄ β π΅) β (π΅ β¬ πΆ) = π΅) | ||
Theorem | sgrp2rid2 18843* | A small semigroup (with two elements) with two right identities which are different if π΄ β π΅. (Contributed by AV, 10-Feb-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if(π₯ = π΄, π΄, π΅)) & β’ β¬ = (+gβπ) β β’ ((π΄ β π β§ π΅ β π) β βπ₯ β π βπ¦ β π (π¦ β¬ π₯) = π¦) | ||
Theorem | sgrp2rid2ex 18844* | A small semigroup (with two elements) with two right identities which are different. (Contributed by AV, 10-Feb-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if(π₯ = π΄, π΄, π΅)) & β’ β¬ = (+gβπ) β β’ ((β―βπ) = 2 β βπ₯ β π βπ§ β π βπ¦ β π (π₯ β π§ β§ (π¦ β¬ π₯) = π¦ β§ (π¦ β¬ π§) = π¦)) | ||
Theorem | sgrp2nmndlem4 18845* | Lemma 4 for sgrp2nmnd 18847: M is a semigroup. (Contributed by AV, 29-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if(π₯ = π΄, π΄, π΅)) β β’ ((β―βπ) = 2 β π β Smgrp) | ||
Theorem | sgrp2nmndlem5 18846* | Lemma 5 for sgrp2nmnd 18847: M is not a monoid. (Contributed by AV, 29-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if(π₯ = π΄, π΄, π΅)) β β’ ((β―βπ) = 2 β π β Mnd) | ||
Theorem | sgrp2nmnd 18847* | A small semigroup (with two elements) which is not a monoid. (Contributed by AV, 26-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if(π₯ = π΄, π΄, π΅)) β β’ ((β―βπ) = 2 β (π β Smgrp β§ π β Mnd)) | ||
Theorem | mgmnsgrpex 18848 | There is a magma which is not a semigroup. (Contributed by AV, 29-Jan-2020.) |
β’ βπ β Mgm π β Smgrp | ||
Theorem | sgrpnmndex 18849 | There is a semigroup which is not a monoid. (Contributed by AV, 29-Jan-2020.) |
β’ βπ β Smgrp π β Mnd | ||
Theorem | sgrpssmgm 18850 | The class of all semigroups is a proper subclass of the class of all magmas. (Contributed by AV, 29-Jan-2020.) |
β’ Smgrp β Mgm | ||
Theorem | mndsssgrp 18851 | The class of all monoids is a proper subclass of the class of all semigroups. (Contributed by AV, 29-Jan-2020.) |
β’ Mnd β Smgrp | ||
Theorem | pwmndgplus 18852* | The operation of the monoid of the power set of a class π΄ under union. (Contributed by AV, 27-Feb-2024.) |
β’ (Baseβπ) = π« π΄ & β’ (+gβπ) = (π₯ β π« π΄, π¦ β π« π΄ β¦ (π₯ βͺ π¦)) β β’ ((π β π« π΄ β§ π β π« π΄) β (π(+gβπ)π) = (π βͺ π)) | ||
Theorem | pwmndid 18853* | The identity of the monoid of the power set of a class π΄ under union is the empty set. (Contributed by AV, 27-Feb-2024.) |
β’ (Baseβπ) = π« π΄ & β’ (+gβπ) = (π₯ β π« π΄, π¦ β π« π΄ β¦ (π₯ βͺ π¦)) β β’ (0gβπ) = β | ||
Theorem | pwmnd 18854* | The power set of a class π΄ is a monoid under union. (Contributed by AV, 27-Feb-2024.) |
β’ (Baseβπ) = π« π΄ & β’ (+gβπ) = (π₯ β π« π΄, π¦ β π« π΄ β¦ (π₯ βͺ π¦)) β β’ π β Mnd | ||
Syntax | cgrp 18855 | Extend class notation with class of all groups. |
class Grp | ||
Syntax | cminusg 18856 | Extend class notation with inverse of group element. |
class invg | ||
Syntax | csg 18857 | Extend class notation with group subtraction (or division) operation. |
class -g | ||
Definition | df-grp 18858* | Define class of all groups. A group is a monoid (df-mnd 18660) whose internal operation is such that every element admits a left inverse (which can be proven to be a two-sided inverse). Thus, a group πΊ is an algebraic structure formed from a base set of elements (notated (BaseβπΊ) per df-base 17149) and an internal group operation (notated (+gβπΊ) per df-plusg 17214). The operation combines any two elements of the group base set and must satisfy the 4 group axioms: closure (the result of the group operation must always be a member of the base set, see grpcl 18863), associativity (so ((π+gπ)+gπ) = (π+g(π+gπ)) for any a, b, c, see grpass 18864), identity (there must be an element π = (0gβπΊ) such that π+gπ = π+gπ = π for any a), and inverse (for each element a in the base set, there must be an element π = invgπ in the base set such that π+gπ = π+gπ = π). It can be proven that the identity element is unique (grpideu 18866). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 19692). Subgroups can often be formed from groups, see df-subg 19039. An example of an (Abelian) group is the set of complex numbers β over the group operation + (addition), as proven in cnaddablx 19777; an Abelian group is a group as proven in ablgrp 19694. Other structures include groups, including unital rings (df-ring 20129) and fields (df-field 20503). (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ Grp = {π β Mnd β£ βπ β (Baseβπ)βπ β (Baseβπ)(π(+gβπ)π) = (0gβπ)} | ||
Definition | df-minusg 18859* | Define inverse of group element. (Contributed by NM, 24-Aug-2011.) |
β’ invg = (π β V β¦ (π₯ β (Baseβπ) β¦ (β©π€ β (Baseβπ)(π€(+gβπ)π₯) = (0gβπ)))) | ||
Definition | df-sbg 18860* | Define group subtraction (also called division for multiplicative groups). (Contributed by NM, 31-Mar-2014.) |
β’ -g = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯(+gβπ)((invgβπ)βπ¦)))) | ||
Theorem | isgrp 18861* | The predicate "is a group". (This theorem demonstrates the use of symbols as variable names, first proposed by FL in 2010.) (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ (πΊ β Grp β (πΊ β Mnd β§ βπ β π΅ βπ β π΅ (π + π) = 0 )) | ||
Theorem | grpmnd 18862 | A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
β’ (πΊ β Grp β πΊ β Mnd) | ||
Theorem | grpcl 18863 | Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β (π + π) β π΅) | ||
Theorem | grpass 18864 | A group operation is associative. (Contributed by NM, 14-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) + π) = (π + (π + π))) | ||
Theorem | grpinvex 18865* | Every member of a group has a left inverse. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ π β π΅) β βπ¦ β π΅ (π¦ + π) = 0 ) | ||
Theorem | grpideu 18866* | The two-sided identity element of a group is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by NM, 16-Aug-2011.) (Revised by Mario Carneiro, 8-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ (πΊ β Grp β β!π’ β π΅ βπ₯ β π΅ ((π’ + π₯) = π₯ β§ (π₯ + π’) = π₯)) | ||
Theorem | grpassd 18867 | A group operation is associative. (Contributed by SN, 29-Jan-2025.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π + π) + π) = (π + (π + π))) | ||
Theorem | grpmndd 18868 | A group is a monoid. (Contributed by SN, 1-Jun-2024.) |
β’ (π β πΊ β Grp) β β’ (π β πΊ β Mnd) | ||
Theorem | grpcld 18869 | Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π + π) β π΅) | ||
Theorem | grpplusf 18870 | The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π΅ = (BaseβπΊ) & β’ πΉ = (+πβπΊ) β β’ (πΊ β Grp β πΉ:(π΅ Γ π΅)βΆπ΅) | ||
Theorem | grpplusfo 18871 | The group addition operation is a function onto the base set/set of group elements. (Contributed by NM, 30-Oct-2006.) (Revised by AV, 30-Aug-2021.) |
β’ π΅ = (BaseβπΊ) & β’ πΉ = (+πβπΊ) β β’ (πΊ β Grp β πΉ:(π΅ Γ π΅)βontoβπ΅) | ||
Theorem | resgrpplusfrn 18872 | The underlying set of a group operation which is a restriction of a structure. (Contributed by Paul Chapman, 25-Mar-2008.) (Revised by AV, 30-Aug-2021.) |
β’ π΅ = (BaseβπΊ) & β’ π» = (πΊ βΎs π) & β’ πΉ = (+πβπ») β β’ ((π» β Grp β§ π β π΅) β π = ran πΉ) | ||
Theorem | grppropd 18873* | If two structures have the same group components (properties), one is a group iff the other one is. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 2-Oct-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) β β’ (π β (πΎ β Grp β πΏ β Grp)) | ||
Theorem | grpprop 18874 | 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 18875 | 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 18876 | 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 20132, 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 18877* | Deduce a group from its properties. In this version of isgrpd2 18878, 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 18878* | 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 2730, but we make an exception for theorems such as isgrpd2 18878, ismndd 18681, and islmodd 20620 since theorems using them often rewrite the structure components. (Contributed by NM, 10-Aug-2013.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β + = (+gβπΊ)) & β’ (π β 0 = (0gβπΊ)) & β’ (π β πΊ β Mnd) & β’ ((π β§ π₯ β π΅) β π β π΅) & β’ ((π β§ π₯ β π΅) β (π + π₯) = 0 ) β β’ (π β πΊ β Grp) | ||
Theorem | isgrpde 18879* | Deduce a group from its properties. In this version of isgrpd 18880, 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 18880* | Deduce a group from its properties. Unlike isgrpd2 18878, 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 18881* | 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 18882 | A group is a semigroup. (Contributed by AV, 28-Aug-2021.) |
β’ (πΊ β Grp β πΊ β Smgrp) | ||
Theorem | dfgrp2 18883* | 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 18858, 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 18884* | 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 18885* | 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 18886 | 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 18887 | The base set of a group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β π΅ β β ) | ||
Theorem | grplid 18888 | The identity element of a group is a left identity. (Contributed by NM, 18-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ π β π΅) β ( 0 + π) = π) | ||
Theorem | grprid 18889 | The identity element of a group is a right identity. (Contributed by NM, 18-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ π β π΅) β (π + 0 ) = π) | ||
Theorem | grplidd 18890 | The identity element of a group is a left identity. Deduction associated with grplid 18888. (Contributed by SN, 29-Jan-2025.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β π΅) β β’ (π β ( 0 + π) = π) | ||
Theorem | grpridd 18891 | The identity element of a group is a right identity. Deduction associated with grprid 18889. (Contributed by SN, 29-Jan-2025.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β π΅) β β’ (π β (π + 0 ) = π) | ||
Theorem | grpn0 18892 | A group is not empty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007.) (Revised by Mario Carneiro, 2-Dec-2014.) |
β’ (πΊ β Grp β πΊ β β ) | ||
Theorem | hashfingrpnn 18893 | A finite group has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π΅ β Fin) β β’ (π β (β―βπ΅) β β) | ||
Theorem | grprcan 18894 | Right cancellation law for groups. (Contributed by NM, 24-Aug-2011.) (Proof shortened by Mario Carneiro, 6-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) = (π + π) β π = π)) | ||
Theorem | grpinveu 18895* | 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 18896 | 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 18897 | 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 18898* | Deduce the identity element of a group from its properties. Useful in conjunction with isgrpd 18880. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β + = (+gβπΊ)) & β’ (π β 0 β π΅) & β’ ((π β§ π₯ β π΅) β ( 0 + π₯) = π₯) & β’ (π β πΊ β Grp) β β’ (π β 0 = (0gβπΊ)) | ||
Theorem | grpinvfval 18899* | The inverse function of a group. For a shorter proof using ax-rep 5284, see grpinvfvalALT 18900. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 7-Aug-2013.) Remove dependency on ax-rep 5284. (Revised by Rohan Ridenour, 13-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (invgβπΊ) β β’ π = (π₯ β π΅ β¦ (β©π¦ β π΅ (π¦ + π₯) = 0 )) | ||
Theorem | grpinvfvalALT 18900* | Shorter proof of grpinvfval 18899 using ax-rep 5284. (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 )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |