![]() |
Metamath
Proof Explorer Theorem List (p. 189 of 491) | < 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-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | imasmndf1 18801 | 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 18802 | The binary product of monoids is a monoid. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑇 ∈ Mnd) | ||
Theorem | xpsmnd0 18803 | The identity element of a binary product of monoids. (Contributed by AV, 25-Feb-2025.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → (0g‘𝑇) = 〈(0g‘𝑅), (0g‘𝑆)〉) | ||
Theorem | mnd1 18804 | 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 18805 | The singleton element of a trivial monoid is its identity element. (Contributed by AV, 23-Jan-2020.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉} ⇒ ⊢ (𝐼 ∈ 𝑉 → (0g‘𝑀) = 𝐼) | ||
Syntax | cmhm 18806 | Hom-set generator class for monoids. |
class MndHom | ||
Syntax | csubmnd 18807 | Class function taking a monoid to its lattice of submonoids. |
class SubMnd | ||
Definition | df-mhm 18808* | 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 18809* | 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 18810* | 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 18811* | Deduction version of ismhm 18810. (Contributed by SN, 27-Jul-2024.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝑍 = (0g‘𝑇) & ⊢ (𝜑 → 𝑆 ∈ Mnd) & ⊢ (𝜑 → 𝑇 ∈ Mnd) & ⊢ (𝜑 → 𝐹:𝐵⟶𝐶) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦))) & ⊢ (𝜑 → (𝐹‘ 0 ) = 𝑍) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆 MndHom 𝑇)) | ||
Theorem | mhmrcl1 18812 | Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑆 ∈ Mnd) | ||
Theorem | mhmrcl2 18813 | Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑇 ∈ Mnd) | ||
Theorem | mhmf 18814 | A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:𝐵⟶𝐶) | ||
Theorem | ismhm0 18815 | Property of a monoid homomorphism, expressed by a magma homomorphism. (Contributed by AV, 17-Apr-2020.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝑌 = (0g‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹 ∈ (𝑆 MgmHom 𝑇) ∧ (𝐹‘ 0 ) = 𝑌))) | ||
Theorem | mhmismgmhm 18816 | Each monoid homomorphism is a magma homomorphism. (Contributed by AV, 29-Feb-2020.) |
⊢ (𝐹 ∈ (𝑅 MndHom 𝑆) → 𝐹 ∈ (𝑅 MgmHom 𝑆)) | ||
Theorem | mhmpropd 18817* | 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 18818 | A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌))) | ||
Theorem | mhm0 18819 | A monoid homomorphism preserves zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 0 = (0g‘𝑆) & ⊢ 𝑌 = (0g‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹‘ 0 ) = 𝑌) | ||
Theorem | idmhm 18820 | The identity homomorphism on a monoid. (Contributed by AV, 14-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → ( I ↾ 𝐵) ∈ (𝑀 MndHom 𝑀)) | ||
Theorem | mhmf1o 18821 | 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 | mndvcl 18822 | Tuple-wise additive closure in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f + 𝑌) ∈ (𝐵 ↑m 𝐼)) | ||
Theorem | mndvass 18823 | Tuple-wise associativity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ (𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼) ∧ 𝑍 ∈ (𝐵 ↑m 𝐼))) → ((𝑋 ∘f + 𝑌) ∘f + 𝑍) = (𝑋 ∘f + (𝑌 ∘f + 𝑍))) | ||
Theorem | mndvlid 18824 | Tuple-wise left identity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 0 = (0g‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → ((𝐼 × { 0 }) ∘f + 𝑋) = 𝑋) | ||
Theorem | mndvrid 18825 | Tuple-wise right identity in monoids. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 0 = (0g‘𝑀) ⇒ ⊢ ((𝑀 ∈ Mnd ∧ 𝑋 ∈ (𝐵 ↑m 𝐼)) → (𝑋 ∘f + (𝐼 × { 0 })) = 𝑋) | ||
Theorem | mhmvlin 18826 | Tuple extension of monoid homomorphisms. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ ⨣ = (+g‘𝑁) ⇒ ⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (𝐵 ↑m 𝐼) ∧ 𝑌 ∈ (𝐵 ↑m 𝐼)) → (𝐹 ∘ (𝑋 ∘f + 𝑌)) = ((𝐹 ∘ 𝑋) ∘f ⨣ (𝐹 ∘ 𝑌))) | ||
Theorem | submrcl 18827 | Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑀 ∈ Mnd) | ||
Theorem | issubm 18828* | Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆))) | ||
Theorem | issubm2 18829 | 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 18830 | The submonoid predicate. Analogous to issubg 19156. (Contributed by AV, 1-Feb-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝐺) ↔ ((𝐺 ∈ Mnd ∧ (𝐺 ↾s 𝑆) ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆))) | ||
Theorem | issubmd 18831* | 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 18832 | 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 19176. (Contributed by AV, 17-Feb-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = (Base‘𝐻) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) → ((𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → 𝑆 ∈ (SubMnd‘𝐺))) | ||
Theorem | resmndismnd 18833 | 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 19177. (Contributed by AV, 17-Feb-2024.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = (Base‘𝐻) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) → ((𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ (+g‘𝐻) = ((+g‘𝐺) ↾ (𝑆 × 𝑆))) → (𝐺 ↾s 𝑆) ∈ Mnd)) | ||
Theorem | submss 18834 | Submonoids are subsets of the base set. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 ⊆ 𝐵) | ||
Theorem | submid 18835 | Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → 𝐵 ∈ (SubMnd‘𝑀)) | ||
Theorem | subm0cl 18836 | Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 0 = (0g‘𝑀) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 ∈ 𝑆) | ||
Theorem | submcl 18837 | Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑆 ∈ (SubMnd‘𝑀) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆) | ||
Theorem | submmnd 18838 | Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐻 = (𝑀 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝐻 ∈ Mnd) | ||
Theorem | submbas 18839 | The base set of a submonoid. (Contributed by Stefan O'Rear, 15-Jun-2015.) |
⊢ 𝐻 = (𝑀 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 = (Base‘𝐻)) | ||
Theorem | subm0 18840 | Submonoids have the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐻 = (𝑀 ↾s 𝑆) & ⊢ 0 = (0g‘𝑀) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 = (0g‘𝐻)) | ||
Theorem | subsubm 18841 | A submonoid of a submonoid is a submonoid. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝐺) → (𝐴 ∈ (SubMnd‘𝐻) ↔ (𝐴 ∈ (SubMnd‘𝐺) ∧ 𝐴 ⊆ 𝑆))) | ||
Theorem | 0subm 18842 | The zero submonoid of an arbitrary monoid. (Contributed by AV, 17-Feb-2024.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → { 0 } ∈ (SubMnd‘𝐺)) | ||
Theorem | insubm 18843 | The intersection of two submonoids is a submonoid. (Contributed by AV, 25-Feb-2024.) |
⊢ ((𝐴 ∈ (SubMnd‘𝑀) ∧ 𝐵 ∈ (SubMnd‘𝑀)) → (𝐴 ∩ 𝐵) ∈ (SubMnd‘𝑀)) | ||
Theorem | 0mhm 18844 | 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 18845 | Restriction of a monoid homomorphism to a submonoid is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ 𝑈 = (𝑆 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MndHom 𝑇)) | ||
Theorem | resmhm2 18846 | One direction of resmhm2b 18847. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → 𝐹 ∈ (𝑆 MndHom 𝑇)) | ||
Theorem | resmhm2b 18847 | Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) ⇒ ⊢ ((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ (𝑆 MndHom 𝑈))) | ||
Theorem | mhmco 18848 | The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ ((𝐹 ∈ (𝑇 MndHom 𝑈) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 MndHom 𝑈)) | ||
Theorem | mhmimalem 18849* | Lemma for mhmima 18850 and similar theorems, formerly part of proof for mhmima 18850. (Contributed by Mario Carneiro, 10-Mar-2015.) (Revised by AV, 16-Feb-2025.) |
⊢ (𝜑 → 𝐹 ∈ (𝑀 MndHom 𝑁)) & ⊢ (𝜑 → 𝑋 ⊆ (Base‘𝑀)) & ⊢ (𝜑 → ⊕ = (+g‘𝑀)) & ⊢ (𝜑 → + = (+g‘𝑁)) & ⊢ ((𝜑 ∧ 𝑧 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑧 ⊕ 𝑥) ∈ 𝑋) ⇒ ⊢ (𝜑 → ∀𝑥 ∈ (𝐹 “ 𝑋)∀𝑦 ∈ (𝐹 “ 𝑋)(𝑥 + 𝑦) ∈ (𝐹 “ 𝑋)) | ||
Theorem | mhmima 18850 | The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015.) (Proof shortened by AV, 8-Mar-2025.) |
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (SubMnd‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubMnd‘𝑁)) | ||
Theorem | mhmeql 18851 | 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 18852 | Submonoids are an algebraic closure system. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → (SubMnd‘𝐺) ∈ (ACS‘𝐵)) | ||
Theorem | mndind 18853* | 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 18854* | 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 18855* | 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 18856* | Diagonal monoid homomorphism into a structure power. (Contributed by Stefan O'Rear, 12-Mar-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 MndHom 𝑌)) | ||
Theorem | pwsco1mhm 18857* | 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 18858* | 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 17488. If order is not significant, it is simpler to use families instead. | ||
Theorem | gsumvallem2 18859* | 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 18860 | Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹)) | ||
Theorem | gsumz 18861* | Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) | ||
Theorem | gsumwsubmcl 18862 | 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 18863 | A singleton composite recovers the initial symbol. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑆 ∈ 𝐵 → (𝐺 Σg 〈“𝑆”〉) = 𝑆) | ||
Theorem | gsumwcl 18864 | Closure of the composite of a word in a structure 𝐺. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵) | ||
Theorem | gsumsgrpccat 18865 | Homomorphic property of not empty composites of a group sum over a semigroup. Formerly part of proof for gsumccat 18866. (Contributed by AV, 26-Dec-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Smgrp ∧ (𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) ∧ (𝑊 ≠ ∅ ∧ 𝑋 ≠ ∅)) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) | ||
Theorem | gsumccat 18866 | 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 18867 | 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 18868 | Homomorphic property of composites with a singleton. (Contributed by AV, 20-Jan-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ 〈“𝑍”〉)) = ((𝐺 Σg 𝑊) + 𝑍)) | ||
Theorem | gsumspl 18869 | 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 18870 | Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊))) | ||
Theorem | gsumwspan 18871* | 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 18872 | Extend class definition with the free monoid construction. |
class freeMnd | ||
Syntax | cvrmd 18873 | Extend class notation with free monoid injection. |
class varFMnd | ||
Definition | df-frmd 18874 | 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 18875* | 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 18876 | Value of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ (𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼) & ⊢ + = ( ++ ↾ (𝐵 × 𝐵)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉}) | ||
Theorem | frmdbas 18877 | 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 18878 | 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 18879 | 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 18880 | Value of the monoid operation of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ++ 𝑌)) | ||
Theorem | vrmdfval 18881* | 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 18882 | The value of the generating elements of a free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑈 = (varFMnd‘𝐼) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = 〈“𝐴”〉) | ||
Theorem | vrmdf 18883 | 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 18884 | A free monoid is a monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑀 = (freeMnd‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd) | ||
Theorem | frmd0 18885 | The identity of the free monoid is the empty word. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (freeMnd‘𝐼) ⇒ ⊢ ∅ = (0g‘𝑀) | ||
Theorem | frmdsssubm 18886 | 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 18887 | 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 18888 | 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 18889* | 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 18890* | 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 18891* | Lemma for frmdup3 18892. (Contributed by Mario Carneiro, 18-Jul-2016.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑈 = (varFMnd‘𝐼) ⇒ ⊢ (((𝐺 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴:𝐼⟶𝐵) ∧ (𝐹 ∈ (𝑀 MndHom 𝐺) ∧ (𝐹 ∘ 𝑈) = 𝐴)) → 𝐹 = (𝑥 ∈ Word 𝐼 ↦ (𝐺 Σg (𝐴 ∘ 𝑥)))) | ||
Theorem | frmdup3 18892* | 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 18893 | Extend class notation to include the class of monoids of endofunctions. |
class EndoFMnd | ||
Definition | df-efmnd 18894* | 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 19401 and symgvalstruct 19428. (Contributed by AV, 25-Jan-2024.) |
⊢ EndoFMnd = (𝑥 ∈ V ↦ ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{〈(Base‘ndx), 𝑏〉, 〈(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))〉, 〈(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))〉}) | ||
Theorem | efmnd 18895* | The monoid of endofunctions on set 𝐴. (Contributed by AV, 25-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (𝐴 ↑m 𝐴) & ⊢ + = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (𝑓 ∘ 𝑔)) & ⊢ 𝐽 = (∏t‘(𝐴 × {𝒫 𝐴})) ⇒ ⊢ (𝐴 ∈ 𝑉 → 𝐺 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉, 〈(TopSet‘ndx), 𝐽〉}) | ||
Theorem | efmndbas 18896 | The base set of the monoid of endofunctions on class 𝐴. (Contributed by AV, 25-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝐵 = (𝐴 ↑m 𝐴) | ||
Theorem | efmndbasabf 18897* | 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 18898 | Two ways of saying a function is a mapping of 𝐴 to itself. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑉 → (𝐹 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐴)) | ||
Theorem | elefmndbas2 18899 | 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 18900 | Elements in the monoid of endofunctions on 𝐴 are functions from 𝐴 into itself. (Contributed by AV, 27-Jan-2024.) |
⊢ 𝐺 = (EndoFMnd‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐹 ∈ 𝐵 → 𝐹:𝐴⟶𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |