Home | Metamath
Proof Explorer Theorem List (p. 187 of 450) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pmtr3ncomlem1 18601 | Lemma 1 for pmtr3ncom 18603. (Contributed by AV, 17-Mar-2018.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌}) & ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍}) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝐺 ∘ 𝐹)‘𝑋) ≠ ((𝐹 ∘ 𝐺)‘𝑋)) | ||
Theorem | pmtr3ncomlem2 18602 | Lemma 2 for pmtr3ncom 18603. (Contributed by AV, 17-Mar-2018.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌}) & ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍}) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐺 ∘ 𝐹) ≠ (𝐹 ∘ 𝐺)) | ||
Theorem | pmtr3ncom 18603* | 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 18604 | Lemma 1 for pmtrdifel 18608. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ (𝑄 ∈ 𝑇 → 𝑆 ∈ 𝑅) | ||
Theorem | pmtrdifellem2 18605 | Lemma 2 for pmtrdifel 18608. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ (𝑄 ∈ 𝑇 → dom (𝑆 ∖ I ) = dom (𝑄 ∖ I )) | ||
Theorem | pmtrdifellem3 18606* | Lemma 3 for pmtrdifel 18608. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ (𝑄 ∈ 𝑇 → ∀𝑥 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑥) = (𝑆‘𝑥)) | ||
Theorem | pmtrdifellem4 18607 | Lemma 4 for pmtrdifel 18608. (Contributed by AV, 28-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → (𝑆‘𝐾) = 𝐾) | ||
Theorem | pmtrdifel 18608* | 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 18609* | Lemma 1 for pmtrdifwrdel 18613. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I ))) ⇒ ⊢ (𝑊 ∈ Word 𝑇 → 𝑈 ∈ Word 𝑅) | ||
Theorem | pmtrdifwrdellem2 18610* | Lemma 2 for pmtrdifwrdel 18613. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I ))) ⇒ ⊢ (𝑊 ∈ Word 𝑇 → (♯‘𝑊) = (♯‘𝑈)) | ||
Theorem | pmtrdifwrdellem3 18611* | Lemma 3 for pmtrdifwrdel 18613. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I ))) ⇒ ⊢ (𝑊 ∈ Word 𝑇 → ∀𝑖 ∈ (0..^(♯‘𝑊))∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)) | ||
Theorem | pmtrdifwrdel2lem1 18612* | Lemma 1 for pmtrdifwrdel2 18614. (Contributed by AV, 31-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I ))) ⇒ ⊢ ((𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁) → ∀𝑖 ∈ (0..^(♯‘𝑊))((𝑈‘𝑖)‘𝐾) = 𝐾) | ||
Theorem | pmtrdifwrdel 18613* | 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 18614* | 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 18615* | The transpositions on a pair. (Contributed by AV, 9-Dec-2018.) |
⊢ (pmTrsp‘{1, 2}) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) | ||
Theorem | pmtrprfvalrn 18616 | 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〉}} | ||
Syntax | cpsgn 18617 | Syntax for the sign of a permutation. |
class pmSgn | ||
Syntax | cevpm 18618 | Syntax for even permutations. |
class pmEven | ||
Definition | df-psgn 18619* | 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 18620 | Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018.) |
⊢ pmEven = (𝑑 ∈ V ↦ (◡(pmSgn‘𝑑) “ {1})) | ||
Theorem | psgnunilem1 18621* | Lemma for psgnuni 18627. 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 18622* | Lemma for psgnuni 18627. 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 18623* | Lemma for psgnuni 18627. 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 18624* | Lemma for psgnuni 18627. 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 18625 | Lemma for psgnuni 18627. 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 18626 | Addition and subtraction of parities are the same. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (-1↑(𝑋 − 𝑌)) = (-1↑(𝑋 + 𝑌))) | ||
Theorem | psgnuni 18627 | 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 18628* | 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 18629* | 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 18630 | The finitary permutations are a subgroup. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) ⇒ ⊢ (𝐷 ∈ 𝑉 → dom 𝑁 ∈ (SubGrp‘𝐺)) | ||
Theorem | psgneldm 18631 | Property of being a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑃 ∈ dom 𝑁 ↔ (𝑃 ∈ 𝐵 ∧ dom (𝑃 ∖ I ) ∈ Fin)) | ||
Theorem | psgneldm2 18632* | 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 18633 | 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 18634* | 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 18635* | Value of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝑇 = ran (pmTrsp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) ⇒ ⊢ (𝑃 ∈ dom 𝑁 → (𝑁‘𝑃) = (℩𝑠∃𝑤 ∈ Word 𝑇(𝑃 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))) | ||
Theorem | psgnvali 18636* | 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 18637 | 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 18638 | All transpositions are odd. (Contributed by Stefan O'Rear, 29-Aug-2015.) |
⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝑇 = ran (pmTrsp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) ⇒ ⊢ (𝑃 ∈ 𝑇 → (𝑁‘𝑃) = -1) | ||
Theorem | psgn0fv0 18639 | The permutation sign function for an empty set at an empty set is 1. (Contributed by AV, 27-Feb-2019.) |
⊢ ((pmSgn‘∅)‘∅) = 1 | ||
Theorem | sygbasnfpfi 18640 | 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 18641* | 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 18642* | 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 18643 | The range of the permutation sign function for finite permutations. (Contributed by AV, 1-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑆 = (pmSgn‘𝑁) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃) → (𝑆‘𝑄) ∈ {1, -1}) | ||
Theorem | gsmtrcl 18644 | The group sum of transpositions of a finite set is a permutation, see also psgneldm2i 18633. (Contributed by AV, 19-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑇 = ran (pmTrsp‘𝑁) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇) → (𝑆 Σg 𝑊) ∈ 𝐵) | ||
Theorem | psgnfitr 18645* | 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 18646* | 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 18647 | 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 18648 | The permutation sign function for a singleton. (Contributed by AV, 6-Aug-2019.) |
⊢ 𝐷 = {𝐴} & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (pmSgn‘𝐷) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = 1) | ||
Theorem | psgnprfval 18649* | 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 18650 | 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 18651 | 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 | ||
Syntax | cod 18652 | Extend class notation to include the order function on the elements of a group. |
class od | ||
Syntax | cgex 18653 | Extend class notation to include the order function on the elements of a group. |
class gEx | ||
Syntax | cpgp 18654 | Extend class notation to include the class of all p-groups. |
class pGrp | ||
Syntax | cslw 18655 | Extend class notation to include the class of all Sylow p-subgroups of a group. |
class pSyl | ||
Definition | df-od 18656* | 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 18657* | 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 18658* | 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 18659* | 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 18660* | Value of the order function. For a shorter proof using ax-rep 5190, see odfvalALT 18661. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by AV, 5-Oct-2020.) Remove depedency on ax-rep 5190. (Revised by Rohan Ridenour, 17-Aug-2023.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ 𝑂 = (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) | ||
Theorem | odfvalALT 18661* | Shorter proof of odfval 18660 using ax-rep 5190. (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 18662* | 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 18663* | 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 18664 | 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 18665 | 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 18666 | 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 18667 | 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 18668 | 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 18669 | Lemma for mndodcong 18670. (Contributed by Mario Carneiro, 23-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 < (𝑂‘𝐴)) & ⊢ (𝜑 → 𝑁 < (𝑂‘𝐴)) & ⊢ (𝜑 → (𝑀 · 𝐴) = (𝑁 · 𝐴)) ⇒ ⊢ ((𝜑 ∧ 𝑀 ≤ 𝑁) → 𝑀 = 𝑁) | ||
Theorem | mndodcong 18670 | 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 18671 | 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 18672 | 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 18673 | 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 18674 | 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 18675 | 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 18676 | 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 18677 | 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 18678* | The oddvds 18675 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 18679* | 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 18680 | The order of a group element is always a nonnegative integer, deduction form of odcl 18664. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ0) | ||
Theorem | odmulgid 18681 | 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 18682 | 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 18683 | 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 18684 | 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 18685* | 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 18686 | 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 18687 | 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 18688 | The order of the inverse of a group element. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑂‘(𝐼‘𝐴)) = (𝑂‘𝐴)) | ||
Theorem | odf1 18689* | 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 18690* | 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 18691* | 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 18692 | The order of an element of a finite group is finite. (Contributed by Mario Carneiro, 14-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∈ ℕ) | ||
Theorem | oddvds2 18693 | 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 18694 | 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 18695 | 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 18696 | 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 18697* | 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 18698* | 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 18699 | 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 18700 | 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 ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) ∈ ℕ) → (♯‘(𝐾‘{𝐴})) = (𝑂‘𝐴)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |