P. 191 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19001-19100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pmtrdifellem3 19001*	Lemma 3 for pmtrdifel 19003. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ (𝑄 ∈ 𝑇 → ∀𝑥 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑥) = (𝑆‘𝑥))
Theorem	pmtrdifellem4 19002	Lemma 4 for pmtrdifel 19003. (Contributed by AV, 28-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → (𝑆‘𝐾) = 𝐾)
Theorem	pmtrdifel 19003*	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 19004*	Lemma 1 for pmtrdifwrdel 19008. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → 𝑈 ∈ Word 𝑅)
Theorem	pmtrdifwrdellem2 19005*	Lemma 2 for pmtrdifwrdel 19008. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → (♯‘𝑊) = (♯‘𝑈))
Theorem	pmtrdifwrdellem3 19006*	Lemma 3 for pmtrdifwrdel 19008. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → ∀𝑖 ∈ (0..^(♯‘𝑊))∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))
Theorem	pmtrdifwrdel2lem1 19007*	Lemma 1 for pmtrdifwrdel2 19009. (Contributed by AV, 31-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ ((𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁) → ∀𝑖 ∈ (0..^(♯‘𝑊))((𝑈‘𝑖)‘𝐾) = 𝐾)
Theorem	pmtrdifwrdel 19008*	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 19009*	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 19010*	The transpositions on a pair. (Contributed by AV, 9-Dec-2018.)
⊢ (pmTrsp‘{1, 2}) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1)))
Theorem	pmtrprfvalrn 19011	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 19012	Syntax for the sign of a permutation.
class pmSgn
Syntax	cevpm 19013	Syntax for even permutations.
class pmEven
Definition	df-psgn 19014*	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 19015	Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018.)
⊢ pmEven = (𝑑 ∈ V ↦ (◡(pmSgn‘𝑑) “ {1}))
Theorem	psgnunilem1 19016*	Lemma for psgnuni 19022. 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 19017*	Lemma for psgnuni 19022. 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 19018*	Lemma for psgnuni 19022. 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 19019*	Lemma for psgnuni 19022. 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 19020	Lemma for psgnuni 19022. 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 19021	Addition and subtraction of parities are the same. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (-1↑(𝑋 − 𝑌)) = (-1↑(𝑋 + 𝑌)))
Theorem	psgnuni 19022	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 19023*	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 19024*	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 19025	The finitary permutations are a subgroup. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → dom 𝑁 ∈ (SubGrp‘𝐺))
Theorem	psgneldm 19026	Property of being a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑃 ∈ dom 𝑁 ↔ (𝑃 ∈ 𝐵 ∧ dom (𝑃 ∖ I ) ∈ Fin))
Theorem	psgneldm2 19027*	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 19028	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 19029*	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 19030*	Value of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑃 ∈ dom 𝑁 → (𝑁‘𝑃) = (℩𝑠∃𝑤 ∈ Word 𝑇(𝑃 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤)))))
Theorem	psgnvali 19031*	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 19032	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 19033	All transpositions are odd. (Contributed by Stefan O'Rear, 29-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑃 ∈ 𝑇 → (𝑁‘𝑃) = -1)
Theorem	psgn0fv0 19034	The permutation sign function for an empty set at an empty set is 1. (Contributed by AV, 27-Feb-2019.)
⊢ ((pmSgn‘∅)‘∅) = 1
Theorem	sygbasnfpfi 19035	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 19036*	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 19037*	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 19038	The range of the permutation sign function for finite permutations. (Contributed by AV, 1-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃) → (𝑆‘𝑄) ∈ {1, -1})
Theorem	gsmtrcl 19039	The group sum of transpositions of a finite set is a permutation, see also psgneldm2i 19028. (Contributed by AV, 19-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑇 = ran (pmTrsp‘𝑁)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇) → (𝑆 Σg 𝑊) ∈ 𝐵)
Theorem	psgnfitr 19040*	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 19041*	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 19042	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 19043	The permutation sign function for a singleton. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐷 = {𝐴}    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = 1)
Theorem	psgnprfval 19044*	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 19045	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 19046	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 19047	Extend class notation to include the order function on the elements of a group.
class od
Syntax	cgex 19048	Extend class notation to include the order function on the elements of a group.
class gEx
Syntax	cpgp 19049	Extend class notation to include the class of all p-groups.
class pGrp
Syntax	cslw 19050	Extend class notation to include the class of all Sylow p-subgroups of a group.
class pSyl
Definition	df-od 19051*	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 19052*	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 19053*	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 19054*	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 19055*	Value of the order function. For a shorter proof using ax-rep 5205, see odfvalALT 19056. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by AV, 5-Oct-2020.) Remove dependency on ax-rep 5205. (Revised by Rohan Ridenour, 17-Aug-2023.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ 𝑂 = (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
Theorem	odfvalALT 19056*	Shorter proof of odfval 19055 using ax-rep 5205. (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 19057*	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 19058*	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 19059	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 19060	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 19061	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 19062	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 19063	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 19064	Lemma for mndodcong 19065. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 < (𝑂‘𝐴))    &   ⊢ (𝜑 → 𝑁 < (𝑂‘𝐴))    &   ⊢ (𝜑 → (𝑀 · 𝐴) = (𝑁 · 𝐴))    ⇒   ⊢ ((𝜑 ∧ 𝑀 ≤ 𝑁) → 𝑀 = 𝑁)
Theorem	mndodcong 19065	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 19066	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 19067	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 19068	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 19069	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 19070	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 19071	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 19072	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 19073*	The oddvds 19070 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 19074*	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 19075	The order of a group element is always a nonnegative integer, deduction form of odcl 19059. (Contributed by Rohan Ridenour, 3-Aug-2023.)
⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ (𝜑 → 𝐴 ∈ 𝐵)    ⇒   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ0)
Theorem	odmulgid 19076	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 19077	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 19078	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 19079	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 19080*	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 19081	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 19082	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 19083	The order of the inverse of a group element. (Contributed by Mario Carneiro, 20-Oct-2015.)
⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐼 = (invg‘𝐺)    &   ⊢ 𝑋 = (Base‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑂‘(𝐼‘𝐴)) = (𝑂‘𝐴))
Theorem	odf1 19084*	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 19085*	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 19086*	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 19087	The order of an element of a finite group is finite. (Contributed by Mario Carneiro, 14-Jan-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∈ ℕ)
Theorem	oddvds2 19088	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	submod 19089	The order of an element is the same in a subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by AV, 5-Oct-2020.)
⊢ 𝐻 = (𝐺 ↾s 𝑌)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝑃 = (od‘𝐻)    ⇒   ⊢ ((𝑌 ∈ (SubMnd‘𝐺) ∧ 𝐴 ∈ 𝑌) → (𝑂‘𝐴) = (𝑃‘𝐴))
Theorem	subgod 19090	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 19091	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 19092*	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 19093*	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 19094	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 19095	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 19096	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 19097*	A cyclic subgroup of size (𝑂‘𝐴) has (ϕ‘(𝑂‘𝐴)) generators. (Contributed by Stefan O'Rear, 12-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺))    ⇒   ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) ∈ ℕ) → (♯‘{𝑥 ∈ (𝐾‘{𝐴}) ∣ (𝑂‘𝑥) = (𝑂‘𝐴)}) = (ϕ‘(𝑂‘𝐴)))
Theorem	gexval 19098*	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 19099*	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 19100	The exponent of a group is a nonnegative integer. (Contributed by Mario Carneiro, 23-Apr-2016.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐸 = (gEx‘𝐺)    ⇒   ⊢ (𝐺 ∈ 𝑉 → 𝐸 ∈ ℕ0)