P. 198 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19701-19800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pmtrdifwrdellem1 19701*	Lemma 1 for pmtrdifwrdel 19705. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → 𝑈 ∈ Word 𝑅)
Theorem	pmtrdifwrdellem2 19702*	Lemma 2 for pmtrdifwrdel 19705. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → (♯‘𝑊) = (♯‘𝑈))
Theorem	pmtrdifwrdellem3 19703*	Lemma 3 for pmtrdifwrdel 19705. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → ∀𝑖 ∈ (0..^(♯‘𝑊))∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))
Theorem	pmtrdifwrdel2lem1 19704*	Lemma 1 for pmtrdifwrdel2 19706. (Contributed by AV, 31-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ ((𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁) → ∀𝑖 ∈ (0..^(♯‘𝑊))((𝑈‘𝑖)‘𝐾) = 𝐾)
Theorem	pmtrdifwrdel 19705*	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 19706*	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 19707*	The transpositions on a pair. (Contributed by AV, 9-Dec-2018.)
⊢ (pmTrsp‘{1, 2}) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1)))
Theorem	pmtrprfvalrn 19708	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 19709	Syntax for the sign of a permutation.
class pmSgn
Syntax	cevpm 19710	Syntax for even permutations.
class pmEven
Definition	df-psgn 19711*	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 19712	Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018.)
⊢ pmEven = (𝑑 ∈ V ↦ (◡(pmSgn‘𝑑) “ {1}))
Theorem	psgnunilem1 19713*	Lemma for psgnuni 19719. 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 19714*	Lemma for psgnuni 19719. 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 19715*	Lemma for psgnuni 19719. 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 19716*	Lemma for psgnuni 19719. 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 19717	Lemma for psgnuni 19719. 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 19718	Addition and subtraction of parities are the same. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ( -1↑(𝑋 − 𝑌)) = ( -1↑(𝑋 + 𝑌)))
Theorem	psgnuni 19719	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 19720*	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 19721*	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 19722	The finitary permutations are a subgroup. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → dom 𝑁 ∈ (SubGrp‘𝐺))
Theorem	psgneldm 19723	Property of being a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑃 ∈ dom 𝑁 ↔ (𝑃 ∈ 𝐵 ∧ dom (𝑃 ∖ I ) ∈ Fin))
Theorem	psgneldm2 19724*	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 19725	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 19726*	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 19727*	Value of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑃 ∈ dom 𝑁 → (𝑁‘𝑃) = (℩𝑠∃𝑤 ∈ Word 𝑇(𝑃 = (𝐺 Σg 𝑤) ∧ 𝑠 = ( -1↑(♯‘𝑤)))))
Theorem	psgnvali 19728*	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 19729	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 19730	All transpositions are odd. (Contributed by Stefan O'Rear, 29-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑃 ∈ 𝑇 → (𝑁‘𝑃) = -1)
Theorem	psgn0fv0 19731	The permutation sign function for an empty set at an empty set is 1. (Contributed by AV, 27-Feb-2019.)
⊢ ((pmSgn‘∅)‘∅) = 1
Theorem	sygbasnfpfi 19732	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 19733*	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 19734*	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 19735	The range of the permutation sign function for finite permutations. (Contributed by AV, 1-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃) → (𝑆‘𝑄) ∈ {1, -1})
Theorem	gsmtrcl 19736	The group sum of transpositions of a finite set is a permutation, see also psgneldm2i 19725. (Contributed by AV, 19-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑇 = ran (pmTrsp‘𝑁)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇) → (𝑆 Σg 𝑊) ∈ 𝐵)
Theorem	psgnfitr 19737*	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 19738*	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 19739	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 19740	The permutation sign function for a singleton. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐷 = {𝐴}    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = 1)
Theorem	psgnprfval 19741*	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 19742	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 19743	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 19744	Extend class notation to include the order function on the elements of a group.
class od
Syntax	cgex 19745	Extend class notation to include the order function on the elements of a group.
class gEx
Syntax	cpgp 19746	Extend class notation to include the class of all p-groups.
class pGrp
Syntax	cslw 19747	Extend class notation to include the class of all Sylow p-subgroups of a group.
class pSyl
Definition	df-od 19748*	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 19749*	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 19750*	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 19751*	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 19752*	Value of the order function. For a shorter proof using ax-rep 5231, see odfvalALT 19753. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by AV, 5-Oct-2020.) Remove dependency on ax-rep 5231. (Revised by Rohan Ridenour, 17-Aug-2023.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ 𝑂 = (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
Theorem	odfvalALT 19753*	Shorter proof of odfval 19752 using ax-rep 5231. (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 19754*	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 19755*	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 19756	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 19757	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 19758	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 19759	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 19760	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 19761	Lemma for mndodcong 19762. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 < (𝑂‘𝐴))    &   ⊢ (𝜑 → 𝑁 < (𝑂‘𝐴))    &   ⊢ (𝜑 → (𝑀 · 𝐴) = (𝑁 · 𝐴))    ⇒   ⊢ ((𝜑 ∧ 𝑀 ≤ 𝑁) → 𝑀 = 𝑁)
Theorem	mndodcong 19762	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 19763	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 19764	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 19765	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 19766	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 19767	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 19768	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 19769	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 19770*	The oddvds 19767 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 19771*	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 19772	The order of a group element is always a nonnegative integer, deduction form of odcl 19756. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ0)
Theorem	odm1inv 19773	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 19774	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 19775	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 19776	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 19777	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 19778*	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 19779	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 19780	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 19781	The order of the inverse of a group element. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑂‘(𝐼‘𝐴)) = (𝑂‘𝐴))
Theorem	odf1 19782*	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 19783*	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 19784*	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 19785	The order of an element of a finite group is finite. (Contributed by Mario Carneiro, 14-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∈ ℕ)
Theorem	oddvds2 19786	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 ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∥ (♯‘𝑋))
Theorem	finodsubmsubg 19787*	A submonoid whose elements have finite order is a subgroup. (Contributed by SN, 31-Jan-2025.)
⊢ 𝑂 = (od‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (𝑂‘𝑎) ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))
Theorem	0subgALT 19788	A shorter proof of 0subg 19368 using df-od 19748. (Contributed by SN, 31-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → { 0 } ∈ (SubGrp‘𝐺))
Theorem	submod 19789	The order of an element is the same in a submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by AV, 5-Oct-2020.)
⊢ 𝐻 = (𝐺 ↾s 𝑌)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑃 = (od‘𝐻)    ⇒   ⊢ ((𝑌 ∈ (SubMnd‘𝐺) ∧ 𝐴 ∈ 𝑌) → (𝑂‘𝐴) = (𝑃‘𝐴))
Theorem	subgod 19790	The order of an element is the same in a subgroup. (Contributed by Mario Carneiro, 14-Jan-2015.) (Proof shortened by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝐻 = (𝐺 ↾s 𝑌)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑃 = (od‘𝐻)    ⇒   ⊢ ((𝑌 ∈ (SubGrp‘𝐺) ∧ 𝐴 ∈ 𝑌) → (𝑂‘𝐴) = (𝑃‘𝐴))
Theorem	odsubdvds 19791	The order of an element of a subgroup divides the order of the subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.)
⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑆 ∈ Fin ∧ 𝐴 ∈ 𝑆) → (𝑂‘𝐴) ∥ (♯‘𝑆))
Theorem	odf1o1 19792*	An element with zero order has infinitely many multiples. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → (𝑥 ∈ ℤ ↦ (𝑥 · 𝐴)):ℤ–1-1-onto→(𝐾‘{𝐴}))
Theorem	odf1o2 19793*	An element with nonzero order has as many multiples as its order. (Contributed by Stefan O'Rear, 6-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) ∈ ℕ) → (𝑥 ∈ (0..^(𝑂‘𝐴)) ↦ (𝑥 · 𝐴)):(0..^(𝑂‘𝐴))–1-1-onto→(𝐾‘{𝐴}))
Theorem	odhash 19794	An element of zero order generates an infinite subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) = 0) → (♯‘(𝐾‘{𝐴})) = +∞)
Theorem	odhash2 19795	If an element has nonzero order, it generates a subgroup with size equal to the order. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) ∈ ℕ) → (♯‘(𝐾‘{𝐴})) = (𝑂‘𝐴))
Theorem	odhash3 19796	An element which generates a finite subgroup has order the size of that subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝐾‘{𝐴}) ∈ Fin) → (𝑂‘𝐴) = (♯‘(𝐾‘{𝐴})))
Theorem	odngen 19797*	A cyclic subgroup of size (𝑂‘𝐴) has (ϕ‘(𝑂‘𝐴)) generators. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) ∈ ℕ) → (♯‘{𝑥 ∈ (𝐾‘{𝐴}) ∣ (𝑂‘𝑥) = (𝑂‘𝐴)}) = (ϕ‘(𝑂‘𝐴)))
Theorem	gexval 19798*	Value of the exponent of a group. (Contributed by Mario Carneiro, 23-Apr-2016.) (Revised by AV, 26-Sep-2020.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 𝐼 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 }    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝐸 = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < )))
Theorem	gexlem1 19799*	The group element order is either zero or a nonzero multiplier that annihilates the element. (Contributed by Mario Carneiro, 23-Apr-2016.) (Proof shortened by AV, 26-Sep-2020.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 𝐼 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 }    ⇒   ⊢ (𝐺 ∈ 𝑉 → ((𝐸 = 0 ∧ 𝐼 = ∅) ∨ 𝐸 ∈ 𝐼))
Theorem	gexcl 19800	The exponent of a group is a nonnegative integer. (Contributed by Mario Carneiro, 23-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝐸 ∈ ℕ0)