Home | Metamath
Proof Explorer Theorem List (p. 174 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mndcl 17301 | Closure of the operation of a monoid. (Contributed by NM, 14-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.) (Proof shortened by AV, 8-Feb-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) ∈ 𝐵) | ||
Theorem | mndass 17302 | A monoid operation is associative. (Contributed by NM, 14-Aug-2011.) (Proof shortened by AV, 8-Feb-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | mndid 17303* | A monoid has a two-sided identity element. (Contributed by NM, 16-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → ∃𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥)) | ||
Theorem | mndideu 17304* | 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 17305 | Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → (𝑌 + 𝑍) = (𝑍 + 𝑌)) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌)) | ||
Theorem | mnd12g 17306 | Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) ⇒ ⊢ (𝜑 → (𝑋 + (𝑌 + 𝑍)) = (𝑌 + (𝑋 + 𝑍))) | ||
Theorem | mnd4g 17307 | Commutative/associative law for commutative monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → (𝑌 + 𝑍) = (𝑍 + 𝑌)) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) | ||
Theorem | mndidcl 17308 | 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 | mndplusf 17309 | 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 17310 | 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 17311 | The identity element of a monoid is a left identity. (Contributed by NM, 18-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) | ||
Theorem | mndrid 17312 | The identity element of a monoid is a right identity. (Contributed by NM, 18-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋) | ||
Theorem | ismndd 17313* | Deduce a monoid from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 0 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) ⇒ ⊢ (𝜑 → 𝐺 ∈ Mnd) | ||
Theorem | mndpfo 17314 | 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 17315 | 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 17316* | 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 17317 | 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 17318* | Characterize a submonoid by closure properties. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) → (𝐻 ∈ Mnd ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)) | ||
Theorem | ress0g 17319 | 0g is unaffected by restriction. This is a bit more generic than submnd0 17320. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 0 = (0g‘𝑆)) | ||
Theorem | submnd0 17320 | 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.) (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (((𝐺 ∈ Mnd ∧ 𝐻 ∈ Mnd) ∧ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆)) → 0 = (0g‘𝐻)) | ||
Theorem | prdsplusgcl 17321 | 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 17322* | 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 17323 | The product of a family of monoids is a monoid. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Mnd) ⇒ ⊢ (𝜑 → 𝑌 ∈ Mnd) | ||
Theorem | prds0g 17324 | Zero in a product of monoids. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Mnd) ⇒ ⊢ (𝜑 → (0g ∘ 𝑅) = (0g‘𝑌)) | ||
Theorem | pwsmnd 17325 | The structure power of a monoid is a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Mnd) | ||
Theorem | pws0g 17326 | Zero in a product of monoids. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) → (𝐼 × { 0 }) = (0g‘𝑌)) | ||
Theorem | imasmnd2 17327* | 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 17328* | 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 17329 | 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 17330 | The binary product of monoids is a monoid. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑇 ∈ Mnd) | ||
Theorem | mnd1 17331 | 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 17332 | The singleton element of a trivial monoid is its identity element. (Contributed by AV, 23-Jan-2020.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉} ⇒ ⊢ (𝐼 ∈ 𝑉 → (0g‘𝑀) = 𝐼) | ||
Syntax | cmhm 17333 | Hom-set generator class for monoids. |
class MndHom | ||
Syntax | csubmnd 17334 | Class function taking a monoid to its lattice of submonoids. |
class SubMnd | ||
Definition | df-mhm 17335* | 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‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))}) | ||
Definition | df-submnd 17336* | 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 17337* | Property of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) & ⊢ 0 = (0g‘𝑆) & ⊢ 𝑌 = (0g‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ ((𝑆 ∈ Mnd ∧ 𝑇 ∈ Mnd) ∧ (𝐹:𝐵⟶𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝐹‘(𝑥 + 𝑦)) = ((𝐹‘𝑥) ⨣ (𝐹‘𝑦)) ∧ (𝐹‘ 0 ) = 𝑌))) | ||
Theorem | mhmrcl1 17338 | Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑆 ∈ Mnd) | ||
Theorem | mhmrcl2 17339 | Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑇 ∈ Mnd) | ||
Theorem | mhmf 17340 | A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:𝐵⟶𝐶) | ||
Theorem | mhmpropd 17341* | 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 17342 | A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌))) | ||
Theorem | mhm0 17343 | A monoid homomorphism preserves zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 0 = (0g‘𝑆) & ⊢ 𝑌 = (0g‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹‘ 0 ) = 𝑌) | ||
Theorem | idmhm 17344 | The identity homomorphism on a monoid. (Contributed by AV, 14-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → ( I ↾ 𝐵) ∈ (𝑀 MndHom 𝑀)) | ||
Theorem | mhmf1o 17345 | 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 17346 | Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑀 ∈ Mnd) | ||
Theorem | issubm 17347* | Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆))) | ||
Theorem | issubm2 17348 | 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 | issubmd 17349* | 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 | submss 17350 | Submonoids are subsets of the base set. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 ⊆ 𝐵) | ||
Theorem | submid 17351 | Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → 𝐵 ∈ (SubMnd‘𝑀)) | ||
Theorem | subm0cl 17352 | Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 0 = (0g‘𝑀) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 ∈ 𝑆) | ||
Theorem | submcl 17353 | Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑆 ∈ (SubMnd‘𝑀) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆) | ||
Theorem | submmnd 17354 | Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐻 = (𝑀 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝐻 ∈ Mnd) | ||
Theorem | submbas 17355 | The base set of a submonoid. (Contributed by Stefan O'Rear, 15-Jun-2015.) |
⊢ 𝐻 = (𝑀 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 = (Base‘𝐻)) | ||
Theorem | subm0 17356 | Submonoids have the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐻 = (𝑀 ↾s 𝑆) & ⊢ 0 = (0g‘𝑀) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 = (0g‘𝐻)) | ||
Theorem | subsubm 17357 | A submonoid of a submonoid is a submonoid. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝐺) → (𝐴 ∈ (SubMnd‘𝐻) ↔ (𝐴 ∈ (SubMnd‘𝐺) ∧ 𝐴 ⊆ 𝑆))) | ||
Theorem | 0mhm 17358 | 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 17359 | Restriction of a monoid homomorphism to a submonoid is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ 𝑈 = (𝑆 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MndHom 𝑇)) | ||
Theorem | resmhm2 17360 | One direction of resmhm2b 17361. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → 𝐹 ∈ (𝑆 MndHom 𝑇)) | ||
Theorem | resmhm2b 17361 | Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) ⇒ ⊢ ((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ (𝑆 MndHom 𝑈))) | ||
Theorem | mhmco 17362 | The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ ((𝐹 ∈ (𝑇 MndHom 𝑈) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 MndHom 𝑈)) | ||
Theorem | mhmima 17363 | The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (SubMnd‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubMnd‘𝑁)) | ||
Theorem | mhmeql 17364 | 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 17365 | Submonoids are an algebraic closure system. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → (SubMnd‘𝐺) ∈ (ACS‘𝐵)) | ||
Theorem | mrcmndind 17366* | (( From SO's determinants branch )). TODO: Appropriate description to be added! (Contributed by SO, 14-Jul-2018.) |
⊢ (𝑥 = 𝑦 → (𝜓 ↔ 𝜒)) & ⊢ (𝑥 = (𝑦 + 𝑧) → (𝜓 ↔ 𝜃)) & ⊢ (𝑥 = 0 → (𝜓 ↔ 𝜏)) & ⊢ (𝑥 = 𝐴 → (𝜓 ↔ 𝜂)) & ⊢ 0 = (0g‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Mnd) & ⊢ (𝜑 → 𝐺 ⊆ 𝐵) & ⊢ (𝜑 → 𝐵 = ((mrCls‘(SubMnd‘𝑀))‘𝐺)) & ⊢ (𝜑 → 𝜏) & ⊢ (((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐺) ∧ 𝜒) → 𝜃) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝜂) | ||
Theorem | prdspjmhm 17367* | 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 17368* | A projection from a product of monoids to one of the factors is a monoid homomorphism. (Contributed by Mario Carneiro, 15-Jun-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑌) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑥 ∈ 𝐵 ↦ (𝑥‘𝐴)) ∈ (𝑌 MndHom 𝑅)) | ||
Theorem | pwsdiagmhm 17369* | Diagonal monoid homomorphism into a structure power. (Contributed by Stefan O'Rear, 12-Mar-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 MndHom 𝑌)) | ||
Theorem | pwsco1mhm 17370* | 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 17371* | 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 16103. If order is not significant, it is simpler to use families instead. | ||
Theorem | gsumvallem2 17372* | 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 17373 | Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹)) | ||
Theorem | gsumz 17374* | Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) | ||
Theorem | gsumwsubmcl 17375 | 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 17376 | A singleton composite recovers the initial symbol. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑆 ∈ 𝐵 → (𝐺 Σg 〈“𝑆”〉) = 𝑆) | ||
Theorem | gsumwcl 17377 | Closure of the composite of a word in a structure 𝐺. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵) | ||
Theorem | gsumccat 17378 | Homomorphic property of composites. (Contributed by Stefan O'Rear, 16-Aug-2015.) (Revised by Mario Carneiro, 1-Oct-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑋 ∈ Word 𝐵) → (𝐺 Σg (𝑊 ++ 𝑋)) = ((𝐺 Σg 𝑊) + (𝐺 Σg 𝑋))) | ||
Theorem | gsumws2 17379 | 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 17380 | Homomorphic property of composites with a singleton. (Contributed by AV, 20-Jan-2019.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵 ∧ 𝑍 ∈ 𝐵) → (𝐺 Σg (𝑊 ++ 〈“𝑍”〉)) = ((𝐺 Σg 𝑊) + 𝑍)) | ||
Theorem | gsumspl 17381 | 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 17382 | Behavior of homomorphisms on finite monoidal sums. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ ((𝐻 ∈ (𝑀 MndHom 𝑁) ∧ 𝑊 ∈ Word 𝐵) → (𝐻‘(𝑀 Σg 𝑊)) = (𝑁 Σg (𝐻 ∘ 𝑊))) | ||
Theorem | gsumwspan 17383* | 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 17384 | Extend class definition with the free monoid construction. |
class freeMnd | ||
Syntax | cvrmd 17385 | Extend class notation with free monoid injection. |
class varFMnd | ||
Definition | df-frmd 17386 | 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 17387* | 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 17388 | Value of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ (𝐼 ∈ 𝑉 → 𝐵 = Word 𝐼) & ⊢ + = ( ++ ↾ (𝐵 × 𝐵)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 = {〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx), + 〉}) | ||
Theorem | frmdbas 17389 | 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 17390 | 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 17391 | 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 17392 | Value of the monoid operation of the free monoid construction. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (freeMnd‘𝐼) & ⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 + 𝑌) = (𝑋 ++ 𝑌)) | ||
Theorem | vrmdfval 17393* | 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 17394 | The value of the generating elements of a free monoid. (Contributed by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑈 = (varFMnd‘𝐼) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) → (𝑈‘𝐴) = 〈“𝐴”〉) | ||
Theorem | vrmdf 17395 | 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 17396 | A free monoid is a monoid. (Contributed by Mario Carneiro, 27-Sep-2015.) (Revised by Mario Carneiro, 27-Feb-2016.) |
⊢ 𝑀 = (freeMnd‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ Mnd) | ||
Theorem | frmd0 17397 | The identity of the free monoid is the empty word. (Contributed by Mario Carneiro, 27-Sep-2015.) |
⊢ 𝑀 = (freeMnd‘𝐼) ⇒ ⊢ ∅ = (0g‘𝑀) | ||
Theorem | frmdsssubm 17398 | 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 17399 | 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 17400 | 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 𝐽 ⊆ 𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |