P. 329 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32801-32900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	gsumsra 32801	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 32802*	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 32803*	Express a finite sum over a two-dimensional range as a double sum. See also gsum2d 19926. (Contributed by Thierry Arnoux, 27-Apr-2020.)
⊢ Ⅎ𝑧𝐶    &   ⊢ Ⅎ𝑦𝜑    &   ⊢ 𝐵 = (Base‘𝑊)    &   ⊢ (𝑥 = ⟨𝑦, 𝑧⟩ → 𝐶 = 𝐷)    &   ⊢ (𝜑 → Rel 𝐴)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → 𝑊 ∈ CMnd)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ 𝐴 ↦ 𝐶)) = (𝑊 Σg (𝑦 ∈ dom 𝐴 ↦ (𝑊 Σg (𝑧 ∈ (𝐴 “ {𝑦}) ↦ 𝐷)))))
Theorem	lmodvslmhm 32804*	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 32805*	Pull a scalar multiplication out of a sum of vectors. This theorem properly generalizes gsummulc1 20251, 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 32806*	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 32807*	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 32808	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 32809*	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 32810*	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 32811*	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 32812	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 32813	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 𝐹))
21.3.9.4  Centralizers and centers - misc additions
Theorem	cntzun 32814	The centralizer of a union is the intersection of the centralizers. (Contributed by Thierry Arnoux, 27-Nov-2023.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ 𝑍 = (Cntz‘𝑀)    ⇒   ⊢ ((𝑋 ⊆ 𝐵 ∧ 𝑌 ⊆ 𝐵) → (𝑍‘(𝑋 ∪ 𝑌)) = ((𝑍‘𝑋) ∩ (𝑍‘𝑌)))
Theorem	cntzsnid 32815	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 32816	The center of a ring is a commutative ring. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝑍 = (𝑅 ↾s (Cntr‘(mulGrp‘𝑅)))    ⇒   ⊢ (𝑅 ∈ Ring → 𝑍 ∈ CRing)
21.3.9.5  Totally ordered monoids and groups
Syntax	comnd 32817	Extend class notation with the class of all right ordered monoids.
class oMnd
Syntax	cogrp 32818	Extend class notation with the class of all right ordered groups.
class oGrp
Definition	df-omnd 32819*	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 32820	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 32821*	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 32822	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 32823	A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.)
⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp)
Theorem	omndmnd 32824	A left-ordered monoid is a monoid. (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Mnd)
Theorem	omndtos 32825	A left-ordered monoid is a totally ordered set. (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset)
Theorem	omndadd 32826	In an ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ≤ = (le‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 + 𝑍) ≤ (𝑌 + 𝑍))
Theorem	omndaddr 32827	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 32828	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 32829	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 32830	A submonoid of an ordered monoid is also ordered. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ oMnd)
Theorem	xrge0omnd 32831	The nonnegative extended real numbers form an ordered monoid. (Contributed by Thierry Arnoux, 22-Mar-2018.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ oMnd
Theorem	omndmul2 32832	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 32833	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 32834	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 32835	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 32836	In an ordered group, the ordering is compatible with group subtraction. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ≤ = (le‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 − 𝑍) ≤ (𝑌 − 𝑍))
Theorem	ogrpaddlt 32837	In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ < = (lt‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 + 𝑍) < (𝑌 + 𝑍))
Theorem	ogrpaddltbi 32838	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 32839	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 32840	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 32841	In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ < = (lt‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 − 𝑍) < (𝑌 − 𝑍))
Theorem	ogrpinv0lt 32842	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 32843	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 32844	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 𝐺))
21.3.9.6  The symmetric group
Theorem	symgfcoeu 32845*	Uniqueness property of permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ 𝐺 = (Base‘(SymGrp‘𝐷))    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑄 = (𝑃 ∘ 𝑝))
Theorem	symgcom 32846	Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 15-Oct-2023.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸))    &   ⊢ (𝜑 → (𝑌 ↾ 𝐹) = ( I ↾ 𝐹))    &   ⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅)    &   ⊢ (𝜑 → (𝐸 ∪ 𝐹) = 𝐴)    ⇒   ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋))
Theorem	symgcom2 32847	Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 17-Nov-2023.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (dom (𝑋 ∖ I ) ∩ dom (𝑌 ∖ I )) = ∅)    ⇒   ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋))
Theorem	symgcntz 32848*	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 32849	The composition of two odd permutations is even. (Contributed by Thierry Arnoux, 15-Oct-2023.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (pmEven‘𝐷)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝑋 ∈ (𝐵 ∖ 𝐴) ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → (𝑋 ∘ 𝑌) ∈ 𝐴)
Theorem	symgsubg 32850	The value of the group subtraction operation of the symmetric group. (Contributed by Thierry Arnoux, 15-Oct-2023.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 ∘ ◡𝑌))
Theorem	pmtrprfv2 32851	In a transposition of two given points, each maps to the other. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑌) = 𝑋)
Theorem	pmtrcnel 32852	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 32853	Variation on pmtrcnel 32852. (Contributed by Thierry Arnoux, 16-Nov-2023.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝐹‘𝐼)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ dom (𝐹 ∖ I ))    ⇒   ⊢ (𝜑 → (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽}) ⊆ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ))
Theorem	pmtrcnelor 32854	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 )    ⇒   ⊢ (𝜑 → (𝐴 = (𝐸 ∖ {𝐼, 𝐽}) ∨ 𝐴 = (𝐸 ∖ {𝐼})))
21.3.9.7  Transpositions
Theorem	pmtridf1o 32855	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 32856	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 32857	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‘𝐴)‘{𝑋, 𝑌}))    ⇒   ⊢ (𝜑 → (𝑇‘𝑌) = 𝑋)
21.3.9.8  Permutation Signs
Theorem	psgnid 32858	Permutation sign of the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.)
⊢ 𝑆 = (pmSgn‘𝐷)    ⇒   ⊢ (𝐷 ∈ Fin → (𝑆‘( I ↾ 𝐷)) = 1)
Theorem	psgndmfi 32859	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 32860	Useful lemma for the following theorems. (Contributed by Thierry Arnoux, 21-Aug-2020.)
⊢ 𝐷 = (1...𝑁)    &   ⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝑇‘{𝐾, (𝐾 + 1)}) ∈ ran 𝑇)
Theorem	psgnfzto1stlem 32861*	Lemma for psgnfzto1st 32866. 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 32862*	Value of our permutation 𝑃 at 1. (Contributed by Thierry Arnoux, 23-Aug-2020.)
⊢ 𝐷 = (1...𝑁)    &   ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)))    ⇒   ⊢ (𝐼 ∈ 𝐷 → (𝑃‘1) = 𝐼)
Theorem	fzto1st1 32863*	Special case where the permutation defined in psgnfzto1st 32866 is the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.)
⊢ 𝐷 = (1...𝑁)    &   ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)))    ⇒   ⊢ (𝐼 = 1 → 𝑃 = ( I ↾ 𝐷))
Theorem	fzto1st 32864*	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 32865*	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 32866*	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)))
21.3.9.9  Permutation cycles
Syntax	ctocyc 32867	Extend class notation with the permutation cycle builder.
class toCyc
Definition	df-tocyc 32868*	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 32869*	Value of the cycle builder. (Contributed by Thierry Arnoux, 22-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝐶 = (𝑤 ∈ {𝑢 ∈ Word 𝐷 ∣ 𝑢:dom 𝑢–1-1→𝐷} ↦ (( I ↾ (𝐷 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤))))
Theorem	tocycfv 32870	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 32871	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 32872	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 32873	Lemma for cycpmfv1 32874 and cycpmfv2 32875. (Contributed by Thierry Arnoux, 22-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝑊)))    ⇒   ⊢ (𝜑 → ((𝐶‘𝑊)‘(𝑊‘𝑁)) = (((𝑊 cyclShift 1) ∘ ◡𝑊)‘(𝑊‘𝑁)))
Theorem	cycpmfv1 32874	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 32875	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 32876	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 32877	Cyclic permutations are permutations. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝜑 → (𝐶‘𝑊) ∈ (Base‘𝑆))
Theorem	tocycf 32878*	The permutation cycle builder as a function. (Contributed by Thierry Arnoux, 25-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝐶:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵)
Theorem	tocyc01 32879	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 32880	A cyclic permutation of 2 elements is a transposition. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽”⟩) = (𝑇‘{𝐼, 𝐽}))
Theorem	cycpm2cl 32881	Closure for the 2-cycles. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
Theorem	cyc2fv1 32882	Function value of a 2-cycle at the first point. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽”⟩)‘𝐼) = 𝐽)
Theorem	cyc2fv2 32883	Function value of a 2-cycle at the second point. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽”⟩)‘𝐽) = 𝐼)
Theorem	trsp2cyc 32884*	Exhibit the word a transposition corresponds to, as a cycle. (Contributed by Thierry Arnoux, 25-Sep-2023.)
⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝐶 = (toCyc‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) → ∃𝑖 ∈ 𝐷 ∃𝑗 ∈ 𝐷 (𝑖 ≠ 𝑗 ∧ 𝑃 = (𝐶‘⟨“𝑖𝑗”⟩)))
Theorem	cycpmco2f1 32885	The word U used in cycpmco2 32894 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 32886	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 32887	Lemma for cycpmco2 32894. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    ⇒   ⊢ (𝜑 → ((𝑀‘𝑊)‘((𝑀‘⟨“𝐼𝐽”⟩)‘𝐼)) = ((𝑀‘𝑊)‘𝐽))
Theorem	cycpmco2lem2 32888	Lemma for cycpmco2 32894. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    ⇒   ⊢ (𝜑 → (𝑈‘𝐸) = 𝐼)
Theorem	cycpmco2lem3 32889	Lemma for cycpmco2 32894. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    ⇒   ⊢ (𝜑 → ((♯‘𝑈) − 1) = (♯‘𝑊))
Theorem	cycpmco2lem4 32890	Lemma for cycpmco2 32894. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    ⇒   ⊢ (𝜑 → ((𝑀‘𝑊)‘((𝑀‘⟨“𝐼𝐽”⟩)‘𝐼)) = ((𝑀‘𝑈)‘𝐼))
Theorem	cycpmco2lem5 32891	Lemma for cycpmco2 32894. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    &   ⊢ (𝜑 → 𝐾 ∈ ran 𝑊)    &   ⊢ (𝜑 → (◡𝑈‘𝐾) = ((♯‘𝑈) − 1))    ⇒   ⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾))
Theorem	cycpmco2lem6 32892	Lemma for cycpmco2 32894. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    &   ⊢ (𝜑 → 𝐾 ∈ ran 𝑊)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    &   ⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (𝐸..^((♯‘𝑈) − 1)))    ⇒   ⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾))
Theorem	cycpmco2lem7 32893	Lemma for cycpmco2 32894. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    &   ⊢ (𝜑 → 𝐾 ∈ ran 𝑊)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐽)    &   ⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (0..^𝐸))    ⇒   ⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾))
Theorem	cycpmco2 32894	The composition of a cyclic permutation and a transposition of one element in the cycle and one outside the cycle results in a cyclic permutation with one more element in its orbit. (Contributed by Thierry Arnoux, 2-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    ⇒   ⊢ (𝜑 → ((𝑀‘𝑊) ∘ (𝑀‘⟨“𝐼𝐽”⟩)) = (𝑀‘𝑈))
Theorem	cyc2fvx 32895	Function value of a 2-cycle outside of its orbit. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽”⟩)‘𝐾) = 𝐾)
Theorem	cycpm3cl 32896	Closure of the 3-cycles in the permutations. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽𝐾”⟩) ∈ (Base‘𝑆))
Theorem	cycpm3cl2 32897	Closure of the 3-cycles in the class of 3-cycles. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽𝐾”⟩) ∈ (𝐶 “ (◡♯ “ {3})))
Theorem	cyc3fv1 32898	Function value of a 3-cycle at the first point. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽𝐾”⟩)‘𝐼) = 𝐽)
Theorem	cyc3fv2 32899	Function value of a 3-cycle at the second point. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽𝐾”⟩)‘𝐽) = 𝐾)
Theorem	cyc3fv3 32900	Function value of a 3-cycle at the third point. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽𝐾”⟩)‘𝐾) = 𝐼)