P. 195 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19401-19500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	symgsssg 19401*	The symmetric group has subgroups restricting the set of non-fixed points. (Contributed by Stefan O'Rear, 24-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐷 ∈ 𝑉 → {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ⊆ 𝑋} ∈ (SubGrp‘𝐺))
Theorem	symgfisg 19402*	The symmetric group has a subgroup of permutations that move finitely many points. (Contributed by Stefan O'Rear, 24-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝐷 ∈ 𝑉 → {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin} ∈ (SubGrp‘𝐺))
Theorem	symgtrf 19403	Transpositions are elements of the symmetric group. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝑇 ⊆ 𝐵
Theorem	symggen 19404*	The span of the transpositions is the subgroup that moves finitely many points. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubMnd‘𝐺))    ⇒   ⊢ (𝐷 ∈ 𝑉 → (𝐾‘𝑇) = {𝑥 ∈ 𝐵 ∣ dom (𝑥 ∖ I ) ∈ Fin})
Theorem	symggen2 19405	A finite permutation group is generated by the transpositions, see also Theorem 3.4 in [Rotman] p. 31. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubMnd‘𝐺))    ⇒   ⊢ (𝐷 ∈ Fin → (𝐾‘𝑇) = 𝐵)
Theorem	symgtrinv 19406	To invert a permutation represented as a sequence of transpositions, reverse the sequence. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐼 = (invg‘𝐺)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → (𝐼‘(𝐺 Σg 𝑊)) = (𝐺 Σg (reverse‘𝑊)))
Theorem	pmtr3ncomlem1 19407	Lemma 1 for pmtr3ncom 19409. (Contributed by AV, 17-Mar-2018.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌})    &   ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍})    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝐺 ∘ 𝐹)‘𝑋) ≠ ((𝐹 ∘ 𝐺)‘𝑋))
Theorem	pmtr3ncomlem2 19408	Lemma 2 for pmtr3ncom 19409. (Contributed by AV, 17-Mar-2018.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌})    &   ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍})    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐺 ∘ 𝐹) ≠ (𝐹 ∘ 𝐺))
Theorem	pmtr3ncom 19409*	Transpositions over sets with at least 3 elements are not commutative, see also the remark in [Rotman] p. 28. (Contributed by AV, 21-Mar-2019.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 3 ≤ (♯‘𝐷)) → ∃𝑓 ∈ ran 𝑇∃𝑔 ∈ ran 𝑇(𝑔 ∘ 𝑓) ≠ (𝑓 ∘ 𝑔))
Theorem	pmtrdifellem1 19410	Lemma 1 for pmtrdifel 19414. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ (𝑄 ∈ 𝑇 → 𝑆 ∈ 𝑅)
Theorem	pmtrdifellem2 19411	Lemma 2 for pmtrdifel 19414. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ (𝑄 ∈ 𝑇 → dom (𝑆 ∖ I ) = dom (𝑄 ∖ I ))
Theorem	pmtrdifellem3 19412*	Lemma 3 for pmtrdifel 19414. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ (𝑄 ∈ 𝑇 → ∀𝑥 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑥) = (𝑆‘𝑥))
Theorem	pmtrdifellem4 19413	Lemma 4 for pmtrdifel 19414. (Contributed by AV, 28-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → (𝑆‘𝐾) = 𝐾)
Theorem	pmtrdifel 19414*	A transposition of elements of a set without a special element corresponds to a transposition of elements of the set. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    ⇒   ⊢ ∀𝑡 ∈ 𝑇 ∃𝑟 ∈ 𝑅 ∀𝑥 ∈ (𝑁 ∖ {𝐾})(𝑡‘𝑥) = (𝑟‘𝑥)
Theorem	pmtrdifwrdellem1 19415*	Lemma 1 for pmtrdifwrdel 19419. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → 𝑈 ∈ Word 𝑅)
Theorem	pmtrdifwrdellem2 19416*	Lemma 2 for pmtrdifwrdel 19419. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → (♯‘𝑊) = (♯‘𝑈))
Theorem	pmtrdifwrdellem3 19417*	Lemma 3 for pmtrdifwrdel 19419. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → ∀𝑖 ∈ (0..^(♯‘𝑊))∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))
Theorem	pmtrdifwrdel2lem1 19418*	Lemma 1 for pmtrdifwrdel2 19420. (Contributed by AV, 31-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ ((𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁) → ∀𝑖 ∈ (0..^(♯‘𝑊))((𝑈‘𝑖)‘𝐾) = 𝐾)
Theorem	pmtrdifwrdel 19419*	A sequence of transpositions of elements of a set without a special element corresponds to a sequence of transpositions of elements of the set. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    ⇒   ⊢ ∀𝑤 ∈ Word 𝑇∃𝑢 ∈ Word 𝑅((♯‘𝑤) = (♯‘𝑢) ∧ ∀𝑖 ∈ (0..^(♯‘𝑤))∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥))
Theorem	pmtrdifwrdel2 19420*	A sequence of transpositions of elements of a set without a special element corresponds to a sequence of transpositions of elements of the set not moving the special element. (Contributed by AV, 31-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    ⇒   ⊢ (𝐾 ∈ 𝑁 → ∀𝑤 ∈ Word 𝑇∃𝑢 ∈ Word 𝑅((♯‘𝑤) = (♯‘𝑢) ∧ ∀𝑖 ∈ (0..^(♯‘𝑤))(((𝑢‘𝑖)‘𝐾) = 𝐾 ∧ ∀𝑥 ∈ (𝑁 ∖ {𝐾})((𝑤‘𝑖)‘𝑥) = ((𝑢‘𝑖)‘𝑥))))
Theorem	pmtrprfval 19421*	The transpositions on a pair. (Contributed by AV, 9-Dec-2018.)
⊢ (pmTrsp‘{1, 2}) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1)))
Theorem	pmtrprfvalrn 19422	The range of the transpositions on a pair is actually a singleton: the transposition of the two elements of the pair. (Contributed by AV, 9-Dec-2018.)
⊢ ran (pmTrsp‘{1, 2}) = {{⟨1, 2⟩, ⟨2, 1⟩}}
10.2.10.5  The sign of a permutation
Syntax	cpsgn 19423	Syntax for the sign of a permutation.
class pmSgn
Syntax	cevpm 19424	Syntax for even permutations.
class pmEven
Definition	df-psgn 19425*	Define a function which takes the value 1 for even permutations and -1 for odd. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ pmSgn = (𝑑 ∈ V ↦ (𝑥 ∈ {𝑝 ∈ (Base‘(SymGrp‘𝑑)) ∣ dom (𝑝 ∖ I ) ∈ Fin} ↦ (℩𝑠∃𝑤 ∈ Word ran (pmTrsp‘𝑑)(𝑥 = ((SymGrp‘𝑑) Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))))
Definition	df-evpm 19426	Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018.)
⊢ pmEven = (𝑑 ∈ V ↦ (◡(pmSgn‘𝑑) “ {1}))
Theorem	psgnunilem1 19427*	Lemma for psgnuni 19433. Given two consequtive transpositions in a representation of a permutation, either they are equal and therefore equivalent to the identity, or they are not and it is possible to commute them such that a chosen point in the left transposition is preserved in the right. By repeating this process, a point can be removed from a representation of the identity. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑃 ∈ 𝑇)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑇)    &   ⊢ (𝜑 → 𝐴 ∈ dom (𝑃 ∖ I ))    ⇒   ⊢ (𝜑 → ((𝑃 ∘ 𝑄) = ( I ↾ 𝐷) ∨ ∃𝑟 ∈ 𝑇 ∃𝑠 ∈ 𝑇 ((𝑃 ∘ 𝑄) = (𝑟 ∘ 𝑠) ∧ 𝐴 ∈ dom (𝑠 ∖ I ) ∧ ¬ 𝐴 ∈ dom (𝑟 ∖ I ))))
Theorem	psgnunilem5 19428*	Lemma for psgnuni 19433. It is impossible to shift a transposition off the end because if the active transposition is at the right end, it is the only transposition moving 𝐴 in contradiction to this being a representation of the identity. (Contributed by Stefan O'Rear, 25-Aug-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) (Proof shortened by AV, 12-Oct-2022.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑇)    &   ⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))    &   ⊢ (𝜑 → (♯‘𝑊) = 𝐿)    &   ⊢ (𝜑 → 𝐼 ∈ (0..^𝐿))    &   ⊢ (𝜑 → 𝐴 ∈ dom ((𝑊‘𝐼) ∖ I ))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝐼) ¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ))    ⇒   ⊢ (𝜑 → (𝐼 + 1) ∈ (0..^𝐿))
Theorem	psgnunilem2 19429*	Lemma for psgnuni 19433. Induction step for moving a transposition as far to the right as possible. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by Mario Carneiro, 28-Feb-2016.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑇)    &   ⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))    &   ⊢ (𝜑 → (♯‘𝑊) = 𝐿)    &   ⊢ (𝜑 → 𝐼 ∈ (0..^𝐿))    &   ⊢ (𝜑 → 𝐴 ∈ dom ((𝑊‘𝐼) ∖ I ))    &   ⊢ (𝜑 → ∀𝑘 ∈ (0..^𝐼) ¬ 𝐴 ∈ dom ((𝑊‘𝑘) ∖ I ))    &   ⊢ (𝜑 → ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))    ⇒   ⊢ (𝜑 → ∃𝑤 ∈ Word 𝑇(((𝐺 Σg 𝑤) = ( I ↾ 𝐷) ∧ (♯‘𝑤) = 𝐿) ∧ ((𝐼 + 1) ∈ (0..^𝐿) ∧ 𝐴 ∈ dom ((𝑤‘(𝐼 + 1)) ∖ I ) ∧ ∀𝑗 ∈ (0..^(𝐼 + 1)) ¬ 𝐴 ∈ dom ((𝑤‘𝑗) ∖ I ))))
Theorem	psgnunilem3 19430*	Lemma for psgnuni 19433. Any nonempty representation of the identity can be incrementally transformed into a representation two shorter. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑇)    &   ⊢ (𝜑 → (♯‘𝑊) = 𝐿)    &   ⊢ (𝜑 → (♯‘𝑊) ∈ ℕ)    &   ⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))    &   ⊢ (𝜑 → ¬ ∃𝑥 ∈ Word 𝑇((♯‘𝑥) = (𝐿 − 2) ∧ (𝐺 Σg 𝑥) = ( I ↾ 𝐷)))    ⇒   ⊢ ¬ 𝜑
Theorem	psgnunilem4 19431	Lemma for psgnuni 19433. An odd-length representation of the identity is impossible, as it could be repeatedly shortened to a length of 1, but a length 1 permutation must be a transposition. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑇)    &   ⊢ (𝜑 → (𝐺 Σg 𝑊) = ( I ↾ 𝐷))    ⇒   ⊢ (𝜑 → (-1↑(♯‘𝑊)) = 1)
Theorem	m1expaddsub 19432	Addition and subtraction of parities are the same. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (-1↑(𝑋 − 𝑌)) = (-1↑(𝑋 + 𝑌)))
Theorem	psgnuni 19433	If the same permutation can be written in more than one way as a product of transpositions, the parity of those products must agree; otherwise the product of one with the inverse of the other would be an odd representation of the identity. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑊 ∈ Word 𝑇)    &   ⊢ (𝜑 → 𝑋 ∈ Word 𝑇)    &   ⊢ (𝜑 → (𝐺 Σg 𝑊) = (𝐺 Σg 𝑋))    ⇒   ⊢ (𝜑 → (-1↑(♯‘𝑊)) = (-1↑(♯‘𝑋)))
Theorem	psgnfval 19434*	Function definition of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐹 = {𝑝 ∈ 𝐵 ∣ dom (𝑝 ∖ I ) ∈ Fin}    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ 𝑁 = (𝑥 ∈ 𝐹 ↦ (℩𝑠∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))))
Theorem	psgnfn 19435*	Functionality and domain of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝐹 = {𝑝 ∈ 𝐵 ∣ dom (𝑝 ∖ I ) ∈ Fin}    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ 𝑁 Fn 𝐹
Theorem	psgndmsubg 19436	The finitary permutations are a subgroup. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → dom 𝑁 ∈ (SubGrp‘𝐺))
Theorem	psgneldm 19437	Property of being a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑃 ∈ dom 𝑁 ↔ (𝑃 ∈ 𝐵 ∧ dom (𝑃 ∖ I ) ∈ Fin))
Theorem	psgneldm2 19438*	The finitary permutations are the span of the transpositions. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → (𝑃 ∈ dom 𝑁 ↔ ∃𝑤 ∈ Word 𝑇𝑃 = (𝐺 Σg 𝑤)))
Theorem	psgneldm2i 19439	A sequence of transpositions describes a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → (𝐺 Σg 𝑊) ∈ dom 𝑁)
Theorem	psgneu 19440*	A finitary permutation has exactly one parity. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑃 ∈ dom 𝑁 → ∃!𝑠∃𝑤 ∈ Word 𝑇(𝑃 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))
Theorem	psgnval 19441*	Value of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑃 ∈ dom 𝑁 → (𝑁‘𝑃) = (℩𝑠∃𝑤 ∈ Word 𝑇(𝑃 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))))
Theorem	psgnvali 19442*	A finitary permutation has at least one representation for its parity. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑃 ∈ dom 𝑁 → ∃𝑤 ∈ Word 𝑇(𝑃 = (𝐺 Σg 𝑤) ∧ (𝑁‘𝑃) = (-1↑(♯‘𝑤))))
Theorem	psgnvalii 19443	Any representation of a permutation is length matching the permutation sign. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑊 ∈ Word 𝑇) → (𝑁‘(𝐺 Σg 𝑊)) = (-1↑(♯‘𝑊)))
Theorem	psgnpmtr 19444	All transpositions are odd. (Contributed by Stefan O'Rear, 29-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑃 ∈ 𝑇 → (𝑁‘𝑃) = -1)
Theorem	psgn0fv0 19445	The permutation sign function for an empty set at an empty set is 1. (Contributed by AV, 27-Feb-2019.)
⊢ ((pmSgn‘∅)‘∅) = 1
Theorem	sygbasnfpfi 19446	The class of non-fixed points of a permutation of a finite set is finite. (Contributed by AV, 13-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵) → dom (𝑃 ∖ I ) ∈ Fin)
Theorem	psgnfvalfi 19447*	Function definition of the permutation sign function for permutations of finite sets. (Contributed by AV, 13-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝐷 ∈ Fin → 𝑁 = (𝑥 ∈ 𝐵 ↦ (℩𝑠∃𝑤 ∈ Word 𝑇(𝑥 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))))
Theorem	psgnvalfi 19448*	Value of the permutation sign function for permutations of finite sets. (Contributed by AV, 13-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ ((𝐷 ∈ Fin ∧ 𝑃 ∈ 𝐵) → (𝑁‘𝑃) = (℩𝑠∃𝑤 ∈ Word 𝑇(𝑃 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))))
Theorem	psgnran 19449	The range of the permutation sign function for finite permutations. (Contributed by AV, 1-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃) → (𝑆‘𝑄) ∈ {1, -1})
Theorem	gsmtrcl 19450	The group sum of transpositions of a finite set is a permutation, see also psgneldm2i 19439. (Contributed by AV, 19-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑇 = ran (pmTrsp‘𝑁)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇) → (𝑆 Σg 𝑊) ∈ 𝐵)
Theorem	psgnfitr 19451*	A permutation of a finite set is generated by transpositions. (Contributed by AV, 13-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑇 = ran (pmTrsp‘𝑁)    ⇒   ⊢ (𝑁 ∈ Fin → (𝑄 ∈ 𝐵 ↔ ∃𝑤 ∈ Word 𝑇𝑄 = (𝐺 Σg 𝑤)))
Theorem	psgnfieu 19452*	A permutation of a finite set has exactly one parity. (Contributed by AV, 13-Jan-2019.)
⊢ 𝐺 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑇 = ran (pmTrsp‘𝑁)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑄 ∈ 𝐵) → ∃!𝑠∃𝑤 ∈ Word 𝑇(𝑄 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))
Theorem	pmtrsn 19453	The value of the transposition generator function for a singleton is empty, i.e. there is no transposition for a singleton. This also holds for 𝐴 ∉ V, i.e. for the empty set {𝐴} = ∅ resulting in (pmTrsp‘∅) = ∅. (Contributed by AV, 6-Aug-2019.)
⊢ (pmTrsp‘{𝐴}) = ∅
Theorem	psgnsn 19454	The permutation sign function for a singleton. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐷 = {𝐴}    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = 1)
Theorem	psgnprfval 19455*	The permutation sign function for a pair. (Contributed by AV, 10-Dec-2018.)
⊢ 𝐷 = {1, 2}    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑋 ∈ 𝐵 → (𝑁‘𝑋) = (℩𝑠∃𝑤 ∈ Word 𝑇(𝑋 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))))
Theorem	psgnprfval1 19456	The permutation sign of the identity for a pair. (Contributed by AV, 11-Dec-2018.)
⊢ 𝐷 = {1, 2}    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑁‘{⟨1, 1⟩, ⟨2, 2⟩}) = 1
Theorem	psgnprfval2 19457	The permutation sign of the transposition for a pair. (Contributed by AV, 10-Dec-2018.)
⊢ 𝐷 = {1, 2}    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑁‘{⟨1, 2⟩, ⟨2, 1⟩}) = -1
10.2.11  p-Groups and Sylow groups; Sylow's theorems
Syntax	cod 19458	Extend class notation to include the order function on the elements of a group.
class od
Syntax	cgex 19459	Extend class notation to include the order function on the elements of a group.
class gEx
Syntax	cpgp 19460	Extend class notation to include the class of all p-groups.
class pGrp
Syntax	cslw 19461	Extend class notation to include the class of all Sylow p-subgroups of a group.
class pSyl
Definition	df-od 19462*	Define the order of an element in a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.) (Revised by AV, 5-Oct-2020.)
⊢ od = (𝑔 ∈ V ↦ (𝑥 ∈ (Base‘𝑔) ↦ ⦋{𝑛 ∈ ℕ ∣ (𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))))
Definition	df-gex 19463*	Define the exponent of a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.) (Revised by AV, 26-Sep-2020.)
⊢ gEx = (𝑔 ∈ V ↦ ⦋{𝑛 ∈ ℕ ∣ ∀𝑥 ∈ (Base‘𝑔)(𝑛(.g‘𝑔)𝑥) = (0g‘𝑔)} / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
Definition	df-pgp 19464*	Define the set of p-groups, which are groups such that every element has a power of 𝑝 as its order. (Contributed by Mario Carneiro, 15-Jan-2015.) (Revised by AV, 5-Oct-2020.)
⊢ pGrp = {⟨𝑝, 𝑔⟩ ∣ ((𝑝 ∈ ℙ ∧ 𝑔 ∈ Grp) ∧ ∀𝑥 ∈ (Base‘𝑔)∃𝑛 ∈ ℕ0 ((od‘𝑔)‘𝑥) = (𝑝↑𝑛))}
Definition	df-slw 19465*	Define the set of Sylow p-subgroups of a group 𝑔. A Sylow p-subgroup is a p-group that is not a subgroup of any other p-groups in 𝑔. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ pSyl = (𝑝 ∈ ℙ, 𝑔 ∈ Grp ↦ {ℎ ∈ (SubGrp‘𝑔) ∣ ∀𝑘 ∈ (SubGrp‘𝑔)((ℎ ⊆ 𝑘 ∧ 𝑝 pGrp (𝑔 ↾s 𝑘)) ↔ ℎ = 𝑘)})
Theorem	odfval 19466*	Value of the order function. For a shorter proof using ax-rep 5225, see odfvalALT 19467. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by AV, 5-Oct-2020.) Remove dependency on ax-rep 5225. (Revised by Rohan Ridenour, 17-Aug-2023.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ 𝑂 = (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
Theorem	odfvalALT 19467*	Shorter proof of odfval 19466 using ax-rep 5225. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by AV, 5-Oct-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ 𝑂 = (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
Theorem	odval 19468*	Second substitution for the group order definition. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 5-Sep-2015.) (Revised by AV, 5-Oct-2020.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐼 = {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }    ⇒   ⊢ (𝐴 ∈ 𝑋 → (𝑂‘𝐴) = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < )))
Theorem	odlem1 19469*	The group element order is either zero or a nonzero multiplier that annihilates the element. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.) (Revised by AV, 5-Oct-2020.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐼 = {𝑦 ∈ ℕ ∣ (𝑦 · 𝐴) = 0 }    ⇒   ⊢ (𝐴 ∈ 𝑋 → (((𝑂‘𝐴) = 0 ∧ 𝐼 = ∅) ∨ (𝑂‘𝐴) ∈ 𝐼))
Theorem	odcl 19470	The order of a group element is always a nonnegative integer. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑋 → (𝑂‘𝐴) ∈ ℕ0)
Theorem	odf 19471	Functionality of the group element order. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 5-Oct-2020.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ 𝑂:𝑋⟶ℕ0
Theorem	odid 19472	Any element to the power of its order is the identity. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑋 → ((𝑂‘𝐴) · 𝐴) = 0 )
Theorem	odlem2 19473	Any positive annihilator of a group element is an upper bound on the (positive) order of the element. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 5-Oct-2020.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ ∧ (𝑁 · 𝐴) = 0 ) → (𝑂‘𝐴) ∈ (1...𝑁))
Theorem	odmodnn0 19474	Reduce the argument of a group multiple by modding out the order of the element. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → ((𝑁 mod (𝑂‘𝐴)) · 𝐴) = (𝑁 · 𝐴))
Theorem	mndodconglem 19475	Lemma for mndodcong 19476. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 < (𝑂‘𝐴))    &   ⊢ (𝜑 → 𝑁 < (𝑂‘𝐴))    &   ⊢ (𝜑 → (𝑀 · 𝐴) = (𝑁 · 𝐴))    ⇒   ⊢ ((𝜑 ∧ 𝑀 ≤ 𝑁) → 𝑀 = 𝑁)
Theorem	mndodcong 19476	If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) ∧ (𝑂‘𝐴) ∈ ℕ) → ((𝑂‘𝐴) ∥ (𝑀 − 𝑁) ↔ (𝑀 · 𝐴) = (𝑁 · 𝐴)))
Theorem	mndodcongi 19477	If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. For monoids, the reverse implication is false for elements with infinite order. For example, the powers of 2 mod 10 are 1,2,4,8,6,2,4,8,6,... so that the identity 1 never repeats, which is infinite order by our definition, yet other numbers like 6 appear many times in the sequence. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑂‘𝐴) ∥ (𝑀 − 𝑁) → (𝑀 · 𝐴) = (𝑁 · 𝐴)))
Theorem	oddvdsnn0 19478	The only multiples of 𝐴 that are equal to the identity are the multiples of the order of 𝐴. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Mnd ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → ((𝑂‘𝐴) ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 ))
Theorem	odnncl 19479	If a nonzero multiple of an element is zero, the element has positive order. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 22-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ) ∧ (𝑁 ≠ 0 ∧ (𝑁 · 𝐴) = 0 )) → (𝑂‘𝐴) ∈ ℕ)
Theorem	odmod 19480	Reduce the argument of a group multiple by modding out the order of the element. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 6-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ) ∧ (𝑂‘𝐴) ∈ ℕ) → ((𝑁 mod (𝑂‘𝐴)) · 𝐴) = (𝑁 · 𝐴))
Theorem	oddvds 19481	The only multiples of 𝐴 that are equal to the identity are the multiples of the order of 𝐴. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ) → ((𝑂‘𝐴) ∥ 𝑁 ↔ (𝑁 · 𝐴) = 0 ))
Theorem	oddvdsi 19482	Any group element is annihilated by any multiple of its order. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) ∥ 𝑁) → (𝑁 · 𝐴) = 0 )
Theorem	odcong 19483	If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. (Contributed by Stefan O'Rear, 5-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ)) → ((𝑂‘𝐴) ∥ (𝑀 − 𝑁) ↔ (𝑀 · 𝐴) = (𝑁 · 𝐴)))
Theorem	odeq 19484*	The oddvds 19481 property uniquely defines the group order. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℕ0) → (𝑁 = (𝑂‘𝐴) ↔ ∀𝑦 ∈ ℕ0 (𝑁 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )))
Theorem	odval2 19485*	A non-conditional definition of the group order. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) = (℩𝑥 ∈ ℕ0 ∀𝑦 ∈ ℕ0 (𝑥 ∥ 𝑦 ↔ (𝑦 · 𝐴) = 0 )))
Theorem	odcld 19486	The order of a group element is always a nonnegative integer, deduction form of odcl 19470. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ0)
Theorem	odm1inv 19487	The (order-1)th multiple of an element is its inverse. (Contributed by SN, 31-Jan-2025.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (((𝑂‘𝐴) − 1) · 𝐴) = (𝐼‘𝐴))
Theorem	odmulgid 19488	A relationship between the order of a multiple and the order of the basepoint. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ) ∧ 𝐾 ∈ ℤ) → ((𝑂‘(𝑁 · 𝐴)) ∥ 𝐾 ↔ (𝑂‘𝐴) ∥ (𝐾 · 𝑁)))
Theorem	odmulg2 19489	The order of a multiple divides the order of the base point. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ) → (𝑂‘(𝑁 · 𝐴)) ∥ (𝑂‘𝐴))
Theorem	odmulg 19490	Relationship between the order of an element and that of a multiple. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ) → (𝑂‘𝐴) = ((𝑁 gcd (𝑂‘𝐴)) · (𝑂‘(𝑁 · 𝐴))))
Theorem	odmulgeq 19491	A multiple of a point of finite order only has the same order if the multiplier is relatively prime. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ) ∧ (𝑂‘𝐴) ∈ ℕ) → ((𝑂‘(𝑁 · 𝐴)) = (𝑂‘𝐴) ↔ (𝑁 gcd (𝑂‘𝐴)) = 1))
Theorem	odbezout 19492*	If 𝑁 is coprime to the order of 𝐴, there is a modular inverse 𝑥 to cancel multiplication by 𝑁. (Contributed by Mario Carneiro, 27-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    ⇒   ⊢ (((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝑁 ∈ ℤ) ∧ (𝑁 gcd (𝑂‘𝐴)) = 1) → ∃𝑥 ∈ ℤ (𝑥 · (𝑁 · 𝐴)) = 𝐴)
Theorem	od1 19493	The order of the group identity is one. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑂 = (od‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → (𝑂‘ 0 ) = 1)
Theorem	odeq1 19494	The group identity is the unique element of a group with order one. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑂 = (od‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ((𝑂‘𝐴) = 1 ↔ 𝐴 = 0 ))
Theorem	odinv 19495	The order of the inverse of a group element. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑂‘(𝐼‘𝐴)) = (𝑂‘𝐴))
Theorem	odf1 19496*	The multiples of an element with infinite order form an infinite cyclic subgroup of 𝐺. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → ((𝑂‘𝐴) = 0 ↔ 𝐹:ℤ–1-1→𝑋))
Theorem	odinf 19497*	The multiples of an element with infinite order form an infinite cyclic subgroup of 𝐺. (Contributed by Mario Carneiro, 14-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → ¬ ran 𝐹 ∈ Fin)
Theorem	dfod2 19498*	An alternative definition of the order of a group element is as the cardinality of the cyclic subgroup generated by the element. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝐹 = (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) = if(ran 𝐹 ∈ Fin, (♯‘ran 𝐹), 0))
Theorem	odcl2 19499	The order of an element of a finite group is finite. (Contributed by Mario Carneiro, 14-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∈ ℕ)
Theorem	oddvds2 19500	The order of an element of a finite group divides the order (cardinality) of the group. Corollary of Lagrange's theorem for the order of a subgroup. (Contributed by Mario Carneiro, 14-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∥ (♯‘𝑋))