Home | Metamath
Proof Explorer Theorem List (p. 179 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | odinv 17801 | The order of the inverse of a group element. (Contributed by Mario Carneiro, 20-Oct-2015.) |
⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐼 = (invg‘𝐺) & ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑂‘(𝐼‘𝐴)) = (𝑂‘𝐴)) | ||
Theorem | odf1 17802* | 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 17803* | 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 17804* | 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 17805 | The order of an element of a finite group is finite. (Contributed by Mario Carneiro, 14-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∈ ℕ) | ||
Theorem | oddvds2 17806 | 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 17807 | 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 17808 | 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 17809 | 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 17810* | 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 17811* | 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 17812 | 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 17813 | If an element has nonzero order, it generates a subgroup with size equal to the order. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) ∈ ℕ) → (#‘(𝐾‘{𝐴})) = (𝑂‘𝐴)) | ||
Theorem | odhash3 17814 | An element which generates a finite subgroup has order the size of that subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝐾‘{𝐴}) ∈ Fin) → (𝑂‘𝐴) = (#‘(𝐾‘{𝐴}))) | ||
Theorem | odngen 17815* | A cyclic subgroup of size (𝑂‘𝐴) has (ϕ‘(𝑂‘𝐴)) generators. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) & ⊢ 𝐾 = (mrCls‘(SubGrp‘𝐺)) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (𝑂‘𝐴) ∈ ℕ) → (#‘{𝑥 ∈ (𝐾‘{𝐴}) ∣ (𝑂‘𝑥) = (𝑂‘𝐴)}) = (ϕ‘(𝑂‘𝐴))) | ||
Theorem | gexval 17816* | Value of the exponent of a group. (Contributed by Mario Carneiro, 23-Apr-2016.) (Revised by AV, 26-Sep-2020.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 𝐼 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝐸 = if(𝐼 = ∅, 0, inf(𝐼, ℝ, < ))) | ||
Theorem | gexlem1 17817* | The group element order is either zero or a nonzero multiplier that annihilates the element. (Contributed by Mario Carneiro, 23-Apr-2016.) (Proof shortened by AV, 26-Sep-2020.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 0 = (0g‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 𝐼 = {𝑦 ∈ ℕ ∣ ∀𝑥 ∈ 𝑋 (𝑦 · 𝑥) = 0 } ⇒ ⊢ (𝐺 ∈ 𝑉 → ((𝐸 = 0 ∧ 𝐼 = ∅) ∨ 𝐸 ∈ 𝐼)) | ||
Theorem | gexcl 17818 | The exponent of a group is a nonnegative integer. (Contributed by Mario Carneiro, 23-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → 𝐸 ∈ ℕ0) | ||
Theorem | gexid 17819 | Any element to the power of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ (𝐴 ∈ 𝑋 → (𝐸 · 𝐴) = 0 ) | ||
Theorem | gexlem2 17820* | Any positive annihilator of all the group elements is an upper bound on the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.) (Proof shortened by AV, 26-Sep-2020.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑁 ∈ ℕ ∧ ∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 ) → 𝐸 ∈ (1...𝑁)) | ||
Theorem | gexdvdsi 17821 | Any group element is annihilated by any multiple of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∥ 𝑁) → (𝑁 · 𝐴) = 0 ) | ||
Theorem | gexdvds 17822* | The only 𝑁 that annihilate all the elements of the group are the multiples of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ · = (.g‘𝐺) & ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → (𝐸 ∥ 𝑁 ↔ ∀𝑥 ∈ 𝑋 (𝑁 · 𝑥) = 0 )) | ||
Theorem | gexdvds2 17823* | An integer divides the group exponent iff it divides all the group orders. In other words, the group exponent is the LCM of the orders of all the elements. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ) → (𝐸 ∥ 𝑁 ↔ ∀𝑥 ∈ 𝑋 (𝑂‘𝑥) ∥ 𝑁)) | ||
Theorem | gexod 17824 | Any group element is annihilated by any multiple of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∥ 𝐸) | ||
Theorem | gexcl3 17825* | If the order of every group element is bounded by 𝑁, the group has finite exponent. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 (𝑂‘𝑥) ∈ (1...𝑁)) → 𝐸 ∈ ℕ) | ||
Theorem | gexnnod 17826 | Every group element has finite order if the exponent is finite. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∈ ℕ) | ||
Theorem | gexcl2 17827 | The exponent of a finite group is finite. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → 𝐸 ∈ ℕ) | ||
Theorem | gexdvds3 17828 | The exponent 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, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → 𝐸 ∥ (#‘𝑋)) | ||
Theorem | gex1 17829 | A group or monoid has exponent 1 iff it is trivial. (Contributed by Mario Carneiro, 24-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → (𝐸 = 1 ↔ 𝑋 ≈ 1𝑜)) | ||
Theorem | ispgp 17830* | A group is a 𝑃-group if every element has some power of 𝑃 as its order. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ 𝐺 ∈ Grp ∧ ∀𝑥 ∈ 𝑋 ∃𝑛 ∈ ℕ0 (𝑂‘𝑥) = (𝑃↑𝑛))) | ||
Theorem | pgpprm 17831 | Reverse closure for the first argument of pGrp. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ (𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ) | ||
Theorem | pgpgrp 17832 | Reverse closure for the second argument of pGrp. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ (𝑃 pGrp 𝐺 → 𝐺 ∈ Grp) | ||
Theorem | pgpfi1 17833 | A finite group with order a power of a prime 𝑃 is a 𝑃-group. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ ∧ 𝑁 ∈ ℕ0) → ((#‘𝑋) = (𝑃↑𝑁) → 𝑃 pGrp 𝐺)) | ||
Theorem | pgp0 17834 | The identity subgroup is a 𝑃-group for every prime 𝑃. (Contributed by Mario Carneiro, 19-Jan-2015.) |
⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ) → 𝑃 pGrp (𝐺 ↾s { 0 })) | ||
Theorem | subgpgp 17835 | A subgroup of a p-group is a p-group. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ ((𝑃 pGrp 𝐺 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾s 𝑆)) | ||
Theorem | sylow1lem1 17836* | Lemma for sylow1 17841. The p-adic valuation of the size of 𝑆 is equal to the number of excess powers of 𝑃 in (#‘𝑋) / (𝑃↑𝑁). (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝑃↑𝑁) ∥ (#‘𝑋)) & ⊢ + = (+g‘𝐺) & ⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)} ⇒ ⊢ (𝜑 → ((#‘𝑆) ∈ ℕ ∧ (𝑃 pCnt (#‘𝑆)) = ((𝑃 pCnt (#‘𝑋)) − 𝑁))) | ||
Theorem | sylow1lem2 17837* | Lemma for sylow1 17841. The function ⊕ is a group action on 𝑆. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝑃↑𝑁) ∥ (#‘𝑋)) & ⊢ + = (+g‘𝐺) & ⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)} & ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) ⇒ ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑆)) | ||
Theorem | sylow1lem3 17838* | Lemma for sylow1 17841. One of the orbits of the group action has p-adic valuation less than the prime count of the set 𝑆. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝑃↑𝑁) ∥ (#‘𝑋)) & ⊢ + = (+g‘𝐺) & ⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)} & ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) & ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑆 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ⇒ ⊢ (𝜑 → ∃𝑤 ∈ 𝑆 (𝑃 pCnt (#‘[𝑤] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) | ||
Theorem | sylow1lem4 17839* | Lemma for sylow1 17841. The stabilizer subgroup of any element of 𝑆 is at most 𝑃↑𝑁 in size. (Contributed by Mario Carneiro, 15-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝑃↑𝑁) ∥ (#‘𝑋)) & ⊢ + = (+g‘𝐺) & ⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)} & ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) & ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑆 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐵) = 𝐵} ⇒ ⊢ (𝜑 → (#‘𝐻) ≤ (𝑃↑𝑁)) | ||
Theorem | sylow1lem5 17840* | Lemma for sylow1 17841. Using Lagrange's theorem and the orbit-stabilizer theorem, show that there is a subgroup with size exactly 𝑃↑𝑁. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝑃↑𝑁) ∥ (#‘𝑋)) & ⊢ + = (+g‘𝐺) & ⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)} & ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) & ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑆 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐵) = 𝐵} & ⊢ (𝜑 → (𝑃 pCnt (#‘[𝐵] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) ⇒ ⊢ (𝜑 → ∃ℎ ∈ (SubGrp‘𝐺)(#‘ℎ) = (𝑃↑𝑁)) | ||
Theorem | sylow1 17841* | Sylow's first theorem. If 𝑃↑𝑁 is a prime power that divides the cardinality of 𝐺, then 𝐺 has a supgroup with size 𝑃↑𝑁. This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝑃↑𝑁) ∥ (#‘𝑋)) ⇒ ⊢ (𝜑 → ∃𝑔 ∈ (SubGrp‘𝐺)(#‘𝑔) = (𝑃↑𝑁)) | ||
Theorem | odcau 17842* | Cauchy's theorem for the order of an element in a group. A finite group whose order divides a prime 𝑃 contains an element of order 𝑃. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ (((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) ∧ 𝑃 ∥ (#‘𝑋)) → ∃𝑔 ∈ 𝑋 (𝑂‘𝑔) = 𝑃) | ||
Theorem | pgpfi 17843* | The converse to pgpfi1 17833. A finite group is a 𝑃-group iff it has size some power of 𝑃. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0 (#‘𝑋) = (𝑃↑𝑛)))) | ||
Theorem | pgpfi2 17844 | Alternate version of pgpfi 17843. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ (#‘𝑋) = (𝑃↑(𝑃 pCnt (#‘𝑋)))))) | ||
Theorem | pgphash 17845 | The order of a p-group. (Contributed by Mario Carneiro, 27-Apr-2016.) |
⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝑃 pGrp 𝐺 ∧ 𝑋 ∈ Fin) → (#‘𝑋) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) | ||
Theorem | isslw 17846* | The property of being a Sylow subgroup. A Sylow 𝑃-subgroup is a 𝑃-group which has no proper supersets that are also 𝑃-groups. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) ↔ (𝑃 ∈ ℙ ∧ 𝐻 ∈ (SubGrp‘𝐺) ∧ ∀𝑘 ∈ (SubGrp‘𝐺)((𝐻 ⊆ 𝑘 ∧ 𝑃 pGrp (𝐺 ↾s 𝑘)) ↔ 𝐻 = 𝑘))) | ||
Theorem | slwprm 17847 | Reverse closure for the first argument of a Sylow 𝑃-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) (Revised by Mario Carneiro, 2-May-2015.) |
⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) → 𝑃 ∈ ℙ) | ||
Theorem | slwsubg 17848 | A Sylow 𝑃-subgroup is a subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) → 𝐻 ∈ (SubGrp‘𝐺)) | ||
Theorem | slwispgp 17849 | Defining property of a Sylow 𝑃-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ 𝑆 = (𝐺 ↾s 𝐾) ⇒ ⊢ ((𝐻 ∈ (𝑃 pSyl 𝐺) ∧ 𝐾 ∈ (SubGrp‘𝐺)) → ((𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆) ↔ 𝐻 = 𝐾)) | ||
Theorem | slwpss 17850 | A proper superset of a Sylow subgroup is not a 𝑃-group. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ 𝑆 = (𝐺 ↾s 𝐾) ⇒ ⊢ ((𝐻 ∈ (𝑃 pSyl 𝐺) ∧ 𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐻 ⊊ 𝐾) → ¬ 𝑃 pGrp 𝑆) | ||
Theorem | slwpgp 17851 | A Sylow 𝑃-subgroup is a 𝑃-group. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ 𝑆 = (𝐺 ↾s 𝐻) ⇒ ⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) → 𝑃 pGrp 𝑆) | ||
Theorem | pgpssslw 17852* | Every 𝑃-subgroup is contained in a Sylow 𝑃-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝑆 = (𝐺 ↾s 𝐻) & ⊢ 𝐹 = (𝑥 ∈ {𝑦 ∈ (SubGrp‘𝐺) ∣ (𝑃 pGrp (𝐺 ↾s 𝑦) ∧ 𝐻 ⊆ 𝑦)} ↦ (#‘𝑥)) ⇒ ⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ 𝑋 ∈ Fin ∧ 𝑃 pGrp 𝑆) → ∃𝑘 ∈ (𝑃 pSyl 𝐺)𝐻 ⊆ 𝑘) | ||
Theorem | slwn0 17853 | Every finite group contains a Sylow 𝑃-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) → (𝑃 pSyl 𝐺) ≠ ∅) | ||
Theorem | subgslw 17854 | A Sylow subgroup that is contained in a larger subgroup is also Sylow with respect to the subgroup. (The converse need not be true.) (Contributed by Mario Carneiro, 19-Jan-2015.) |
⊢ 𝐻 = (𝐺 ↾s 𝑆) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝐾 ∈ (𝑃 pSyl 𝐺) ∧ 𝐾 ⊆ 𝑆) → 𝐾 ∈ (𝑃 pSyl 𝐻)) | ||
Theorem | sylow2alem1 17855* | Lemma for sylow2a 17857. An equivalence class of fixed points is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌)) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ∈ Fin) & ⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢} & ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → [𝐴] ∼ = {𝐴}) | ||
Theorem | sylow2alem2 17856* | Lemma for sylow2a 17857. All the orbits which are not for fixed points have size ∣ 𝐺 ∣ / ∣ 𝐺𝑥 ∣ (where 𝐺𝑥 is the stabilizer subgroup) and thus are powers of 𝑃. And since they are all nontrivial (because any orbit which is a singleton is a fixed point), they all divide 𝑃, and so does the sum of all of them. (Contributed by Mario Carneiro, 17-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌)) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ∈ Fin) & ⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢} & ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ⇒ ⊢ (𝜑 → 𝑃 ∥ Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫 𝑍)(#‘𝑧)) | ||
Theorem | sylow2a 17857* | A named lemma of Sylow's second and third theorems. If 𝐺 is a finite 𝑃-group that acts on the finite set 𝑌, then the set 𝑍 of all points of 𝑌 fixed by every element of 𝐺 has cardinality equivalent to the cardinality of 𝑌, mod 𝑃. (Contributed by Mario Carneiro, 17-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌)) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ∈ Fin) & ⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢} & ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ⇒ ⊢ (𝜑 → 𝑃 ∥ ((#‘𝑌) − (#‘𝑍))) | ||
Theorem | sylow2blem1 17858* | Lemma for sylow2b 17861. Evaluate the group action on a left coset. (Contributed by Mario Carneiro, 17-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) & ⊢ + = (+g‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝐾) & ⊢ · = (𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐵 · [𝐶] ∼ ) = [(𝐵 + 𝐶)] ∼ ) | ||
Theorem | sylow2blem2 17859* | Lemma for sylow2b 17861. Left multiplication in a subgroup 𝐻 is a group action on the set of all left cosets of 𝐾. (Contributed by Mario Carneiro, 17-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) & ⊢ + = (+g‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝐾) & ⊢ · = (𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) ⇒ ⊢ (𝜑 → · ∈ ((𝐺 ↾s 𝐻) GrpAct (𝑋 / ∼ ))) | ||
Theorem | sylow2blem3 17860* | Sylow's second theorem. Putting together the results of sylow2a 17857 and the orbit-stabilizer theorem to show that 𝑃 does not divide the set of all fixed points under the group action, we get that there is a fixed point of the group action, so that there is some 𝑔 ∈ 𝑋 with ℎ𝑔𝐾 = 𝑔𝐾 for all ℎ ∈ 𝐻. This implies that invg(𝑔)ℎ𝑔 ∈ 𝐾, so ℎ is in the conjugated subgroup 𝑔𝐾invg(𝑔). (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) & ⊢ + = (+g‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝐾) & ⊢ · = (𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) & ⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s 𝐻)) & ⊢ (𝜑 → (#‘𝐾) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝜑 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) | ||
Theorem | sylow2b 17861* | Sylow's second theorem. Any 𝑃-group 𝐻 is a subgroup of a conjugated 𝑃-group 𝐾 of order 𝑃↑𝑛 ∥ (#‘𝑋) with 𝑛 maximal. This is usually stated under the assumption that 𝐾 is a Sylow subgroup, but we use a slightly different definition, whose equivalence to this one requires this theorem. This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) & ⊢ + = (+g‘𝐺) & ⊢ (𝜑 → 𝑃 pGrp (𝐺 ↾s 𝐻)) & ⊢ (𝜑 → (#‘𝐾) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝜑 → ∃𝑔 ∈ 𝑋 𝐻 ⊆ ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) | ||
Theorem | slwhash 17862 | A sylow subgroup has cardinality equal to the maximum power of 𝑃 dividing the group. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐻 ∈ (𝑃 pSyl 𝐺)) ⇒ ⊢ (𝜑 → (#‘𝐻) = (𝑃↑(𝑃 pCnt (#‘𝑋)))) | ||
Theorem | fislw 17863 | The sylow subgroups of a finite group are exactly the groups which have cardinality equal to the maximum power of 𝑃 dividing the group. (Contributed by Mario Carneiro, 16-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) → (𝐻 ∈ (𝑃 pSyl 𝐺) ↔ (𝐻 ∈ (SubGrp‘𝐺) ∧ (#‘𝐻) = (𝑃↑(𝑃 pCnt (#‘𝑋)))))) | ||
Theorem | sylow2 17864* | Sylow's second theorem. See also sylow2b 17861 for the "hard" part of the proof. Any two Sylow 𝑃-subgroups are conjugate to one another, and hence the same size, namely 𝑃↑(𝑃 pCnt ∣ 𝑋 ∣ ) (see fislw 17863). This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐻 ∈ (𝑃 pSyl 𝐺)) & ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺)) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝜑 → ∃𝑔 ∈ 𝑋 𝐻 = ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) | ||
Theorem | sylow3lem1 17865* | Lemma for sylow3 17871, first part. (Contributed by Mario Carneiro, 19-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) ⇒ ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺))) | ||
Theorem | sylow3lem2 17866* | Lemma for sylow3 17871, first part. The stabilizer of a given Sylow subgroup 𝐾 in the group action ⊕ acting on all of 𝐺 is the normalizer NG(K). (Contributed by Mario Carneiro, 19-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) & ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺)) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾} & ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)} ⇒ ⊢ (𝜑 → 𝐻 = 𝑁) | ||
Theorem | sylow3lem3 17867* | Lemma for sylow3 17871, first part. The number of Sylow subgroups is the same as the index (number of cosets) of the normalizer of the Sylow subgroup 𝐾. (Contributed by Mario Carneiro, 19-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) & ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺)) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾} & ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)} ⇒ ⊢ (𝜑 → (#‘(𝑃 pSyl 𝐺)) = (#‘(𝑋 / (𝐺 ~QG 𝑁)))) | ||
Theorem | sylow3lem4 17868* | Lemma for sylow3 17871, first part. The number of Sylow subgroups is a divisor of the size of 𝐺 reduced by the size of a Sylow subgroup of 𝐺. (Contributed by Mario Carneiro, 19-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) & ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺)) & ⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐾) = 𝐾} & ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝐾 ↔ (𝑦 + 𝑥) ∈ 𝐾)} ⇒ ⊢ (𝜑 → (#‘(𝑃 pSyl 𝐺)) ∥ ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋))))) | ||
Theorem | sylow3lem5 17869* | Lemma for sylow3 17871, second part. Reduce the group action of sylow3lem1 17865 to a given Sylow subgroup. (Contributed by Mario Carneiro, 19-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺)) & ⊢ ⊕ = (𝑥 ∈ 𝐾, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) ⇒ ⊢ (𝜑 → ⊕ ∈ ((𝐺 ↾s 𝐾) GrpAct (𝑃 pSyl 𝐺))) | ||
Theorem | sylow3lem6 17870* | Lemma for sylow3 17871, second part. Using the lemma sylow2a 17857, show that the number of sylow subgroups is equivalent mod 𝑃 to the number of fixed points under the group action. But 𝐾 is the unique element of the set of Sylow subgroups that is fixed under the group action, so there is exactly one fixed point and so ((#‘(𝑃 pSyl 𝐺)) mod 𝑃) = 1. (Contributed by Mario Carneiro, 19-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺)) & ⊢ ⊕ = (𝑥 ∈ 𝐾, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) & ⊢ 𝑁 = {𝑥 ∈ 𝑋 ∣ ∀𝑦 ∈ 𝑋 ((𝑥 + 𝑦) ∈ 𝑠 ↔ (𝑦 + 𝑥) ∈ 𝑠)} ⇒ ⊢ (𝜑 → ((#‘(𝑃 pSyl 𝐺)) mod 𝑃) = 1) | ||
Theorem | sylow3 17871 | Sylow's third theorem. The number of Sylow subgroups is a divisor of ∣ 𝐺 ∣ / 𝑑, where 𝑑 is the common order of a Sylow subgroup, and is equivalent to 1 mod 𝑃. This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 19-Jan-2015.) |
⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ 𝑁 = (#‘(𝑃 pSyl 𝐺)) ⇒ ⊢ (𝜑 → (𝑁 ∥ ((#‘𝑋) / (𝑃↑(𝑃 pCnt (#‘𝑋)))) ∧ (𝑁 mod 𝑃) = 1)) | ||
Syntax | clsm 17872 | Extend class notation with subgroup sum. |
class LSSum | ||
Syntax | cpj1 17873 | Extend class notation with left projection. |
class proj1 | ||
Definition | df-lsm 17874* | Define subgroup sum (inner direct product of subgroups). (Contributed by NM, 28-Jan-2014.) |
⊢ LSSum = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑤)𝑦)))) | ||
Definition | df-pj1 17875* | Define the left projection function, which takes two subgroups 𝑡, 𝑢 with trivial intersection and returns a function mapping the elements of the subgroup sum 𝑡 + 𝑢 to their projections onto 𝑡. (The other projection function can be obtained by swapping the roles of 𝑡 and 𝑢.) (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ proj1 = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ (𝑧 ∈ (𝑡(LSSum‘𝑤)𝑢) ↦ (℩𝑥 ∈ 𝑡 ∃𝑦 ∈ 𝑢 𝑧 = (𝑥(+g‘𝑤)𝑦))))) | ||
Theorem | lsmfval 17876* | The subgroup sum function (for a group or vector space). (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝐺 ∈ 𝑉 → ⊕ = (𝑡 ∈ 𝒫 𝐵, 𝑢 ∈ 𝒫 𝐵 ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥 + 𝑦)))) | ||
Theorem | lsmvalx 17877* | Subspace sum value (for a group or vector space). Extended domain version of lsmval 17886. (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇 ⊕ 𝑈) = ran (𝑥 ∈ 𝑇, 𝑦 ∈ 𝑈 ↦ (𝑥 + 𝑦))) | ||
Theorem | lsmelvalx 17878* | Subspace sum membership (for a group or vector space). Extended domain version of lsmelval 17887. (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑋 = (𝑦 + 𝑧))) | ||
Theorem | lsmelvalix 17879 | Subspace sum membership (for a group or vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) ∧ (𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑈)) → (𝑋 + 𝑌) ∈ (𝑇 ⊕ 𝑈)) | ||
Theorem | oppglsm 17880 | The subspace sum operation in the opposite group. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝑂 = (oppg‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝑇(LSSum‘𝑂)𝑈) = (𝑈 ⊕ 𝑇) | ||
Theorem | lsmssv 17881 | Subgroup sum is a subset of the base. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇 ⊕ 𝑈) ⊆ 𝐵) | ||
Theorem | lsmless1x 17882 | Subset implies subgroup sum subset (extended domain version). (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) ∧ 𝑅 ⊆ 𝑇) → (𝑅 ⊕ 𝑈) ⊆ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmless2x 17883 | Subset implies subgroup sum subset (extended domain version). (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (((𝐺 ∈ 𝑉 ∧ 𝑅 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) ∧ 𝑇 ⊆ 𝑈) → (𝑅 ⊕ 𝑇) ⊆ (𝑅 ⊕ 𝑈)) | ||
Theorem | lsmub1x 17884 | Subgroup sum is an upper bound of its arguments. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ⊆ 𝐵 ∧ 𝑈 ∈ (SubMnd‘𝐺)) → 𝑇 ⊆ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmub2x 17885 | Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubMnd‘𝐺) ∧ 𝑈 ⊆ 𝐵) → 𝑈 ⊆ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmval 17886* | Subgroup sum value (for a left module or left vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊕ 𝑈) = ran (𝑥 ∈ 𝑇, 𝑦 ∈ 𝑈 ↦ (𝑥 + 𝑦))) | ||
Theorem | lsmelval 17887* | Subgroup sum membership (for a left module or left vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑋 = (𝑦 + 𝑧))) | ||
Theorem | lsmelvali 17888 | Subgroup sum membership (for a left module or left vector space). (Contributed by NM, 4-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ (𝑋 ∈ 𝑇 ∧ 𝑌 ∈ 𝑈)) → (𝑋 + 𝑌) ∈ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmelvalm 17889* | Subgroup sum membership analogue of lsmelval 17887 using vector subtraction. TODO: any way to shorten proof? (Contributed by NM, 16-Mar-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ − = (-g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑋 = (𝑦 − 𝑧))) | ||
Theorem | lsmelvalmi 17890 | Membership of vector subtraction in subgroup sum. (Contributed by NM, 27-Apr-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ − = (-g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑋 ∈ 𝑇) & ⊢ (𝜑 → 𝑌 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋 − 𝑌) ∈ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmsubm 17891 | The sum of two commuting submonoids is a submonoid. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubMnd‘𝐺) ∧ 𝑈 ∈ (SubMnd‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) ∈ (SubMnd‘𝐺)) | ||
Theorem | lsmsubg 17892 | The sum of two commuting subgroups is a subgroup. (Contributed by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) ∈ (SubGrp‘𝐺)) | ||
Theorem | lsmcom2 17893 | Subgroup sum commutes. (Contributed by Mario Carneiro, 22-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) | ||
Theorem | lsmub1 17894 | Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑇 ⊆ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmub2 17895 | Subgroup sum is an upper bound of its arguments. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → 𝑈 ⊆ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmunss 17896 | Union of subgroups is a subset of subgroup sum. (Contributed by NM, 6-Feb-2014.) (Proof shortened by Mario Carneiro, 21-Jun-2014.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ∪ 𝑈) ⊆ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmless1 17897 | Subset implies subgroup sum subset. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑆 ⊆ 𝑇) → (𝑆 ⊕ 𝑈) ⊆ (𝑇 ⊕ 𝑈)) | ||
Theorem | lsmless2 17898 | Subset implies subgroup sum subset. (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ 𝑈) → (𝑆 ⊕ 𝑇) ⊆ (𝑆 ⊕ 𝑈)) | ||
Theorem | lsmless12 17899 | Subset implies subgroup sum subset. (Contributed by NM, 14-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ (𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈)) → (𝑅 ⊕ 𝑇) ⊆ (𝑆 ⊕ 𝑈)) | ||
Theorem | lsmidm 17900 | Subgroup sum is idempotent. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝑈 ⊕ 𝑈) = 𝑈) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |