| Metamath
Proof Explorer Theorem List (p. 197 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | gexdvdsi 19601 | 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 19602* | 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 19603* | 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 19604 | 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 19605* | 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 19606 | Every group element has finite order if the exponent is finite. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) & ⊢ 𝑂 = (od‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝐸 ∈ ℕ ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) ∈ ℕ) | ||
| Theorem | gexcl2 19607 | The exponent of a finite group is finite. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → 𝐸 ∈ ℕ) | ||
| Theorem | gexdvds3 19608 | 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 19609 | A group or monoid has exponent 1 iff it is trivial. (Contributed by Mario Carneiro, 24-Apr-2016.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ 𝐸 = (gEx‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → (𝐸 = 1 ↔ 𝑋 ≈ 1o)) | ||
| Theorem | ispgp 19610* | 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 19611 | Reverse closure for the first argument of pGrp. (Contributed by Mario Carneiro, 15-Jan-2015.) |
| ⊢ (𝑃 pGrp 𝐺 → 𝑃 ∈ ℙ) | ||
| Theorem | pgpgrp 19612 | Reverse closure for the second argument of pGrp. (Contributed by Mario Carneiro, 15-Jan-2015.) |
| ⊢ (𝑃 pGrp 𝐺 → 𝐺 ∈ Grp) | ||
| Theorem | pgpfi1 19613 | 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 19614 | The identity subgroup is a 𝑃-group for every prime 𝑃. (Contributed by Mario Carneiro, 19-Jan-2015.) |
| ⊢ 0 = (0g‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑃 ∈ ℙ) → 𝑃 pGrp (𝐺 ↾s { 0 })) | ||
| Theorem | subgpgp 19615 | A subgroup of a p-group is a p-group. (Contributed by Mario Carneiro, 27-Apr-2016.) |
| ⊢ ((𝑃 pGrp 𝐺 ∧ 𝑆 ∈ (SubGrp‘𝐺)) → 𝑃 pGrp (𝐺 ↾s 𝑆)) | ||
| Theorem | sylow1lem1 19616* | Lemma for sylow1 19621. 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 19617* | Lemma for sylow1 19621. The function ⊕ is a group action on 𝑆. (Contributed by Mario Carneiro, 15-Jan-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝑃↑𝑁) ∥ (♯‘𝑋)) & ⊢ + = (+g‘𝐺) & ⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃↑𝑁)} & ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) ⇒ ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑆)) | ||
| Theorem | sylow1lem3 19618* | Lemma for sylow1 19621. 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 19619* | Lemma for sylow1 19621. 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 19620* | Lemma for sylow1 19621. 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 19621* | 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 19622* | 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 19623* | The converse to pgpfi1 19613. 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 19624 | Alternate version of pgpfi 19623. (Contributed by Mario Carneiro, 27-Apr-2016.) |
| ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ (♯‘𝑋) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))))) | ||
| Theorem | pgphash 19625 | The order of a p-group. (Contributed by Mario Carneiro, 27-Apr-2016.) |
| ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝑃 pGrp 𝐺 ∧ 𝑋 ∈ Fin) → (♯‘𝑋) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))) | ||
| Theorem | isslw 19626* | 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 19627 | 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 19628 | A Sylow 𝑃-subgroup is a subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) |
| ⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) → 𝐻 ∈ (SubGrp‘𝐺)) | ||
| Theorem | slwispgp 19629 | Defining property of a Sylow 𝑃-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) |
| ⊢ 𝑆 = (𝐺 ↾s 𝐾) ⇒ ⊢ ((𝐻 ∈ (𝑃 pSyl 𝐺) ∧ 𝐾 ∈ (SubGrp‘𝐺)) → ((𝐻 ⊆ 𝐾 ∧ 𝑃 pGrp 𝑆) ↔ 𝐻 = 𝐾)) | ||
| Theorem | slwpss 19630 | A proper superset of a Sylow subgroup is not a 𝑃-group. (Contributed by Mario Carneiro, 16-Jan-2015.) |
| ⊢ 𝑆 = (𝐺 ↾s 𝐾) ⇒ ⊢ ((𝐻 ∈ (𝑃 pSyl 𝐺) ∧ 𝐾 ∈ (SubGrp‘𝐺) ∧ 𝐻 ⊊ 𝐾) → ¬ 𝑃 pGrp 𝑆) | ||
| Theorem | slwpgp 19631 | A Sylow 𝑃-subgroup is a 𝑃-group. (Contributed by Mario Carneiro, 16-Jan-2015.) |
| ⊢ 𝑆 = (𝐺 ↾s 𝐻) ⇒ ⊢ (𝐻 ∈ (𝑃 pSyl 𝐺) → 𝑃 pGrp 𝑆) | ||
| Theorem | pgpssslw 19632* | 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 19633 | Every finite group contains a Sylow 𝑃-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) ⇒ ⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) → (𝑃 pSyl 𝐺) ≠ ∅) | ||
| Theorem | subgslw 19634 | 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 19635* | Lemma for sylow2a 19637. An equivalence class of fixed points is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌)) & ⊢ (𝜑 → 𝑃 pGrp 𝐺) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑌 ∈ Fin) & ⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢} & ⊢ ∼ = {〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} ⇒ ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑍) → [𝐴] ∼ = {𝐴}) | ||
| Theorem | sylow2alem2 19636* | Lemma for sylow2a 19637. 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 19637* | 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 19638* | Lemma for sylow2b 19641. Evaluate the group action on a left coset. (Contributed by Mario Carneiro, 17-Jan-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝐾 ∈ (SubGrp‘𝐺)) & ⊢ + = (+g‘𝐺) & ⊢ ∼ = (𝐺 ~QG 𝐾) & ⊢ · = (𝑥 ∈ 𝐻, 𝑦 ∈ (𝑋 / ∼ ) ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) ⇒ ⊢ ((𝜑 ∧ 𝐵 ∈ 𝐻 ∧ 𝐶 ∈ 𝑋) → (𝐵 · [𝐶] ∼ ) = [(𝐵 + 𝐶)] ∼ ) | ||
| Theorem | sylow2blem2 19639* | Lemma for sylow2b 19641. 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 19640* | Sylow's second theorem. Putting together the results of sylow2a 19637 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 19641* | 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 19642 | 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 19643 | 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 19644* | Sylow's second theorem. See also sylow2b 19641 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 19643). This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝐻 ∈ (𝑃 pSyl 𝐺)) & ⊢ (𝜑 → 𝐾 ∈ (𝑃 pSyl 𝐺)) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) ⇒ ⊢ (𝜑 → ∃𝑔 ∈ 𝑋 𝐻 = ran (𝑥 ∈ 𝐾 ↦ ((𝑔 + 𝑥) − 𝑔))) | ||
| Theorem | sylow3lem1 19645* | Lemma for sylow3 19651, first part. (Contributed by Mario Carneiro, 19-Jan-2015.) |
| ⊢ 𝑋 = (Base‘𝐺) & ⊢ (𝜑 → 𝐺 ∈ Grp) & ⊢ (𝜑 → 𝑋 ∈ Fin) & ⊢ (𝜑 → 𝑃 ∈ ℙ) & ⊢ + = (+g‘𝐺) & ⊢ − = (-g‘𝐺) & ⊢ ⊕ = (𝑥 ∈ 𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧 ∈ 𝑦 ↦ ((𝑥 + 𝑧) − 𝑥))) ⇒ ⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺))) | ||
| Theorem | sylow3lem2 19646* | Lemma for sylow3 19651, 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 19647* | Lemma for sylow3 19651, 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 19648* | Lemma for sylow3 19651, 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 19649* | Lemma for sylow3 19651, second part. Reduce the group action of sylow3lem1 19645 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 19650* | Lemma for sylow3 19651, second part. Using the lemma sylow2a 19637, 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 19651 | 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 19652 | Extend class notation with subgroup sum. |
| class LSSum | ||
| Syntax | cpj1 19653 | Extend class notation with left projection. |
| class proj1 | ||
| Definition | df-lsm 19654* | Define subgroup sum (inner direct product of subgroups). (Contributed by NM, 28-Jan-2014.) |
| ⊢ LSSum = (𝑤 ∈ V ↦ (𝑡 ∈ 𝒫 (Base‘𝑤), 𝑢 ∈ 𝒫 (Base‘𝑤) ↦ ran (𝑥 ∈ 𝑡, 𝑦 ∈ 𝑢 ↦ (𝑥(+g‘𝑤)𝑦)))) | ||
| Definition | df-pj1 19655* | 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 19656* | 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 19657* | Subspace sum value (for a group or vector space). Extended domain version of lsmval 19666. (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇 ⊕ 𝑈) = ran (𝑥 ∈ 𝑇, 𝑦 ∈ 𝑈 ↦ (𝑥 + 𝑦))) | ||
| Theorem | lsmelvalx 19658* | Subspace sum membership (for a group or vector space). Extended domain version of lsmelval 19667. (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ + = (+g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ 𝑉 ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑋 ∈ (𝑇 ⊕ 𝑈) ↔ ∃𝑦 ∈ 𝑇 ∃𝑧 ∈ 𝑈 𝑋 = (𝑦 + 𝑧))) | ||
| Theorem | lsmelvalix 19659 | 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 19660 | The subspace sum operation in the opposite group. (Contributed by Mario Carneiro, 19-Apr-2016.) (Proof shortened by AV, 2-Mar-2024.) |
| ⊢ 𝑂 = (oppg‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝑇(LSSum‘𝑂)𝑈) = (𝑈 ⊕ 𝑇) | ||
| Theorem | lsmssv 19661 | Subgroup sum is a subset of the base. (Contributed by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝐺 ∈ Mnd ∧ 𝑇 ⊆ 𝐵 ∧ 𝑈 ⊆ 𝐵) → (𝑇 ⊕ 𝑈) ⊆ 𝐵) | ||
| Theorem | lsmless1x 19662 | 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 19663 | 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 19664 | Subgroup sum is an upper bound of its arguments. (Contributed by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 𝐵 = (Base‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ⊆ 𝐵 ∧ 𝑈 ∈ (SubMnd‘𝐺)) → 𝑇 ⊆ (𝑇 ⊕ 𝑈)) | ||
| Theorem | lsmub2x 19665 | 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 19666* | 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 19667* | 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 19668 | 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 19669* | Subgroup sum membership analogue of lsmelval 19667 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 19670 | 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 19671 | The sum of two commuting submonoids is a submonoid. (Contributed by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubMnd‘𝐺) ∧ 𝑈 ∈ (SubMnd‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) ∈ (SubMnd‘𝐺)) | ||
| Theorem | lsmsubg 19672 | The sum of two commuting subgroups is a subgroup. (Contributed by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) ∈ (SubGrp‘𝐺)) | ||
| Theorem | lsmcom2 19673 | Subgroup sum commutes. (Contributed by Mario Carneiro, 22-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ (𝑍‘𝑈)) → (𝑇 ⊕ 𝑈) = (𝑈 ⊕ 𝑇)) | ||
| Theorem | smndlsmidm 19674 | The direct product is idempotent for submonoids. (Contributed by AV, 27-Dec-2023.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝑈 ∈ (SubMnd‘𝐺) → (𝑈 ⊕ 𝑈) = 𝑈) | ||
| Theorem | lsmub1 19675 | 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 19676 | 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 19677 | 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 19678 | Subset implies subgroup sum subset. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑆 ⊆ 𝑇) → (𝑆 ⊕ 𝑈) ⊆ (𝑇 ⊕ 𝑈)) | ||
| Theorem | lsmless2 19679 | Subset implies subgroup sum subset. (Contributed by NM, 25-Feb-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ 𝑈) → (𝑆 ⊕ 𝑇) ⊆ (𝑆 ⊕ 𝑈)) | ||
| Theorem | lsmless12 19680 | Subset implies subgroup sum subset. (Contributed by NM, 14-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ (𝑅 ⊆ 𝑆 ∧ 𝑇 ⊆ 𝑈)) → (𝑅 ⊕ 𝑇) ⊆ (𝑆 ⊕ 𝑈)) | ||
| Theorem | lsmidm 19681 | Subgroup sum is idempotent. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) (Proof shortened by AV, 27-Dec-2023.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝑈 ∈ (SubGrp‘𝐺) → (𝑈 ⊕ 𝑈) = 𝑈) | ||
| Theorem | lsmlub 19682 | The least upper bound property of subgroup sum. (Contributed by NM, 6-Feb-2014.) (Revised by Mario Carneiro, 21-Jun-2014.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → ((𝑆 ⊆ 𝑈 ∧ 𝑇 ⊆ 𝑈) ↔ (𝑆 ⊕ 𝑇) ⊆ 𝑈)) | ||
| Theorem | lsmss1 19683 | Subgroup sum with a subset. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ 𝑈) → (𝑇 ⊕ 𝑈) = 𝑈) | ||
| Theorem | lsmss1b 19684 | Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑇 ⊆ 𝑈 ↔ (𝑇 ⊕ 𝑈) = 𝑈)) | ||
| Theorem | lsmss2 19685 | Subgroup sum with a subset. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺) ∧ 𝑈 ⊆ 𝑇) → (𝑇 ⊕ 𝑈) = 𝑇) | ||
| Theorem | lsmss2b 19686 | Subgroup sum with a subset. (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → (𝑈 ⊆ 𝑇 ↔ (𝑇 ⊕ 𝑈) = 𝑇)) | ||
| Theorem | lsmass 19687 | Subgroup sum is associative. (Contributed by NM, 2-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ ((𝑅 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) → ((𝑅 ⊕ 𝑇) ⊕ 𝑈) = (𝑅 ⊕ (𝑇 ⊕ 𝑈))) | ||
| Theorem | mndlsmidm 19688 | Subgroup sum is idempotent for monoids. This corresponds to the observation in [Lang] p. 6. (Contributed by AV, 27-Dec-2023.) |
| ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐵 = (Base‘𝐺) ⇒ ⊢ (𝐺 ∈ Mnd → (𝐵 ⊕ 𝐵) = 𝐵) | ||
| Theorem | lsm01 19689 | Subgroup sum with the zero subgroup. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝑋 ∈ (SubGrp‘𝐺) → (𝑋 ⊕ { 0 }) = 𝑋) | ||
| Theorem | lsm02 19690 | Subgroup sum with the zero subgroup. (Contributed by NM, 27-Mar-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ 0 = (0g‘𝐺) & ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (𝑋 ∈ (SubGrp‘𝐺) → ({ 0 } ⊕ 𝑋) = 𝑋) | ||
| Theorem | subglsm 19691 | The subgroup sum evaluated within a subgroup. (Contributed by Mario Carneiro, 27-Apr-2016.) |
| ⊢ 𝐻 = (𝐺 ↾s 𝑆) & ⊢ ⊕ = (LSSum‘𝐺) & ⊢ 𝐴 = (LSSum‘𝐻) ⇒ ⊢ ((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ⊆ 𝑆 ∧ 𝑈 ⊆ 𝑆) → (𝑇 ⊕ 𝑈) = (𝑇𝐴𝑈)) | ||
| Theorem | lssnle 19692 | Equivalent expressions for "not less than". (chnlei 31504 analog.) (Contributed by NM, 10-Jan-2015.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) ⇒ ⊢ (𝜑 → (¬ 𝑈 ⊆ 𝑇 ↔ 𝑇 ⊊ (𝑇 ⊕ 𝑈))) | ||
| Theorem | lsmmod 19693 | The modular law holds for subgroup sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 2-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑆 ⊆ 𝑈) → (𝑆 ⊕ (𝑇 ∩ 𝑈)) = ((𝑆 ⊕ 𝑇) ∩ 𝑈)) | ||
| Theorem | lsmmod2 19694 | Modular law dual for subgroup sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 8-Jan-2015.) (Revised by Mario Carneiro, 21-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) ⇒ ⊢ (((𝑆 ∈ (SubGrp‘𝐺) ∧ 𝑇 ∈ (SubGrp‘𝐺) ∧ 𝑈 ∈ (SubGrp‘𝐺)) ∧ 𝑈 ⊆ 𝑆) → (𝑆 ∩ (𝑇 ⊕ 𝑈)) = ((𝑆 ∩ 𝑇) ⊕ 𝑈)) | ||
| Theorem | lsmpropd 19695* | If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 29-Jun-2015.) (Revised by AV, 25-Apr-2024.) |
| ⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥(+g‘𝐾)𝑦) = (𝑥(+g‘𝐿)𝑦)) & ⊢ (𝜑 → 𝐾 ∈ 𝑉) & ⊢ (𝜑 → 𝐿 ∈ 𝑊) ⇒ ⊢ (𝜑 → (LSSum‘𝐾) = (LSSum‘𝐿)) | ||
| Theorem | cntzrecd 19696 | Commute the "subgroups commute" predicate. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ 𝑍 = (Cntz‘𝐺) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ⊆ (𝑍‘𝑈)) ⇒ ⊢ (𝜑 → 𝑈 ⊆ (𝑍‘𝑇)) | ||
| Theorem | lsmcntz 19697 | The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ⊆ (𝑍‘𝑈) ↔ (𝑆 ⊆ (𝑍‘𝑈) ∧ 𝑇 ⊆ (𝑍‘𝑈)))) | ||
| Theorem | lsmcntzr 19698 | The "subgroups commute" predicate applied to a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 𝑍 = (Cntz‘𝐺) ⇒ ⊢ (𝜑 → (𝑆 ⊆ (𝑍‘(𝑇 ⊕ 𝑈)) ↔ (𝑆 ⊆ (𝑍‘𝑇) ∧ 𝑆 ⊆ (𝑍‘𝑈)))) | ||
| Theorem | lsmdisj 19699 | Disjointness from a subgroup sum. (Contributed by Mario Carneiro, 21-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 }) ⇒ ⊢ (𝜑 → ((𝑆 ∩ 𝑈) = { 0 } ∧ (𝑇 ∩ 𝑈) = { 0 })) | ||
| Theorem | lsmdisj2 19700 | Association of the disjointness constraint in a subgroup sum. (Contributed by Mario Carneiro, 22-Apr-2016.) |
| ⊢ ⊕ = (LSSum‘𝐺) & ⊢ (𝜑 → 𝑆 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑇 ∈ (SubGrp‘𝐺)) & ⊢ (𝜑 → 𝑈 ∈ (SubGrp‘𝐺)) & ⊢ 0 = (0g‘𝐺) & ⊢ (𝜑 → ((𝑆 ⊕ 𝑇) ∩ 𝑈) = { 0 }) & ⊢ (𝜑 → (𝑆 ∩ 𝑇) = { 0 }) ⇒ ⊢ (𝜑 → (𝑇 ∩ (𝑆 ⊕ 𝑈)) = { 0 }) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |