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
Definition	df-psgn 19401*	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 19402	Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018.)
⊢ pmEven = (𝑑 ∈ V ↦ (◡(pmSgn‘𝑑) “ {1}))
Theorem	psgnunilem1 19403*	Lemma for psgnuni 19409. 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 19404*	Lemma for psgnuni 19409. 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 19405*	Lemma for psgnuni 19409. 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 19406*	Lemma for psgnuni 19409. 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 19407	Lemma for psgnuni 19409. 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 19408	Addition and subtraction of parities are the same. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (-1↑(𝑋 − 𝑌)) = (-1↑(𝑋 + 𝑌)))
Theorem	psgnuni 19409	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 19410*	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 19411*	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 19412	The finitary permutations are a subgroup. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → dom 𝑁 ∈ (SubGrp‘𝐺))
Theorem	psgneldm 19413	Property of being a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑃 ∈ dom 𝑁 ↔ (𝑃 ∈ 𝐵 ∧ dom (𝑃 ∖ I ) ∈ Fin))
Theorem	psgneldm2 19414*	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 19415	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 19416*	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 19417*	Value of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑃 ∈ dom 𝑁 → (𝑁‘𝑃) = (℩𝑠∃𝑤 ∈ Word 𝑇(𝑃 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))))
Theorem	psgnvali 19418*	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 19419	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 19420	All transpositions are odd. (Contributed by Stefan O'Rear, 29-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑃 ∈ 𝑇 → (𝑁‘𝑃) = -1)
Theorem	psgn0fv0 19421	The permutation sign function for an empty set at an empty set is 1. (Contributed by AV, 27-Feb-2019.)
⊢ ((pmSgn‘∅)‘∅) = 1
Theorem	sygbasnfpfi 19422	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 19423*	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 19424*	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 19425	The range of the permutation sign function for finite permutations. (Contributed by AV, 1-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃) → (𝑆‘𝑄) ∈ {1, -1})
Theorem	gsmtrcl 19426	The group sum of transpositions of a finite set is a permutation, see also psgneldm2i 19415. (Contributed by AV, 19-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑇 = ran (pmTrsp‘𝑁)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇) → (𝑆 Σg 𝑊) ∈ 𝐵)
Theorem	psgnfitr 19427*	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 19428*	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 19429	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 19430	The permutation sign function for a singleton. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐷 = {𝐴}    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = 1)
Theorem	psgnprfval 19431*	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 19432	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 19433	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 19434	Extend class notation to include the order function on the elements of a group.
class od
Syntax	cgex 19435	Extend class notation to include the order function on the elements of a group.
class gEx
Syntax	cpgp 19436	Extend class notation to include the class of all p-groups.
class pGrp
Syntax	cslw 19437	Extend class notation to include the class of all Sylow p-subgroups of a group.
class pSyl
Definition	df-od 19438*	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 19439*	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 19440*	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 19441*	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 19442*	Value of the order function. For a shorter proof using ax-rep 5285, see odfvalALT 19443. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by AV, 5-Oct-2020.) Remove dependency on ax-rep 5285. (Revised by Rohan Ridenour, 17-Aug-2023.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ 𝑂 = (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
Theorem	odfvalALT 19443*	Shorter proof of odfval 19442 using ax-rep 5285. (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 19444*	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 19445*	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 19446	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 19447	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 19448	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 19449	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 19450	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 19451	Lemma for mndodcong 19452. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 < (𝑂‘𝐴))    &   ⊢ (𝜑 → 𝑁 < (𝑂‘𝐴))    &   ⊢ (𝜑 → (𝑀 · 𝐴) = (𝑁 · 𝐴))    ⇒   ⊢ ((𝜑 ∧ 𝑀 ≤ 𝑁) → 𝑀 = 𝑁)
Theorem	mndodcong 19452	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 19453	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 19454	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 19455	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 19456	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 19457	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 19458	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 19459	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 19460*	The oddvds 19457 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 19461*	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 19462	The order of a group element is always a nonnegative integer, deduction form of odcl 19446. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ0)
Theorem	odm1inv 19463	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 19464	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 19465	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 19466	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 19467	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 19468*	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 19469	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 19470	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 19471	The order of the inverse of a group element. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑂‘(𝐼‘𝐴)) = (𝑂‘𝐴))
Theorem	odf1 19472*	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 19473*	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 19474*	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 19475	The order of an element of a finite group is finite. (Contributed by Mario Carneiro, 14-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∈ ℕ)
Theorem	oddvds2 19476	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 19477*	A submonoid whose elements have finite order is a subgroup. (Contributed by SN, 31-Jan-2025.)
⊢ 𝑂 = (od‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Grp)    &   ⊢ (𝜑 → 𝑆 ∈ (SubMnd‘𝐺))    &   ⊢ (𝜑 → ∀𝑎 ∈ 𝑆 (𝑂‘𝑎) ∈ ℕ)    ⇒   ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺))
Theorem	0subgALT 19478	A shorter proof of 0subg 19068 using df-od 19438. (Contributed by SN, 31-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐺 ∈ Grp → { 0 } ∈ (SubGrp‘𝐺))
Theorem	submod 19479	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 19480	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 19481	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 19482*	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 19483*	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 19484	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 19485	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 19486	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 19487*	A cyclic subgroup of size (𝑂‘𝐴) has (ϕ‘(𝑂‘𝐴)) generators. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) ∈ ℕ) → (♯‘{𝑥 ∈ (𝐾‘{𝐴}) ∣ (𝑂‘𝑥) = (𝑂‘𝐴)}) = (ϕ‘(𝑂‘𝐴)))
Theorem	gexval 19488*	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 19489*	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 19490	The exponent of a group is a nonnegative integer. (Contributed by Mario Carneiro, 23-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝐸 ∈ ℕ0)
Theorem	gexid 19491	Any element to the power of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ (𝐴 ∈ 𝑋 → (𝐸 · 𝐴) = 0 )
Theorem	gexlem2 19492*	Any positive annihilator of all the group elements is an upper bound on the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.) (Proof shortened by AV, 26-Sep-2020.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ ∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 ) → 𝐸 ∈ (1...𝑁))
Theorem	gexdvdsi 19493	Any group element is annihilated by any multiple of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁) → (𝑁 · 𝐴) = 0 )
Theorem	gexdvds 19494*	The only 𝑁 that annihilate all the elements of the group are the multiples of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → (𝐸 ∥ 𝑁 ↔ ∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 ))
Theorem	gexdvds2 19495*	An integer divides the group exponent iff it divides all the group orders. In other words, the group exponent is the LCM of the orders of all the elements. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → (𝐸 ∥ 𝑁 ↔ ∀𝑥 ∈ 𝑋 (𝑂‘𝑥) ∥ 𝑁))
Theorem	gexod 19496	Any group element is annihilated by any multiple of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∥ 𝐸)
Theorem	gexcl3 19497*	If the order of every group element is bounded by 𝑁, the group has finite exponent. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (𝑂‘𝑥) ∈ (1...𝑁)) → 𝐸 ∈ ℕ)
Theorem	gexnnod 19498	Every group element has finite order if the exponent is finite. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∈ ℕ)
Theorem	gexcl2 19499	The exponent of a finite group is finite. (Contributed by Mario Carneiro, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → 𝐸 ∈ ℕ)
Theorem	gexdvds3 19500	The exponent 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, 24-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → 𝐸 ∥ (♯‘𝑋))