P. 323 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32201-32300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cntrcrng 32201	The center of a ring is a commutative ring. (Contributed by Thierry Arnoux, 21-Aug-2023.)
⊢ 𝑍 = (𝑅 ↾s (Cntr‘(mulGrp‘𝑅)))    ⇒   ⊢ (𝑅 ∈ Ring → 𝑍 ∈ CRing)
21.3.9.4  Totally ordered monoids and groups
Syntax	comnd 32202	Extend class notation with the class of all right ordered monoids.
class oMnd
Syntax	cogrp 32203	Extend class notation with the class of all right ordered groups.
class oGrp
Definition	df-omnd 32204*	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 32205	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 32206*	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 32207	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 32208	A left-ordered group is a group. (Contributed by Thierry Arnoux, 9-Jul-2018.)
⊢ (𝐺 ∈ oGrp → 𝐺 ∈ Grp)
Theorem	omndmnd 32209	A left-ordered monoid is a monoid. (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Mnd)
Theorem	omndtos 32210	A left-ordered monoid is a totally ordered set. (Contributed by Thierry Arnoux, 13-Mar-2018.)
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset)
Theorem	omndadd 32211	In an ordered monoid, the ordering is compatible with group addition. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝑀)    &   ⊢ ≤ = (le‘𝑀)    &   ⊢ + = (+g‘𝑀)    ⇒   ⊢ ((𝑀 ∈ oMnd ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 + 𝑍) ≤ (𝑌 + 𝑍))
Theorem	omndaddr 32212	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 32213	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 32214	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 32215	A submonoid of an ordered monoid is also ordered. (Contributed by Thierry Arnoux, 23-Mar-2018.)
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ oMnd)
Theorem	xrge0omnd 32216	The nonnegative extended real numbers form an ordered monoid. (Contributed by Thierry Arnoux, 22-Mar-2018.)
⊢ (ℝ*𝑠 ↾s (0[,]+∞)) ∈ oMnd
Theorem	omndmul2 32217	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 32218	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 32219	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 32220	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 32221	In an ordered group, the ordering is compatible with group subtraction. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ≤ = (le‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 − 𝑍) ≤ (𝑌 − 𝑍))
Theorem	ogrpaddlt 32222	In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ < = (lt‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 + 𝑍) < (𝑌 + 𝑍))
Theorem	ogrpaddltbi 32223	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 32224	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 32225	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 32226	In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ < = (lt‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 − 𝑍) < (𝑌 − 𝑍))
Theorem	ogrpinv0lt 32227	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 32228	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 32229	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.5  The symmetric group
Theorem	symgfcoeu 32230*	Uniqueness property of permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ 𝐺 = (Base‘(SymGrp‘𝐷))    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑄 = (𝑃 ∘ 𝑝))
Theorem	symgcom 32231	Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 15-Oct-2023.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸))    &   ⊢ (𝜑 → (𝑌 ↾ 𝐹) = ( I ↾ 𝐹))    &   ⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅)    &   ⊢ (𝜑 → (𝐸 ∪ 𝐹) = 𝐴)    ⇒   ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋))
Theorem	symgcom2 32232	Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 17-Nov-2023.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (dom (𝑋 ∖ I ) ∩ dom (𝑌 ∖ I )) = ∅)    ⇒   ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋))
Theorem	symgcntz 32233*	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 32234	The composition of two odd permutations is even. (Contributed by Thierry Arnoux, 15-Oct-2023.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (pmEven‘𝐷)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝑋 ∈ (𝐵 ∖ 𝐴) ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → (𝑋 ∘ 𝑌) ∈ 𝐴)
Theorem	symgsubg 32235	The value of the group subtraction operation of the symmetric group. (Contributed by Thierry Arnoux, 15-Oct-2023.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 ∘ ◡𝑌))
Theorem	pmtrprfv2 32236	In a transposition of two given points, each maps to the other. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑌) = 𝑋)
Theorem	pmtrcnel 32237	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 32238	Variation on pmtrcnel 32237. (Contributed by Thierry Arnoux, 16-Nov-2023.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝐹‘𝐼)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ dom (𝐹 ∖ I ))    ⇒   ⊢ (𝜑 → (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽}) ⊆ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ))
Theorem	pmtrcnelor 32239	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.6  Transpositions
Theorem	pmtridf1o 32240	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 32241	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 32242	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.7  Permutation Signs
Theorem	psgnid 32243	Permutation sign of the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.)
⊢ 𝑆 = (pmSgn‘𝐷)    ⇒   ⊢ (𝐷 ∈ Fin → (𝑆‘( I ↾ 𝐷)) = 1)
Theorem	psgndmfi 32244	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 32245	Useful lemma for the following theorems. (Contributed by Thierry Arnoux, 21-Aug-2020.)
⊢ 𝐷 = (1...𝑁)    &   ⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝑇‘{𝐾, (𝐾 + 1)}) ∈ ran 𝑇)
Theorem	psgnfzto1stlem 32246*	Lemma for psgnfzto1st 32251. 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 32247*	Value of our permutation 𝑃 at 1. (Contributed by Thierry Arnoux, 23-Aug-2020.)
⊢ 𝐷 = (1...𝑁)    &   ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)))    ⇒   ⊢ (𝐼 ∈ 𝐷 → (𝑃‘1) = 𝐼)
Theorem	fzto1st1 32248*	Special case where the permutation defined in psgnfzto1st 32251 is the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.)
⊢ 𝐷 = (1...𝑁)    &   ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)))    ⇒   ⊢ (𝐼 = 1 → 𝑃 = ( I ↾ 𝐷))
Theorem	fzto1st 32249*	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 32250*	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 32251*	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.8  Permutation cycles
Syntax	ctocyc 32252	Extend class notation with the permutation cycle builder.
class toCyc
Definition	df-tocyc 32253*	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 32254*	Value of the cycle builder. (Contributed by Thierry Arnoux, 22-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝐶 = (𝑤 ∈ {𝑢 ∈ Word 𝐷 ∣ 𝑢:dom 𝑢–1-1→𝐷} ↦ (( I ↾ (𝐷 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤))))
Theorem	tocycfv 32255	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 32256	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 32257	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 32258	Lemma for cycpmfv1 32259 and cycpmfv2 32260. (Contributed by Thierry Arnoux, 22-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝑊)))    ⇒   ⊢ (𝜑 → ((𝐶‘𝑊)‘(𝑊‘𝑁)) = (((𝑊 cyclShift 1) ∘ ◡𝑊)‘(𝑊‘𝑁)))
Theorem	cycpmfv1 32259	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 32260	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 32261	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 32262	Cyclic permutations are permutations. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝜑 → (𝐶‘𝑊) ∈ (Base‘𝑆))
Theorem	tocycf 32263*	The permutation cycle builder as a function. (Contributed by Thierry Arnoux, 25-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝐶:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵)
Theorem	tocyc01 32264	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 32265	A cyclic permutation of 2 elements is a transposition. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽”⟩) = (𝑇‘{𝐼, 𝐽}))
Theorem	cycpm2cl 32266	Closure for the 2-cycles. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
Theorem	cyc2fv1 32267	Function value of a 2-cycle at the first point. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽”⟩)‘𝐼) = 𝐽)
Theorem	cyc2fv2 32268	Function value of a 2-cycle at the second point. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽”⟩)‘𝐽) = 𝐼)
Theorem	trsp2cyc 32269*	Exhibit the word a transposition corresponds to, as a cycle. (Contributed by Thierry Arnoux, 25-Sep-2023.)
⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝐶 = (toCyc‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) → ∃𝑖 ∈ 𝐷 ∃𝑗 ∈ 𝐷 (𝑖 ≠ 𝑗 ∧ 𝑃 = (𝐶‘⟨“𝑖𝑗”⟩)))
Theorem	cycpmco2f1 32270	The word U used in cycpmco2 32279 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 32271	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 32272	Lemma for cycpmco2 32279. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    ⇒   ⊢ (𝜑 → ((𝑀‘𝑊)‘((𝑀‘⟨“𝐼𝐽”⟩)‘𝐼)) = ((𝑀‘𝑊)‘𝐽))
Theorem	cycpmco2lem2 32273	Lemma for cycpmco2 32279. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    ⇒   ⊢ (𝜑 → (𝑈‘𝐸) = 𝐼)
Theorem	cycpmco2lem3 32274	Lemma for cycpmco2 32279. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    ⇒   ⊢ (𝜑 → ((♯‘𝑈) − 1) = (♯‘𝑊))
Theorem	cycpmco2lem4 32275	Lemma for cycpmco2 32279. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    ⇒   ⊢ (𝜑 → ((𝑀‘𝑊)‘((𝑀‘⟨“𝐼𝐽”⟩)‘𝐼)) = ((𝑀‘𝑈)‘𝐼))
Theorem	cycpmco2lem5 32276	Lemma for cycpmco2 32279. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    &   ⊢ (𝜑 → 𝐾 ∈ ran 𝑊)    &   ⊢ (𝜑 → (◡𝑈‘𝐾) = ((♯‘𝑈) − 1))    ⇒   ⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾))
Theorem	cycpmco2lem6 32277	Lemma for cycpmco2 32279. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    &   ⊢ (𝜑 → 𝐾 ∈ ran 𝑊)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    &   ⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (𝐸..^((♯‘𝑈) − 1)))    ⇒   ⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾))
Theorem	cycpmco2lem7 32278	Lemma for cycpmco2 32279. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    &   ⊢ (𝜑 → 𝐾 ∈ ran 𝑊)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐽)    &   ⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (0..^𝐸))    ⇒   ⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾))
Theorem	cycpmco2 32279	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 32280	Function value of a 2-cycle outside of its orbit. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽”⟩)‘𝐾) = 𝐾)
Theorem	cycpm3cl 32281	Closure of the 3-cycles in the permutations. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽𝐾”⟩) ∈ (Base‘𝑆))
Theorem	cycpm3cl2 32282	Closure of the 3-cycles in the class of 3-cycles. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽𝐾”⟩) ∈ (𝐶 “ (◡♯ “ {3})))
Theorem	cyc3fv1 32283	Function value of a 3-cycle at the first point. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽𝐾”⟩)‘𝐼) = 𝐽)
Theorem	cyc3fv2 32284	Function value of a 3-cycle at the second point. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽𝐾”⟩)‘𝐽) = 𝐾)
Theorem	cyc3fv3 32285	Function value of a 3-cycle at the third point. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽𝐾”⟩)‘𝐾) = 𝐼)
Theorem	cyc3co2 32286	Represent a 3-cycle as a composition of two 2-cycles. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    &   ⊢ · = (+g‘𝑆)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽𝐾”⟩) = ((𝐶‘⟨“𝐼𝐾”⟩) · (𝐶‘⟨“𝐼𝐽”⟩)))
Theorem	cycpmconjvlem 32287	Lemma for cycpmconjv 32288. (Contributed by Thierry Arnoux, 9-Oct-2023.)
⊢ (𝜑 → 𝐹:𝐷–1-1-onto→𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐷)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ (𝐷 ∖ 𝐵)) ∘ ◡𝐹) = ( I ↾ (𝐷 ∖ ran (𝐹 ↾ 𝐵))))
Theorem	cycpmconjv 32288	A formula for computing conjugacy classes of cyclic permutations. Formula in property (b) of [Lang] p. 32. (Contributed by Thierry Arnoux, 9-Oct-2023.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ + = (+g‘𝑆)    &   ⊢ − = (-g‘𝑆)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝐺 ∈ 𝐵 ∧ 𝑊 ∈ dom 𝑀) → ((𝐺 + (𝑀‘𝑊)) − 𝐺) = (𝑀‘(𝐺 ∘ 𝑊)))
Theorem	cycpmrn 32289	The range of the word used to build a cycle is the cycle's orbit, i.e., the set of points it moves. (Contributed by Thierry Arnoux, 20-Nov-2023.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    &   ⊢ (𝜑 → 1 < (♯‘𝑊))    ⇒   ⊢ (𝜑 → ran 𝑊 = dom ((𝑀‘𝑊) ∖ I ))
Theorem	tocyccntz 32290*	All elements of a (finite) set of cycles commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 27-Nov-2023.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑍 = (Cntz‘𝑆)    &   ⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 ran 𝑥)    &   ⊢ (𝜑 → 𝐴 ⊆ dom 𝑀)    ⇒   ⊢ (𝜑 → (𝑀 “ 𝐴) ⊆ (𝑍‘(𝑀 “ 𝐴)))
21.3.9.9  The Alternating Group
Theorem	evpmval 32291	Value of the set of even permutations, the alternating group. (Contributed by Thierry Arnoux, 1-Nov-2023.)
⊢ 𝐴 = (pmEven‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝐴 = (◡(pmSgn‘𝐷) “ {1}))
Theorem	cnmsgn0g 32292	The neutral element of the sign subgroup of the complex numbers. (Contributed by Thierry Arnoux, 1-Nov-2023.)
⊢ 𝑈 = ((mulGrp‘ℂfld) ↾s {1, -1})    ⇒   ⊢ 1 = (0g‘𝑈)
Theorem	evpmsubg 32293	The alternating group is a subgroup of the symmetric group. (Contributed by Thierry Arnoux, 1-Nov-2023.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝐴 = (pmEven‘𝐷)    ⇒   ⊢ (𝐷 ∈ Fin → 𝐴 ∈ (SubGrp‘𝑆))
Theorem	evpmid 32294	The identity is an even permutation. (Contributed by Thierry Arnoux, 18-Sep-2023.)
⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝐷 ∈ Fin → ( I ↾ 𝐷) ∈ (pmEven‘𝐷))
Theorem	altgnsg 32295	The alternating group (pmEven‘𝐷) is a normal subgroup of the symmetric group. (Contributed by Thierry Arnoux, 18-Sep-2023.)
⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝐷 ∈ Fin → (pmEven‘𝐷) ∈ (NrmSGrp‘𝑆))
Theorem	cyc3evpm 32296	3-Cycles are even permutations. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = ((toCyc‘𝐷) “ (◡♯ “ {3}))    &   ⊢ 𝐴 = (pmEven‘𝐷)    ⇒   ⊢ (𝐷 ∈ Fin → 𝐶 ⊆ 𝐴)
Theorem	cyc3genpmlem 32297*	Lemma for cyc3genpm 32298. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (𝑀 “ (◡♯ “ {3}))    &   ⊢ 𝐴 = (pmEven‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (♯‘𝐷)    &   ⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ · = (+g‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐿 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))    &   ⊢ (𝜑 → 𝐹 = (𝑀‘⟨“𝐾𝐿”⟩))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐿)    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
Theorem	cyc3genpm 32298*	The alternating group 𝐴 is generated by 3-cycles. Property (a) of [Lang] p. 32 . (Contributed by Thierry Arnoux, 27-Sep-2023.)
⊢ 𝐶 = (𝑀 “ (◡♯ “ {3}))    &   ⊢ 𝐴 = (pmEven‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (♯‘𝐷)    &   ⊢ 𝑀 = (toCyc‘𝐷)    ⇒   ⊢ (𝐷 ∈ Fin → (𝑄 ∈ 𝐴 ↔ ∃𝑤 ∈ Word 𝐶𝑄 = (𝑆 Σg 𝑤)))
Theorem	cycpmgcl 32299	Cyclic permutations are permutations, similar to cycpmcl 32262, but where the set of cyclic permutations of length 𝑃 is expressed in terms of a preimage. (Contributed by Thierry Arnoux, 13-Oct-2023.)
⊢ 𝐶 = (𝑀 “ (◡♯ “ {𝑃}))    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (♯‘𝐷)    &   ⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ (0...𝑁)) → 𝐶 ⊆ 𝐵)
Theorem	cycpmconjslem1 32300	Lemma for cycpmconjs 32302. (Contributed by Thierry Arnoux, 14-Oct-2023.)
⊢ 𝐶 = (𝑀 “ (◡♯ “ {𝑃}))    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (♯‘𝐷)    &   ⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    &   ⊢ (𝜑 → (♯‘𝑊) = 𝑃)    ⇒   ⊢ (𝜑 → ((◡𝑊 ∘ (𝑀‘𝑊)) ∘ 𝑊) = (( I ↾ (0..^𝑃)) cyclShift 1))