HomeTheorem List (p. 330 of 494)
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. 330 of 494) | < 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-30831) |
Hilbert Space Explorer
(30832-32354) |
Users' Mathboxes
(32355-49389) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | mgcf1olem2 32901 | Property of a Galois connection, lemma for mgcf1o 32902. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
| ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ (𝜑 → 𝑉 ∈ Poset) & ⊢ (𝜑 → 𝑊 ∈ Poset) & ⊢ (𝜑 → 𝐹𝐻𝐺) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺‘(𝐹‘(𝐺‘𝑌))) = (𝐺‘𝑌)) | ||
| Theorem | mgcf1o 32902 | Given a Galois connection, exhibit an order isomorphism. (Contributed by Thierry Arnoux, 26-Jul-2024.) |
| ⊢ 𝐻 = (𝑉MGalConn𝑊) & ⊢ 𝐴 = (Base‘𝑉) & ⊢ 𝐵 = (Base‘𝑊) & ⊢ ≤ = (le‘𝑉) & ⊢ ≲ = (le‘𝑊) & ⊢ (𝜑 → 𝑉 ∈ Poset) & ⊢ (𝜑 → 𝑊 ∈ Poset) & ⊢ (𝜑 → 𝐹𝐻𝐺) ⇒ ⊢ (𝜑 → (𝐹 ↾ ran 𝐺) Isom ≤ , ≲ (ran 𝐺, ran 𝐹)) | ||
| Syntax | cchn 32903 | Extend class notation with the class of (finite) chains. |
| class ( < Chain𝐴) | ||
| Definition | df-chn 32904* | Define the class of (finite) chains. A chain is defined to be a sequence of objects, where each object is less than the next one in the sequence. The term "chain" is usually used in order theory. In the context of algebra, chains are often called "towers", for example for fields, or "series", for example for subgroup or subnormal series. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
| ⊢ ( < Chain𝐴) = {𝑐 ∈ Word 𝐴 ∣ ∀𝑛 ∈ (dom 𝑐 ∖ {0})(𝑐‘(𝑛 − 1)) < (𝑐‘𝑛)} | ||
| Theorem | ischn 32905* | Property of being a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
| ⊢ (𝐶 ∈ ( < Chain𝐴) ↔ (𝐶 ∈ Word 𝐴 ∧ ∀𝑛 ∈ (dom 𝐶 ∖ {0})(𝐶‘(𝑛 − 1)) < (𝐶‘𝑛))) | ||
| Theorem | chnwrd 32906 | A chain is an ordered sequence, i.e. a word. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) ⇒ ⊢ (𝜑 → 𝐶 ∈ Word 𝐴) | ||
| Theorem | chnltm1 32907 | Basic property of a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) & ⊢ (𝜑 → 𝑁 ∈ (dom 𝐶 ∖ {0})) ⇒ ⊢ (𝜑 → (𝐶‘(𝑁 − 1)) < (𝐶‘𝑁)) | ||
| Theorem | pfxchn 32908 | A prefix of a chain is still a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
| ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) & ⊢ (𝜑 → 𝐿 ∈ (0...(♯‘𝐶))) ⇒ ⊢ (𝜑 → (𝐶 prefix 𝐿) ∈ ( < Chain𝐴)) | ||
| Theorem | s1chn 32909 | A singleton word is always a chain. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝐴) ⇒ ⊢ (𝜑 → ⟨“𝑋”⟩ ∈ ( < Chain𝐴)) | ||
| Theorem | chnind 32910* | Induction over a chain. See nnind 12250 for an explanation about the hypotheses. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
| ⊢ (𝑐 = ∅ → (𝜓 ↔ 𝜒)) & ⊢ (𝑐 = 𝑑 → (𝜓 ↔ 𝜃)) & ⊢ (𝑐 = (𝑑 ++ ⟨“𝑥”⟩) → (𝜓 ↔ 𝜏)) & ⊢ (𝑐 = 𝐶 → (𝜓 ↔ 𝜂)) & ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) & ⊢ (𝜑 → 𝜒) & ⊢ (((((𝜑 ∧ 𝑑 ∈ ( < Chain𝐴)) ∧ 𝑥 ∈ 𝐴) ∧ (𝑑 = ∅ ∨ (lastS‘𝑑) < 𝑥)) ∧ 𝜃) → 𝜏) ⇒ ⊢ (𝜑 → 𝜂) | ||
| Theorem | chnub 32911 | In a chain, the last element is an upper bound. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
| ⊢ (𝜑 → < Po 𝐴) & ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) & ⊢ (𝜑 → 𝐼 ∈ (0..^((♯‘𝐶) − 1))) ⇒ ⊢ (𝜑 → (𝐶‘𝐼) < (lastS‘𝐶)) | ||
| Theorem | chnlt 32912 | Compare any two elements in a chain. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
| ⊢ (𝜑 → < Po 𝐴) & ⊢ (𝜑 → 𝐶 ∈ ( < Chain𝐴)) & ⊢ (𝜑 → 𝐽 ∈ (0..^(♯‘𝐶))) & ⊢ (𝜑 → 𝐼 ∈ (0..^𝐽)) ⇒ ⊢ (𝜑 → (𝐶‘𝐼) < (𝐶‘𝐽)) | ||
| Theorem | chnso 32913 | A chain induces a total order. (Contributed by Thierry Arnoux, 19-Jun-2025.) |
| ⊢ (( < Po 𝐴 ∧ 𝐶 ∈ ( < Chain𝐴)) → < Or ran 𝐶) | ||
| Theorem | chnccats1 32914 | Extend a chain with a single element. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑇 ∈ ( < Chain𝐴)) & ⊢ (𝜑 → (𝑇 = ∅ ∨ (lastS‘𝑇) < 𝑋)) ⇒ ⊢ (𝜑 → (𝑇 ++ ⟨“𝑋”⟩) ∈ ( < Chain𝐴)) | ||
| Axiom | ax-xrssca 32915 | Assume the scalar component of the extended real structure is the field of the real numbers (this has to be defined in the main body of set.mm). (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| ⊢ ℝfld = (Scalar‘ℝ*𝑠) | ||
| Axiom | ax-xrsvsca 32916 | Assume the scalar product of the extended real structure is the extended real number multiplication operation (this has to be defined in the main body of set.mm). (Contributed by Thierry Arnoux, 22-Oct-2017.) |
| ⊢ ·e = ( ·𝑠 ‘ℝ*𝑠) | ||
| Theorem | xrs0 32917 | The zero of the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13257 and df-xrs 17501), however it has a zero. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
| ⊢ 0 = (0g‘ℝ*𝑠) | ||
| Theorem | xrslt 32918 | The "strictly less than" relation for the extended real structure. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ < = (lt‘ℝ*𝑠) | ||
| Theorem | xrsinvgval 32919 | The inversion operation in the extended real numbers. The extended real is not a group, as its addition is not associative. (cf. xaddass 13257 and df-xrs 17501), however it has an inversion operation. (Contributed by Thierry Arnoux, 13-Jun-2017.) |
| ⊢ (𝐵 ∈ ℝ* → ((invg‘ℝ*𝑠)‘𝐵) = -𝑒𝐵) | ||
| Theorem | xrsmulgzz 32920 | The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
| ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵)) | ||
| Theorem | xrstos 32921 | The extended real numbers form a toset. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
| ⊢ ℝ*𝑠 ∈ Toset | ||
| Theorem | xrsclat 32922 | The extended real numbers form a complete lattice. (Contributed by Thierry Arnoux, 15-Feb-2018.) |
| ⊢ ℝ*𝑠 ∈ CLat | ||
| Theorem | xrsp0 32923 | The poset 0 of the extended real numbers is minus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) (Proof shortened by AV, 28-Sep-2020.) |
| ⊢ -∞ = (0.‘ℝ*𝑠) | ||
| Theorem | xrsp1 32924 | The poset 1 of the extended real numbers is plus infinity. (Contributed by Thierry Arnoux, 18-Feb-2018.) |
| ⊢ +∞ = (1.‘ℝ*𝑠) | ||
| Theorem | xrge0base 32925 | The base of the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
| ⊢ (0[,]+∞) = (Base‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
| Theorem | xrge00 32926 | The zero of the extended nonnegative real numbers monoid. (Contributed by Thierry Arnoux, 30-Jan-2017.) |
| ⊢ 0 = (0g‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
| Theorem | xrge0plusg 32927 | The additive law of the extended nonnegative real numbers monoid is the addition in the extended real numbers. (Contributed by Thierry Arnoux, 20-Mar-2017.) |
| ⊢ +𝑒 = (+g‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
| Theorem | xrge0le 32928 | The "less than or equal to" relation in the extended real numbers. (Contributed by Thierry Arnoux, 14-Mar-2018.) |
| ⊢ ≤ = (le‘(ℝ*𝑠 ↾s (0[,]+∞))) | ||
| Theorem | xrge0mulgnn0 32929 | The group multiple function in the extended nonnegative real numbers. (Contributed by Thierry Arnoux, 14-Jun-2017.) |
| ⊢ ((𝐴 ∈ ℕ0 ∧ 𝐵 ∈ (0[,]+∞)) → (𝐴(.g‘(ℝ*𝑠 ↾s (0[,]+∞)))𝐵) = (𝐴 ·e 𝐵)) | ||
| Theorem | xrge0addass 32930 | Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) | ||
| Theorem | xrge0addgt0 32931 | The sum of nonnegative and positive numbers is positive. See addgtge0 11717. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
| ⊢ (((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) ∧ 0 < 𝐴) → 0 < (𝐴 +𝑒 𝐵)) | ||
| Theorem | xrge0adddir 32932 | Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) | ||
| Theorem | xrge0adddi 32933 | Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝐶 ·e (𝐴 +𝑒 𝐵)) = ((𝐶 ·e 𝐴) +𝑒 (𝐶 ·e 𝐵))) | ||
| Theorem | xrge0npcan 32934 | Extended nonnegative real version of npcan 11483. (Contributed by Thierry Arnoux, 9-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐵 ≤ 𝐴) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴) | ||
| Theorem | fsumrp0cl 32935* | Closure of a finite sum of nonnegative reals. (Contributed by Thierry Arnoux, 25-Jun-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ (0[,)+∞)) | ||
| Theorem | mndcld 32936 | Closure of the operation of a monoid. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝐵) | ||
| Theorem | mndassd 32937 | A monoid operation is associative. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍))) | ||
| Theorem | mndlrinv 32938 | In a monoid, if an element 𝑋 has both a left inverse 𝑀 and a right inverse 𝑁, they are equal. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 0 = (0g‘𝐸) & ⊢ + = (+g‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ 𝐵) & ⊢ (𝜑 → (𝑀 + 𝑋) = 0 ) & ⊢ (𝜑 → (𝑋 + 𝑁) = 0 ) ⇒ ⊢ (𝜑 → 𝑀 = 𝑁) | ||
| Theorem | mndlrinvb 32939* | In a monoid, if an element has both a left-inverse and a right-inverse, they are equal. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 0 = (0g‘𝐸) & ⊢ + = (+g‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((∃𝑢 ∈ 𝐵 (𝑋 + 𝑢) = 0 ∧ ∃𝑣 ∈ 𝐵 (𝑣 + 𝑋) = 0 ) ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 ))) | ||
| Theorem | mndlactf1 32940* | If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐹 is injective. See also grplactf1o 19012. Remark in chapter I. of [BourbakiAlg1] p. 17 . (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 0 = (0g‘𝐸) & ⊢ + = (+g‘𝐸) & ⊢ 𝐹 = (𝑎 ∈ 𝐵 ↦ (𝑋 + 𝑎)) & ⊢ (𝜑 → 𝐸 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑌 + 𝑋) = 0 ) ⇒ ⊢ (𝜑 → 𝐹:𝐵–1-1→𝐵) | ||
| Theorem | mndlactfo 32941* | An element 𝑋 of a monoid 𝐸 is left-invertible iff its left-translation 𝐹 is surjective. See also grplactf1o 19012. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 0 = (0g‘𝐸) & ⊢ + = (+g‘𝐸) & ⊢ 𝐹 = (𝑎 ∈ 𝐵 ↦ (𝑋 + 𝑎)) & ⊢ (𝜑 → 𝐸 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝐵–onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 (𝑋 + 𝑦) = 0 )) | ||
| Theorem | mndractf1 32942* | If an element 𝑋 of a monoid 𝐸 is right-invertible, with inverse 𝑌, then its left-translation 𝐺 is injective. See also grplactf1o 19012. Remark in chapter I. of [BourbakiAlg1] p. 17 . (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 0 = (0g‘𝐸) & ⊢ + = (+g‘𝐸) & ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ (𝑎 + 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑋 + 𝑌) = 0 ) ⇒ ⊢ (𝜑 → 𝐺:𝐵–1-1→𝐵) | ||
| Theorem | mndractfo 32943* | An element 𝑋 of a monoid 𝐸 is right-invertible iff its right-translation 𝐺 is surjective. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 0 = (0g‘𝐸) & ⊢ + = (+g‘𝐸) & ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ (𝑎 + 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺:𝐵–onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 (𝑦 + 𝑋) = 0 )) | ||
| Theorem | mndlactf1o 32944* | An element 𝑋 of a monoid 𝐸 is invertible iff its left-translation 𝐹 is bijective. See also grplactf1o 19012. Remark in chapter I. of [BourbakiAlg1] p. 17. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 0 = (0g‘𝐸) & ⊢ + = (+g‘𝐸) & ⊢ 𝐹 = (𝑎 ∈ 𝐵 ↦ (𝑋 + 𝑎)) & ⊢ (𝜑 → 𝐸 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐹:𝐵–1-1-onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 ))) | ||
| Theorem | mndractf1o 32945* | An element 𝑋 of a monoid 𝐸 is invertible iff its right-translation 𝐺 is bijective. See also mndlactf1o 32944. Remark in chapter I. of [BourbakiAlg1] p. 17 . (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 0 = (0g‘𝐸) & ⊢ + = (+g‘𝐸) & ⊢ 𝐺 = (𝑎 ∈ 𝐵 ↦ (𝑎 + 𝑋)) & ⊢ (𝜑 → 𝐸 ∈ Mnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺:𝐵–1-1-onto→𝐵 ↔ ∃𝑦 ∈ 𝐵 ((𝑋 + 𝑦) = 0 ∧ (𝑦 + 𝑋) = 0 ))) | ||
| Theorem | cmn4d 32946 | Commutative/associative law for commutative monoids. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊))) | ||
| Theorem | cmn246135 32947 | Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33181. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → 𝑉 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑌 + (𝑈 + 𝑊)) + (𝑋 + (𝑍 + 𝑉)))) | ||
| Theorem | cmn145236 32948 | Rearrange terms in a commutative monoid sum. Lemma for rlocaddval 33181. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑈 ∈ 𝐵) & ⊢ (𝜑 → 𝑉 ∈ 𝐵) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) ⇒ ⊢ (𝜑 → ((𝑋 + 𝑌) + ((𝑍 + 𝑈) + (𝑉 + 𝑊))) = ((𝑋 + (𝑈 + 𝑉)) + (𝑌 + (𝑍 + 𝑊)))) | ||
| Theorem | submcld 32949 | Submonoids are closed under the monoid operation. (Contributed by Thierry Arnoux, 4-May-2025.) |
| ⊢ + = (+g‘𝑀) & ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝑀)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑆) | ||
| Theorem | abliso 32950 | The image of an Abelian group by a group isomorphism is also Abelian. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
| ⊢ ((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) → 𝑁 ∈ Abel) | ||
| Theorem | lmhmghmd 32951 | A module homomorphism is a group homomorphism. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMHom 𝑇)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑆 GrpHom 𝑇)) | ||
| Theorem | mhmimasplusg 32952 | Value of the operation of the surjective image. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑊 = (𝐹 “s 𝑉) & ⊢ 𝐵 = (Base‘𝑉) & ⊢ 𝐶 = (Base‘𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹:𝐵–onto→𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑉 MndHom 𝑊)) & ⊢ + = (+g‘𝑉) & ⊢ ⨣ = (+g‘𝑊) ⇒ ⊢ (𝜑 → ((𝐹‘𝑋) ⨣ (𝐹‘𝑌)) = (𝐹‘(𝑋 + 𝑌))) | ||
| Theorem | lmhmimasvsca 32953 | Value of the scalar product of the surjective image of a module. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑊 = (𝐹 “s 𝑉) & ⊢ 𝐵 = (Base‘𝑉) & ⊢ 𝐶 = (Base‘𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝐹:𝐵–onto→𝐶) & ⊢ (𝜑 → 𝐹 ∈ (𝑉 LMHom 𝑊)) & ⊢ · = ( ·𝑠 ‘𝑉) & ⊢ × = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘(Scalar‘𝑉)) ⇒ ⊢ (𝜑 → (𝑋 × (𝐹‘𝑌)) = (𝐹‘(𝑋 · 𝑌))) | ||
| Theorem | grpsubcld 32954 | Closure of group subtraction. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝐵) | ||
| Theorem | subgcld 32955 | A subgroup is closed under group operation. (Contributed by Thierry Arnoux, 3-Jun-2025.) |
| ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑆) | ||
| Theorem | subgsubcld 32956 | A subgroup is closed under group subtraction. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ 𝑆) & ⊢ (𝜑 → 𝑌 ∈ 𝑆) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ 𝑆) | ||
| Theorem | subgmulgcld 32957 | Closure of the group multiple within a subgroup. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ · = (.g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝑅)) & ⊢ (𝜑 → 𝑍 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑍 · 𝐴) ∈ 𝑆) | ||
| Theorem | gsumsubg 32958 | The group sum in a subgroup is the same as the group sum. (Contributed by Thierry Arnoux, 28-May-2023.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐵 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐻 Σg 𝐹)) | ||
| Theorem | gsumsra 32959 | The group sum in a subring algebra is the same as the ring's group sum. (Contributed by Thierry Arnoux, 28-May-2023.) |
| ⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝑈) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝑊) & ⊢ (𝜑 → 𝐵 ⊆ (Base‘𝑅)) ⇒ ⊢ (𝜑 → (𝑅 Σg 𝐹) = (𝐴 Σg 𝐹)) | ||
| Theorem | gsummpt2co 32960* | Split a finite sum into a sum of a collection of sums over disjoint subsets. (Contributed by Thierry Arnoux, 27-Mar-2018.) |
| ⊢ 𝐵 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐷 ∈ 𝐸) & ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐷) ⇒ ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ 𝐸 ↦ (𝑊 Σg (𝑥 ∈ (◡𝐹 “ {𝑦}) ↦ 𝐶))))) | ||
| Theorem | gsummpt2d 32961* | Express a finite sum over a two-dimensional range as a double sum. See also gsum2d 19938. (Contributed by Thierry Arnoux, 27-Apr-2020.) |
| ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑦𝜑 & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → 𝐶 = 𝐷) & ⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑊 ∈ CMnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))))) | ||
| Theorem | lmodvslmhm 32962* | Scalar multiplication in a left module by a fixed element is a group homomorphism. (Contributed by Thierry Arnoux, 12-Jun-2023.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ ((𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑥 ∈ 𝐾 ↦ (𝑥 · 𝑌)) ∈ (𝐹 GrpHom 𝑊)) | ||
| Theorem | gsumvsmul1 32963* | Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 20261, since every ring is a left module over itself. (Contributed by Thierry Arnoux, 12-Jun-2023.) |
| ⊢ 𝐵 = (Base‘𝑅) & ⊢ 𝑆 = (Scalar‘𝑅) & ⊢ 𝐾 = (Base‘𝑆) & ⊢ 0 = (0g‘𝑆) & ⊢ · = ( ·𝑠 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ LMod) & ⊢ (𝜑 → 𝑆 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝑋) finSupp 0 ) ⇒ ⊢ (𝜑 → (𝑅 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = ((𝑆 Σg (𝑘 ∈ 𝐴 ↦ 𝑋)) · 𝑌)) | ||
| Theorem | gsummptres 32964* | Extend a finite group sum by padding outside with zeroes. Proof generated using OpenAI's proof assistant. (Contributed by Thierry Arnoux, 11-Jul-2020.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝐷)) → 𝐶 = 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝐺 Σg (𝑥 ∈ (𝐴 ∩ 𝐷) ↦ 𝐶))) | ||
| Theorem | gsummptres2 32965* | Extend a finite group sum by padding outside with zeroes. (Contributed by Thierry Arnoux, 22-Jun-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ 𝑆)) → 𝑌 = 0 ) & ⊢ (𝜑 → 𝑆 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑆 ⊆ 𝐴) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝑌)) = (𝐺 Σg (𝑥 ∈ 𝑆 ↦ 𝑌))) | ||
| Theorem | gsummptfsf1o 32966* | Re-index a finite group sum using a bijection. A version of gsummptf1o 19929 expressed using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ Ⅎ𝑥𝐻 & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝑥 = 𝐸 → 𝐶 = 𝐻) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) finSupp 0 ) & ⊢ (𝜑 → 𝐹 ⊆ 𝐵) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐹) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐷) → 𝐸 ∈ 𝐴) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃!𝑦 ∈ 𝐷 𝑥 = 𝐸) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝐺 Σg (𝑦 ∈ 𝐷 ↦ 𝐻))) | ||
| Theorem | gsumfs2d 32967* | Express a finite sum over a two-dimensional range as a double sum. Version of gsum2d 19938 using finite support. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ Ⅎ𝑥𝜑 & ⊢ 𝐵 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ (𝜑 → 𝑊 ∈ CMnd) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝑊 Σg 𝐹) = (𝑊 Σg (𝑥 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑦 ∈ (𝐴 “ {𝑥}) ↦ (𝐹‘⟨𝑥, 𝑦⟩)))))) | ||
| Theorem | gsumzresunsn 32968 | Append an element to a finite group sum expressed as a function restriction. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ 𝑌 = (𝐹‘𝑋) & ⊢ (𝜑 → 𝐹:𝐶⟶𝐵) & ⊢ (𝜑 → 𝐴 ⊆ 𝐶) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ¬ 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑋 ∈ 𝐶) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝐹 “ (𝐴 ∪ {𝑋})) ⊆ (𝑍‘(𝐹 “ (𝐴 ∪ {𝑋})))) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝐹 ↾ (𝐴 ∪ {𝑋}))) = ((𝐺 Σg (𝐹 ↾ 𝐴)) + 𝑌)) | ||
| Theorem | gsumpart 32969* | Express a group sum as a double sum, grouping along a (possibly infinite) partition. (Contributed by Thierry Arnoux, 22-Jun-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝑊) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶) & ⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ 𝐶))))) | ||
| Theorem | gsumtp 32970* | Group sum of an unordered triple. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝑘 = 𝑀 → 𝐴 = 𝐶) & ⊢ (𝑘 = 𝑁 → 𝐴 = 𝐷) & ⊢ (𝑘 = 𝑂 → 𝐴 = 𝐸) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝑀 ∈ 𝑉) & ⊢ (𝜑 → 𝑁 ∈ 𝑊) & ⊢ (𝜑 → 𝑂 ∈ 𝑋) & ⊢ (𝜑 → 𝑀 ≠ 𝑁) & ⊢ (𝜑 → 𝑁 ≠ 𝑂) & ⊢ (𝜑 → 𝑀 ≠ 𝑂) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) & ⊢ (𝜑 → 𝐷 ∈ 𝐵) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐺 Σg (𝑘 ∈ {𝑀, 𝑁, 𝑂} ↦ 𝐴)) = ((𝐶 + 𝐷) + 𝐸)) | ||
| Theorem | gsumzrsum 32971* | Relate a group sum on ℤring to a finite sum on the complex numbers. See also gsumfsum 21387. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℤ) ⇒ ⊢ (𝜑 → (ℤring Σg (𝑘 ∈ 𝐴 ↦ 𝐵)) = Σ𝑘 ∈ 𝐴 𝐵) | ||
| Theorem | gsummulgc2 32972* | A finite group sum multiplied by a constant. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ · = (.g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ Grp) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑋 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝑀 Σg (𝑘 ∈ 𝐴 ↦ (𝑋 · 𝑌))) = (Σ𝑘 ∈ 𝐴 𝑋 · 𝑌)) | ||
| Theorem | gsumhashmul 32973* | Express a group sum by grouping by nonzero values. (Contributed by Thierry Arnoux, 22-Jun-2024.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ CMnd) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 0 ) ⇒ ⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((♯‘(◡𝐹 “ {𝑥})) · 𝑥)))) | ||
| Theorem | xrge0tsmsd 32974* | Any finite or infinite sum in the nonnegative extended reals is uniquely convergent to the supremum of all finite sums. (Contributed by Mario Carneiro, 13-Sep-2015.) (Revised by Thierry Arnoux, 30-Jan-2017.) |
| ⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) & ⊢ (𝜑 → 𝑆 = sup(ran (𝑠 ∈ (𝒫 𝐴 ∩ Fin) ↦ (𝐺 Σg (𝐹 ↾ 𝑠))), ℝ*, < )) ⇒ ⊢ (𝜑 → (𝐺 tsums 𝐹) = {𝑆}) | ||
| Theorem | xrge0tsmsbi 32975 | Any limit of a finite or infinite sum in the nonnegative extended reals is the union of the sets limits, since this set is a singleton. (Contributed by Thierry Arnoux, 23-Jun-2017.) |
| ⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) ⇒ ⊢ (𝜑 → (𝐶 ∈ (𝐺 tsums 𝐹) ↔ 𝐶 = ∪ (𝐺 tsums 𝐹))) | ||
| Theorem | xrge0tsmseq 32976 | Any limit of a finite or infinite sum in the nonnegative extended reals is the union of the sets limits, since this set is a singleton. (Contributed by Thierry Arnoux, 24-Mar-2017.) |
| ⊢ 𝐺 = (ℝ*𝑠 ↾s (0[,]+∞)) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐹:𝐴⟶(0[,]+∞)) & ⊢ (𝜑 → 𝐶 ∈ (𝐺 tsums 𝐹)) ⇒ ⊢ (𝜑 → 𝐶 = ∪ (𝐺 tsums 𝐹)) | ||
| Theorem | gsumwun 32977* | In a commutative ring, a group sum of a word 𝑊 of characters taken from two submonoids 𝐸 and 𝐹 can be written as a simple sum. (Contributed by Thierry Arnoux, 6-Oct-2025.) |
| ⊢ + = (+g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ CMnd) & ⊢ (𝜑 → 𝐸 ∈ (SubMnd‘𝑀)) & ⊢ (𝜑 → 𝐹 ∈ (SubMnd‘𝑀)) & ⊢ (𝜑 → 𝑊 ∈ Word (𝐸 ∪ 𝐹)) ⇒ ⊢ (𝜑 → ∃𝑒 ∈ 𝐸 ∃𝑓 ∈ 𝐹 (𝑀 Σg 𝑊) = (𝑒 + 𝑓)) | ||
| Theorem | gsumwrd2dccatlem 32978* | Lemma for gsumwrd2dccat 32979. Expose a bijection 𝐹 between (ordered) pairs of words and words with a length of a subword. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝑈 = ∪ 𝑤 ∈ Word 𝐴({𝑤} × (0...(♯‘𝑤))) & ⊢ 𝐹 = (𝑎 ∈ (Word 𝐴 × Word 𝐴) ↦ ⟨((1st ‘𝑎) ++ (2nd ‘𝑎)), (♯‘(1st ‘𝑎))⟩) & ⊢ 𝐺 = (𝑏 ∈ 𝑈 ↦ ⟨((1st ‘𝑏) prefix (2nd ‘𝑏)), ((1st ‘𝑏) substr ⟨(2nd ‘𝑏), (♯‘(1st ‘𝑏))⟩)⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐹:(Word 𝐴 × Word 𝐴)–1-1-onto→𝑈 ∧ ◡𝐹 = 𝐺)) | ||
| Theorem | gsumwrd2dccat 32979* | Rewrite a sum ranging over pairs of words as a sum of sums over concatenated subwords. (Contributed by Thierry Arnoux, 5-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (0g‘𝑀) & ⊢ (𝜑 → 𝐹:(Word 𝐴 × Word 𝐴)⟶𝐵) & ⊢ (𝜑 → 𝐹 finSupp 𝑍) & ⊢ (𝜑 → 𝑀 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → (𝑀 Σg 𝐹) = (𝑀 Σg (𝑤 ∈ Word 𝐴 ↦ (𝑀 Σg (𝑗 ∈ (0...(♯‘𝑤)) ↦ (𝐹‘⟨(𝑤 prefix 𝑗), (𝑤 substr ⟨𝑗, (♯‘𝑤)⟩)⟩)))))) | ||
| Theorem | cntzun 32980 | The centralizer of a union is the intersection of the centralizers. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) → (𝑍‘(𝑋 ∪ 𝑌)) = ((𝑍‘𝑋) ∩ (𝑍‘𝑌))) | ||
| Theorem | cntzsnid 32981 | The centralizer of the identity element is the whole base set. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) & ⊢ 0 = (0g‘𝑀) ⇒ ⊢ (𝑀 ∈ Mnd → (𝑍‘{ 0 }) = 𝐵) | ||
| Theorem | cntrcrng 32982 | The center of a ring is a commutative ring. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
| ⊢ 𝑍 = (𝑅 ↾s (Cntr‘(mulGrp‘𝑅))) ⇒ ⊢ (𝑅 ∈ Ring → 𝑍 ∈ CRing) | ||
| Syntax | comnd 32983 | Extend class notation with the class of all right ordered monoids. |
| class oMnd | ||
| Syntax | cogrp 32984 | Extend class notation with the class of all right ordered groups. |
| class oGrp | ||
| Definition | df-omnd 32985* | Define class of all right ordered monoids. An ordered monoid is a monoid with a total ordering compatible with its operation. It is possible to use this definition also for left ordered monoids, by applying it to (oppg‘𝑀). (Contributed by Thierry Arnoux, 13-Mar-2018.) |
| ⊢ oMnd = {𝑔 ∈ Mnd ∣ [(Base‘𝑔) / 𝑣][(+g‘𝑔) / 𝑝][(le‘𝑔) / 𝑙](𝑔 ∈ Toset ∧ ∀𝑎 ∈ 𝑣 ∀𝑏 ∈ 𝑣 ∀𝑐 ∈ 𝑣 (𝑎𝑙𝑏 → (𝑎𝑝𝑐)𝑙(𝑏𝑝𝑐)))} | ||
| Definition | df-ogrp 32986 | Define class of all ordered groups. An ordered group is a group with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
| ⊢ oGrp = (Grp ∩ oMnd) | ||
| Theorem | isomnd 32987* | A (left) ordered monoid is a monoid with a total ordering compatible with its operation. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ ≤ = (le‘𝑀) ⇒ ⊢ (𝑀 ∈ oMnd ↔ (𝑀 ∈ Mnd ∧ 𝑀 ∈ Toset ∧ ∀𝑎 ∈ 𝐵 ∀𝑏 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝑎 ≤ 𝑏 → (𝑎 + 𝑐) ≤ (𝑏 + 𝑐)))) | ||
| Theorem | isogrp 32988 | A (left-)ordered group is a group with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ (𝐺 ∈ oGrp ↔ (𝐺 ∈ Grp ∧ 𝐺 ∈ oMnd)) | ||
| Theorem | ogrpgrp 32989 | A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.) |
| ⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp) | ||
| Theorem | omndmnd 32990 | A left-ordered monoid is a monoid. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
| ⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Mnd) | ||
| Theorem | omndtos 32991 | A left-ordered monoid is a totally ordered set. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
| ⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset) | ||
| Theorem | omndadd 32992 | In an ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 + 𝑍) ≤ (𝑌 + 𝑍)) | ||
| Theorem | omndaddr 32993 | In a right ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ (((oppg‘𝑀) ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑍 + 𝑋) ≤ (𝑍 + 𝑌)) | ||
| Theorem | omndadd2d 32994 | In a commutative left ordered monoid, the ordering is compatible with monoid addition. Double addition version. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ oMnd) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≤ 𝑍) & ⊢ (𝜑 → 𝑌 ≤ 𝑊) & ⊢ (𝜑 → 𝑀 ∈ CMnd) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ≤ (𝑍 + 𝑊)) | ||
| Theorem | omndadd2rd 32995 | In a left- and right- ordered monoid, the ordering is compatible with monoid addition. Double addition version. (Contributed by Thierry Arnoux, 2-May-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ + = (+g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ oMnd) & ⊢ (𝜑 → 𝑊 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 ≤ 𝑍) & ⊢ (𝜑 → 𝑌 ≤ 𝑊) & ⊢ (𝜑 → (oppg‘𝑀) ∈ oMnd) ⇒ ⊢ (𝜑 → (𝑋 + 𝑌) ≤ (𝑍 + 𝑊)) | ||
| Theorem | submomnd 32996 | A submonoid of an ordered monoid is also ordered. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ oMnd) | ||
| Theorem | xrge0omnd 32997 | The nonnegative extended real numbers form an ordered monoid. (Contributed by Thierry Arnoux, 22-Mar-2018.) |
| ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ oMnd | ||
| Theorem | omndmul2 32998 | In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ · = (.g‘𝑀) & ⊢ 0 = (0g‘𝑀) ⇒ ⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑁 ∈ ℕ0) ∧ 0 ≤ 𝑋) → 0 ≤ (𝑁 · 𝑋)) | ||
| Theorem | omndmul3 32999 | In an ordered monoid, the ordering is compatible with group power. This version does not require the monoid to be commutative. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ · = (.g‘𝑀) & ⊢ 0 = (0g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ oMnd) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑃 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ≤ 𝑃) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 0 ≤ 𝑋) ⇒ ⊢ (𝜑 → (𝑁 · 𝑋) ≤ (𝑃 · 𝑋)) | ||
| Theorem | omndmul 33000 | In a commutative ordered monoid, the ordering is compatible with group power. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ · = (.g‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ oMnd) & ⊢ (𝜑 → 𝑀 ∈ CMnd) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → (𝑁 · 𝑋) ≤ (𝑁 · 𝑌)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |