P. 322 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32101-32200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	omndmul2 32101	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 32102	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 32103	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 32104	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 32105	In an ordered group, the ordering is compatible with group subtraction. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ ≤ = (le‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 − 𝑍) ≤ (𝑌 − 𝑍))
Theorem	ogrpaddlt 32106	In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 20-Jan-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ < = (lt‘𝐺)    &   ⊢ + = (+g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 + 𝑍) < (𝑌 + 𝑍))
Theorem	ogrpaddltbi 32107	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 32108	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 32109	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 32110	In an ordered group, strict ordering is compatible with group addition. (Contributed by Thierry Arnoux, 3-Sep-2018.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ < = (lt‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ oGrp ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋 < 𝑌) → (𝑋 − 𝑍) < (𝑌 − 𝑍))
Theorem	ogrpinv0lt 32111	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 32112	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 32113	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 32114*	Uniqueness property of permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ 𝐺 = (Base‘(SymGrp‘𝐷))    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝐺 ∧ 𝑄 ∈ 𝐺) → ∃!𝑝 ∈ 𝐺 𝑄 = (𝑃 ∘ 𝑝))
Theorem	symgcom 32115	Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 15-Oct-2023.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (𝑋 ↾ 𝐸) = ( I ↾ 𝐸))    &   ⊢ (𝜑 → (𝑌 ↾ 𝐹) = ( I ↾ 𝐹))    &   ⊢ (𝜑 → (𝐸 ∩ 𝐹) = ∅)    &   ⊢ (𝜑 → (𝐸 ∪ 𝐹) = 𝐴)    ⇒   ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋))
Theorem	symgcom2 32116	Two permutations 𝑋 and 𝑌 commute if their orbits are disjoint. (Contributed by Thierry Arnoux, 17-Nov-2023.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → (dom (𝑋 ∖ I ) ∩ dom (𝑌 ∖ I )) = ∅)    ⇒   ⊢ (𝜑 → (𝑋 ∘ 𝑌) = (𝑌 ∘ 𝑋))
Theorem	symgcntz 32117*	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 32118	The composition of two odd permutations is even. (Contributed by Thierry Arnoux, 15-Oct-2023.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐴 = (pmEven‘𝐷)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝑋 ∈ (𝐵 ∖ 𝐴) ∧ 𝑌 ∈ (𝐵 ∖ 𝐴)) → (𝑋 ∘ 𝑌) ∈ 𝐴)
Theorem	symgsubg 32119	The value of the group subtraction operation of the symmetric group. (Contributed by Thierry Arnoux, 15-Oct-2023.)
⊢ 𝐺 = (SymGrp‘𝐴)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ − = (-g‘𝐺)    ⇒   ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 − 𝑌) = (𝑋 ∘ ◡𝑌))
Theorem	pmtrprfv2 32120	In a transposition of two given points, each maps to the other. (Contributed by Thierry Arnoux, 22-Aug-2020.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑌) = 𝑋)
Theorem	pmtrcnel 32121	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 32122	Variation on pmtrcnel 32121. (Contributed by Thierry Arnoux, 16-Nov-2023.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝐽 = (𝐹‘𝐼)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐵)    &   ⊢ (𝜑 → 𝐼 ∈ dom (𝐹 ∖ I ))    ⇒   ⊢ (𝜑 → (dom (𝐹 ∖ I ) ∖ {𝐼, 𝐽}) ⊆ dom (((𝑇‘{𝐼, 𝐽}) ∘ 𝐹) ∖ I ))
Theorem	pmtrcnelor 32123	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 32124	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 32125	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 32126	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 32127	Permutation sign of the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.)
⊢ 𝑆 = (pmSgn‘𝐷)    ⇒   ⊢ (𝐷 ∈ Fin → (𝑆‘( I ↾ 𝐷)) = 1)
Theorem	psgndmfi 32128	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 32129	Useful lemma for the following theorems. (Contributed by Thierry Arnoux, 21-Aug-2020.)
⊢ 𝐷 = (1...𝑁)    &   ⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐾 ∈ ℕ ∧ (𝐾 + 1) ∈ 𝐷) → (𝑇‘{𝐾, (𝐾 + 1)}) ∈ ran 𝑇)
Theorem	psgnfzto1stlem 32130*	Lemma for psgnfzto1st 32135. 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 32131*	Value of our permutation 𝑃 at 1. (Contributed by Thierry Arnoux, 23-Aug-2020.)
⊢ 𝐷 = (1...𝑁)    &   ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)))    ⇒   ⊢ (𝐼 ∈ 𝐷 → (𝑃‘1) = 𝐼)
Theorem	fzto1st1 32132*	Special case where the permutation defined in psgnfzto1st 32135 is the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.)
⊢ 𝐷 = (1...𝑁)    &   ⊢ 𝑃 = (𝑖 ∈ 𝐷 ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖)))    ⇒   ⊢ (𝐼 = 1 → 𝑃 = ( I ↾ 𝐷))
Theorem	fzto1st 32133*	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 32134*	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 32135*	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 32136	Extend class notation with the permutation cycle builder.
class toCyc
Definition	df-tocyc 32137*	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 32138*	Value of the cycle builder. (Contributed by Thierry Arnoux, 22-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝐶 = (𝑤 ∈ {𝑢 ∈ Word 𝐷 ∣ 𝑢:dom 𝑢–1-1→𝐷} ↦ (( I ↾ (𝐷 ∖ ran 𝑤)) ∪ ((𝑤 cyclShift 1) ∘ ◡𝑤))))
Theorem	tocycfv 32139	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 32140	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 32141	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 32142	Lemma for cycpmfv1 32143 and cycpmfv2 32144. (Contributed by Thierry Arnoux, 22-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    &   ⊢ (𝜑 → 𝑁 ∈ (0..^(♯‘𝑊)))    ⇒   ⊢ (𝜑 → ((𝐶‘𝑊)‘(𝑊‘𝑁)) = (((𝑊 cyclShift 1) ∘ ◡𝑊)‘(𝑊‘𝑁)))
Theorem	cycpmfv1 32143	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 32144	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 32145	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 32146	Cyclic permutations are permutations. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝜑 → (𝐶‘𝑊) ∈ (Base‘𝑆))
Theorem	tocycf 32147*	The permutation cycle builder as a function. (Contributed by Thierry Arnoux, 25-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝐶:{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤–1-1→𝐷}⟶𝐵)
Theorem	tocyc01 32148	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 32149	A cyclic permutation of 2 elements is a transposition. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽”⟩) = (𝑇‘{𝐼, 𝐽}))
Theorem	cycpm2cl 32150	Closure for the 2-cycles. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽”⟩) ∈ (Base‘𝑆))
Theorem	cyc2fv1 32151	Function value of a 2-cycle at the first point. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽”⟩)‘𝐼) = 𝐽)
Theorem	cyc2fv2 32152	Function value of a 2-cycle at the second point. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽”⟩)‘𝐽) = 𝐼)
Theorem	trsp2cyc 32153*	Exhibit the word a transposition corresponds to, as a cycle. (Contributed by Thierry Arnoux, 25-Sep-2023.)
⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝐶 = (toCyc‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ∈ 𝑇) → ∃𝑖 ∈ 𝐷 ∃𝑗 ∈ 𝐷 (𝑖 ≠ 𝑗 ∧ 𝑃 = (𝐶‘⟨“𝑖𝑗”⟩)))
Theorem	cycpmco2f1 32154	The word U used in cycpmco2 32163 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 32155	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 32156	Lemma for cycpmco2 32163. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    ⇒   ⊢ (𝜑 → ((𝑀‘𝑊)‘((𝑀‘⟨“𝐼𝐽”⟩)‘𝐼)) = ((𝑀‘𝑊)‘𝐽))
Theorem	cycpmco2lem2 32157	Lemma for cycpmco2 32163. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    ⇒   ⊢ (𝜑 → (𝑈‘𝐸) = 𝐼)
Theorem	cycpmco2lem3 32158	Lemma for cycpmco2 32163. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    ⇒   ⊢ (𝜑 → ((♯‘𝑈) − 1) = (♯‘𝑊))
Theorem	cycpmco2lem4 32159	Lemma for cycpmco2 32163. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    ⇒   ⊢ (𝜑 → ((𝑀‘𝑊)‘((𝑀‘⟨“𝐼𝐽”⟩)‘𝐼)) = ((𝑀‘𝑈)‘𝐼))
Theorem	cycpmco2lem5 32160	Lemma for cycpmco2 32163. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    &   ⊢ (𝜑 → 𝐾 ∈ ran 𝑊)    &   ⊢ (𝜑 → (◡𝑈‘𝐾) = ((♯‘𝑈) − 1))    ⇒   ⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾))
Theorem	cycpmco2lem6 32161	Lemma for cycpmco2 32163. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    &   ⊢ (𝜑 → 𝐾 ∈ ran 𝑊)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    &   ⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (𝐸..^((♯‘𝑈) − 1)))    ⇒   ⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾))
Theorem	cycpmco2lem7 32162	Lemma for cycpmco2 32163. (Contributed by Thierry Arnoux, 4-Jan-2024.)
⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ dom 𝑀)    &   ⊢ (𝜑 → 𝐼 ∈ (𝐷 ∖ ran 𝑊))    &   ⊢ (𝜑 → 𝐽 ∈ ran 𝑊)    &   ⊢ 𝐸 = ((◡𝑊‘𝐽) + 1)    &   ⊢ 𝑈 = (𝑊 splice ⟨𝐸, 𝐸, ⟨“𝐼”⟩⟩)    &   ⊢ (𝜑 → 𝐾 ∈ ran 𝑊)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐽)    &   ⊢ (𝜑 → (◡𝑈‘𝐾) ∈ (0..^𝐸))    ⇒   ⊢ (𝜑 → ((𝑀‘𝑈)‘𝐾) = ((𝑀‘𝑊)‘𝐾))
Theorem	cycpmco2 32163	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 32164	Function value of a 2-cycle outside of its orbit. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽”⟩)‘𝐾) = 𝐾)
Theorem	cycpm3cl 32165	Closure of the 3-cycles in the permutations. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽𝐾”⟩) ∈ (Base‘𝑆))
Theorem	cycpm3cl2 32166	Closure of the 3-cycles in the class of 3-cycles. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽𝐾”⟩) ∈ (𝐶 “ (◡♯ “ {3})))
Theorem	cyc3fv1 32167	Function value of a 3-cycle at the first point. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽𝐾”⟩)‘𝐼) = 𝐽)
Theorem	cyc3fv2 32168	Function value of a 3-cycle at the second point. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽𝐾”⟩)‘𝐽) = 𝐾)
Theorem	cyc3fv3 32169	Function value of a 3-cycle at the third point. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    ⇒   ⊢ (𝜑 → ((𝐶‘⟨“𝐼𝐽𝐾”⟩)‘𝐾) = 𝐼)
Theorem	cyc3co2 32170	Represent a 3-cycle as a composition of two 2-cycles. (Contributed by Thierry Arnoux, 19-Sep-2023.)
⊢ 𝐶 = (toCyc‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐽 ≠ 𝐾)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐼)    &   ⊢ · = (+g‘𝑆)    ⇒   ⊢ (𝜑 → (𝐶‘⟨“𝐼𝐽𝐾”⟩) = ((𝐶‘⟨“𝐼𝐾”⟩) · (𝐶‘⟨“𝐼𝐽”⟩)))
Theorem	cycpmconjvlem 32171	Lemma for cycpmconjv 32172. (Contributed by Thierry Arnoux, 9-Oct-2023.)
⊢ (𝜑 → 𝐹:𝐷–1-1-onto→𝐷)    &   ⊢ (𝜑 → 𝐵 ⊆ 𝐷)    ⇒   ⊢ (𝜑 → ((𝐹 ↾ (𝐷 ∖ 𝐵)) ∘ ◡𝐹) = ( I ↾ (𝐷 ∖ ran (𝐹 ↾ 𝐵))))
Theorem	cycpmconjv 32172	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 32173	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 32174*	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 32175	Value of the set of even permutations, the alternating group. (Contributed by Thierry Arnoux, 1-Nov-2023.)
⊢ 𝐴 = (pmEven‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝐴 = (◡(pmSgn‘𝐷) “ {1}))
Theorem	cnmsgn0g 32176	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 32177	The alternating group is a subgroup of the symmetric group. (Contributed by Thierry Arnoux, 1-Nov-2023.)
⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝐴 = (pmEven‘𝐷)    ⇒   ⊢ (𝐷 ∈ Fin → 𝐴 ∈ (SubGrp‘𝑆))
Theorem	evpmid 32178	The identity is an even permutation. (Contributed by Thierry Arnoux, 18-Sep-2023.)
⊢ 𝑆 = (SymGrp‘𝐷)    ⇒   ⊢ (𝐷 ∈ Fin → ( I ↾ 𝐷) ∈ (pmEven‘𝐷))
Theorem	altgnsg 32179	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 32180	3-Cycles are even permutations. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = ((toCyc‘𝐷) “ (◡♯ “ {3}))    &   ⊢ 𝐴 = (pmEven‘𝐷)    ⇒   ⊢ (𝐷 ∈ Fin → 𝐶 ⊆ 𝐴)
Theorem	cyc3genpmlem 32181*	Lemma for cyc3genpm 32182. (Contributed by Thierry Arnoux, 24-Sep-2023.)
⊢ 𝐶 = (𝑀 “ (◡♯ “ {3}))    &   ⊢ 𝐴 = (pmEven‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (♯‘𝐷)    &   ⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ · = (+g‘𝑆)    &   ⊢ (𝜑 → 𝐼 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐾 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐿 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐸 = (𝑀‘⟨“𝐼𝐽”⟩))    &   ⊢ (𝜑 → 𝐹 = (𝑀‘⟨“𝐾𝐿”⟩))    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐼 ≠ 𝐽)    &   ⊢ (𝜑 → 𝐾 ≠ 𝐿)    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ Word 𝐶(𝐸 · 𝐹) = (𝑆 Σg 𝑐))
Theorem	cyc3genpm 32182*	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 32183	Cyclic permutations are permutations, similar to cycpmcl 32146, 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 32184	Lemma for cycpmconjs 32186. (Contributed by Thierry Arnoux, 14-Oct-2023.)
⊢ 𝐶 = (𝑀 “ (◡♯ “ {𝑃}))    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (♯‘𝐷)    &   ⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝐷)    &   ⊢ (𝜑 → 𝑊:dom 𝑊–1-1→𝐷)    &   ⊢ (𝜑 → (♯‘𝑊) = 𝑃)    ⇒   ⊢ (𝜑 → ((◡𝑊 ∘ (𝑀‘𝑊)) ∘ 𝑊) = (( I ↾ (0..^𝑃)) cyclShift 1))
Theorem	cycpmconjslem2 32185*	Lemma for cycpmconjs 32186. (Contributed by Thierry Arnoux, 14-Oct-2023.)
⊢ 𝐶 = (𝑀 “ (◡♯ “ {𝑃}))    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (♯‘𝐷)    &   ⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ − = (-g‘𝑆)    &   ⊢ (𝜑 → 𝑃 ∈ (0...𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ∃𝑞(𝑞:(0..^𝑁)–1-1-onto→𝐷 ∧ ((◡𝑞 ∘ 𝑄) ∘ 𝑞) = ((( I ↾ (0..^𝑃)) cyclShift 1) ∪ ( I ↾ (𝑃..^𝑁)))))
Theorem	cycpmconjs 32186*	All cycles of the same length are conjugate in the symmetric group. (Contributed by Thierry Arnoux, 14-Oct-2023.)
⊢ 𝐶 = (𝑀 “ (◡♯ “ {𝑃}))    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (♯‘𝐷)    &   ⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ + = (+g‘𝑆)    &   ⊢ − = (-g‘𝑆)    &   ⊢ (𝜑 → 𝑃 ∈ (0...𝑁))    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ 𝐵 𝑄 = ((𝑝 + 𝑇) − 𝑝))
Theorem	cyc3conja 32187*	All 3-cycles are conjugate in the alternating group An for n>= 5. Property (b) of [Lang] p. 32. (Contributed by Thierry Arnoux, 15-Oct-2023.)
⊢ 𝐶 = (𝑀 “ (◡♯ “ {3}))    &   ⊢ 𝐴 = (pmEven‘𝐷)    &   ⊢ 𝑆 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (♯‘𝐷)    &   ⊢ 𝑀 = (toCyc‘𝐷)    &   ⊢ + = (+g‘𝑆)    &   ⊢ − = (-g‘𝑆)    &   ⊢ (𝜑 → 5 ≤ 𝑁)    &   ⊢ (𝜑 → 𝐷 ∈ Fin)    &   ⊢ (𝜑 → 𝑄 ∈ 𝐶)    &   ⊢ (𝜑 → 𝑇 ∈ 𝐶)    ⇒   ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 𝑄 = ((𝑝 + 𝑇) − 𝑝))
21.3.9.10  Signum in an ordered monoid
Syntax	csgns 32188	Extend class notation to include the Signum function.
class sgns
Definition	df-sgns 32189*	Signum function for a structure. See also df-sgn 15016 for the version for extended reals. (Contributed by Thierry Arnoux, 10-Sep-2018.)
⊢ sgns = (𝑟 ∈ V ↦ (𝑥 ∈ (Base‘𝑟) ↦ if(𝑥 = (0g‘𝑟), 0, if((0g‘𝑟)(lt‘𝑟)𝑥, 1, -1))))
Theorem	sgnsv 32190*	The sign mapping. (Contributed by Thierry Arnoux, 9-Sep-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ < = (lt‘𝑅)    &   ⊢ 𝑆 = (sgns‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝑆 = (𝑥 ∈ 𝐵 ↦ if(𝑥 = 0 , 0, if( 0 < 𝑥, 1, -1))))
Theorem	sgnsval 32191	The sign value. (Contributed by Thierry Arnoux, 9-Sep-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ < = (lt‘𝑅)    &   ⊢ 𝑆 = (sgns‘𝑅)    ⇒   ⊢ ((𝑅 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑆‘𝑋) = if(𝑋 = 0 , 0, if( 0 < 𝑋, 1, -1)))
Theorem	sgnsf 32192	The sign function. (Contributed by Thierry Arnoux, 9-Sep-2018.)
⊢ 𝐵 = (Base‘𝑅)    &   ⊢ 0 = (0g‘𝑅)    &   ⊢ < = (lt‘𝑅)    &   ⊢ 𝑆 = (sgns‘𝑅)    ⇒   ⊢ (𝑅 ∈ 𝑉 → 𝑆:𝐵⟶{-1, 0, 1})
21.3.9.11  The Archimedean property for generic ordered algebraic structures
Syntax	cinftm 32193	Class notation for the infinitesimal relation.
class ⋘
Syntax	carchi 32194	Class notation for the Archimedean property.
class Archi
Definition	df-inftm 32195*	Define the relation "𝑥 is infinitesimal with respect to 𝑦 " for a structure 𝑤. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ ⋘ = (𝑤 ∈ V ↦ {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (Base‘𝑤) ∧ 𝑦 ∈ (Base‘𝑤)) ∧ ((0g‘𝑤)(lt‘𝑤)𝑥 ∧ ∀𝑛 ∈ ℕ (𝑛(.g‘𝑤)𝑥)(lt‘𝑤)𝑦))})
Definition	df-archi 32196	A structure said to be Archimedean if it has no infinitesimal elements. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ Archi = {𝑤 ∣ (⋘‘𝑤) = ∅}
Theorem	inftmrel 32197	The infinitesimal relation for a structure 𝑊. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑉 → (⋘‘𝑊) ⊆ (𝐵 × 𝐵))
Theorem	isinftm 32198*	Express 𝑥 is infinitesimal with respect to 𝑦 for a structure 𝑊. (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ · = (.g‘𝑊)    &   ⊢ < = (lt‘𝑊)    ⇒   ⊢ ((𝑊 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋(⋘‘𝑊)𝑌 ↔ ( 0 < 𝑋 ∧ ∀𝑛 ∈ ℕ (𝑛 · 𝑋) < 𝑌)))
Theorem	isarchi 32199*	Express the predicate "𝑊 is Archimedean ". (Contributed by Thierry Arnoux, 30-Jan-2018.)
⊢ 𝐵 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    &   ⊢ < = (⋘‘𝑊)    ⇒   ⊢ (𝑊 ∈ 𝑉 → (𝑊 ∈ Archi ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ¬ 𝑥 < 𝑦))
Theorem	pnfinf 32200	Plus infinity is an infinite for the completed real line, as any real number is infinitesimal compared to it. (Contributed by Thierry Arnoux, 1-Feb-2018.)
⊢ (𝐴 ∈ ℝ+ → 𝐴(⋘‘ℝ*𝑠)+∞)