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