Home | Metamath
Proof Explorer Theorem List (p. 187 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-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | vrmdfval 18601* | The canonical injection from the generating set πΌ to the base set of the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.) |
β’ π = (varFMndβπΌ) β β’ (πΌ β π β π = (π β πΌ β¦ β¨βπββ©)) | ||
Theorem | vrmdval 18602 | The value of the generating elements of a free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.) |
β’ π = (varFMndβπΌ) β β’ ((πΌ β π β§ π΄ β πΌ) β (πβπ΄) = β¨βπ΄ββ©) | ||
Theorem | vrmdf 18603 | The mapping from the index set to the generators is a function into the free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.) |
β’ π = (varFMndβπΌ) β β’ (πΌ β π β π:πΌβΆWord πΌ) | ||
Theorem | frmdmnd 18604 | A free monoid is a monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
β’ π = (freeMndβπΌ) β β’ (πΌ β π β π β Mnd) | ||
Theorem | frmd0 18605 | The identity of the free monoid is the empty word. (Contributed by Mario Carneiro, 27-Sep-2015.) |
β’ π = (freeMndβπΌ) β β’ β = (0gβπ) | ||
Theorem | frmdsssubm 18606 | The set of words taking values in a subset is a (free) submonoid of the free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
β’ π = (freeMndβπΌ) β β’ ((πΌ β π β§ π½ β πΌ) β Word π½ β (SubMndβπ)) | ||
Theorem | frmdgsum 18607 | Any word in a free monoid can be expressed as the sum of the singletons composing it. (Contributed by Mario Carneiro, 27-Sep-2015.) |
β’ π = (freeMndβπΌ) & β’ π = (varFMndβπΌ) β β’ ((πΌ β π β§ π β Word πΌ) β (π Ξ£g (π β π)) = π) | ||
Theorem | frmdss2 18608 | A subset of generators is contained in a submonoid iff the set of words on the generators is in the submonoid. This can be viewed as an elementary way of saying "the monoidal closure of π½ is Word π½". (Contributed by Mario Carneiro, 2-Oct-2015.) |
β’ π = (freeMndβπΌ) & β’ π = (varFMndβπΌ) β β’ ((πΌ β π β§ π½ β πΌ β§ π΄ β (SubMndβπ)) β ((π β π½) β π΄ β Word π½ β π΄)) | ||
Theorem | frmdup1 18609* | Any assignment of the generators to target elements can be extended (uniquely) to a homomorphism from a free monoid to an arbitrary other monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) |
β’ π = (freeMndβπΌ) & β’ π΅ = (BaseβπΊ) & β’ πΈ = (π₯ β Word πΌ β¦ (πΊ Ξ£g (π΄ β π₯))) & β’ (π β πΊ β Mnd) & β’ (π β πΌ β π) & β’ (π β π΄:πΌβΆπ΅) β β’ (π β πΈ β (π MndHom πΊ)) | ||
Theorem | frmdup2 18610* | The evaluation map has the intended behavior on the generators. (Contributed by Mario Carneiro, 27-Sep-2015.) |
β’ π = (freeMndβπΌ) & β’ π΅ = (BaseβπΊ) & β’ πΈ = (π₯ β Word πΌ β¦ (πΊ Ξ£g (π΄ β π₯))) & β’ (π β πΊ β Mnd) & β’ (π β πΌ β π) & β’ (π β π΄:πΌβΆπ΅) & β’ π = (varFMndβπΌ) & β’ (π β π β πΌ) β β’ (π β (πΈβ(πβπ)) = (π΄βπ)) | ||
Theorem | frmdup3lem 18611* | Lemma for frmdup3 18612. (Contributed by Mario Carneiro, 18-Jul-2016.) |
β’ π = (freeMndβπΌ) & β’ π΅ = (BaseβπΊ) & β’ π = (varFMndβπΌ) β β’ (((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β§ (πΉ β (π MndHom πΊ) β§ (πΉ β π) = π΄)) β πΉ = (π₯ β Word πΌ β¦ (πΊ Ξ£g (π΄ β π₯)))) | ||
Theorem | frmdup3 18612* | Universal property of the free monoid by existential uniqueness. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by Mario Carneiro, 18-Jul-2016.) |
β’ π = (freeMndβπΌ) & β’ π΅ = (BaseβπΊ) & β’ π = (varFMndβπΌ) β β’ ((πΊ β Mnd β§ πΌ β π β§ π΄:πΌβΆπ΅) β β!π β (π MndHom πΊ)(π β π) = π΄) | ||
According to Wikipedia ("Endomorphism", 25-Jan-2024, https://en.wikipedia.org/wiki/Endomorphism) "An endofunction is a function whose domain is equal to its codomain.". An endofunction is sometimes also called "self-mapping" (see https://www.wikidata.org/wiki/Q1691962) or "self-map" (see https://mathworld.wolfram.com/Self-Map.html), in German "Selbstabbildung" (see https://de.wikipedia.org/wiki/Selbstabbildung). | ||
Syntax | cefmnd 18613 | Extend class notation to include the class of monoids of endofunctions. |
class EndoFMnd | ||
Definition | df-efmnd 18614* | Define the monoid of endofunctions on set π₯. We represent the monoid as the set of functions from π₯ to itself ((π₯ βm π₯)) under function composition, and topologize it as a function space assuming the set is discrete. Analogous to the former definition of SymGrp, see df-symg 19081 and symgvalstruct 19110. (Contributed by AV, 25-Jan-2024.) |
β’ EndoFMnd = (π₯ β V β¦ β¦(π₯ βm π₯) / πβ¦{β¨(Baseβndx), πβ©, β¨(+gβndx), (π β π, π β π β¦ (π β π))β©, β¨(TopSetβndx), (βtβ(π₯ Γ {π« π₯}))β©}) | ||
Theorem | efmnd 18615* | The monoid of endofunctions on set π΄. (Contributed by AV, 25-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (π΄ βm π΄) & β’ + = (π β π΅, π β π΅ β¦ (π β π)) & β’ π½ = (βtβ(π΄ Γ {π« π΄})) β β’ (π΄ β π β πΊ = {β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(TopSetβndx), π½β©}) | ||
Theorem | efmndbas 18616 | The base set of the monoid of endofunctions on class π΄. (Contributed by AV, 25-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) β β’ π΅ = (π΄ βm π΄) | ||
Theorem | efmndbasabf 18617* | The base set of the monoid of endofunctions on class π΄ is the set of functions from π΄ into itself. (Contributed by AV, 29-Mar-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) β β’ π΅ = {π β£ π:π΄βΆπ΄} | ||
Theorem | elefmndbas 18618 | Two ways of saying a function is a mapping of π΄ to itself. (Contributed by AV, 27-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β (πΉ β π΅ β πΉ:π΄βΆπ΄)) | ||
Theorem | elefmndbas2 18619 | Two ways of saying a function is a mapping of π΄ to itself. (Contributed by AV, 27-Jan-2024.) (Proof shortened by AV, 29-Mar-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (πΉ β π β (πΉ β π΅ β πΉ:π΄βΆπ΄)) | ||
Theorem | efmndbasf 18620 | Elements in the monoid of endofunctions on π΄ are functions from π΄ into itself. (Contributed by AV, 27-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (πΉ β π΅ β πΉ:π΄βΆπ΄) | ||
Theorem | efmndhash 18621 | The monoid of endofunctions on π objects has cardinality πβπ. (Contributed by AV, 27-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β Fin β (β―βπ΅) = ((β―βπ΄)β(β―βπ΄))) | ||
Theorem | efmndbasfi 18622 | The monoid of endofunctions on a finite set π΄ is finite. (Contributed by AV, 27-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β Fin β π΅ β Fin) | ||
Theorem | efmndfv 18623 | The function value of an endofunction. (Contributed by AV, 27-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) β β’ ((πΉ β π΅ β§ π β π΄) β (πΉβπ) β π΄) | ||
Theorem | efmndtset 18624 | The topology of the monoid of endofunctions on π΄. This component is defined on a larger set than the true base - the product topology is defined on the set of all functions, not just endofunctions - but the definition of TopOpen ensures that it is trimmed down before it gets use. (Contributed by AV, 25-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) β β’ (π΄ β π β (βtβ(π΄ Γ {π« π΄})) = (TopSetβπΊ)) | ||
Theorem | efmndplusg 18625* | The group operation of a monoid of endofunctions is the function composition. (Contributed by AV, 27-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ + = (π β π΅, π β π΅ β¦ (π β π)) | ||
Theorem | efmndov 18626 | The value of the group operation of the monoid of endofunctions on π΄. (Contributed by AV, 27-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((π β π΅ β§ π β π΅) β (π + π) = (π β π)) | ||
Theorem | efmndcl 18627 | The group operation of the monoid of endofunctions on π΄ is closed. (Contributed by AV, 27-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((π β π΅ β§ π β π΅) β (π + π) β π΅) | ||
Theorem | efmndtopn 18628 | The topology of the monoid of endofunctions on π΄. (Contributed by AV, 31-Jan-2024.) |
β’ πΊ = (EndoFMndβπ) & β’ π΅ = (BaseβπΊ) β β’ (π β π β ((βtβ(π Γ {π« π})) βΎt π΅) = (TopOpenβπΊ)) | ||
Theorem | symggrplem 18629* | Lemma for symggrp 19114 and efmndsgrp 18631. Conditions for an operation to be associative. Formerly part of proof for symggrp 19114. (Contributed by AV, 28-Jan-2024.) |
β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) β π΅) & β’ ((π₯ β π΅ β§ π¦ β π΅) β (π₯ + π¦) = (π₯ β π¦)) β β’ ((π β π΅ β§ π β π΅ β§ π β π΅) β ((π + π) + π) = (π + (π + π))) | ||
Theorem | efmndmgm 18630 | The monoid of endofunctions on a class π΄ is a magma. (Contributed by AV, 28-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) β β’ πΊ β Mgm | ||
Theorem | efmndsgrp 18631 | The monoid of endofunctions on a class π΄ is a semigroup. (Contributed by AV, 28-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) β β’ πΊ β Smgrp | ||
Theorem | ielefmnd 18632 | 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 18633 | 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 18634 | The monoid of endofunctions on a set π΄ is actually a monoid. (Contributed by AV, 31-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) β β’ (π΄ β π β πΊ β Mnd) | ||
Theorem | efmnd0nmnd 18635 | Even the monoid of endofunctions on the empty set is actually a monoid. (Contributed by AV, 31-Jan-2024.) |
β’ (EndoFMndββ ) β Mnd | ||
Theorem | efmndbas0 18636 | 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 18637 | The monoid of endofunctions on a singleton has cardinality 1. (Contributed by AV, 27-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ} β β’ (πΌ β π β (β―βπ΅) = 1) | ||
Theorem | efmnd1bas 18638 | The monoid of endofunctions on a singleton consists of the identity only. (Contributed by AV, 31-Jan-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ} β β’ (πΌ β π β π΅ = {{β¨πΌ, πΌβ©}}) | ||
Theorem | efmnd2hash 18639 | The monoid of endofunctions on a (proper) pair has cardinality 4. (Contributed by AV, 18-Feb-2024.) |
β’ πΊ = (EndoFMndβπ΄) & β’ π΅ = (BaseβπΊ) & β’ π΄ = {πΌ, π½} β β’ ((πΌ β π β§ π½ β π β§ πΌ β π½) β (β―βπ΅) = 4) | ||
Theorem | submefmnd 18640* | 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 19123. (Contributed by AV, 17-Feb-2024.) |
β’ π = (EndoFMndβπ΄) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΉ = (Baseβπ) β β’ (π΄ β π β (((π β Mnd β§ πΉ β π΅ β§ 0 β πΉ) β§ (+gβπ) = (π β πΉ, π β πΉ β¦ (π β π))) β πΉ β (SubMndβπ))) | ||
Theorem | sursubmefmnd 18641* | 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 18642* | 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 18643 | 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 18644 | 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 18645 | The modulo function πΌ is an endofunction on β0. (Contributed by AV, 12-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) β β’ πΌ β (Baseβπ) | ||
Theorem | smndex1iidm 18646* | The modulo function πΌ is idempotent. (Contributed by AV, 12-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) β β’ (πΌ β πΌ) = πΌ | ||
Theorem | smndex1gbas 18647* | The constant functions (πΊβπΎ) are endofunctions on β0. (Contributed by AV, 12-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) β β’ (πΎ β (0..^π) β (πΊβπΎ) β (Baseβπ)) | ||
Theorem | smndex1gid 18648* | 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 18649* | 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 18650* | 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 18651* | 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 18652* | 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 18653* | 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 18654* | Lemma for smndex1mnd 18655 and smndex1id 18656. (Contributed by AV, 16-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π β β & β’ πΌ = (π₯ β β0 β¦ (π₯ mod π)) & β’ πΊ = (π β (0..^π) β¦ (π₯ β β0 β¦ π)) & β’ π΅ = ({πΌ} βͺ βͺ π β (0..^π){(πΊβπ)}) & β’ π = (π βΎs π΅) β β’ (π β π΅ β ((πΌ β π) = π β§ (π β πΌ) = π)) | ||
Theorem | smndex1mnd 18655* | 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 18656* | 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 18657* | 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 18658* | 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 18659 | The doubling function π· is an endofunction on β0. (Contributed by AV, 18-Feb-2024.) |
β’ π = (EndoFMndββ0) & β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ π· = (π₯ β β0 β¦ (2 Β· π₯)) β β’ π· β π΅ | ||
Theorem | smndex2dnrinv 18660 | 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 18661 | 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 18662* | 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 18663* | Lemma 1 for mgm2nsgrp 18667: π is a magma, even if π΄ = π΅ (π is the trivial magma in this case, see mgmb1mgm1 18445). (Contributed by AV, 27-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if((π₯ = π΄ β§ π¦ = π΄), π΅, π΄)) β β’ ((π΄ β π β§ π΅ β π) β π β Mgm) | ||
Theorem | mgm2nsgrplem2 18664* | Lemma 2 for mgm2nsgrp 18667. (Contributed by AV, 27-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if((π₯ = π΄ β§ π¦ = π΄), π΅, π΄)) & β’ β¬ = (+gβπ) β β’ ((π΄ β π β§ π΅ β π) β ((π΄ β¬ π΄) β¬ π΅) = π΄) | ||
Theorem | mgm2nsgrplem3 18665* | Lemma 3 for mgm2nsgrp 18667. (Contributed by AV, 28-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if((π₯ = π΄ β§ π¦ = π΄), π΅, π΄)) & β’ β¬ = (+gβπ) β β’ ((π΄ β π β§ π΅ β π) β (π΄ β¬ (π΄ β¬ π΅)) = π΅) | ||
Theorem | mgm2nsgrplem4 18666* | Lemma 4 for mgm2nsgrp 18667: 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 18667* | 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 18668* | Lemma 1 for sgrp2nmnd 18675: π is a magma, even if π΄ = π΅ (π is the trivial magma in this case, see mgmb1mgm1 18445). (Contributed by AV, 29-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if(π₯ = π΄, π΄, π΅)) β β’ ((π΄ β π β§ π΅ β π) β π β Mgm) | ||
Theorem | sgrp2nmndlem2 18669* | Lemma 2 for sgrp2nmnd 18675. (Contributed by AV, 29-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if(π₯ = π΄, π΄, π΅)) & β’ β¬ = (+gβπ) β β’ ((π΄ β π β§ πΆ β π) β (π΄ β¬ πΆ) = π΄) | ||
Theorem | sgrp2nmndlem3 18670* | Lemma 3 for sgrp2nmnd 18675. (Contributed by AV, 29-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if(π₯ = π΄, π΄, π΅)) & β’ β¬ = (+gβπ) β β’ ((πΆ β π β§ π΅ β π β§ π΄ β π΅) β (π΅ β¬ πΆ) = π΅) | ||
Theorem | sgrp2rid2 18671* | 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 18672* | 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 18673* | Lemma 4 for sgrp2nmnd 18675: M is a semigroup. (Contributed by AV, 29-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if(π₯ = π΄, π΄, π΅)) β β’ ((β―βπ) = 2 β π β Smgrp) | ||
Theorem | sgrp2nmndlem5 18674* | Lemma 5 for sgrp2nmnd 18675: M is not a monoid. (Contributed by AV, 29-Jan-2020.) |
β’ π = {π΄, π΅} & β’ (Baseβπ) = π & β’ (+gβπ) = (π₯ β π, π¦ β π β¦ if(π₯ = π΄, π΄, π΅)) β β’ ((β―βπ) = 2 β π β Mnd) | ||
Theorem | sgrp2nmnd 18675* | 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 18676 | There is a magma which is not a semigroup. (Contributed by AV, 29-Jan-2020.) |
β’ βπ β Mgm π β Smgrp | ||
Theorem | sgrpnmndex 18677 | There is a semigroup which is not a monoid. (Contributed by AV, 29-Jan-2020.) |
β’ βπ β Smgrp π β Mnd | ||
Theorem | sgrpssmgm 18678 | 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 18679 | 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 18680* | 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 18681* | 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 18682* | The power set of a class π΄ is a monoid under union. (Contributed by AV, 27-Feb-2024.) |
β’ (Baseβπ) = π« π΄ & β’ (+gβπ) = (π₯ β π« π΄, π¦ β π« π΄ β¦ (π₯ βͺ π¦)) β β’ π β Mnd | ||
Syntax | cgrp 18683 | Extend class notation with class of all groups. |
class Grp | ||
Syntax | cminusg 18684 | Extend class notation with inverse of group element. |
class invg | ||
Syntax | csg 18685 | Extend class notation with group subtraction (or division) operation. |
class -g | ||
Definition | df-grp 18686* | Define class of all groups. A group is a monoid (df-mnd 18492) 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 17019) and an internal group operation (notated (+gβπΊ) per df-plusg 17081). 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 18691), associativity (so ((π+gπ)+gπ) = (π+g(π+gπ)) for any a, b, c, see grpass 18692), 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 18694). Groups need not be commutative; a commutative group is an Abelian group (see df-abl 19494). Subgroups can often be formed from groups, see df-subg 18858. An example of an (Abelian) group is the set of complex numbers β over the group operation + (addition), as proven in cnaddablx 19575; an Abelian group is a group as proven in ablgrp 19496. Other structures include groups, including unital rings (df-ring 19890) and fields (df-field 20111). (Contributed by NM, 17-Oct-2012.) (Revised by Mario Carneiro, 6-Jan-2015.) |
β’ Grp = {π β Mnd β£ βπ β (Baseβπ)βπ β (Baseβπ)(π(+gβπ)π) = (0gβπ)} | ||
Definition | df-minusg 18687* | Define inverse of group element. (Contributed by NM, 24-Aug-2011.) |
β’ invg = (π β V β¦ (π₯ β (Baseβπ) β¦ (β©π€ β (Baseβπ)(π€(+gβπ)π₯) = (0gβπ)))) | ||
Definition | df-sbg 18688* | Define group subtraction (also called division for multiplicative groups). (Contributed by NM, 31-Mar-2014.) |
β’ -g = (π β V β¦ (π₯ β (Baseβπ), π¦ β (Baseβπ) β¦ (π₯(+gβπ)((invgβπ)βπ¦)))) | ||
Theorem | isgrp 18689* | 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 18690 | A group is a monoid. (Contributed by Mario Carneiro, 6-Jan-2015.) |
β’ (πΊ β Grp β πΊ β Mnd) | ||
Theorem | grpcl 18691 | Closure of the operation of a group. (Contributed by NM, 14-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Grp β§ π β π΅ β§ π β π΅) β (π + π) β π΅) | ||
Theorem | grpass 18692 | A group operation is associative. (Contributed by NM, 14-Aug-2011.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((πΊ β Grp β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π + π) + π) = (π + (π + π))) | ||
Theorem | grpinvex 18693* | 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 18694* | 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 | grpmndd 18695 | A group is a monoid. (Contributed by SN, 1-Jun-2024.) |
β’ (π β πΊ β Grp) β β’ (π β πΊ β Mnd) | ||
Theorem | grpcld 18696 | Closure of the operation of a group. (Contributed by SN, 29-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π + π) β π΅) | ||
Theorem | grpplusf 18697 | The group addition operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π΅ = (BaseβπΊ) & β’ πΉ = (+πβπΊ) β β’ (πΊ β Grp β πΉ:(π΅ Γ π΅)βΆπ΅) | ||
Theorem | grpplusfo 18698 | 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 18699 | 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 18700* | 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)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |