HomeTheorem List (p. 313 of 464)
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. 313 of 464) | < 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-29181) |
Hilbert Space Explorer
(29182-30704) |
Users' Mathboxes
(30705-46395) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | xrge0addass 31201 | Associativity of extended nonnegative real addition. (Contributed by Thierry Arnoux, 8-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) +𝑒 𝐶) = (𝐴 +𝑒 (𝐵 +𝑒 𝐶))) | ||
| Theorem | xrge0addgt0 31202 | The sum of nonnegative and positive numbers is positive. See addgtge0 11393. (Contributed by Thierry Arnoux, 6-Jul-2017.) |
| ⊢ (((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞)) ∧ 0 < 𝐴) → 0 < (𝐴 +𝑒 𝐵)) | ||
| Theorem | xrge0adddir 31203 | Right-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 30-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → ((𝐴 +𝑒 𝐵) ·e 𝐶) = ((𝐴 ·e 𝐶) +𝑒 (𝐵 ·e 𝐶))) | ||
| Theorem | xrge0adddi 31204 | Left-distributivity of extended nonnegative real multiplication over addition. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐶 ∈ (0[,]+∞)) → (𝐶 ·e (𝐴 +𝑒 𝐵)) = ((𝐶 ·e 𝐴) +𝑒 (𝐶 ·e 𝐵))) | ||
| Theorem | xrge0npcan 31205 | Extended nonnegative real version of npcan 11160. (Contributed by Thierry Arnoux, 9-Jun-2017.) |
| ⊢ ((𝐴 ∈ (0[,]+∞) ∧ 𝐵 ∈ (0[,]+∞) ∧ 𝐵 ≤ 𝐴) → ((𝐴 +𝑒 -𝑒𝐵) +𝑒 𝐵) = 𝐴) | ||
| Theorem | fsumrp0cl 31206* | Closure of a finite sum of nonnegative reals. (Contributed by Thierry Arnoux, 25-Jun-2017.) |
| ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ (0[,)+∞)) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 ∈ (0[,)+∞)) | ||
| Theorem | abliso 31207 | The image of an Abelian group by a group isomorphism is also Abelian. (Contributed by Thierry Arnoux, 8-Mar-2018.) |
| ⊢ ((𝑀 ∈ Abel ∧ 𝐹 ∈ (𝑀 GrpIso 𝑁)) → 𝑁 ∈ Abel) | ||
| Theorem | gsumsubg 31208 | 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 31209 | 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 31210* | 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 31211* | Express a finite sum over a two-dimensional range as a double sum. See also gsum2d 19488. (Contributed by Thierry Arnoux, 27-Apr-2020.) |
| ⊢ Ⅎ𝑧𝐶 & ⊢ Ⅎ𝑦𝜑 & ⊢ 𝐵 = (Base‘𝑊) & ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → 𝐶 = 𝐷) & ⊢ (𝜑 → Rel 𝐴) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝑊 ∈ CMnd) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷))))) | ||
| Theorem | lmodvslmhm 31212* | 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 31213* | Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 19760, 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 31214* | 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 31215* | 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 | gsumzresunsn 31216 | 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 31217* | 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 | gsumhashmul 31218* | 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 31219* | 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 31220 | 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 31221 | 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 | cntzun 31222 | The centralizer of a union is the intersection of the centralizers. (Contributed by Thierry Arnoux, 27-Nov-2023.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ 𝑍 = (Cntz‘𝑀) ⇒ ⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) → (𝑍‘(𝑋 ∪ 𝑌)) = ((𝑍‘𝑋) ∩ (𝑍‘𝑌))) | ||
| Theorem | cntzsnid 31223 | 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 31224 | The center of a ring is a commutative ring. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
| ⊢ 𝑍 = (𝑅 ↾s (Cntr‘(mulGrp‘𝑅))) ⇒ ⊢ (𝑅 ∈ Ring → 𝑍 ∈ CRing) | ||
| Syntax | comnd 31225 | Extend class notation with the class of all right ordered monoids. |
| class oMnd | ||
| Syntax | cogrp 31226 | Extend class notation with the class of all right ordered groups. |
| class oGrp | ||
| Definition | df-omnd 31227* | 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 31228 | 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 31229* | 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 31230 | 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 31231 | A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.) |
| ⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp) | ||
| Theorem | omndmnd 31232 | A left-ordered monoid is a monoid. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
| ⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Mnd) | ||
| Theorem | omndtos 31233 | A left-ordered monoid is a totally ordered set. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
| ⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset) | ||
| Theorem | omndadd 31234 | In an ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ + = (+g‘𝑀) ⇒ ⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 + 𝑍) ≤ (𝑌 + 𝑍)) | ||
| Theorem | omndaddr 31235 | 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 31236 | 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 31237 | 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 31238 | A submonoid of an ordered monoid is also ordered. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
| ⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ oMnd) | ||
| Theorem | xrge0omnd 31239 | The nonnegative extended real numbers form an ordered monoid. (Contributed by Thierry Arnoux, 22-Mar-2018.) |
| ⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ oMnd | ||
| Theorem | omndmul2 31240 | 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 31241 | 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 31242 | 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) & ⊢ (𝜑 → 𝑋 ≤ 𝑌) ⇒ ⊢ (𝜑 → (𝑁 · 𝑋) ≤ (𝑁 · 𝑌)) | ||
| Theorem | ogrpinv0le 31243 | In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ≤ = (le‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) → ( 0 ≤ 𝑋 ↔ (𝐼‘𝑋) ≤ 0 )) | ||
| Theorem | ogrpsub 31244 | In an ordered group, the ordering is compatible with group subtraction. (Contributed by Thierry Arnoux, 30-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ≤ = (le‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 − 𝑍) ≤ (𝑌 − 𝑍)) | ||
| Theorem | ogrpaddlt 31245 | In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 20-Jan-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 + 𝑍) < (𝑌 + 𝑍)) | ||
| Theorem | ogrpaddltbi 31246 | In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ + = (+g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 < 𝑌 ↔ (𝑋 + 𝑍) < (𝑌 + 𝑍))) | ||
| Theorem | ogrpaddltrd 31247 | In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → (oppg‘𝐺) ∈ oGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) & ⊢ (𝜑 → 𝑋 < 𝑌) ⇒ ⊢ (𝜑 → (𝑍 + 𝑋) < (𝑍 + 𝑌)) | ||
| Theorem | ogrpaddltrbid 31248 | In a right ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 4-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ 𝑉) & ⊢ (𝜑 → (oppg‘𝐺) ∈ oGrp) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → 𝑍 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑋 < 𝑌 ↔ (𝑍 + 𝑋) < (𝑍 + 𝑌))) | ||
| Theorem | ogrpsublt 31249 | In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 − 𝑍) < (𝑌 − 𝑍)) | ||
| Theorem | ogrpinv0lt 31250 | In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ oGrp ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ (𝐼‘𝑋) < 0 )) | ||
| Theorem | ogrpinvlt 31251 | In an ordered group, the ordering is compatible with group inverse. (Contributed by Thierry Arnoux, 3-Sep-2018.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ < = (lt‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) ⇒ ⊢ (((𝐺 ∈ oGrp ∧ (oppg‘𝐺) ∈ oGrp) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ (𝐼‘𝑌) < (𝐼‘𝑋))) | ||
| Theorem | gsumle 31252 | A finite sum in an ordered monoid is monotonic. This proof would be much easier in an ordered group, where an inverse element would be available. (Contributed by Thierry Arnoux, 13-Mar-2018.) |
| ⊢ 𝐵 = (Base‘𝑀) & ⊢ ≤ = (le‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ oMnd) & ⊢ (𝜑 → 𝑀 ∈ CMnd) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → 𝐹:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐺:𝐴⟶𝐵) & ⊢ (𝜑 → 𝐹 ∘r ≤ 𝐺) ⇒ ⊢ (𝜑 → (𝑀 Σg 𝐹) ≤ (𝑀 Σg 𝐺)) | ||
| Theorem | symgfcoeu 31253* | Uniqueness property of permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐺 = (Base‘(SymGrp‘𝐷)) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑄 = (𝑃 ∘ 𝑝)) | ||
| Theorem | symgcom 31254 | Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
| ⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸)) & ⊢ (𝜑 → (𝑌 ↾ 𝐹) = ( I ↾ 𝐹)) & ⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅) & ⊢ (𝜑 → (𝐸 ∪ 𝐹) = 𝐴) ⇒ ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋)) | ||
| Theorem | symgcom2 31255 | Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 17-Nov-2023.) |
| ⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝑌 ∈ 𝐵) & ⊢ (𝜑 → (dom (𝑋 ∖ I ) ∩ dom (𝑌 ∖ I )) = ∅) ⇒ ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋)) | ||
| Theorem | symgcntz 31256* | All elements of a (finite) set of permutations commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 20-Nov-2023.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑍 = (Cntz‘𝑆) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) & ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 dom (𝑥 ∖ I )) ⇒ ⊢ (𝜑 → 𝐴 ⊆ (𝑍‘𝐴)) | ||
| Theorem | odpmco 31257 | The composition of two odd permutations is even. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐴 = (pmEven‘𝐷) ⇒ ⊢ ((𝐷 ∈ Fin ∧ 𝑋 ∈ (𝐵 ∖ 𝐴) ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → (𝑋 ∘ 𝑌) ∈ 𝐴) | ||
| Theorem | symgsubg 31258 | The value of the group subtraction operation of the symmetric group. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
| ⊢ 𝐺 = (SymGrp‘𝐴) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 ∘ ◡𝑌)) | ||
| Theorem | pmtrprfv2 31259 | In a transposition of two given points, each maps to the other. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑌) = 𝑋) | ||
| Theorem | pmtrcnel 31260 | Composing a permutation 𝐹 with a transposition which results in moving at least one less point. Here the set of points moved by a permutation 𝐹 is expressed as dom (𝐹 ∖ I ). (Contributed by Thierry Arnoux, 16-Nov-2023.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐽 = (𝐹‘𝐼) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ dom (𝐹 ∖ I )) ⇒ ⊢ (𝜑 → dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) ⊆ (dom (𝐹 ∖ I ) ∖ {𝐼})) | ||
| Theorem | pmtrcnel2 31261 | Variation on pmtrcnel 31260. (Contributed by Thierry Arnoux, 16-Nov-2023.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐽 = (𝐹‘𝐼) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ dom (𝐹 ∖ I )) ⇒ ⊢ (𝜑 → (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽}) ⊆ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I )) | ||
| Theorem | pmtrcnelor 31262 | Composing a permutation 𝐹 with a transposition which results in moving one or two less points. (Contributed by Thierry Arnoux, 16-Nov-2023.) |
| ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝐽 = (𝐹‘𝐼) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐼 ∈ dom (𝐹 ∖ I )) & ⊢ 𝐸 = dom (𝐹 ∖ I ) & ⊢ 𝐴 = dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ) ⇒ ⊢ (𝜑 → (𝐴 = (𝐸 ∖ {𝐼, 𝐽}) ∨ 𝐴 = (𝐸 ∖ {𝐼}))) | ||
| Theorem | pmtridf1o 31263 | Transpositions of 𝑋 and 𝑌 (understood to be the identity when 𝑋 = 𝑌), are bijections. (Contributed by Thierry Arnoux, 1-Jan-2022.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ 𝑇 = if(𝑋 = 𝑌, ( I ↾ 𝐴), ((pmTrsp‘𝐴)‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → 𝑇:𝐴–1-1-onto→𝐴) | ||
| Theorem | pmtridfv1 31264 | Value at X of the transposition of 𝑋 and 𝑌 (understood to be the identity when X = Y ). (Contributed by Thierry Arnoux, 3-Jan-2022.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ 𝑇 = if(𝑋 = 𝑌, ( I ↾ 𝐴), ((pmTrsp‘𝐴)‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝑇‘𝑋) = 𝑌) | ||
| Theorem | pmtridfv2 31265 | Value at Y of the transposition of 𝑋 and 𝑌 (understood to be the identity when X = Y ). (Contributed by Thierry Arnoux, 3-Jan-2022.) |
| ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝑋 ∈ 𝐴) & ⊢ (𝜑 → 𝑌 ∈ 𝐴) & ⊢ 𝑇 = if(𝑋 = 𝑌, ( I ↾ 𝐴), ((pmTrsp‘𝐴)‘{𝑋, 𝑌})) ⇒ ⊢ (𝜑 → (𝑇‘𝑌) = 𝑋) | ||
| Theorem | psgnid 31266 | Permutation sign of the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
| ⊢ 𝑆 = (pmSgn‘𝐷) ⇒ ⊢ (𝐷 ∈ Fin → (𝑆‘( I ↾ 𝐷)) = 1) | ||
| Theorem | psgndmfi 31267 | For a finite base set, the permutation sign is defined for all permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝑆 = (pmSgn‘𝐷) & ⊢ 𝐺 = (Base‘(SymGrp‘𝐷)) ⇒ ⊢ (𝐷 ∈ Fin → 𝑆 Fn 𝐺) | ||
| Theorem | pmtrto1cl 31268 | Useful lemma for the following theorems. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) & ⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝑇‘{𝐾, (𝐾 + 1)}) ∈ ran 𝑇) | ||
| Theorem | psgnfzto1stlem 31269* | Lemma for psgnfzto1st 31274. Our permutation of rank (𝑛 + 1) can be written as a permutation of rank 𝑛 composed with a transposition. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) ⇒ ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, (𝐾 + 1), if(𝑖 ≤ (𝐾 + 1), (𝑖 − 1), 𝑖))) = (((pmTrsp‘𝐷)‘{𝐾, (𝐾 + 1)}) ∘ (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐾, if(𝑖 ≤ 𝐾, (𝑖 − 1), 𝑖))))) | ||
| Theorem | fzto1stfv1 31270* | Value of our permutation 𝑃 at 1. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) ⇒ ⊢ (𝐼 ∈ 𝐷 → (𝑃‘1) = 𝐼) | ||
| Theorem | fzto1st1 31271* | Special case where the permutation defined in psgnfzto1st 31274 is the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) ⇒ ⊢ (𝐼 = 1 → 𝑃 = ( I ↾ 𝐷)) | ||
| Theorem | fzto1st 31272* | The function moving one element to the first position (and shifting all elements before it) is a permutation. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐼 ∈ 𝐷 → 𝑃 ∈ 𝐵) | ||
| Theorem | fzto1stinvn 31273* | Value of the inverse of our permutation 𝑃 at 𝐼. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐼 ∈ 𝐷 → (◡𝑃‘𝐼) = 1) | ||
| Theorem | psgnfzto1st 31274* | The permutation sign for moving one element to the first position. (Contributed by Thierry Arnoux, 21-Aug-2020.) |
| ⊢ 𝐷 = (1...𝑁) & ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑆 = (pmSgn‘𝐷) ⇒ ⊢ (𝐼 ∈ 𝐷 → (𝑆‘𝑃) = (-1↑(𝐼 + 1))) | ||
| Syntax | ctocyc 31275 | Extend class notation with the permutation cycle builder. |
| class toCyc | ||
| Definition | df-tocyc 31276* | Define a convenience permutation cycle builder. Given a list of elements to be cycled, in the form of a word, this function produces the corresponding permutation cycle. See definition in [Lang] p. 30. (Contributed by Thierry Arnoux, 19-Sep-2023.) |
| ⊢ toCyc = (𝑑 ∈ V ↦ (𝑤 ∈ {𝑢 ∈ Word 𝑑 ∣ 𝑢:dom 𝑢–1-1→𝑑} ↦ (( I ↾ (𝑑 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤)))) | ||
| Theorem | tocycval 31277* | Value of the cycle builder. (Contributed by Thierry Arnoux, 22-Sep-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) ⇒ ⊢ (𝐷 ∈ 𝑉 → 𝐶 = (𝑤 ∈ {𝑢 ∈ Word 𝐷 ∣ 𝑢:dom 𝑢–1-1→𝐷} ↦ (( I ↾ (𝐷 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤)))) | ||
| Theorem | tocycfv 31278 | Function value of a permutation cycle built from a word. (Contributed by Thierry Arnoux, 18-Sep-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Word 𝐷) & ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) ⇒ ⊢ (𝜑 → (𝐶‘𝑊) = (( I ↾ (𝐷 ∖ ran 𝑊)) ∪ ((𝑊 cyclShift 1) ∘ ◡𝑊))) | ||
| Theorem | tocycfvres1 31279 | A cyclic permutation is a cyclic shift on its orbit. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Word 𝐷) & ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) ⇒ ⊢ (𝜑 → ((𝐶‘𝑊) ↾ ran 𝑊) = ((𝑊 cyclShift 1) ∘ ◡𝑊)) | ||
| Theorem | tocycfvres2 31280 | A cyclic permutation is the identity outside of its orbit. (Contributed by Thierry Arnoux, 15-Oct-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Word 𝐷) & ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) ⇒ ⊢ (𝜑 → ((𝐶‘𝑊) ↾ (𝐷 ∖ ran 𝑊)) = ( I ↾ (𝐷 ∖ ran 𝑊))) | ||
| Theorem | cycpmfvlem 31281 | Lemma for cycpmfv1 31282 and cycpmfv2 31283. (Contributed by Thierry Arnoux, 22-Sep-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Word 𝐷) & ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) & ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝑊))) ⇒ ⊢ (𝜑 → ((𝐶‘𝑊)‘(𝑊‘𝑁)) = (((𝑊 cyclShift 1) ∘ ◡𝑊)‘(𝑊‘𝑁))) | ||
| Theorem | cycpmfv1 31282 | Value of a cycle function for any element but the last. (Contributed by Thierry Arnoux, 22-Sep-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Word 𝐷) & ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) & ⊢ (𝜑 → 𝑁 ∈ (0..^((♯‘𝑊) − 1))) ⇒ ⊢ (𝜑 → ((𝐶‘𝑊)‘(𝑊‘𝑁)) = (𝑊‘(𝑁 + 1))) | ||
| Theorem | cycpmfv2 31283 | Value of a cycle function for the last element of the orbit. (Contributed by Thierry Arnoux, 22-Sep-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Word 𝐷) & ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) & ⊢ (𝜑 → 0 < (♯‘𝑊)) & ⊢ (𝜑 → 𝑁 = ((♯‘𝑊) − 1)) ⇒ ⊢ (𝜑 → ((𝐶‘𝑊)‘(𝑊‘𝑁)) = (𝑊‘0)) | ||
| Theorem | cycpmfv3 31284 | Values outside of the orbit are unchanged by a cycle. (Contributed by Thierry Arnoux, 22-Sep-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Word 𝐷) & ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) & ⊢ (𝜑 → 𝑋 ∈ 𝐷) & ⊢ (𝜑 → ¬ 𝑋 ∈ ran 𝑊) ⇒ ⊢ (𝜑 → ((𝐶‘𝑊)‘𝑋) = 𝑋) | ||
| Theorem | cycpmcl 31285 | Cyclic permutations are permutations. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ Word 𝐷) & ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷) & ⊢ 𝑆 = (SymGrp‘𝐷) ⇒ ⊢ (𝜑 → (𝐶‘𝑊) ∈ (Base‘𝑆)) | ||
| Theorem | tocycf 31286* | The permutation cycle builder as a function. (Contributed by Thierry Arnoux, 25-Sep-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) & ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝑆) ⇒ ⊢ (𝐷 ∈ 𝑉 → 𝐶:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵) | ||
| Theorem | tocyc01 31287 | Permutation cycles built from the empty set or a singleton are the identity. (Contributed by Thierry Arnoux, 21-Nov-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ (dom 𝐶 ∩ (◡♯ “ {0, 1}))) → (𝐶‘𝑊) = ( I ↾ 𝐷)) | ||
| Theorem | cycpm2tr 31288 | A cyclic permutation of 2 elements is a transposition. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝐷) & ⊢ (𝜑 → 𝐽 ∈ 𝐷) & ⊢ (𝜑 → 𝐼 ≠ 𝐽) & ⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽”⟩) = (𝑇‘{𝐼, 𝐽})) | ||
| Theorem | cycpm2cl 31289 | Closure for the 2-cycles. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝐷) & ⊢ (𝜑 → 𝐽 ∈ 𝐷) & ⊢ (𝜑 → 𝐼 ≠ 𝐽) & ⊢ 𝑆 = (SymGrp‘𝐷) ⇒ ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆)) | ||
| Theorem | cyc2fv1 31290 | Function value of a 2-cycle at the first point. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝐷) & ⊢ (𝜑 → 𝐽 ∈ 𝐷) & ⊢ (𝜑 → 𝐼 ≠ 𝐽) & ⊢ 𝑆 = (SymGrp‘𝐷) ⇒ ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽”⟩)‘𝐼) = 𝐽) | ||
| Theorem | cyc2fv2 31291 | Function value of a 2-cycle at the second point. (Contributed by Thierry Arnoux, 24-Sep-2023.) |
| ⊢ 𝐶 = (toCyc‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝐼 ∈ 𝐷) & ⊢ (𝜑 → 𝐽 ∈ 𝐷) & ⊢ (𝜑 → 𝐼 ≠ 𝐽) & ⊢ 𝑆 = (SymGrp‘𝐷) ⇒ ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽”⟩)‘𝐽) = 𝐼) | ||
| Theorem | trsp2cyc 31292* | Exhibit the word a transposition corresponds to, as a cycle. (Contributed by Thierry Arnoux, 25-Sep-2023.) |
| ⊢ 𝑇 = ran (pmTrsp‘𝐷) & ⊢ 𝐶 = (toCyc‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) → ∃𝑖 ∈ 𝐷 ∃𝑗 ∈ 𝐷 (𝑖 ≠ 𝑗 ∧ 𝑃 = (𝐶‘⟨“𝑖𝑗”⟩))) | ||
| Theorem | cycpmco2f1 31293 | The word U used in cycpmco2 31302 is injective, so it can represent a cycle and form a cyclic permutation (𝑀‘𝑈). (Contributed by Thierry Arnoux, 4-Jan-2024.) |
| ⊢ 𝑀 = (toCyc‘𝐷) & ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) & ⊢ (𝜑 → 𝐽 ∈ ran 𝑊) & ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) & ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) ⇒ ⊢ (𝜑 → 𝑈:dom 𝑈–1-1→𝐷) | ||
| Theorem | cycpmco2rn 31294 | The orbit of the composition of a cyclic permutation and a well-chosen transposition is one element more than the orbit of the original permutation. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
| ⊢ 𝑀 = (toCyc‘𝐷) & ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) & ⊢ (𝜑 → 𝐽 ∈ ran 𝑊) & ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) & ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) ⇒ ⊢ (𝜑 → ran 𝑈 = (ran 𝑊 ∪ {𝐼})) | ||
| Theorem | cycpmco2lem1 31295 | Lemma for cycpmco2 31302. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
| ⊢ 𝑀 = (toCyc‘𝐷) & ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) & ⊢ (𝜑 → 𝐽 ∈ ran 𝑊) & ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) & ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) ⇒ ⊢ (𝜑 → ((𝑀‘𝑊)‘((𝑀‘⟨“𝐼𝐽”⟩)‘𝐼)) = ((𝑀‘𝑊)‘𝐽)) | ||
| Theorem | cycpmco2lem2 31296 | Lemma for cycpmco2 31302. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
| ⊢ 𝑀 = (toCyc‘𝐷) & ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) & ⊢ (𝜑 → 𝐽 ∈ ran 𝑊) & ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) & ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) ⇒ ⊢ (𝜑 → (𝑈‘𝐸) = 𝐼) | ||
| Theorem | cycpmco2lem3 31297 | Lemma for cycpmco2 31302. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
| ⊢ 𝑀 = (toCyc‘𝐷) & ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) & ⊢ (𝜑 → 𝐽 ∈ ran 𝑊) & ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) & ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) ⇒ ⊢ (𝜑 → ((♯‘𝑈) − 1) = (♯‘𝑊)) | ||
| Theorem | cycpmco2lem4 31298 | Lemma for cycpmco2 31302. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
| ⊢ 𝑀 = (toCyc‘𝐷) & ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) & ⊢ (𝜑 → 𝐽 ∈ ran 𝑊) & ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) & ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) ⇒ ⊢ (𝜑 → ((𝑀‘𝑊)‘((𝑀‘⟨“𝐼𝐽”⟩)‘𝐼)) = ((𝑀‘𝑈)‘𝐼)) | ||
| Theorem | cycpmco2lem5 31299 | Lemma for cycpmco2 31302. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
| ⊢ 𝑀 = (toCyc‘𝐷) & ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) & ⊢ (𝜑 → 𝐽 ∈ ran 𝑊) & ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) & ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) & ⊢ (𝜑 → 𝐾 ∈ ran 𝑊) & ⊢ (𝜑 → (◡𝑈‘𝐾) = ((♯‘𝑈) − 1)) ⇒ ⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾)) | ||
| Theorem | cycpmco2lem6 31300 | Lemma for cycpmco2 31302. (Contributed by Thierry Arnoux, 4-Jan-2024.) |
| ⊢ 𝑀 = (toCyc‘𝐷) & ⊢ 𝑆 = (SymGrp‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ (𝜑 → 𝑊 ∈ dom 𝑀) & ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊)) & ⊢ (𝜑 → 𝐽 ∈ ran 𝑊) & ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1) & ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩) & ⊢ (𝜑 → 𝐾 ∈ ran 𝑊) & ⊢ (𝜑 → 𝐾 ≠ 𝐼) & ⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (𝐸..^((♯‘𝑈) − 1))) ⇒ ⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |