Home | Metamath
Proof Explorer Theorem List (p. 172 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | gsum0 17101 | Value of the empty group sum. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐺 Σg ∅) = 0 | ||
Theorem | gsumval2a 17102* | Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵) & ⊢ 𝑂 = {𝑥 ∈ 𝐵 ∣ ∀𝑦 ∈ 𝐵 ((𝑥 + 𝑦) = 𝑦 ∧ (𝑦 + 𝑥) = 𝑦)} & ⊢ (𝜑 → ¬ ran 𝐹 ⊆ 𝑂) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq𝑀( + , 𝐹)‘𝑁)) | ||
Theorem | gsumval2 17103 | Value of the group sum operation over a finite set of sequential integers. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘𝑀)) & ⊢ (𝜑 → 𝐹:(𝑀...𝑁)⟶𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (seq𝑀( + , 𝐹)‘𝑁)) | ||
Theorem | gsumprval 17104 | Value of the group sum operation over a pair of sequential integers. (Contributed by AV, 14-Dec-2018.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝑁 = (𝑀 + 1)) & ⊢ (𝜑 → 𝐹:{𝑀, 𝑁}⟶𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐹‘𝑀) + (𝐹‘𝑁))) | ||
Theorem | gsumpr12val 17105 | Value of the group sum operation over the pair {1, 2}. (Contributed by AV, 14-Dec-2018.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:{1, 2}⟶𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = ((𝐹‘1) + (𝐹‘2))) | ||
The definition of semigroups (SGrp, see df-sgrp 17107) is according to Wikipedia ("Semigroup", 8-Jan-2020, https://en.wikipedia.org/wiki/Semigroup) "In mathematics, a semigroup is an algebraic structure consisting of a set together with an associative binary operation. ... Semigroups may be considered a special case of magmas, where the operation is associative, or as a generalization of groups, without requiring the existence of an identity element or inverses.". | ||
Syntax | csgrp 17106 | Extend class notation with class of all semigroups. |
class SGrp | ||
Definition | df-sgrp 17107* | A semigroup is a set equipped with an everywhere defined internal operation (so, a magma, see df-mgm 17065), whose operation is associative. Definition in section II.1 of [Bruck] p. 23, or of an "associative magma" in definition 5 of [BourbakiAlg1] p. 4 . (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
⊢ SGrp = {𝑔 ∈ Mgm ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑜]∀𝑥 ∈ 𝑏 ∀𝑦 ∈ 𝑏 ∀𝑧 ∈ 𝑏 ((𝑥𝑜𝑦)𝑜𝑧) = (𝑥𝑜(𝑦𝑜𝑧))} | ||
Theorem | issgrp 17108* | The predicate "is a semigroup". (Contributed by FL, 2-Nov-2009.) (Revised by by AV, 6-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ SGrp ↔ (𝑀 ∈ Mgm ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧)))) | ||
Theorem | issgrpv 17109* | The predicate "is a semigroup" for a structure which is a set. (Contributed by AV, 1-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ SGrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))) | ||
Theorem | issgrpn0 17110* | The predicate "is a semigroup" for a structure with a nonempty base set. (Contributed by AV, 1-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (𝐴 ∈ 𝐵 → (𝑀 ∈ SGrp ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ∈ 𝐵 ∧ ∀𝑧 ∈ 𝐵 ((𝑥 ⚬ 𝑦) ⚬ 𝑧) = (𝑥 ⚬ (𝑦 ⚬ 𝑧))))) | ||
Theorem | isnsgrp 17111 | A condition for a structure not to be a semigroup. (Contributed by AV, 30-Jan-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) → (((𝑋 ⚬ 𝑌) ⚬ 𝑍) ≠ (𝑋 ⚬ (𝑌 ⚬ 𝑍)) → 𝑀 ∉ SGrp)) | ||
Theorem | sgrpmgm 17112 | A semigroup is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) |
⊢ (𝑀 ∈ SGrp → 𝑀 ∈ Mgm) | ||
Theorem | sgrpass 17113 | A semigroup operation is associative. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 30-Jan-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ ⚬ = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ SGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ⚬ 𝑌) ⚬ 𝑍) = (𝑋 ⚬ (𝑌 ⚬ 𝑍))) | ||
Theorem | sgrp0 17114 | Any set with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021.) |
⊢ ((𝑀 ∈ 𝑉 ∧ (Base‘𝑀) = ∅) → 𝑀 ∈ SGrp) | ||
Theorem | sgrp0b 17115 | The structure with an empty base set and any group operation is a semigroup. (Contributed by AV, 28-Aug-2021.) |
⊢ {〈(Base‘ndx), ∅〉, 〈(+g‘ndx), 𝑂〉} ∈ SGrp | ||
Theorem | sgrp1 17116 | The structure with one element and the only closed internal operation for a singleton is a semigroup. (Contributed by AV, 10-Feb-2020.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉} ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝑀 ∈ SGrp) | ||
According to Wikipedia ("Monoid", https://en.wikipedia.org/wiki/Monoid, 6-Feb-2020,) "In abstract algebra [...] a monoid is an algebraic structure with a single associative binary operation and an identity element. Monoids are semigroups with identity.". In the following, monoids are defined in the second way (as semigroups with identity), see df-mnd 17118, whereas many authors define magmas in the first way (as algebraic structure with a single associative binary operation and an identity element, i.e. without the need of a definition for/knowledge about semigroups), see ismnd 17120. See, for example, the definition in [Lang] p. 3: "A monoid is a set G, with a law of composition which is associative, and having a unit element". | ||
Syntax | cmnd 17117 | Extend class notation with class of all monoids. |
class Mnd | ||
Definition | df-mnd 17118* | A monoid is a semigroup, which has a two-sided neutral element. Definition 2 in [BourbakiAlg1] p. 12. In other words (according to the definition in [Lang] p. 3), a monoid is a set equipped with an everywhere defined internal operation (see mndcl 17124), whose operation is associative (see mndass 17125) and has a two-sided neutral element (see mndid 17126), see also ismnd 17120. (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.) |
⊢ Mnd = {𝑔 ∈ SGrp ∣ [(Base‘𝑔) / 𝑏][(+g‘𝑔) / 𝑝]∃𝑒 ∈ 𝑏 ∀𝑥 ∈ 𝑏 ((𝑒𝑝𝑥) = 𝑥 ∧ (𝑥𝑝𝑒) = 𝑥)} | ||
Theorem | ismnddef 17119* | The predicate "is a monoid", corresponding 1-to-1 to the definition. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 1-Feb-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd ↔ (𝐺 ∈ SGrp ∧ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎))) | ||
Theorem | ismnd 17120* | The predicate "is a monoid". This is the definig theorem of a monoid by showing that a set is a monoid if and only if it is a set equipped with a closed, everywhere defined internal operation (so, a magma, see mndcl 17124), whose operation is associative (so, a semigroup, see also mndass 17125) and has a two-sided neutral element (see mndid 17126). (Contributed by Mario Carneiro, 6-Jan-2015.) (Revised by AV, 1-Feb-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd ↔ (∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ((𝑎 + 𝑏) ∈ 𝐵 ∧ ∀𝑐 ∈ 𝐵 ((𝑎 + 𝑏) + 𝑐) = (𝑎 + (𝑏 + 𝑐))) ∧ ∃𝑒 ∈ 𝐵 ∀𝑎 ∈ 𝐵 ((𝑒 + 𝑎) = 𝑎 ∧ (𝑎 + 𝑒) = 𝑎))) | ||
Theorem | isnmnd 17121* | A condition for a structure not to be a monoid: every element of the base set is not a left identity for at least one element of the base set. (Contributed by AV, 4-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ ⚬ = (+g‘𝑀) ⇒ ⊢ (∀𝑧 ∈ 𝐵 ∃𝑥 ∈ 𝐵 (𝑧 ⚬ 𝑥) ≠ 𝑥 → 𝑀 ∉ Mnd) | ||
Theorem | mndsgrp 17122 | A monoid is a semigroup. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) (Proof shortened by AV, 6-Feb-2020.) |
⊢ (𝐺 ∈ Mnd → 𝐺 ∈ SGrp) | ||
Theorem | mndmgm 17123 | A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (Revised by AV, 6-Jan-2020.) (Proof shortened by AV, 6-Feb-2020.) |
⊢ (𝑀 ∈ Mnd → 𝑀 ∈ Mgm) | ||
Theorem | mndcl 17124 | 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 17125 | A monoid operation is associative. (Contributed by NM, 14-Aug-2011.) (Proof shortened by AV, 8-Feb-2020.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
Theorem | mndid 17126* | A monoid has a two-sided identity element. (Contributed by NM, 16-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → ∃𝑢 ∈ 𝐵 ∀𝑥 ∈ 𝐵 ((𝑢 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑢) = 𝑥)) | ||
Theorem | mndideu 17127* | 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 17128 | Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → (𝑌 + 𝑍) = (𝑍 + 𝑌)) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = ((𝑋 + 𝑍) + 𝑌)) | ||
Theorem | mnd12g 17129 | Commutative/associative law for monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → (𝑋 + 𝑌) = (𝑌 + 𝑋)) ⇒ ⊢ (𝜑 → (𝑋 + (𝑌 + 𝑍)) = (𝑌 + (𝑋 + 𝑍))) | ||
Theorem | mnd4g 17130 | Commutative/associative law for commutative monoids, with an explicit commutativity hypothesis. (Contributed by Mario Carneiro, 21-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → (𝑌 + 𝑍) = (𝑍 + 𝑌)) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) | ||
Theorem | mndidcl 17131 | 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 17132 | 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 17133 | 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 17134 | The identity element of a monoid is a left identity. (Contributed by NM, 18-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → ( 0 + 𝑋) = 𝑋) | ||
Theorem | mndrid 17135 | The identity element of a monoid is a right identity. (Contributed by NM, 18-Aug-2011.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑋 ∈ 𝐵) → (𝑋 + 0 ) = 𝑋) | ||
Theorem | ismndd 17136* | Deduce a monoid from its properties. (Contributed by Mario Carneiro, 6-Jan-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐺)) & ⊢ (𝜑 → + = (+g‘𝐺)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧))) & ⊢ (𝜑 → 0 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ( 0 + 𝑥) = 𝑥) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑥 + 0 ) = 𝑥) ⇒ ⊢ (𝜑 → 𝐺 ∈ Mnd) | ||
Theorem | mndpfo 17137 | 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 17138 | 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 17139* | 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 17140 | 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 17141* | Characterize a submonoid by closure properties. (Contributed by Mario Carneiro, 10-Jan-2015.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆) → (𝐻 ∈ Mnd ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆)) | ||
Theorem | ress0g 17142 | 0g is unaffected by restriction. This is a bit more generic than submnd0 17143. (Contributed by Thierry Arnoux, 23-Oct-2017.) |
⊢ 𝑆 = (𝑅 ↾s 𝐴) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 0 ∈ 𝐴 ∧ 𝐴 ⊆ 𝐵) → 0 = (0g‘𝑆)) | ||
Theorem | submnd0 17143 | 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 17144 | 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 17145* | 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 17146 | The product of a family of monoids is a monoid. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Mnd) ⇒ ⊢ (𝜑 → 𝑌 ∈ Mnd) | ||
Theorem | prds0g 17147 | Zero in a product of monoids. (Contributed by Stefan O'Rear, 10-Jan-2015.) |
⊢ 𝑌 = (𝑆Xs𝑅) & ⊢ (𝜑 → 𝐼 ∈ 𝑊) & ⊢ (𝜑 → 𝑆 ∈ 𝑉) & ⊢ (𝜑 → 𝑅:𝐼⟶Mnd) ⇒ ⊢ (𝜑 → (0g ∘ 𝑅) = (0g‘𝑌)) | ||
Theorem | pwsmnd 17148 | The structure power of a monoid is a monoid. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) → 𝑌 ∈ Mnd) | ||
Theorem | pws0g 17149 | Zero in a product of monoids. (Contributed by Mario Carneiro, 11-Jan-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 0 = (0g‘𝑅) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑉) → (𝐼 × { 0 }) = (0g‘𝑌)) | ||
Theorem | imasmnd2 17150* | 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 17151* | 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 17152 | 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 17153 | The binary product of monoids is a monoid. (Contributed by Mario Carneiro, 20-Aug-2015.) |
⊢ 𝑇 = (𝑅 ×s 𝑆) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝑆 ∈ Mnd) → 𝑇 ∈ Mnd) | ||
Theorem | mnd1 17154 | 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 17155 | The singleton element of a trivial monoid is its identity element. (Contributed by AV, 23-Jan-2020.) |
⊢ 𝑀 = {〈(Base‘ndx), {𝐼}〉, 〈(+g‘ndx), {〈〈𝐼, 𝐼〉, 𝐼〉}〉} ⇒ ⊢ (𝐼 ∈ 𝑉 → (0g‘𝑀) = 𝐼) | ||
Syntax | cmhm 17156 | Hom-set generator class for monoids. |
class MndHom | ||
Syntax | csubmnd 17157 | Class function taking a monoid to its lattice of submonoids. |
class SubMnd | ||
Definition | df-mhm 17158* | 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 17159* | 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 17160* | 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 17161 | Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑆 ∈ Mnd) | ||
Theorem | mhmrcl2 17162 | Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝑇 ∈ Mnd) | ||
Theorem | mhmf 17163 | A monoid homomorphism is a function. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐶 = (Base‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → 𝐹:𝐵⟶𝐶) | ||
Theorem | mhmpropd 17164* | 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 17165 | A monoid homomorphism commutes with composition. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑆) & ⊢ + = (+g‘𝑆) & ⊢ ⨣ = (+g‘𝑇) ⇒ ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘(𝑋 + 𝑌)) = ((𝐹‘𝑋) ⨣ (𝐹‘𝑌))) | ||
Theorem | mhm0 17166 | A monoid homomorphism preserves zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 0 = (0g‘𝑆) & ⊢ 𝑌 = (0g‘𝑇) ⇒ ⊢ (𝐹 ∈ (𝑆 MndHom 𝑇) → (𝐹‘ 0 ) = 𝑌) | ||
Theorem | idmhm 17167 | The identity homomorphism on a monoid. (Contributed by AV, 14-Feb-2020.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → ( I ↾ 𝐵) ∈ (𝑀 MndHom 𝑀)) | ||
Theorem | mhmf1o 17168 | 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 17169 | Reverse closure for submonoids. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑀 ∈ Mnd) | ||
Theorem | issubm 17170* | Expand definition of a submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → (𝑆 ∈ (SubMnd‘𝑀) ↔ (𝑆 ⊆ 𝐵 ∧ 0 ∈ 𝑆 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥 + 𝑦) ∈ 𝑆))) | ||
Theorem | issubm2 17171 | 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 17172* | 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 17173 | Submonoids are subsets of the base set. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 ⊆ 𝐵) | ||
Theorem | submid 17174 | Every monoid is trivially a submonoid of itself. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ 𝐵 = (Base‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → 𝐵 ∈ (SubMnd‘𝑀)) | ||
Theorem | subm0cl 17175 | Submonoids contain zero. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 0 = (0g‘𝑀) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 ∈ 𝑆) | ||
Theorem | submcl 17176 | Submonoids are closed under the monoid operation. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑆 ∈ (SubMnd‘𝑀) ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆) | ||
Theorem | submmnd 17177 | Submonoids are themselves monoids under the given operation. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐻 = (𝑀 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝐻 ∈ Mnd) | ||
Theorem | submbas 17178 | The base set of a submonoid. (Contributed by Stefan O'Rear, 15-Jun-2015.) |
⊢ 𝐻 = (𝑀 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 𝑆 = (Base‘𝐻)) | ||
Theorem | subm0 17179 | Submonoids have the same identity. (Contributed by Mario Carneiro, 7-Mar-2015.) |
⊢ 𝐻 = (𝑀 ↾s 𝑆) & ⊢ 0 = (0g‘𝑀) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝑀) → 0 = (0g‘𝐻)) | ||
Theorem | subsubm 17180 | A submonoid of a submonoid is a submonoid. (Contributed by Mario Carneiro, 21-Jun-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝑆 ∈ (SubMnd‘𝐺) → (𝐴 ∈ (SubMnd‘𝐻) ↔ (𝐴 ∈ (SubMnd‘𝐺) ∧ 𝐴 ⊆ 𝑆))) | ||
Theorem | 0mhm 17181 | 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 17182 | Restriction of a monoid homomorphism to a submonoid is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.) |
⊢ 𝑈 = (𝑆 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑇) ∧ 𝑋 ∈ (SubMnd‘𝑆)) → (𝐹 ↾ 𝑋) ∈ (𝑈 MndHom 𝑇)) | ||
Theorem | resmhm2 17183 | One direction of resmhm2b 17184. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) ⇒ ⊢ ((𝐹 ∈ (𝑆 MndHom 𝑈) ∧ 𝑋 ∈ (SubMnd‘𝑇)) → 𝐹 ∈ (𝑆 MndHom 𝑇)) | ||
Theorem | resmhm2b 17184 | Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015.) |
⊢ 𝑈 = (𝑇 ↾s 𝑋) ⇒ ⊢ ((𝑋 ∈ (SubMnd‘𝑇) ∧ ran 𝐹 ⊆ 𝑋) → (𝐹 ∈ (𝑆 MndHom 𝑇) ↔ 𝐹 ∈ (𝑆 MndHom 𝑈))) | ||
Theorem | mhmco 17185 | The composition of monoid homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
⊢ ((𝐹 ∈ (𝑇 MndHom 𝑈) ∧ 𝐺 ∈ (𝑆 MndHom 𝑇)) → (𝐹 ∘ 𝐺) ∈ (𝑆 MndHom 𝑈)) | ||
Theorem | mhmima 17186 | The homomorphic image of a submonoid is a submonoid. (Contributed by Mario Carneiro, 10-Mar-2015.) |
⊢ ((𝐹 ∈ (𝑀 MndHom 𝑁) ∧ 𝑋 ∈ (SubMnd‘𝑀)) → (𝐹 “ 𝑋) ∈ (SubMnd‘𝑁)) | ||
Theorem | mhmeql 17187 | 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 17188 | Submonoids are an algebraic closure system. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → (SubMnd‘𝐺) ∈ (ACS‘𝐵)) | ||
Theorem | mrcmndind 17189* | (( 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 17190* | 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 17191* | 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 17192* | Diagonal monoid homomorphism into a structure power. (Contributed by Stefan O'Rear, 12-Mar-2015.) |
⊢ 𝑌 = (𝑅 ↑s 𝐼) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐼 × {𝑥})) ⇒ ⊢ ((𝑅 ∈ Mnd ∧ 𝐼 ∈ 𝑊) → 𝐹 ∈ (𝑅 MndHom 𝑌)) | ||
Theorem | pwsco1mhm 17193* | 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 17194* | 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 15926. If order is not significant, it is simpler to use families instead. | ||
Theorem | gsumvallem2 17195* | 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 17196 | Evaluate a group sum in a submonoid. (Contributed by Mario Carneiro, 19-Dec-2014.) |
⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺)) & ⊢ (𝜑 → 𝐹:𝐴⟶𝑆) & ⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹)) | ||
Theorem | gsumz 17197* | Value of a group sum over the zero element. (Contributed by Mario Carneiro, 7-Dec-2014.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑉) → (𝐺 Σg (𝑘 ∈ 𝐴 ↦ 0 )) = 0 ) | ||
Theorem | gsumwsubmcl 17198 | 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 17199 | A singleton composite recovers the initial symbol. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑆 ∈ 𝐵 → (𝐺 Σg 〈“𝑆”〉) = 𝑆) | ||
Theorem | gsumwcl 17200 | Closure of the composite of a word in a structure 𝐺. (Contributed by Stefan O'Rear, 15-Aug-2015.) |
⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑊 ∈ Word 𝐵) → (𝐺 Σg 𝑊) ∈ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |