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	mvdco 19701	Composing two permutations moves at most the union of the points. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ dom ((𝐹 ∘ 𝐺) ∖ I ) ⊆ (dom (𝐹 ∖ I ) ∪ dom (𝐺 ∖ I ))
Theorem	f1omvdconj 19702	Conjugation of a permutation takes the image of the moved subclass. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴⟶1-1onto𝐴) → dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) = (𝐺 “ dom (𝐹 ∖ I )))
Theorem	f1otrspeq 19703	A transposition is characterized by the points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ (((𝐹:𝐴⟶1-1onto𝐴 ∧ 𝐺:𝐴⟶1-1onto𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2o ∧ dom (𝐺 ∖ I ) = dom (𝐹 ∖ I ))) → 𝐹 = 𝐺)
Theorem	f1omvdco2 19704	If exactly one of two permutations is limited to a set of points, then the composition will not be. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ ((𝐹:𝐴⟶1-1onto𝐴 ∧ 𝐺:𝐴⟶1-1onto𝐴 ∧ (dom (𝐹 ∖ I ) ⊆ 𝑋 ⊻ dom (𝐺 ∖ I ) ⊆ 𝑋)) → ¬ dom ((𝐹 ∘ 𝐺) ∖ I ) ⊆ 𝑋)
Theorem	f1omvdco3 19705	If a point is moved by exactly one of two permutations, then it will be moved by their composite. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ ((𝐹:𝐴⟶1-1onto𝐴 ∧ 𝐺:𝐴⟶1-1onto𝐴 ∧ (𝑋 ∈ dom (𝐹 ∖ I ) ⊻ 𝑋 ∈ dom (𝐺 ∖ I ))) → 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ∖ I ))
Theorem	pmtrfval 19706*	The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → 𝑇 = (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧))))
Theorem	pmtrval 19707*	A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧)))
Theorem	pmtrfv 19708	General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) ∧ 𝑍 ∈ 𝐷) → ((𝑇‘𝑃)‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍))
Theorem	pmtrprfv 19709	In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑋) = 𝑌)
Theorem	pmtrprfv3 19710	In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝑇‘{𝑋, 𝑌})‘𝑍) = 𝑍)
Theorem	pmtrf 19711	Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃):𝐷⟶𝐷)
Theorem	pmtrmvd 19712	A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → dom ((𝑇‘𝑃) ∖ I ) = 𝑃)
Theorem	pmtrrn 19713	Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) ∈ 𝑅)
Theorem	pmtrfrn 19714	A transposition (as a kind of function) is the function transposing the two points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    &   ⊢ 𝑃 = dom (𝐹 ∖ I )    ⇒   ⊢ (𝐹 ∈ 𝑅 → ((𝐷 ∈ V ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) ∧ 𝐹 = (𝑇‘𝑃)))
Theorem	pmtrffv 19715	Mapping of a point under a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    &   ⊢ 𝑃 = dom (𝐹 ∖ I )    ⇒   ⊢ ((𝐹 ∈ 𝑅 ∧ 𝑍 ∈ 𝐷) → (𝐹‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍))
Theorem	pmtrrn2 19716*	For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦})))
Theorem	pmtrfinv 19717	A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) = ( I ↾ 𝐷))
Theorem	pmtrfmvdn0 19718	A transposition moves at least one point. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≠ ∅)
Theorem	pmtrff1o 19719	A transposition function is a permutation. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → 𝐹:𝐷⟶1-1onto𝐷)
Theorem	pmtrfcnv 19720	A transposition function is its own inverse. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 → ◡𝐹 = 𝐹)
Theorem	pmtrfb 19721	An intrinsic characterization of the transposition permutations. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ (𝐹 ∈ 𝑅 ↔ (𝐷 ∈ V ∧ 𝐹:𝐷⟶1-1onto𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o))
Theorem	pmtrfconj 19722	Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝑅 = ran 𝑇    ⇒   ⊢ ((𝐹 ∈ 𝑅 ∧ 𝐺:𝐷⟶1-1onto𝐷) → ((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∈ 𝑅)
Theorem	symgsssg 19723*	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 19724*	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 19725	Transpositions are elements of the symmetric group. (Contributed by Stefan O'Rear, 23-Aug-2015.)
⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ 𝑇 ⊆ 𝐵
Theorem	symggen 19726*	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 19727	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 19728	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 19729	Lemma 1 for pmtr3ncom 19731. (Contributed by AV, 17-Mar-2018.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌})    &   ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍})    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝐺 ∘ 𝐹)‘𝑋) ≠ ((𝐹 ∘ 𝐺)‘𝑋))
Theorem	pmtr3ncomlem2 19730	Lemma 2 for pmtr3ncom 19731. (Contributed by AV, 17-Mar-2018.)
⊢ 𝑇 = (pmTrsp‘𝐷)    &   ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌})    &   ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍})    ⇒   ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐺 ∘ 𝐹) ≠ (𝐹 ∘ 𝐺))
Theorem	pmtr3ncom 19731*	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 19732	Lemma 1 for pmtrdifel 19736. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ (𝑄 ∈ 𝑇 → 𝑆 ∈ 𝑅)
Theorem	pmtrdifellem2 19733	Lemma 2 for pmtrdifel 19736. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ (𝑄 ∈ 𝑇 → dom (𝑆 ∖ I ) = dom (𝑄 ∖ I ))
Theorem	pmtrdifellem3 19734*	Lemma 3 for pmtrdifel 19736. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ (𝑄 ∈ 𝑇 → ∀𝑥 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑥) = (𝑆‘𝑥))
Theorem	pmtrdifellem4 19735	Lemma 4 for pmtrdifel 19736. (Contributed by AV, 28-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I ))    ⇒   ⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → (𝑆‘𝐾) = 𝐾)
Theorem	pmtrdifel 19736*	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 19737*	Lemma 1 for pmtrdifwrdel 19741. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → 𝑈 ∈ Word 𝑅)
Theorem	pmtrdifwrdellem2 19738*	Lemma 2 for pmtrdifwrdel 19741. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → (♯‘𝑊) = (♯‘𝑈))
Theorem	pmtrdifwrdellem3 19739*	Lemma 3 for pmtrdifwrdel 19741. (Contributed by AV, 15-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ (𝑊 ∈ Word 𝑇 → ∀𝑖 ∈ (0..^(♯‘𝑊))∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛))
Theorem	pmtrdifwrdel2lem1 19740*	Lemma 1 for pmtrdifwrdel2 19742. (Contributed by AV, 31-Jan-2019.)
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾}))    &   ⊢ 𝑅 = ran (pmTrsp‘𝑁)    &   ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I )))    ⇒   ⊢ ((𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁) → ∀𝑖 ∈ (0..^(♯‘𝑊))((𝑈‘𝑖)‘𝐾) = 𝐾)
Theorem	pmtrdifwrdel 19741*	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 19742*	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 19743*	The transpositions on a pair. (Contributed by AV, 9-Dec-2018.)
⊢ (pmTrsp‘{1, 2}) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1)))
Theorem	pmtrprfvalrn 19744	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 19745	Syntax for the sign of a permutation.
class pmSgn
Syntax	cevpm 19746	Syntax for even permutations.
class pmEven
Definition	df-psgn 19747*	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 19748	Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018.)
⊢ pmEven = (𝑑 ∈ V ↦ (◡(pmSgn‘𝑑) “ {1}))
Theorem	psgnunilem1 19749*	Lemma for psgnuni 19755. 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 19750*	Lemma for psgnuni 19755. 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 19751*	Lemma for psgnuni 19755. 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 19752*	Lemma for psgnuni 19755. 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 19753	Lemma for psgnuni 19755. 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 19754	Addition and subtraction of parities are the same. (Contributed by Stefan O'Rear, 27-Aug-2015.)
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ( -1↑(𝑋 − 𝑌)) = ( -1↑(𝑋 + 𝑌)))
Theorem	psgnuni 19755	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 19756*	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 19757*	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 19758	The finitary permutations are a subgroup. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝐷 ∈ 𝑉 → dom 𝑁 ∈ (SubGrp‘𝐺))
Theorem	psgneldm 19759	Property of being a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    ⇒   ⊢ (𝑃 ∈ dom 𝑁 ↔ (𝑃 ∈ 𝐵 ∧ dom (𝑃 ∖ I ) ∈ Fin))
Theorem	psgneldm2 19760*	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 19761	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 19762*	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 19763*	Value of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑃 ∈ dom 𝑁 → (𝑁‘𝑃) = (℩𝑠∃𝑤 ∈ Word 𝑇(𝑃 = (𝐺 Σg 𝑤) ∧ 𝑠 = ( -1↑(♯‘𝑤)))))
Theorem	psgnvali 19764*	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 19765	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 19766	All transpositions are odd. (Contributed by Stefan O'Rear, 29-Aug-2015.)
⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝑇 = ran (pmTrsp‘𝐷)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ (𝑃 ∈ 𝑇 → (𝑁‘𝑃) = -1)
Theorem	psgn0fv0 19767	The permutation sign function for an empty set at an empty set is 1. (Contributed by AV, 27-Feb-2019.)
⊢ ((pmSgn‘∅)‘∅) = 1
Theorem	sygbasnfpfi 19768	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 19769*	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 19770*	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 19771	The range of the permutation sign function for finite permutations. (Contributed by AV, 1-Jan-2019.)
⊢ 𝑃 = (Base‘(SymGrp‘𝑁))    &   ⊢ 𝑆 = (pmSgn‘𝑁)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃) → (𝑆‘𝑄) ∈ {1, -1})
Theorem	gsmtrcl 19772	The group sum of transpositions of a finite set is a permutation, see also psgneldm2i 19761. (Contributed by AV, 19-Jan-2019.)
⊢ 𝑆 = (SymGrp‘𝑁)    &   ⊢ 𝐵 = (Base‘𝑆)    &   ⊢ 𝑇 = ran (pmTrsp‘𝑁)    ⇒   ⊢ ((𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇) → (𝑆 Σg 𝑊) ∈ 𝐵)
Theorem	psgnfitr 19773*	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 19774*	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 19775	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 19776	The permutation sign function for a singleton. (Contributed by AV, 6-Aug-2019.)
⊢ 𝐷 = {𝐴}    &   ⊢ 𝐺 = (SymGrp‘𝐷)    &   ⊢ 𝐵 = (Base‘𝐺)    &   ⊢ 𝑁 = (pmSgn‘𝐷)    ⇒   ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = 1)
Theorem	psgnprfval 19777*	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 19778	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 19779	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 19780	Extend class notation to include the order function on the elements of a group.
class od
Syntax	cgex 19781	Extend class notation to include the order function on the elements of a group.
class gEx
Syntax	cpgp 19782	Extend class notation to include the class of all p-groups.
class pGrp
Syntax	cslw 19783	Extend class notation to include the class of all Sylow p-subgroups of a group.
class pSyl
Definition	df-od 19784*	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 19785*	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 19786*	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 19787*	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 19788*	Value of the order function. For a shorter proof using ax-rep 5236, see odfvalALT 19789. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by AV, 5-Oct-2020.) Remove dependency on ax-rep 5236. (Revised by Rohan Ridenour, 17-Aug-2023.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    ⇒   ⊢ 𝑂 = (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < )))
Theorem	odfvalALT 19789*	Shorter proof of odfval 19788 using ax-rep 5236. (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 19790*	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 19791*	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 19792	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 19793	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 19794	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 19795	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 19796	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 19797	Lemma for mndodcong 19798. (Contributed by Mario Carneiro, 23-Sep-2015.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝑂 = (od‘𝐺)    &   ⊢ · = (.g‘𝐺)    &   ⊢ 0 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ Mnd)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → 𝑀 < (𝑂‘𝐴))    &   ⊢ (𝜑 → 𝑁 < (𝑂‘𝐴))    &   ⊢ (𝜑 → (𝑀 · 𝐴) = (𝑁 · 𝐴))    ⇒   ⊢ ((𝜑 ∧ 𝑀 ≤ 𝑁) → 𝑀 = 𝑁)
Theorem	mndodcong 19798	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 19799	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 19800	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 ))