Home | Metamath
Proof Explorer Theorem List (p. 186 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 | mndid 18501* | A monoid has a two-sided identity element. (Contributed by NM, 16-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (πΊ β Mnd β βπ’ β π΅ βπ₯ β π΅ ((π’ + π₯) = π₯ β§ (π₯ + π’) = π₯)) | ||
Theorem | mndideu 18502* | 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 18503 | Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β (π + π) = (π + π)) β β’ (π β ((π + π) + π) = ((π + π) + π)) | ||
Theorem | mnd12g 18504 | Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β (π + π) = (π + π)) β β’ (π β (π + (π + π)) = (π + (π + π))) | ||
Theorem | mnd4g 18505 | Commutative/associative law for commutative monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β (π + π) = (π + π)) β β’ (π β ((π + π) + (π + π)) = ((π + π) + (π + π))) | ||
Theorem | mndidcl 18506 | 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 18507 | The base set of a monoid is not empty. Statement in [Lang] p. 3. (Contributed by AV, 29-Dec-2023.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Mnd β π΅ β β ) | ||
Theorem | hashfinmndnn 18508 | A finite monoid has positive integer size. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π΅ β Fin) β β’ (π β (β―βπ΅) β β) | ||
Theorem | mndplusf 18509 | 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 18510 | 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 18511 | The identity element of a monoid is a left identity. (Contributed by NM, 18-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Mnd β§ π β π΅) β ( 0 + π) = π) | ||
Theorem | mndrid 18512 | The identity element of a monoid is a right identity. (Contributed by NM, 18-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Mnd β§ π β π΅) β (π + 0 ) = π) | ||
Theorem | ismndd 18513* | Deduce a monoid from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.) |
β’ (π β π΅ = (BaseβπΊ)) & β’ (π β + = (+gβπΊ)) & β’ ((π β§ π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅ β§ π§ β π΅)) β ((π₯ + π¦) + π§) = (π₯ + (π¦ + π§))) & β’ (π β 0 β π΅) & β’ ((π β§ π₯ β π΅) β ( 0 + π₯) = π₯) & β’ ((π β§ π₯ β π΅) β (π₯ + 0 ) = π₯) β β’ (π β πΊ β Mnd) | ||
Theorem | mndpfo 18514 | 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 18515 | 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 18516* | 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 18517 | 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 18518* | Characterize a submonoid by closure properties. (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) & β’ π» = (πΊ βΎs π) β β’ ((πΊ β Mnd β§ π β π΅ β§ 0 β π) β (π» β Mnd β βπ₯ β π βπ¦ β π (π₯ + π¦) β π)) | ||
Theorem | ress0g 18519 | 0g is unaffected by restriction. This is a bit more generic than submnd0 18520. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
β’ π = (π βΎs π΄) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Mnd β§ 0 β π΄ β§ π΄ β π΅) β 0 = (0gβπ)) | ||
Theorem | submnd0 18520 | 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 18655 and smndex1n0mnd 18657). (Contributed by Mario Carneiro, 10-Jan-2015.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π» = (πΊ βΎs π) β β’ (((πΊ β Mnd β§ π» β Mnd) β§ (π β π΅ β§ 0 β π)) β 0 = (0gβπ»)) | ||
Theorem | mndinvmod 18521* | 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 18522 | 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 18523* | 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 18524 | The product of a family of monoids is a monoid. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆMnd) β β’ (π β π β Mnd) | ||
Theorem | prds0g 18525 | Zero in a product of monoids. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆMnd) β β’ (π β (0g β π ) = (0gβπ)) | ||
Theorem | pwsmnd 18526 | The structure power of a monoid is a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) β β’ ((π β Mnd β§ πΌ β π) β π β Mnd) | ||
Theorem | pws0g 18527 | Zero in a structure power of a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.) |
β’ π = (π βs πΌ) & β’ 0 = (0gβπ ) β β’ ((π β Mnd β§ πΌ β π) β (πΌ Γ { 0 }) = (0gβπ)) | ||
Theorem | imasmnd2 18528* | 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 18529* | 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 18530 | 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 18531 | The binary product of monoids is a monoid. (Contributed by Mario Carneiro, 20-Aug-2015.) |
β’ π = (π Γs π) β β’ ((π β Mnd β§ π β Mnd) β π β Mnd) | ||
Theorem | mnd1 18532 | 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 18533 | The singleton element of a trivial monoid is its identity element. (Contributed by AV, 23-Jan-2020.) |
β’ π = {β¨(Baseβndx), {πΌ}β©, β¨(+gβndx), {β¨β¨πΌ, πΌβ©, πΌβ©}β©} β β’ (πΌ β π β (0gβπ) = πΌ) | ||
Syntax | cmhm 18534 | Hom-set generator class for monoids. |
class MndHom | ||
Syntax | csubmnd 18535 | Class function taking a monoid to its lattice of submonoids. |
class SubMnd | ||
Definition | df-mhm 18536* | 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 18537* | 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 18538* | 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 18539* | Deduction version of ismhm 18538. (Contributed by SN, 27-Jul-2024.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) & β’ 0 = (0gβπ) & β’ π = (0gβπ) & β’ (π β π β Mnd) & β’ (π β π β Mnd) & β’ (π β πΉ:π΅βΆπΆ) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) ⨣ (πΉβπ¦))) & β’ (π β (πΉβ 0 ) = π) β β’ (π β πΉ β (π MndHom π)) | ||
Theorem | mhmrcl1 18540 | Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ (πΉ β (π MndHom π) β π β Mnd) | ||
Theorem | mhmrcl2 18541 | Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ (πΉ β (π MndHom π) β π β Mnd) | ||
Theorem | mhmf 18542 | A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π MndHom π) β πΉ:π΅βΆπΆ) | ||
Theorem | mhmpropd 18543* | 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 18544 | A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ ((πΉ β (π MndHom π) β§ π β π΅ β§ π β π΅) β (πΉβ(π + π)) = ((πΉβπ) ⨣ (πΉβπ))) | ||
Theorem | mhm0 18545 | A monoid homomorphism preserves zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ 0 = (0gβπ) & β’ π = (0gβπ) β β’ (πΉ β (π MndHom π) β (πΉβ 0 ) = π) | ||
Theorem | idmhm 18546 | The identity homomorphism on a monoid. (Contributed by AV, 14-Feb-2020.) |
β’ π΅ = (Baseβπ) β β’ (π β Mnd β ( I βΎ π΅) β (π MndHom π)) | ||
Theorem | mhmf1o 18547 | 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 18548 | Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ (π β (SubMndβπ) β π β Mnd) | ||
Theorem | issubm 18549* | Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ + = (+gβπ) β β’ (π β Mnd β (π β (SubMndβπ) β (π β π΅ β§ 0 β π β§ βπ₯ β π βπ¦ β π (π₯ + π¦) β π))) | ||
Theorem | issubm2 18550 | 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 18551 | The submonoid predicate. Analogous to issubg 18861. (Contributed by AV, 1-Feb-2024.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) β β’ (π β (SubMndβπΊ) β ((πΊ β Mnd β§ (πΊ βΎs π) β Mnd) β§ (π β π΅ β§ 0 β π))) | ||
Theorem | issubmd 18552* | 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 18553 | 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 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 18881. (Contributed by AV, 17-Feb-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (Baseβπ») & β’ 0 = (0gβπΊ) β β’ ((πΊ β Mnd β§ π» β Mnd) β ((π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π))) β π β (SubMndβπΊ))) | ||
Theorem | resmndismnd 18554 | 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 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 18882. (Contributed by AV, 17-Feb-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (Baseβπ») & β’ 0 = (0gβπΊ) β β’ ((πΊ β Mnd β§ π» β Mnd) β ((π β π΅ β§ 0 β π β§ (+gβπ») = ((+gβπΊ) βΎ (π Γ π))) β (πΊ βΎs π) β Mnd)) | ||
Theorem | submss 18555 | Submonoids are subsets of the base set. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π΅ = (Baseβπ) β β’ (π β (SubMndβπ) β π β π΅) | ||
Theorem | submid 18556 | Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ π΅ = (Baseβπ) β β’ (π β Mnd β π΅ β (SubMndβπ)) | ||
Theorem | subm0cl 18557 | Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ 0 = (0gβπ) β β’ (π β (SubMndβπ) β 0 β π) | ||
Theorem | submcl 18558 | Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ + = (+gβπ) β β’ ((π β (SubMndβπ) β§ π β π β§ π β π) β (π + π) β π) | ||
Theorem | submmnd 18559 | Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π» = (π βΎs π) β β’ (π β (SubMndβπ) β π» β Mnd) | ||
Theorem | submbas 18560 | The base set of a submonoid. (Contributed by Stefan O'Rear, 15-Jun-2015.) |
β’ π» = (π βΎs π) β β’ (π β (SubMndβπ) β π = (Baseβπ»)) | ||
Theorem | subm0 18561 | Submonoids have the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π» = (π βΎs π) & β’ 0 = (0gβπ) β β’ (π β (SubMndβπ) β 0 = (0gβπ»)) | ||
Theorem | subsubm 18562 | A submonoid of a submonoid is a submonoid. (Contributed by Mario Carneiro, 21-Jun-2015.) |
β’ π» = (πΊ βΎs π) β β’ (π β (SubMndβπΊ) β (π΄ β (SubMndβπ») β (π΄ β (SubMndβπΊ) β§ π΄ β π))) | ||
Theorem | 0subm 18563 | The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024.) |
β’ 0 = (0gβπΊ) β β’ (πΊ β Mnd β { 0 } β (SubMndβπΊ)) | ||
Theorem | insubm 18564 | The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024.) |
β’ ((π΄ β (SubMndβπ) β§ π΅ β (SubMndβπ)) β (π΄ β© π΅) β (SubMndβπ)) | ||
Theorem | 0mhm 18565 | The constant zero linear function between two monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Mnd β§ π β Mnd) β (π΅ Γ { 0 }) β (π MndHom π)) | ||
Theorem | resmhm 18566 | Restriction of a monoid homomorphism to a submonoid is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β (πΉ βΎ π) β (π MndHom π)) | ||
Theorem | resmhm2 18567 | One direction of resmhm2b 18568. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β πΉ β (π MndHom π)) | ||
Theorem | resmhm2b 18568 | Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ π = (π βΎs π) β β’ ((π β (SubMndβπ) β§ ran πΉ β π) β (πΉ β (π MndHom π) β πΉ β (π MndHom π))) | ||
Theorem | mhmco 18569 | The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β (πΉ β πΊ) β (π MndHom π)) | ||
Theorem | mhmima 18570 | The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ ((πΉ β (π MndHom π) β§ π β (SubMndβπ)) β (πΉ β π) β (SubMndβπ)) | ||
Theorem | mhmeql 18571 | The equalizer of two monoid homomorphisms is a submonoid. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ ((πΉ β (π MndHom π) β§ πΊ β (π MndHom π)) β dom (πΉ β© πΊ) β (SubMndβπ)) | ||
Theorem | submacs 18572 | Submonoids are an algebraic closure system. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Mnd β (SubMndβπΊ) β (ACSβπ΅)) | ||
Theorem | mndind 18573* | Induction in a monoid. In this theorem, π(π₯) is the "generic" proposition to be be proved (the first four hypotheses tell its values at y, y+z, 0, A respectively). The two induction hypotheses mndind.i1 and mndind.i2 tell that it is true at 0, that if it is true at y then it is true at y+z (provided z is in πΊ). The hypothesis mndind.k tells that πΊ is generating. (Contributed by SO, 14-Jul-2018.) |
β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ + π§) β (π β π)) & β’ (π₯ = 0 β (π β π)) & β’ (π₯ = π΄ β (π β π)) & β’ 0 = (0gβπ) & β’ + = (+gβπ) & β’ π΅ = (Baseβπ) & β’ (π β π β Mnd) & β’ (π β πΊ β π΅) & β’ (π β π΅ = ((mrClsβ(SubMndβπ))βπΊ)) & β’ (π β π) & β’ (((π β§ π¦ β π΅ β§ π§ β πΊ) β§ π) β π) & β’ (π β π΄ β π΅) β β’ (π β π) | ||
Theorem | prdspjmhm 18574* | A projection from a product of monoids to one of the factors is a monoid homomorphism. (Contributed by Mario Carneiro, 6-May-2015.) |
β’ π = (πXsπ ) & β’ π΅ = (Baseβπ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆMnd) & β’ (π β π΄ β πΌ) β β’ (π β (π₯ β π΅ β¦ (π₯βπ΄)) β (π MndHom (π βπ΄))) | ||
Theorem | pwspjmhm 18575* | A projection from a structure power of a monoid to the monoid itself is a monoid homomorphism. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ) β β’ ((π β Mnd β§ πΌ β π β§ π΄ β πΌ) β (π₯ β π΅ β¦ (π₯βπ΄)) β (π MndHom π )) | ||
Theorem | pwsdiagmhm 18576* | Diagonal monoid homomorphism into a structure power. (Contributed by Stefan O'Rear, 12-Mar-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ πΉ = (π₯ β π΅ β¦ (πΌ Γ {π₯})) β β’ ((π β Mnd β§ πΌ β π) β πΉ β (π MndHom π)) | ||
Theorem | pwsco1mhm 18577* | Right composition with a function on the index sets yields a monoid homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (π βs π΄) & β’ π = (π βs π΅) & β’ πΆ = (Baseβπ) & β’ (π β π β Mnd) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΉ:π΄βΆπ΅) β β’ (π β (π β πΆ β¦ (π β πΉ)) β (π MndHom π)) | ||
Theorem | pwsco2mhm 18578* | Left composition with a monoid homomorphism yields a monoid homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ π = (π βs π΄) & β’ π = (π βs π΄) & β’ π΅ = (Baseβπ) & β’ (π β π΄ β π) & β’ (π β πΉ β (π MndHom π)) β β’ (π β (π β π΅ β¦ (πΉ β π)) β (π MndHom π)) | ||
One important use of words is as formal composites in cases where order is significant, using the general sum operator df-gsum 17259. If order is not significant, it is simpler to use families instead. | ||
Theorem | gsumvallem2 18579* | Lemma for properties of the set of identities of πΊ. The set of identities of a monoid is exactly the unique identity element. (Contributed by Mario Carneiro, 7-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ + = (+gβπΊ) & β’ π = {π₯ β π΅ β£ βπ¦ β π΅ ((π₯ + π¦) = π¦ β§ (π¦ + π₯) = π¦)} β β’ (πΊ β Mnd β π = { 0 }) | ||
Theorem | gsumsubm 18580 | Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014.) |
β’ (π β π΄ β π) & β’ (π β π β (SubMndβπΊ)) & β’ (π β πΉ:π΄βΆπ) & β’ π» = (πΊ βΎs π) β β’ (π β (πΊ Ξ£g πΉ) = (π» Ξ£g πΉ)) | ||
Theorem | gsumz 18581* | Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.) |
β’ 0 = (0gβπΊ) β β’ ((πΊ β Mnd β§ π΄ β π) β (πΊ Ξ£g (π β π΄ β¦ 0 )) = 0 ) | ||
Theorem | gsumwsubmcl 18582 | Closure of the composite in any submonoid. (Contributed by Stefan O'Rear, 15-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.) |
β’ ((π β (SubMndβπΊ) β§ π β Word π) β (πΊ Ξ£g π) β π) | ||
Theorem | gsumws1 18583 | A singleton composite recovers the initial symbol. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
β’ π΅ = (BaseβπΊ) β β’ (π β π΅ β (πΊ Ξ£g β¨βπββ©) = π) | ||
Theorem | gsumwcl 18584 | Closure of the composite of a word in a structure πΊ. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
β’ π΅ = (BaseβπΊ) β β’ ((πΊ β Mnd β§ π β Word π΅) β (πΊ Ξ£g π) β π΅) | ||
Theorem | gsumsgrpccat 18585 | Homomorphic property of not empty composites of a group sum over a semigroup. Formerly part of proof for gsumccat 18586. (Contributed by AV, 26-Dec-2023.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Smgrp β§ (π β Word π΅ β§ π β Word π΅) β§ (π β β β§ π β β )) β (πΊ Ξ£g (π ++ π)) = ((πΊ Ξ£g π) + (πΊ Ξ£g π))) | ||
Theorem | gsumccat 18586 | Homomorphic property of composites. Second formula in [Lang] p. 4. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.) (Proof shortened by AV, 26-Dec-2023.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Mnd β§ π β Word π΅ β§ π β Word π΅) β (πΊ Ξ£g (π ++ π)) = ((πΊ Ξ£g π) + (πΊ Ξ£g π))) | ||
Theorem | gsumws2 18587 | Valuation of a pair in a monoid. (Contributed by Stefan O'Rear, 23-Aug-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Mnd β§ π β π΅ β§ π β π΅) β (πΊ Ξ£g β¨βππββ©) = (π + π)) | ||
Theorem | gsumccatsn 18588 | Homomorphic property of composites with a singleton. (Contributed by AV, 20-Jan-2019.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Mnd β§ π β Word π΅ β§ π β π΅) β (πΊ Ξ£g (π ++ β¨βπββ©)) = ((πΊ Ξ£g π) + π)) | ||
Theorem | gsumspl 18589 | The primary purpose of the splice construction is to enable local rewrites. Thus, in any monoidal valuation, if a splice does not cause a local change it does not cause a global change. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
β’ π΅ = (Baseβπ) & β’ (π β π β Mnd) & β’ (π β π β Word π΅) & β’ (π β πΉ β (0...π)) & β’ (π β π β (0...(β―βπ))) & β’ (π β π β Word π΅) & β’ (π β π β Word π΅) & β’ (π β (π Ξ£g π) = (π Ξ£g π)) β β’ (π β (π Ξ£g (π splice β¨πΉ, π, πβ©)) = (π Ξ£g (π splice β¨πΉ, π, πβ©))) | ||
Theorem | gsumwmhm 18590 | Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
β’ π΅ = (Baseβπ) β β’ ((π» β (π MndHom π) β§ π β Word π΅) β (π»β(π Ξ£g π)) = (π Ξ£g (π» β π))) | ||
Theorem | gsumwspan 18591* | The submonoid generated by a set of elements is precisely the set of elements which can be expressed as finite products of the generator. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
β’ π΅ = (Baseβπ) & β’ πΎ = (mrClsβ(SubMndβπ)) β β’ ((π β Mnd β§ πΊ β π΅) β (πΎβπΊ) = ran (π€ β Word πΊ β¦ (π Ξ£g π€))) | ||
Syntax | cfrmd 18592 | Extend class definition with the free monoid construction. |
class freeMnd | ||
Syntax | cvrmd 18593 | Extend class notation with free monoid injection. |
class varFMnd | ||
Definition | df-frmd 18594 | Define a free monoid over a set π of generators, defined as the set of finite strings on πΌ with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
β’ freeMnd = (π β V β¦ {β¨(Baseβndx), Word πβ©, β¨(+gβndx), ( ++ βΎ (Word π Γ Word π))β©}) | ||
Definition | df-vrmd 18595* | Define a free monoid over a set π of generators, defined as the set of finite strings on πΌ with the operation of concatenation. (Contributed by Mario Carneiro, 27-Sep-2015.) |
β’ varFMnd = (π β V β¦ (π β π β¦ β¨βπββ©)) | ||
Theorem | frmdval 18596 | Value of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.) |
β’ π = (freeMndβπΌ) & β’ (πΌ β π β π΅ = Word πΌ) & β’ + = ( ++ βΎ (π΅ Γ π΅)) β β’ (πΌ β π β π = {β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©}) | ||
Theorem | frmdbas 18597 | The base set of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
β’ π = (freeMndβπΌ) & β’ π΅ = (Baseβπ) β β’ (πΌ β π β π΅ = Word πΌ) | ||
Theorem | frmdelbas 18598 | An element of the base set of a free monoid is a string on the generators. (Contributed by Mario Carneiro, 27-Feb-2016.) |
β’ π = (freeMndβπΌ) & β’ π΅ = (Baseβπ) β β’ (π β π΅ β π β Word πΌ) | ||
Theorem | frmdplusg 18599 | The monoid operation of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) (Proof shortened by AV, 6-Nov-2024.) |
β’ π = (freeMndβπΌ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) β β’ + = ( ++ βΎ (π΅ Γ π΅)) | ||
Theorem | frmdadd 18600 | Value of the monoid operation of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.) |
β’ π = (freeMndβπΌ) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) β β’ ((π β π΅ β§ π β π΅) β (π + π) = (π ++ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |