![]() |
Metamath
Proof Explorer Theorem List (p. 187 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gsumress 18601* | The group sum in a substructure is the same as the group sum in the original structure. The only requirement on the substructure is that it contain the identity element; neither πΊ nor π» need be groups. (Contributed by Mario Carneiro, 19-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π» = (πΊ βΎs π) & β’ (π β πΊ β π) & β’ (π β π΄ β π) & β’ (π β π β π΅) & β’ (π β πΉ:π΄βΆπ) & β’ (π β 0 β π) & β’ ((π β§ π₯ β π΅) β (( 0 + π₯) = π₯ β§ (π₯ + 0 ) = π₯)) β β’ (π β (πΊ Ξ£g πΉ) = (π» Ξ£g πΉ)) | ||
Theorem | gsumval1 18602* | Value of the group sum operation when every element being summed is an identity of πΊ. (Contributed by Mario Carneiro, 7-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ π = {π₯ β π΅ β£ βπ¦ β π΅ ((π₯ + π¦) = π¦ β§ (π¦ + π₯) = π¦)} & β’ (π β πΊ β π) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆπ) β β’ (π β (πΊ Ξ£g πΉ) = 0 ) | ||
Theorem | gsum0 18603 | Value of the empty group sum. (Contributed by Mario Carneiro, 7-Dec-2014.) |
β’ 0 = (0gβπΊ) β β’ (πΊ Ξ£g β ) = 0 | ||
Theorem | gsumval2a 18604* | Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β π) & β’ (π β π β (β€β₯βπ)) & β’ (π β πΉ:(π...π)βΆπ΅) & β’ π = {π₯ β π΅ β£ βπ¦ β π΅ ((π₯ + π¦) = π¦ β§ (π¦ + π₯) = π¦)} & β’ (π β Β¬ ran πΉ β π) β β’ (π β (πΊ Ξ£g πΉ) = (seqπ( + , πΉ)βπ)) | ||
Theorem | gsumval2 18605 | Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β π) & β’ (π β π β (β€β₯βπ)) & β’ (π β πΉ:(π...π)βΆπ΅) β β’ (π β (πΊ Ξ£g πΉ) = (seqπ( + , πΉ)βπ)) | ||
Theorem | gsumsplit1r 18606 | Splitting off the rightmost summand of a group sum. This corresponds to the (inductive) definition of a (finite) product in [Lang] p. 4, first formula. (Contributed by AV, 26-Dec-2023.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β π) & β’ (π β π β β€) & β’ (π β π β (β€β₯βπ)) & β’ (π β πΉ:(π...(π + 1))βΆπ΅) β β’ (π β (πΊ Ξ£g πΉ) = ((πΊ Ξ£g (πΉ βΎ (π...π))) + (πΉβ(π + 1)))) | ||
Theorem | gsumprval 18607 | Value of the group sum operation over a pair of sequential integers. (Contributed by AV, 14-Dec-2018.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β π) & β’ (π β π β β€) & β’ (π β π = (π + 1)) & β’ (π β πΉ:{π, π}βΆπ΅) β β’ (π β (πΊ Ξ£g πΉ) = ((πΉβπ) + (πΉβπ))) | ||
Theorem | gsumpr12val 18608 | Value of the group sum operation over the pair {1, 2}. (Contributed by AV, 14-Dec-2018.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β π) & β’ (π β πΉ:{1, 2}βΆπ΅) β β’ (π β (πΊ Ξ£g πΉ) = ((πΉβ1) + (πΉβ2))) | ||
A semigroup (Smgrp, see df-sgrp 18610) is a set together with an associative binary operation (see Wikipedia, Semigroup, 8-Jan-2020, https://en.wikipedia.org/wiki/Semigroup 18610). In other words, a semigroup is an associative magma. The notion of semigroup is a generalization of that of group where the existence of an identity or inverses is not required. | ||
Syntax | csgrp 18609 | Extend class notation with class of all semigroups. |
class Smgrp | ||
Definition | df-sgrp 18610* | A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 18561), whose operation is associative. Definition in section II.1 of [Bruck] p. 23, or of an "associative magma" in definition 5 of [BourbakiAlg1] p. 4 . (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
β’ Smgrp = {π β Mgm β£ [(Baseβπ) / π][(+gβπ) / π]βπ₯ β π βπ¦ β π βπ§ β π ((π₯ππ¦)ππ§) = (π₯π(π¦ππ§))} | ||
Theorem | issgrp 18611* | The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π β Smgrp β (π β Mgm β§ βπ₯ β π΅ βπ¦ β π΅ βπ§ β π΅ ((π₯ β¬ π¦) β¬ π§) = (π₯ β¬ (π¦ β¬ π§)))) | ||
Theorem | issgrpv 18612* | The predicate "is a semigroup" for a structure which is a set. (Contributed by AV, 1-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π β π β (π β Smgrp β βπ₯ β π΅ βπ¦ β π΅ ((π₯ β¬ π¦) β π΅ β§ βπ§ β π΅ ((π₯ β¬ π¦) β¬ π§) = (π₯ β¬ (π¦ β¬ π§))))) | ||
Theorem | issgrpn0 18613* | The predicate "is a semigroup" for a structure with a nonempty base set. (Contributed by AV, 1-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (π΄ β π΅ β (π β Smgrp β βπ₯ β π΅ βπ¦ β π΅ ((π₯ β¬ π¦) β π΅ β§ βπ§ β π΅ ((π₯ β¬ π¦) β¬ π§) = (π₯ β¬ (π¦ β¬ π§))))) | ||
Theorem | isnsgrp 18614 | A condition for a structure not to be a semigroup. (Contributed by AV, 30-Jan-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ ((π β π΅ β§ π β π΅ β§ π β π΅) β (((π β¬ π) β¬ π) β (π β¬ (π β¬ π)) β π β Smgrp)) | ||
Theorem | sgrpmgm 18615 | A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
β’ (π β Smgrp β π β Mgm) | ||
Theorem | sgrpass 18616 | A semigroup operation is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 30-Jan-2020.) |
β’ π΅ = (BaseβπΊ) & β’ β¬ = (+gβπΊ) β β’ ((πΊ β Smgrp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¬ π) β¬ π) = (π β¬ (π β¬ π))) | ||
Theorem | sgrpcl 18617 | Closure of the operation of a semigroup. (Contributed by AV, 15-Feb-2025.) |
β’ π΅ = (BaseβπΊ) & β’ β¬ = (+gβπΊ) β β’ ((πΊ β Smgrp β§ π β π΅ β§ π β π΅) β (π β¬ π) β π΅) | ||
Theorem | sgrp0 18618 | Any set with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021.) |
β’ ((π β π β§ (Baseβπ) = β ) β π β Smgrp) | ||
Theorem | sgrp0b 18619 | The structure with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021.) |
β’ {β¨(Baseβndx), β β©, β¨(+gβndx), πβ©} β Smgrp | ||
Theorem | sgrp1 18620 | The structure with one element and the only closed internal operation for a singleton is a semigroup. (Contributed by AV, 10-Feb-2020.) |
β’ π = {β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©} β β’ (πΌ β π β π β Smgrp) | ||
Theorem | issgrpd 18621* | Deduce a semigroup from its properties. (Contributed by AV, 13-Feb-2025.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β + = (+gβπΊ)) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β πΊ β π) β β’ (π β πΊ β Smgrp) | ||
Theorem | sgrppropd 18622* | If two structures are sets, have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a semigroup iff the other one is. (Contributed by AV, 15-Feb-2025.) |
β’ (π β πΎ β π) & β’ (π β πΏ β π) & β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) β β’ (π β (πΎ β Smgrp β πΏ β Smgrp)) | ||
Theorem | prdsplusgsgrpcl 18623 | Structure product pointwise sums are closed when the factors are semigroups. (Contributed by AV, 21-Feb-2025.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π :πΌβΆSmgrp) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (πΉ + πΊ) β π΅) | ||
Theorem | prdssgrpd 18624 | The product of a family of semigroups is a semigroup. (Contributed by AV, 21-Feb-2025.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆSmgrp) β β’ (π β π β Smgrp) | ||
According to Wikipedia ("Monoid", https://en.wikipedia.org/wiki/Monoid, 6-Feb-2020,) "In abstract algebra [...] a monoid is an algebraic structure with a single associative binary operation and an identity element. Monoids are semigroups with identity.". In the following, monoids are defined in the second way (as semigroups with identity), see df-mnd 18626, whereas many authors define magmas in the first way (as algebraic structure with a single associative binary operation and an identity element, i.e. without the need of a definition for/knowledge about semigroups), see ismnd 18628. See, for example, the definition in [Lang] p. 3: "A monoid is a set G, with a law of composition which is associative, and having a unit element". | ||
Syntax | cmnd 18625 | Extend class notation with class of all monoids. |
class Mnd | ||
Definition | df-mnd 18626* | A monoid is a semigroup, which has a two-sided neutral element. Definition 2 in [BourbakiAlg1] p. 12. In other words (according to the definition in [Lang] p. 3), a monoid is a set equipped with an everywhere defined internal operation (see mndcl 18633), whose operation is associative (see mndass 18634) and has a two-sided neutral element (see mndid 18635), see also ismnd 18628. (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.) |
β’ Mnd = {π β Smgrp β£ [(Baseβπ) / π][(+gβπ) / π]βπ β π βπ₯ β π ((πππ₯) = π₯ β§ (π₯ππ) = π₯)} | ||
Theorem | ismnddef 18627* | The predicate "is a monoid", corresponding 1-to-1 to the definition. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 1-Feb-2020.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (πΊ β Mnd β (πΊ β Smgrp β§ βπ β π΅ βπ β π΅ ((π + π) = π β§ (π + π) = π))) | ||
Theorem | ismnd 18628* | The predicate "is a monoid". This is the defining theorem of a monoid by showing that a set is a monoid if and only if it is a set equipped with a closed, everywhere defined internal operation (so, a magma, see mndcl 18633), whose operation is associative (so, a semigroup, see also mndass 18634) and has a two-sided neutral element (see mndid 18635). (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (πΊ β Mnd β (βπ β π΅ βπ β π΅ ((π + π) β π΅ β§ βπ β π΅ ((π + π) + π) = (π + (π + π))) β§ βπ β π΅ βπ β π΅ ((π + π) = π β§ (π + π) = π))) | ||
Theorem | isnmnd 18629* | A condition for a structure not to be a monoid: every element of the base set is not a left identity for at least one element of the base set. (Contributed by AV, 4-Feb-2020.) |
β’ π΅ = (Baseβπ) & β’ β¬ = (+gβπ) β β’ (βπ§ β π΅ βπ₯ β π΅ (π§ β¬ π₯) β π₯ β π β Mnd) | ||
Theorem | sgrpidmnd 18630* | A semigroup with an identity element which is not the empty set is a monoid. Of course there could be monoids with the empty set as identity element (see, for example, the monoid of the power set of a class under union, pwmnd 18818 and pwmndid 18817), but these cannot be proven to be monoids with this theorem. (Contributed by AV, 29-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Smgrp β§ βπ β π΅ (π β β β§ π = 0 )) β πΊ β Mnd) | ||
Theorem | mndsgrp 18631 | A monoid is a semigroup. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) (Proof shortened by AV, 6-Feb-2020.) |
β’ (πΊ β Mnd β πΊ β Smgrp) | ||
Theorem | mndmgm 18632 | A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) (Proof shortened by AV, 6-Feb-2020.) |
β’ (π β Mnd β π β Mgm) | ||
Theorem | mndcl 18633 | Closure of the operation of a monoid. (Contributed by NM, 14-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Proof shortened by AV, 8-Feb-2020.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Mnd β§ π β π΅ β§ π β π΅) β (π + π) β π΅) | ||
Theorem | mndass 18634 | A monoid operation is associative. (Contributed by NM, 14-Aug-2011.) (Proof shortened by AV, 8-Feb-2020.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Mnd β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) + π) = (π + (π + π))) | ||
Theorem | mndid 18635* | A monoid has a two-sided identity element. (Contributed by NM, 16-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (πΊ β Mnd β βπ’ β π΅ βπ₯ β π΅ ((π’ + π₯) = π₯ β§ (π₯ + π’) = π₯)) | ||
Theorem | mndideu 18636* | The two-sided identity element of a monoid is unique. Lemma 2.2.1(a) of [Herstein] p. 55. (Contributed by Mario Carneiro, 8-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (πΊ β Mnd β β!π’ β π΅ βπ₯ β π΅ ((π’ + π₯) = π₯ β§ (π₯ + π’) = π₯)) | ||
Theorem | mnd32g 18637 | Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β (π + π) = (π + π)) β β’ (π β ((π + π) + π) = ((π + π) + π)) | ||
Theorem | mnd12g 18638 | Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β (π + π) = (π + π)) β β’ (π β (π + (π + π)) = (π + (π + π))) | ||
Theorem | mnd4g 18639 | Commutative/associative law for commutative monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β (π + π) = (π + π)) β β’ (π β ((π + π) + (π + π)) = ((π + π) + (π + π))) | ||
Theorem | mndidcl 18640 | The identity element of a monoid belongs to the monoid. (Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro, 27-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) β β’ (πΊ β Mnd β 0 β π΅) | ||
Theorem | mndbn0 18641 | The base set of a monoid is not empty. Statement in [Lang] p. 3. (Contributed by AV, 29-Dec-2023.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Mnd β π΅ β β ) | ||
Theorem | hashfinmndnn 18642 | A finite monoid has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΅ β Fin) β β’ (π β (β―βπ΅) β β) | ||
Theorem | mndplusf 18643 | The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) (Proof shortened by AV, 3-Feb-2020.) |
β’ π΅ = (BaseβπΊ) & ⒠⨣ = (+πβπΊ) β β’ (πΊ β Mnd β ⨣ :(π΅ Γ π΅)βΆπ΅) | ||
Theorem | mndlrid 18644 | A monoid's identity element is a two-sided identity. (Contributed by NM, 18-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Mnd β§ π β π΅) β (( 0 + π) = π β§ (π + 0 ) = π)) | ||
Theorem | mndlid 18645 | The identity element of a monoid is a left identity. (Contributed by NM, 18-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Mnd β§ π β π΅) β ( 0 + π) = π) | ||
Theorem | mndrid 18646 | The identity element of a monoid is a right identity. (Contributed by NM, 18-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Mnd β§ π β π΅) β (π + 0 ) = π) | ||
Theorem | ismndd 18647* | Deduce a monoid from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β + = (+gβπΊ)) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β 0 β π΅) & β’ ((π β§ π₯ β π΅) β ( 0 + π₯) = π₯) & β’ ((π β§ π₯ β π΅) β (π₯ + 0 ) = π₯) β β’ (π β πΊ β Mnd) | ||
Theorem | mndpfo 18648 | The addition operation of a monoid as a function is an onto function. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 11-Oct-2013.) (Revised by AV, 23-Jan-2020.) |
β’ π΅ = (BaseβπΊ) & ⒠⨣ = (+πβπΊ) β β’ (πΊ β Mnd β ⨣ :(π΅ Γ π΅)βontoβπ΅) | ||
Theorem | mndfo 18649 | The addition operation of a monoid is an onto function (assuming it is a function). (Contributed by Mario Carneiro, 11-Oct-2013.) (Proof shortened by AV, 23-Jan-2020.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Mnd β§ + Fn (π΅ Γ π΅)) β + :(π΅ Γ π΅)βontoβπ΅) | ||
Theorem | mndpropd 18650* | If two structures have the same base set, and the values of their group (addition) operations are equal for all pairs of elements of the base set, one is a monoid iff the other one is. (Contributed by Mario Carneiro, 6-Jan-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) β β’ (π β (πΎ β Mnd β πΏ β Mnd)) | ||
Theorem | mndprop 18651 | If two structures have the same group components (properties), one is a monoid iff the other one is. (Contributed by Mario Carneiro, 11-Oct-2013.) |
β’ (BaseβπΎ) = (BaseβπΏ) & β’ (+gβπΎ) = (+gβπΏ) β β’ (πΎ β Mnd β πΏ β Mnd) | ||
Theorem | issubmnd 18652* | Characterize a submonoid by closure properties. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) & β’ π» = (πΊ βΎs π) β β’ ((πΊ β Mnd β§ π β π΅ β§ 0 β π) β (π» β Mnd β βπ₯ β π βπ¦ β π (π₯ + π¦) β π)) | ||
Theorem | ress0g 18653 | 0g is unaffected by restriction. This is a bit more generic than submnd0 18654. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Mnd β§ 0 β π΄ β§ π΄ β π΅) β 0 = (0gβπ)) | ||
Theorem | submnd0 18654 | The zero of a submonoid is the same as the zero in the parent monoid. (Note that we must add the condition that the zero of the parent monoid is actually contained in the submonoid, because it is possible to have "subsets that are monoids" which are not submonoids because they have a different identity element. See, for example, smndex1mnd 18791 and smndex1n0mnd 18793). (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π» = (πΊ βΎs π) β β’ (((πΊ β Mnd β§ π» β Mnd) β§ (π β π΅ β§ 0 β π)) β 0 = (0gβπ»)) | ||
Theorem | mndinvmod 18655* | Uniqueness of an inverse element in a monoid, if it exists. (Contributed by AV, 20-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π΅) β β’ (π β β*π€ β π΅ ((π€ + π΄) = 0 β§ (π΄ + π€) = 0 )) | ||
Theorem | prdsplusgcl 18656 | Structure product pointwise sums are closed when the factors are monoids. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π :πΌβΆMnd) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) β β’ (π β (πΉ + πΊ) β π΅) | ||
Theorem | prdsidlem 18657* | Characterization of identity in a structure product. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π :πΌβΆMnd) & β’ 0 = (0g β π ) β β’ (π β ( 0 β π΅ β§ βπ₯ β π΅ (( 0 + π₯) = π₯ β§ (π₯ + 0 ) = π₯))) | ||
Theorem | prdsmndd 18658 | The product of a family of monoids is a monoid. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆMnd) β β’ (π β π β Mnd) | ||
Theorem | prds0g 18659 | Zero in a product of monoids. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆMnd) β β’ (π β (0g β π ) = (0gβπ)) | ||
Theorem | pwsmnd 18660 | The structure power of a monoid is a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β Mnd β§ πΌ β π) β π β Mnd) | ||
Theorem | pws0g 18661 | Zero in a structure power of a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ 0 = (0gβπ ) β β’ ((π β Mnd β§ πΌ β π) β (πΌ Γ { 0 }) = (0gβπ)) | ||
Theorem | imasmnd2 18662* | The image structure of a monoid is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ + = (+gβπ ) & β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ (π β π β π) & β’ ((π β§ π₯ β π β§ π¦ β π) β (π₯ + π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (πΉβ((π₯ + π¦) + π§)) = (πΉβ(π₯ + (π¦ + π§)))) & β’ (π β 0 β π) & β’ ((π β§ π₯ β π) β (πΉβ( 0 + π₯)) = (πΉβπ₯)) & β’ ((π β§ π₯ β π) β (πΉβ(π₯ + 0 )) = (πΉβπ₯)) β β’ (π β (π β Mnd β§ (πΉβ 0 ) = (0gβπ))) | ||
Theorem | imasmnd 18663* | The image structure of a monoid is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ + = (+gβπ ) & β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ (π β π β Mnd) & β’ 0 = (0gβπ ) β β’ (π β (π β Mnd β§ (πΉβ 0 ) = (0gβπ))) | ||
Theorem | imasmndf1 18664 | The image of a monoid under an injection is a monoid. (Contributed by Mario Carneiro, 24-Feb-2015.) |
β’ π = (πΉ βs π ) & β’ π = (Baseβπ ) β β’ ((πΉ:πβ1-1βπ΅ β§ π β Mnd) β π β Mnd) | ||
Theorem | xpsmnd 18665 | The binary product of monoids is a monoid. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ π = (π Γs π) β β’ ((π β Mnd β§ π β Mnd) β π β Mnd) | ||
Theorem | xpsmnd0 18666 | The identity element of a binary product of monoids. (Contributed by AV, 25-Feb-2025.) |
β’ π = (π Γs π) β β’ ((π β Mnd β§ π β Mnd) β (0gβπ) = β¨(0gβπ ), (0gβπ)β©) | ||
Theorem | mnd1 18667 | The (smallest) structure representing a trivial monoid consists of one element. (Contributed by AV, 28-Apr-2019.) (Proof shortened by AV, 11-Feb-2020.) |
β’ π = {β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©} β β’ (πΌ β π β π β Mnd) | ||
Theorem | mnd1id 18668 | The singleton element of a trivial monoid is its identity element. (Contributed by AV, 23-Jan-2020.) |
β’ π = {β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©} β β’ (πΌ β π β (0gβπ) = πΌ) | ||
Syntax | cmhm 18669 | Hom-set generator class for monoids. |
class MndHom | ||
Syntax | csubmnd 18670 | Class function taking a monoid to its lattice of submonoids. |
class SubMnd | ||
Definition | df-mhm 18671* | A monoid homomorphism is a function on the base sets which preserves the binary operation and the identity. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ MndHom = (π β Mnd, π‘ β Mnd β¦ {π β ((Baseβπ‘) βm (Baseβπ )) β£ (βπ₯ β (Baseβπ )βπ¦ β (Baseβπ )(πβ(π₯(+gβπ )π¦)) = ((πβπ₯)(+gβπ‘)(πβπ¦)) β§ (πβ(0gβπ )) = (0gβπ‘))}) | ||
Definition | df-submnd 18672* | A submonoid is a subset of a monoid which contains the identity and is closed under the operation. Such subsets are themselves monoids with the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ SubMnd = (π β Mnd β¦ {π‘ β π« (Baseβπ ) β£ ((0gβπ ) β π‘ β§ βπ₯ β π‘ βπ¦ β π‘ (π₯(+gβπ )π¦) β π‘)}) | ||
Theorem | ismhm 18673* | Property of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (0gβπ) β β’ (πΉ β (π MndHom π) β ((π β Mnd β§ π β Mnd) β§ (πΉ:π΅βΆπΆ β§ βπ₯ β π΅ βπ¦ β π΅ (πΉβ(π₯ + π¦)) = ((πΉβπ₯) ⨣ (πΉβπ¦)) β§ (πΉβ 0 ) = π))) | ||
Theorem | ismhmd 18674* | Deduction version of ismhm 18673. (Contributed by SN, 27-Jul-2024.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (0gβπ) & β’ (π β π β Mnd) & β’ (π β π β Mnd) & β’ (π β πΉ:π΅βΆπΆ) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) ⨣ (πΉβπ¦))) & β’ (π β (πΉβ 0 ) = π) β β’ (π β πΉ β (π MndHom π)) | ||
Theorem | mhmrcl1 18675 | Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ (πΉ β (π MndHom π) β π β Mnd) | ||
Theorem | mhmrcl2 18676 | Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ (πΉ β (π MndHom π) β π β Mnd) | ||
Theorem | mhmf 18677 | A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π MndHom π) β πΉ:π΅βΆπΆ) | ||
Theorem | mhmpropd 18678* | Monoid homomorphism depends only on the monoidal attributes of structures. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 7-Nov-2015.) |
β’ (π β π΅ = (Baseβπ½)) & β’ (π β πΆ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β πΆ = (Baseβπ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ½)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπ)π¦)) β β’ (π β (π½ MndHom πΎ) = (πΏ MndHom π)) | ||
Theorem | mhmlin 18679 | A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ ((πΉ β (π MndHom π) β§ π β π΅ β§ π β π΅) β (πΉβ(π + π)) = ((πΉβπ) ⨣ (πΉβπ))) | ||
Theorem | mhm0 18680 | A monoid homomorphism preserves zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ 0 = (0gβπ) & β’ π = (0gβπ) β β’ (πΉ β (π MndHom π) β (πΉβ 0 ) = π) | ||
Theorem | idmhm 18681 | The identity homomorphism on a monoid. (Contributed by AV, 14-Feb-2020.) |
β’ π΅ = (Baseβπ) β β’ (π β Mnd β ( I βΎ π΅) β (π MndHom π)) | ||
Theorem | mhmf1o 18682 | A monoid homomorphism is bijective iff its converse is also a monoid homomorphism. (Contributed by AV, 22-Oct-2019.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π MndHom π) β (πΉ:π΅β1-1-ontoβπΆ β β‘πΉ β (π MndHom π ))) | ||
Theorem | submrcl 18683 | Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ (π β (SubMndβπ) β π β Mnd) | ||
Theorem | issubm 18684* | Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ + = (+gβπ) β β’ (π β Mnd β (π β (SubMndβπ) β (π β π΅ β§ 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π))) | ||
Theorem | issubm2 18685 | Submonoids are subsets that are also monoids with the same zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π» = (π βΎs π) β β’ (π β Mnd β (π β (SubMndβπ) β (π β π΅ β§ 0 β π β§ π» β Mnd))) | ||
Theorem | issubmndb 18686 | The submonoid predicate. Analogous to issubg 19006. (Contributed by AV, 1-Feb-2024.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) β β’ (π β (SubMndβπΊ) β ((πΊ β Mnd β§ (πΊ βΎs π) β Mnd) β§ (π β π΅ β§ 0 β π))) | ||
Theorem | issubmd 18687* | Deduction for proving a submonoid. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ 0 = (0gβπ) & β’ (π β π β Mnd) & β’ (π β π) & β’ ((π β§ ((π₯ β π΅ β§ π¦ β π΅) β§ (π β§ π))) β π) & β’ (π§ = 0 β (π β π)) & β’ (π§ = π₯ β (π β π)) & β’ (π§ = π¦ β (π β π)) & β’ (π§ = (π₯ + π¦) β (π β π)) β β’ (π β {π§ β π΅ β£ π} β (SubMndβπ)) | ||
Theorem | mndissubm 18688 | If the base set of a monoid is contained in the base set of another monoid, and the group operation of the monoid is the restriction of the group operation of the other monoid to its base set, and the identity element of the other monoid is contained in the base set of the monoid, then the (base set of the) monoid is a submonoid of the other monoid. Analogous to grpissubg 19026. (Contributed by AV, 17-Feb-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (Baseβπ») & β’ 0 = (0gβπΊ) β β’ ((πΊ β Mnd β§ π» β Mnd) β ((π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π))) β π β (SubMndβπΊ))) | ||
Theorem | resmndismnd 18689 | If the base set of a monoid is contained in the base set of another monoid, and the group operation of the monoid is the restriction of the group operation of the other monoid to its base set, and the identity element of the other monoid is contained in the base set of the monoid, then the other monoid restricted to the base set of the monoid is a monoid. Analogous to resgrpisgrp 19027. (Contributed by AV, 17-Feb-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (Baseβπ») & β’ 0 = (0gβπΊ) β β’ ((πΊ β Mnd β§ π» β Mnd) β ((π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π))) β (πΊ βΎs π) β Mnd)) | ||
Theorem | submss 18690 | Submonoids are subsets of the base set. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π΅ = (Baseβπ) β β’ (π β (SubMndβπ) β π β π΅) | ||
Theorem | submid 18691 | Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ π΅ = (Baseβπ) β β’ (π β Mnd β π΅ β (SubMndβπ)) | ||
Theorem | subm0cl 18692 | Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ 0 = (0gβπ) β β’ (π β (SubMndβπ) β 0 β π) | ||
Theorem | submcl 18693 | Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ + = (+gβπ) β β’ ((π β (SubMndβπ) β§ π β π β§ π β π) β (π + π) β π) | ||
Theorem | submmnd 18694 | Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π» = (π βΎs π) β β’ (π β (SubMndβπ) β π» β Mnd) | ||
Theorem | submbas 18695 | The base set of a submonoid. (Contributed by Stefan O'Rear, 15-Jun-2015.) |
β’ π» = (π βΎs π) β β’ (π β (SubMndβπ) β π = (Baseβπ»)) | ||
Theorem | subm0 18696 | Submonoids have the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π» = (π βΎs π) & β’ 0 = (0gβπ) β β’ (π β (SubMndβπ) β 0 = (0gβπ»)) | ||
Theorem | subsubm 18697 | A submonoid of a submonoid is a submonoid. (Contributed by Mario Carneiro, 21-Jun-2015.) |
β’ π» = (πΊ βΎs π) β β’ (π β (SubMndβπΊ) β (π΄ β (SubMndβπ») β (π΄ β (SubMndβπΊ) β§ π΄ β π))) | ||
Theorem | 0subm 18698 | The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024.) |
β’ 0 = (0gβπΊ) β β’ (πΊ β Mnd β { 0 } β (SubMndβπΊ)) | ||
Theorem | insubm 18699 | The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024.) |
β’ ((π΄ β (SubMndβπ) β§ π΅ β (SubMndβπ)) β (π΄ β© π΅) β (SubMndβπ)) | ||
Theorem | 0mhm 18700 | The constant zero linear function between two monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Mnd β§ π β Mnd) β (π΅ Γ { 0 }) β (π MndHom π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |