Home | Metamath
Proof Explorer Theorem List (p. 186 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | f1omvdcnv 18501 | A permutation and its inverse move the same points. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ (𝐹:𝐴–1-1-onto→𝐴 → dom (◡𝐹 ∖ I ) = dom (𝐹 ∖ I )) | ||
Theorem | mvdco 18502 | 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 18503 | Conjugation of a permutation takes the image of the moved subclass. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ ((𝐹:𝐴⟶𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) → dom (((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∖ I ) = (𝐺 “ dom (𝐹 ∖ I ))) | ||
Theorem | f1otrspeq 18504 | A transposition is characterized by the points it moves. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ (((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2o ∧ dom (𝐺 ∖ I ) = dom (𝐹 ∖ I ))) → 𝐹 = 𝐺) | ||
Theorem | f1omvdco2 18505 | 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-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴 ∧ (dom (𝐹 ∖ I ) ⊆ 𝑋 ⊻ dom (𝐺 ∖ I ) ⊆ 𝑋)) → ¬ dom ((𝐹 ∘ 𝐺) ∖ I ) ⊆ 𝑋) | ||
Theorem | f1omvdco3 18506 | 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-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴 ∧ (𝑋 ∈ dom (𝐹 ∖ I ) ⊻ 𝑋 ∈ dom (𝐺 ∖ I ))) → 𝑋 ∈ dom ((𝐹 ∘ 𝐺) ∖ I )) | ||
Theorem | pmtrfval 18507* | The function generating transpositions on a set. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ (𝐷 ∈ 𝑉 → 𝑇 = (𝑝 ∈ {𝑦 ∈ 𝒫 𝐷 ∣ 𝑦 ≈ 2o} ↦ (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑝, ∪ (𝑝 ∖ {𝑧}), 𝑧)))) | ||
Theorem | pmtrval 18508* | A generated transposition, expressed in a symmetric form. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) = (𝑧 ∈ 𝐷 ↦ if(𝑧 ∈ 𝑃, ∪ (𝑃 ∖ {𝑧}), 𝑧))) | ||
Theorem | pmtrfv 18509 | General value of mapping a point under a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ (((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) ∧ 𝑍 ∈ 𝐷) → ((𝑇‘𝑃)‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍)) | ||
Theorem | pmtrprfv 18510 | In a transposition of two given points, each maps to the other. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑋 ≠ 𝑌)) → ((𝑇‘{𝑋, 𝑌})‘𝑋) = 𝑌) | ||
Theorem | pmtrprfv3 18511 | In a transposition of two given points, all other points are mapped to themselves. (Contributed by AV, 17-Mar-2019.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝑇‘{𝑋, 𝑌})‘𝑍) = 𝑍) | ||
Theorem | pmtrf 18512 | Functionality of a transposition. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃):𝐷⟶𝐷) | ||
Theorem | pmtrmvd 18513 | A transposition moves precisely the transposed points. (Contributed by Stefan O'Rear, 16-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → dom ((𝑇‘𝑃) ∖ I ) = 𝑃) | ||
Theorem | pmtrrn 18514 | Transposing two points gives a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ 𝑃 ⊆ 𝐷 ∧ 𝑃 ≈ 2o) → (𝑇‘𝑃) ∈ 𝑅) | ||
Theorem | pmtrfrn 18515 | 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 18516 | Mapping of a point under a transposition function. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 & ⊢ 𝑃 = dom (𝐹 ∖ I ) ⇒ ⊢ ((𝐹 ∈ 𝑅 ∧ 𝑍 ∈ 𝐷) → (𝐹‘𝑍) = if(𝑍 ∈ 𝑃, ∪ (𝑃 ∖ {𝑍}), 𝑍)) | ||
Theorem | pmtrrn2 18517* | For any transposition there are two points it is transposing. (Contributed by SO, 15-Jul-2018.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → ∃𝑥 ∈ 𝐷 ∃𝑦 ∈ 𝐷 (𝑥 ≠ 𝑦 ∧ 𝐹 = (𝑇‘{𝑥, 𝑦}))) | ||
Theorem | pmtrfinv 18518 | A transposition function is an involution. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → (𝐹 ∘ 𝐹) = ( I ↾ 𝐷)) | ||
Theorem | pmtrfmvdn0 18519 | A transposition moves at least one point. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → dom (𝐹 ∖ I ) ≠ ∅) | ||
Theorem | pmtrff1o 18520 | A transposition function is a permutation. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → 𝐹:𝐷–1-1-onto→𝐷) | ||
Theorem | pmtrfcnv 18521 | A transposition function is its own inverse. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 → ◡𝐹 = 𝐹) | ||
Theorem | pmtrfb 18522 | An intrinsic characterization of the transposition permutations. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ (𝐹 ∈ 𝑅 ↔ (𝐷 ∈ V ∧ 𝐹:𝐷–1-1-onto→𝐷 ∧ dom (𝐹 ∖ I ) ≈ 2o)) | ||
Theorem | pmtrfconj 18523 | Any conjugate of a transposition is a transposition. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝑅 = ran 𝑇 ⇒ ⊢ ((𝐹 ∈ 𝑅 ∧ 𝐺:𝐷–1-1-onto→𝐷) → ((𝐺 ∘ 𝐹) ∘ ◡𝐺) ∈ 𝑅) | ||
Theorem | symgsssg 18524* | 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 18525* | 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 18526 | Transpositions are elements of the symmetric group. (Contributed by Stefan O'Rear, 23-Aug-2015.) |
⊢ 𝑇 = ran (pmTrsp‘𝐷) & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ 𝑇 ⊆ 𝐵 | ||
Theorem | symggen 18527* | 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 18528 | 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 18529 | 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 18530 | Lemma 1 for pmtr3ncom 18532. (Contributed by AV, 17-Mar-2018.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌}) & ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍}) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → ((𝐺 ∘ 𝐹)‘𝑋) ≠ ((𝐹 ∘ 𝐺)‘𝑋)) | ||
Theorem | pmtr3ncomlem2 18531 | Lemma 2 for pmtr3ncom 18532. (Contributed by AV, 17-Mar-2018.) |
⊢ 𝑇 = (pmTrsp‘𝐷) & ⊢ 𝐹 = (𝑇‘{𝑋, 𝑌}) & ⊢ 𝐺 = (𝑇‘{𝑌, 𝑍}) ⇒ ⊢ ((𝐷 ∈ 𝑉 ∧ (𝑋 ∈ 𝐷 ∧ 𝑌 ∈ 𝐷 ∧ 𝑍 ∈ 𝐷) ∧ (𝑋 ≠ 𝑌 ∧ 𝑋 ≠ 𝑍 ∧ 𝑌 ≠ 𝑍)) → (𝐺 ∘ 𝐹) ≠ (𝐹 ∘ 𝐺)) | ||
Theorem | pmtr3ncom 18532* | 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 18533 | Lemma 1 for pmtrdifel 18537. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ (𝑄 ∈ 𝑇 → 𝑆 ∈ 𝑅) | ||
Theorem | pmtrdifellem2 18534 | Lemma 2 for pmtrdifel 18537. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ (𝑄 ∈ 𝑇 → dom (𝑆 ∖ I ) = dom (𝑄 ∖ I )) | ||
Theorem | pmtrdifellem3 18535* | Lemma 3 for pmtrdifel 18537. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ (𝑄 ∈ 𝑇 → ∀𝑥 ∈ (𝑁 ∖ {𝐾})(𝑄‘𝑥) = (𝑆‘𝑥)) | ||
Theorem | pmtrdifellem4 18536 | Lemma 4 for pmtrdifel 18537. (Contributed by AV, 28-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑆 = ((pmTrsp‘𝑁)‘dom (𝑄 ∖ I )) ⇒ ⊢ ((𝑄 ∈ 𝑇 ∧ 𝐾 ∈ 𝑁) → (𝑆‘𝐾) = 𝐾) | ||
Theorem | pmtrdifel 18537* | 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 18538* | Lemma 1 for pmtrdifwrdel 18542. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I ))) ⇒ ⊢ (𝑊 ∈ Word 𝑇 → 𝑈 ∈ Word 𝑅) | ||
Theorem | pmtrdifwrdellem2 18539* | Lemma 2 for pmtrdifwrdel 18542. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I ))) ⇒ ⊢ (𝑊 ∈ Word 𝑇 → (♯‘𝑊) = (♯‘𝑈)) | ||
Theorem | pmtrdifwrdellem3 18540* | Lemma 3 for pmtrdifwrdel 18542. (Contributed by AV, 15-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I ))) ⇒ ⊢ (𝑊 ∈ Word 𝑇 → ∀𝑖 ∈ (0..^(♯‘𝑊))∀𝑛 ∈ (𝑁 ∖ {𝐾})((𝑊‘𝑖)‘𝑛) = ((𝑈‘𝑖)‘𝑛)) | ||
Theorem | pmtrdifwrdel2lem1 18541* | Lemma 1 for pmtrdifwrdel2 18543. (Contributed by AV, 31-Jan-2019.) |
⊢ 𝑇 = ran (pmTrsp‘(𝑁 ∖ {𝐾})) & ⊢ 𝑅 = ran (pmTrsp‘𝑁) & ⊢ 𝑈 = (𝑥 ∈ (0..^(♯‘𝑊)) ↦ ((pmTrsp‘𝑁)‘dom ((𝑊‘𝑥) ∖ I ))) ⇒ ⊢ ((𝑊 ∈ Word 𝑇 ∧ 𝐾 ∈ 𝑁) → ∀𝑖 ∈ (0..^(♯‘𝑊))((𝑈‘𝑖)‘𝐾) = 𝐾) | ||
Theorem | pmtrdifwrdel 18542* | 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 18543* | 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 18544* | The transpositions on a pair. (Contributed by AV, 9-Dec-2018.) |
⊢ (pmTrsp‘{1, 2}) = (𝑝 ∈ {{1, 2}} ↦ (𝑧 ∈ {1, 2} ↦ if(𝑧 = 1, 2, 1))) | ||
Theorem | pmtrprfvalrn 18545 | 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 18546 | Syntax for the sign of a permutation. |
class pmSgn | ||
Syntax | cevpm 18547 | Syntax for even permutations. |
class pmEven | ||
Definition | df-psgn 18548* | 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 18549 | Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018.) |
⊢ pmEven = (𝑑 ∈ V ↦ (◡(pmSgn‘𝑑) “ {1})) | ||
Theorem | psgnunilem1 18550* | Lemma for psgnuni 18556. 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 18551* | Lemma for psgnuni 18556. 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 18552* | Lemma for psgnuni 18556. 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 18553* | Lemma for psgnuni 18556. 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 18554 | Lemma for psgnuni 18556. 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 18555 | Addition and subtraction of parities are the same. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (-1↑(𝑋 − 𝑌)) = (-1↑(𝑋 + 𝑌))) | ||
Theorem | psgnuni 18556 | 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 18557* | 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 18558* | 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 18559 | The finitary permutations are a subgroup. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) ⇒ ⊢ (𝐷 ∈ 𝑉 → dom 𝑁 ∈ (SubGrp‘𝐺)) | ||
Theorem | psgneldm 18560 | Property of being a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝑃 ∈ dom 𝑁 ↔ (𝑃 ∈ 𝐵 ∧ dom (𝑃 ∖ I ) ∈ Fin)) | ||
Theorem | psgneldm2 18561* | 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 18562 | 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 18563* | 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 18564* | Value of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝑇 = ran (pmTrsp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) ⇒ ⊢ (𝑃 ∈ dom 𝑁 → (𝑁‘𝑃) = (℩𝑠∃𝑤 ∈ Word 𝑇(𝑃 = (𝐺 Σg 𝑤) ∧ 𝑠 = (-1↑(♯‘𝑤))))) | ||
Theorem | psgnvali 18565* | 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 18566 | 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 18567 | All transpositions are odd. (Contributed by Stefan O'Rear, 29-Aug-2015.) |
⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝑇 = ran (pmTrsp‘𝐷) & ⊢ 𝑁 = (pmSgn‘𝐷) ⇒ ⊢ (𝑃 ∈ 𝑇 → (𝑁‘𝑃) = -1) | ||
Theorem | psgn0fv0 18568 | The permutation sign function for an empty set at an empty set is 1. (Contributed by AV, 27-Feb-2019.) |
⊢ ((pmSgn‘∅)‘∅) = 1 | ||
Theorem | sygbasnfpfi 18569 | 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 18570* | 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 18571* | 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 18572 | The range of the permutation sign function for finite permutations. (Contributed by AV, 1-Jan-2019.) |
⊢ 𝑃 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑆 = (pmSgn‘𝑁) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃) → (𝑆‘𝑄) ∈ {1, -1}) | ||
Theorem | gsmtrcl 18573 | The group sum of transpositions of a finite set is a permutation, see also psgneldm2i 18562. (Contributed by AV, 19-Jan-2019.) |
⊢ 𝑆 = (SymGrp‘𝑁) & ⊢ 𝐵 = (Base‘𝑆) & ⊢ 𝑇 = ran (pmTrsp‘𝑁) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑊 ∈ Word 𝑇) → (𝑆 Σg 𝑊) ∈ 𝐵) | ||
Theorem | psgnfitr 18574* | 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 18575* | 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 18576 | 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 18577 | The permutation sign function for a singleton. (Contributed by AV, 6-Aug-2019.) |
⊢ 𝐷 = {𝐴} & ⊢ 𝐺 = (SymGrp‘𝐷) & ⊢ 𝐵 = (Base‘𝐺) & ⊢ 𝑁 = (pmSgn‘𝐷) ⇒ ⊢ ((𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝐵) → (𝑁‘𝑋) = 1) | ||
Theorem | psgnprfval 18578* | 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 18579 | 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 18580 | 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 18581 | Extend class notation to include the order function on the elements of a group. |
class od | ||
Syntax | cgex 18582 | Extend class notation to include the order function on the elements of a group. |
class gEx | ||
Syntax | cpgp 18583 | Extend class notation to include the class of all p-groups. |
class pGrp | ||
Syntax | cslw 18584 | Extend class notation to include the class of all Sylow p-subgroups of a group. |
class pSyl | ||
Definition | df-od 18585* | 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 18586* | 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 18587* | 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 18588* | 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 18589* | Value of the order function. For a shorter proof using ax-rep 5181, see odfvalALT 18590. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by AV, 5-Oct-2020.) Remove depedency on ax-rep 5181. (Revised by Rohan Ridenour, 17-Aug-2023.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ 𝑂 = (𝑥 ∈ 𝑋 ↦ ⦋{𝑦 ∈ ℕ ∣ (𝑦 · 𝑥) = 0 } / 𝑖⦌if(𝑖 = ∅, 0, inf(𝑖, ℝ, < ))) | ||
Theorem | odfvalALT 18590* | Shorter proof of odfval 18589 using ax-rep 5181. (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 18591* | 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 18592* | 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 18593 | 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 18594 | 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 18595 | 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 18596 | 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 18597 | 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 18598 | Lemma for mndodcong 18599. (Contributed by Mario Carneiro, 23-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Mnd) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ (𝜑 → (𝑂‘𝐴) ∈ ℕ) & ⊢ (𝜑 → 𝑀 ∈ ℕ0) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑀 < (𝑂‘𝐴)) & ⊢ (𝜑 → 𝑁 < (𝑂‘𝐴)) & ⊢ (𝜑 → (𝑀 · 𝐴) = (𝑁 · 𝐴)) ⇒ ⊢ ((𝜑 ∧ 𝑀 ≤ 𝑁) → 𝑀 = 𝑁) | ||
Theorem | mndodcong 18599 | 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 18600 | 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)) → ((𝑂‘𝐴) ∥ (𝑀 − 𝑁) → (𝑀 · 𝐴) = (𝑁 · 𝐴))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |