HomeTheorem List (p. 181 of 450)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 181 of 450) | < 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-28697) |
Hilbert Space Explorer
(28698-30220) |
Users' Mathboxes
(30221-44913) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | gsumsubm 18001 | Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹)) | ||
| Theorem | gsumz 18002* | Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.) |
| ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) | ||
| Theorem | gsumwsubmcl 18003 | 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 18004 | A singleton composite recovers the initial symbol. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑆 ∈ 𝐵 → (𝐺 Σg ⟨“𝑆”⟩) = 𝑆) | ||
| Theorem | gsumwcl 18005 | Closure of the composite of a word in a structure 𝐺. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
| ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵) | ||
| Theorem | gsumsgrpccat 18006 | Homomorphic property of not empty composites of a group sum over a semigroup. Formerly part of proof for gsumccat 18008. (Contributed by AV, 26-Dec-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) | ||
| Theorem | gsumccatOLD 18007 | Obsolete version of gsumccat 18008 as of 13-Jan-2024. Homomorphic property of composites. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) | ||
| Theorem | gsumccat 18008 | 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 18009 | 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 18010 | Homomorphic property of composites with a singleton. (Contributed by AV, 20-Jan-2019.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ ⟨“𝑍”⟩)) = ((𝐺 Σg 𝑊) + 𝑍)) | ||
| Theorem | gsumspl 18011 | 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 18012 | Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
| ⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊))) | ||
| Theorem | gsumwspan 18013* | 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 18014 | Extend class definition with the free monoid construction. |
| class freeMnd | ||
| Syntax | cvrmd 18015 | Extend class notation with free monoid injection. |
| class varFMnd | ||
| Definition | df-frmd 18016 | 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 18017* | 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 18018 | Value of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.) |
| ⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ (𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼) & ⊢ + = ( ++ ↾ (𝐵 × 𝐵)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩}) | ||
| Theorem | frmdbas 18019 | 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 18020 | 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 18021 | The monoid operation of a free monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
| ⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ + = ( ++ ↾ (𝐵 × 𝐵)) | ||
| Theorem | frmdadd 18022 | Value of the monoid operation of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.) |
| ⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ++ 𝑌)) | ||
| Theorem | vrmdfval 18023* | 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 18024 | The value of the generating elements of a free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.) |
| ⊢ 𝑈 = (varFMnd‘𝐼) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = ⟨“𝐴”⟩) | ||
| Theorem | vrmdf 18025 | 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 18026 | A free monoid is a monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
| ⊢ 𝑀 = (freeMnd‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd) | ||
| Theorem | frmd0 18027 | The identity of the free monoid is the empty word. (Contributed by Mario Carneiro, 27-Sep-2015.) |
| ⊢ 𝑀 = (freeMnd‘𝐼) ⇒ ⊢ ∅ = (0g‘𝑀) | ||
| Theorem | frmdsssubm 18028 | 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 18029 | 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 18030 | 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 18031* | 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 18032* | 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 18033* | Lemma for frmdup3 18034. (Contributed by Mario Carneiro, 18-Jul-2016.) |
| ⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑈 = (varFMnd‘𝐼) ⇒ ⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → 𝐹 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥)))) | ||
| Theorem | frmdup3 18034* | 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 18035 | Extend class notation to include the class of monoids of endofunctions. |
| class EndoFMnd | ||
| Definition | df-efmnd 18036* | 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 18498 and symgvalstruct 18527. (Contributed by AV, 25-Jan-2024.) |
| ⊢ EndoFMnd = (𝑥 ∈ V ↦ ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}) | ||
| Theorem | efmnd 18037* | The monoid of endofunctions on set 𝐴. (Contributed by AV, 25-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (𝐴 ↑m 𝐴) & ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔)) & ⊢ 𝐽 = (∏t‘(𝐴 × {𝒫 𝐴})) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐺 = {⟨(Base‘ndx), 𝐵⟩, ⟨(+g‘ndx), + ⟩, ⟨(TopSet‘ndx), 𝐽⟩}) | ||
| Theorem | efmndbas 18038 | The base set of the monoid of endofunctions on class 𝐴. (Contributed by AV, 25-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 = (𝐴 ↑m 𝐴) | ||
| Theorem | efmndbasabf 18039* | 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 18040 | Two ways of saying a function is a mapping of 𝐴 to itself. (Contributed by AV, 27-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐴)) | ||
| Theorem | elefmndbas2 18041 | 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 18042 | Elements in the monoid of endofunctions on 𝐴 are functions from 𝐴 into itself. (Contributed by AV, 27-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴⟶𝐴) | ||
| Theorem | efmndhash 18043 | The monoid of endofunctions on 𝑛 objects has cardinality 𝑛↑𝑛. (Contributed by AV, 27-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ Fin → (♯‘𝐵) = ((♯‘𝐴)↑(♯‘𝐴))) | ||
| Theorem | efmndbasfi 18044 | The monoid of endofunctions on a finite set 𝐴 is finite. (Contributed by AV, 27-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ Fin → 𝐵 ∈ Fin) | ||
| Theorem | efmndfv 18045 | The function value of an endofunction. (Contributed by AV, 27-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝐴) → (𝐹‘𝑋) ∈ 𝐴) | ||
| Theorem | efmndtset 18046 | 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 18047* | The group operation of a monoid of endofunctions is the function composition. (Contributed by AV, 27-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔)) | ||
| Theorem | efmndov 18048 | The value of the group operation of the monoid of endofunctions on 𝐴. (Contributed by AV, 27-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ∘ 𝑌)) | ||
| Theorem | efmndcl 18049 | The group operation of the monoid of endofunctions on 𝐴 is closed. (Contributed by AV, 27-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) | ||
| Theorem | efmndtopn 18050 | The topology of the monoid of endofunctions on 𝐴. (Contributed by AV, 31-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝑋) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑋 ∈ 𝑉 → ((∏t‘(𝑋 × {𝒫 𝑋})) ↾t 𝐵) = (TopOpen‘𝐺)) | ||
| Theorem | symggrplem 18051* | Lemma for symggrp 18530 and efmndsgrp 18053. Conditions for an operation to be associative. Formerly part of proof for symggrp 18530. (Contributed by AV, 28-Jan-2024.) |
| ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) = (𝑥 ∘ 𝑦)) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
| Theorem | efmndmgm 18052 | The monoid of endofunctions on a class 𝐴 is a magma. (Contributed by AV, 28-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) ⇒ ⊢ 𝐺 ∈ Mgm | ||
| Theorem | efmndsgrp 18053 | The monoid of endofunctions on a class 𝐴 is a semigroup. (Contributed by AV, 28-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) ⇒ ⊢ 𝐺 ∈ Smgrp | ||
| Theorem | ielefmnd 18054 | 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 18055 | 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 18056 | The monoid of endofunctions on a set 𝐴 is actually a monoid. (Contributed by AV, 31-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐺 ∈ Mnd) | ||
| Theorem | efmnd0nmnd 18057 | Even the monoid of endofunctions on the empty set is actually a monoid. (Contributed by AV, 31-Jan-2024.) |
| ⊢ (EndoFMnd‘∅) ∈ Mnd | ||
| Theorem | efmndbas0 18058 | 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 18059 | The monoid of endofunctions on a singleton has cardinality 1. (Contributed by AV, 27-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼} ⇒ ⊢ (𝐼 ∈ 𝑉 → (♯‘𝐵) = 1) | ||
| Theorem | efmnd1bas 18060 | The monoid of endofunctions on a singleton consists of the identity only. (Contributed by AV, 31-Jan-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼} ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐵 = {{⟨𝐼, 𝐼⟩}}) | ||
| Theorem | efmnd2hash 18061 | The monoid of endofunctions on a (proper) pair has cardinality 4. (Contributed by AV, 18-Feb-2024.) |
| ⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝐴 = {𝐼, 𝐽} ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐽 ∈ 𝑊 ∧ 𝐼 ≠ 𝐽) → (♯‘𝐵) = 4) | ||
| Theorem | submefmnd 18062* | 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 18539. (Contributed by AV, 17-Feb-2024.) |
| ⊢ 𝑀 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ 𝐹 = (Base‘𝑆) ⇒ ⊢ (𝐴 ∈ 𝑉 → (((𝑆 ∈ Mnd ∧ 𝐹 ⊆ 𝐵 ∧ 0 ∈ 𝐹) ∧ (+g‘𝑆) = (𝑓 ∈ 𝐹, 𝑔 ∈ 𝐹 ↦ (𝑓 ∘ 𝑔))) → 𝐹 ∈ (SubMnd‘𝑀))) | ||
| Theorem | sursubmefmnd 18063* | 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 18064* | 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 18065 | 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 18066 | 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 18067 | The modulo function 𝐼 is an endofunction on ℕ0. (Contributed by AV, 12-Feb-2024.) |
| ⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) ⇒ ⊢ 𝐼 ∈ (Base‘𝑀) | ||
| Theorem | smndex1iidm 18068* | The modulo function 𝐼 is idempotent. (Contributed by AV, 12-Feb-2024.) |
| ⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) ⇒ ⊢ (𝐼 ∘ 𝐼) = 𝐼 | ||
| Theorem | smndex1gbas 18069* | The constant functions (𝐺‘𝐾) are endofunctions on ℕ0. (Contributed by AV, 12-Feb-2024.) |
| ⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) ⇒ ⊢ (𝐾 ∈ (0..^𝑁) → (𝐺‘𝐾) ∈ (Base‘𝑀)) | ||
| Theorem | smndex1gid 18070* | 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 18071* | 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 18072* | 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 18073* | 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 18074* | 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 18075* | 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 18076* | Lemma for smndex1mnd 18077 and smndex1id 18078. (Contributed by AV, 16-Feb-2024.) |
| ⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝑁 ∈ ℕ & ⊢ 𝐼 = (𝑥 ∈ ℕ0 ↦ (𝑥 mod 𝑁)) & ⊢ 𝐺 = (𝑛 ∈ (0..^𝑁) ↦ (𝑥 ∈ ℕ0 ↦ 𝑛)) & ⊢ 𝐵 = ({𝐼} ∪ ∪ 𝑛 ∈ (0..^𝑁){(𝐺‘𝑛)}) & ⊢ 𝑆 = (𝑀 ↾s 𝐵) ⇒ ⊢ (𝑋 ∈ 𝐵 → ((𝐼 ∘ 𝑋) = 𝑋 ∧ (𝑋 ∘ 𝐼) = 𝑋)) | ||
| Theorem | smndex1mnd 18077* | 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 18078* | 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 18079* | 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 18080* | 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 18081 | The doubling function 𝐷 is an endofunction on ℕ0. (Contributed by AV, 18-Feb-2024.) |
| ⊢ 𝑀 = (EndoFMnd‘ℕ0) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ 𝐷 = (𝑥 ∈ ℕ0 ↦ (2 · 𝑥)) ⇒ ⊢ 𝐷 ∈ 𝐵 | ||
| Theorem | smndex2dnrinv 18082 | 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 18083 | 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 18084* | 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 18085* | Lemma 1 for mgm2nsgrp 18089: 𝑀 is a magma, even if 𝐴 = 𝐵 (𝑀 is the trivial magma in this case, see mgmb1mgm1 17867). (Contributed by AV, 27-Jan-2020.) |
| ⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝑀 ∈ Mgm) | ||
| Theorem | mgm2nsgrplem2 18086* | Lemma 2 for mgm2nsgrp 18089. (Contributed by AV, 27-Jan-2020.) |
| ⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → ((𝐴 ⚬ 𝐴) ⚬ 𝐵) = 𝐴) | ||
| Theorem | mgm2nsgrplem3 18087* | Lemma 3 for mgm2nsgrp 18089. (Contributed by AV, 28-Jan-2020.) |
| ⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if((𝑥 = 𝐴 ∧ 𝑦 = 𝐴), 𝐵, 𝐴)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → (𝐴 ⚬ (𝐴 ⚬ 𝐵)) = 𝐵) | ||
| Theorem | mgm2nsgrplem4 18088* | Lemma 4 for mgm2nsgrp 18089: 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 18089* | 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 18090* | Lemma 1 for sgrp2nmnd 18097: 𝑀 is a magma, even if 𝐴 = 𝐵 (𝑀 is the trivial magma in this case, see mgmb1mgm1 17867). (Contributed by AV, 29-Jan-2020.) |
| ⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊) → 𝑀 ∈ Mgm) | ||
| Theorem | sgrp2nmndlem2 18091* | Lemma 2 for sgrp2nmnd 18097. (Contributed by AV, 29-Jan-2020.) |
| ⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐴 ∈ 𝑆 ∧ 𝐶 ∈ 𝑆) → (𝐴 ⚬ 𝐶) = 𝐴) | ||
| Theorem | sgrp2nmndlem3 18092* | Lemma 3 for sgrp2nmnd 18097. (Contributed by AV, 29-Jan-2020.) |
| ⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝐶 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵) → (𝐵 ⚬ 𝐶) = 𝐵) | ||
| Theorem | sgrp2rid2 18093* | 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 18094* | 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 18095* | Lemma 4 for sgrp2nmnd 18097: M is a semigroup. (Contributed by AV, 29-Jan-2020.) |
| ⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((♯‘𝑆) = 2 → 𝑀 ∈ Smgrp) | ||
| Theorem | sgrp2nmndlem5 18096* | Lemma 5 for sgrp2nmnd 18097: M is not a monoid. (Contributed by AV, 29-Jan-2020.) |
| ⊢ 𝑆 = {𝐴, 𝐵} & ⊢ (Base‘𝑀) = 𝑆 & ⊢ (+g‘𝑀) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ if(𝑥 = 𝐴, 𝐴, 𝐵)) ⇒ ⊢ ((♯‘𝑆) = 2 → 𝑀 ∉ Mnd) | ||
| Theorem | sgrp2nmnd 18097* | 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 18098 | There is a magma which is not a semigroup. (Contributed by AV, 29-Jan-2020.) |
| ⊢ ∃𝑚 ∈ Mgm 𝑚 ∉ Smgrp | ||
| Theorem | sgrpnmndex 18099 | There is a semigroup which is not a monoid. (Contributed by AV, 29-Jan-2020.) |
| ⊢ ∃𝑚 ∈ Smgrp 𝑚 ∉ Mnd | ||
| Theorem | sgrpssmgm 18100 | The class of all semigroups is a proper subclass of the class of all magmas. (Contributed by AV, 29-Jan-2020.) |
| ⊢ Smgrp ⊊ Mgm | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |