![]() |
Metamath
Proof Explorer Theorem List (p. 196 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | odmulg2 19501 | The order of a multiple divides the order of the base point. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ π = (odβπΊ) & β’ Β· = (.gβπΊ) β β’ ((πΊ β Grp β§ π΄ β π β§ π β β€) β (πβ(π Β· π΄)) β₯ (πβπ΄)) | ||
Theorem | odmulg 19502 | Relationship between the order of an element and that of a multiple. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ π = (odβπΊ) & β’ Β· = (.gβπΊ) β β’ ((πΊ β Grp β§ π΄ β π β§ π β β€) β (πβπ΄) = ((π gcd (πβπ΄)) Β· (πβ(π Β· π΄)))) | ||
Theorem | odmulgeq 19503 | A multiple of a point of finite order only has the same order if the multiplier is relatively prime. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ π = (odβπΊ) & β’ Β· = (.gβπΊ) β β’ (((πΊ β Grp β§ π΄ β π β§ π β β€) β§ (πβπ΄) β β) β ((πβ(π Β· π΄)) = (πβπ΄) β (π gcd (πβπ΄)) = 1)) | ||
Theorem | odbezout 19504* | If π is coprime to the order of π΄, there is a modular inverse π₯ to cancel multiplication by π. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ π = (odβπΊ) & β’ Β· = (.gβπΊ) β β’ (((πΊ β Grp β§ π΄ β π β§ π β β€) β§ (π gcd (πβπ΄)) = 1) β βπ₯ β β€ (π₯ Β· (π Β· π΄)) = π΄) | ||
Theorem | od1 19505 | The order of the group identity is one. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.) |
β’ π = (odβπΊ) & β’ 0 = (0gβπΊ) β β’ (πΊ β Grp β (πβ 0 ) = 1) | ||
Theorem | odeq1 19506 | The group identity is the unique element of a group with order one. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.) |
β’ π = (odβπΊ) & β’ 0 = (0gβπΊ) & β’ π = (BaseβπΊ) β β’ ((πΊ β Grp β§ π΄ β π) β ((πβπ΄) = 1 β π΄ = 0 )) | ||
Theorem | odinv 19507 | The order of the inverse of a group element. (Contributed by Mario Carneiro, 20-Oct-2015.) |
β’ π = (odβπΊ) & β’ πΌ = (invgβπΊ) & β’ π = (BaseβπΊ) β β’ ((πΊ β Grp β§ π΄ β π) β (πβ(πΌβπ΄)) = (πβπ΄)) | ||
Theorem | odf1 19508* | 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 19509* | 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 19510* | 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 19511 | The order of an element of a finite group is finite. (Contributed by Mario Carneiro, 14-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ π = (odβπΊ) β β’ ((πΊ β Grp β§ π β Fin β§ π΄ β π) β (πβπ΄) β β) | ||
Theorem | oddvds2 19512 | 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 | finodsubmsubg 19513* | A submonoid whose elements have finite order is a subgroup. (Contributed by SN, 31-Jan-2025.) |
β’ π = (odβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β (SubMndβπΊ)) & β’ (π β βπ β π (πβπ) β β) β β’ (π β π β (SubGrpβπΊ)) | ||
Theorem | 0subgALT 19514 | A shorter proof of 0subg 19097 using df-od 19474. (Contributed by SN, 31-Jan-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ 0 = (0gβπΊ) β β’ (πΊ β Grp β { 0 } β (SubGrpβπΊ)) | ||
Theorem | submod 19515 | The order of an element is the same in a submonoid. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by AV, 5-Oct-2020.) |
β’ π» = (πΊ βΎs π) & β’ π = (odβπΊ) & β’ π = (odβπ») β β’ ((π β (SubMndβπΊ) β§ π΄ β π) β (πβπ΄) = (πβπ΄)) | ||
Theorem | subgod 19516 | 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 19517 | 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 19518* | 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 19519* | 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 19520 | 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 19521 | 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 19522 | 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 19523* | A cyclic subgroup of size (πβπ΄) has (Οβ(πβπ΄)) generators. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ π = (odβπΊ) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ ((πΊ β Grp β§ π΄ β π β§ (πβπ΄) β β) β (β―β{π₯ β (πΎβ{π΄}) β£ (πβπ₯) = (πβπ΄)}) = (Οβ(πβπ΄))) | ||
Theorem | gexval 19524* | 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 19525* | 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 19526 | The exponent of a group is a nonnegative integer. (Contributed by Mario Carneiro, 23-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ πΈ = (gExβπΊ) β β’ (πΊ β π β πΈ β β0) | ||
Theorem | gexid 19527 | Any element to the power of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ πΈ = (gExβπΊ) & β’ Β· = (.gβπΊ) & β’ 0 = (0gβπΊ) β β’ (π΄ β π β (πΈ Β· π΄) = 0 ) | ||
Theorem | gexlem2 19528* | 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 19529 | 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 19530* | 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 19531* | 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 19532 | 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 19533* | 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 19534 | Every group element has finite order if the exponent is finite. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ πΈ = (gExβπΊ) & β’ π = (odβπΊ) β β’ ((πΊ β Grp β§ πΈ β β β§ π΄ β π) β (πβπ΄) β β) | ||
Theorem | gexcl2 19535 | The exponent of a finite group is finite. (Contributed by Mario Carneiro, 24-Apr-2016.) |
β’ π = (BaseβπΊ) & β’ πΈ = (gExβπΊ) β β’ ((πΊ β Grp β§ π β Fin) β πΈ β β) | ||
Theorem | gexdvds3 19536 | 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 19537 | 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 19538* | 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 19539 | Reverse closure for the first argument of pGrp. (Contributed by Mario Carneiro, 15-Jan-2015.) |
β’ (π pGrp πΊ β π β β) | ||
Theorem | pgpgrp 19540 | Reverse closure for the second argument of pGrp. (Contributed by Mario Carneiro, 15-Jan-2015.) |
β’ (π pGrp πΊ β πΊ β Grp) | ||
Theorem | pgpfi1 19541 | 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 19542 | The identity subgroup is a π-group for every prime π. (Contributed by Mario Carneiro, 19-Jan-2015.) |
β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ π β β) β π pGrp (πΊ βΎs { 0 })) | ||
Theorem | subgpgp 19543 | A subgroup of a p-group is a p-group. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ ((π pGrp πΊ β§ π β (SubGrpβπΊ)) β π pGrp (πΊ βΎs π)) | ||
Theorem | sylow1lem1 19544* | Lemma for sylow1 19549. 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 19545* | Lemma for sylow1 19549. The function β is a group action on π. (Contributed by Mario Carneiro, 15-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β Fin) & β’ (π β π β β) & β’ (π β π β β0) & β’ (π β (πβπ) β₯ (β―βπ)) & β’ + = (+gβπΊ) & β’ π = {π β π« π β£ (β―βπ ) = (πβπ)} & β’ β = (π₯ β π, π¦ β π β¦ ran (π§ β π¦ β¦ (π₯ + π§))) β β’ (π β β β (πΊ GrpAct π)) | ||
Theorem | sylow1lem3 19546* | Lemma for sylow1 19549. 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 19547* | Lemma for sylow1 19549. 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 19548* | Lemma for sylow1 19549. 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 19549* | 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 19550* | 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 19551* | The converse to pgpfi1 19541. 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 19552 | Alternate version of pgpfi 19551. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π = (BaseβπΊ) β β’ ((πΊ β Grp β§ π β Fin) β (π pGrp πΊ β (π β β β§ (β―βπ) = (πβ(π pCnt (β―βπ)))))) | ||
Theorem | pgphash 19553 | The order of a p-group. (Contributed by Mario Carneiro, 27-Apr-2016.) |
β’ π = (BaseβπΊ) β β’ ((π pGrp πΊ β§ π β Fin) β (β―βπ) = (πβ(π pCnt (β―βπ)))) | ||
Theorem | isslw 19554* | 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 19555 | 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 19556 | A Sylow π-subgroup is a subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) |
β’ (π» β (π pSyl πΊ) β π» β (SubGrpβπΊ)) | ||
Theorem | slwispgp 19557 | Defining property of a Sylow π-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) |
β’ π = (πΊ βΎs πΎ) β β’ ((π» β (π pSyl πΊ) β§ πΎ β (SubGrpβπΊ)) β ((π» β πΎ β§ π pGrp π) β π» = πΎ)) | ||
Theorem | slwpss 19558 | A proper superset of a Sylow subgroup is not a π-group. (Contributed by Mario Carneiro, 16-Jan-2015.) |
β’ π = (πΊ βΎs πΎ) β β’ ((π» β (π pSyl πΊ) β§ πΎ β (SubGrpβπΊ) β§ π» β πΎ) β Β¬ π pGrp π) | ||
Theorem | slwpgp 19559 | A Sylow π-subgroup is a π-group. (Contributed by Mario Carneiro, 16-Jan-2015.) |
β’ π = (πΊ βΎs π») β β’ (π» β (π pSyl πΊ) β π pGrp π) | ||
Theorem | pgpssslw 19560* | 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 19561 | Every finite group contains a Sylow π-subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) |
β’ π = (BaseβπΊ) β β’ ((πΊ β Grp β§ π β Fin β§ π β β) β (π pSyl πΊ) β β ) | ||
Theorem | subgslw 19562 | 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 19563* | Lemma for sylow2a 19565. An equivalence class of fixed points is a singleton. (Contributed by Mario Carneiro, 17-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ (π β β β (πΊ GrpAct π)) & β’ (π β π pGrp πΊ) & β’ (π β π β Fin) & β’ (π β π β Fin) & β’ π = {π’ β π β£ ββ β π (β β π’) = π’} & β’ βΌ = {β¨π₯, π¦β© β£ ({π₯, π¦} β π β§ βπ β π (π β π₯) = π¦)} β β’ ((π β§ π΄ β π) β [π΄] βΌ = {π΄}) | ||
Theorem | sylow2alem2 19564* | Lemma for sylow2a 19565. 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 19565* | 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 19566* | Lemma for sylow2b 19569. Evaluate the group action on a left coset. (Contributed by Mario Carneiro, 17-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ (π β π β Fin) & β’ (π β π» β (SubGrpβπΊ)) & β’ (π β πΎ β (SubGrpβπΊ)) & β’ + = (+gβπΊ) & β’ βΌ = (πΊ ~QG πΎ) & β’ Β· = (π₯ β π», π¦ β (π / βΌ ) β¦ ran (π§ β π¦ β¦ (π₯ + π§))) β β’ ((π β§ π΅ β π» β§ πΆ β π) β (π΅ Β· [πΆ] βΌ ) = [(π΅ + πΆ)] βΌ ) | ||
Theorem | sylow2blem2 19567* | Lemma for sylow2b 19569. 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 19568* | Sylow's second theorem. Putting together the results of sylow2a 19565 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 19569* | 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 19570 | 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 19571 | 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 19572* | Sylow's second theorem. See also sylow2b 19569 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 19571). This is part of Metamath 100 proof #72. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ (π β π β Fin) & β’ (π β π» β (π pSyl πΊ)) & β’ (π β πΎ β (π pSyl πΊ)) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) β β’ (π β βπ β π π» = ran (π₯ β πΎ β¦ ((π + π₯) β π))) | ||
Theorem | sylow3lem1 19573* | Lemma for sylow3 19579, first part. (Contributed by Mario Carneiro, 19-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π β Fin) & β’ (π β π β β) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ β = (π₯ β π, π¦ β (π pSyl πΊ) β¦ ran (π§ β π¦ β¦ ((π₯ + π§) β π₯))) β β’ (π β β β (πΊ GrpAct (π pSyl πΊ))) | ||
Theorem | sylow3lem2 19574* | Lemma for sylow3 19579, 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 19575* | Lemma for sylow3 19579, 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 19576* | Lemma for sylow3 19579, 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 19577* | Lemma for sylow3 19579, second part. Reduce the group action of sylow3lem1 19573 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 19578* | Lemma for sylow3 19579, second part. Using the lemma sylow2a 19565, 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 19579 | 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 19580 | Extend class notation with subgroup sum. |
class LSSum | ||
Syntax | cpj1 19581 | Extend class notation with left projection. |
class proj1 | ||
Definition | df-lsm 19582* | Define subgroup sum (inner direct product of subgroups). (Contributed by NM, 28-Jan-2014.) |
β’ LSSum = (π€ β V β¦ (π‘ β π« (Baseβπ€), π’ β π« (Baseβπ€) β¦ ran (π₯ β π‘, π¦ β π’ β¦ (π₯(+gβπ€)π¦)))) | ||
Definition | df-pj1 19583* | 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 19584* | 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 19585* | Subspace sum value (for a group or vector space). Extended domain version of lsmval 19594. (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (LSSumβπΊ) β β’ ((πΊ β π β§ π β π΅ β§ π β π΅) β (π β π) = ran (π₯ β π, π¦ β π β¦ (π₯ + π¦))) | ||
Theorem | lsmelvalx 19586* | Subspace sum membership (for a group or vector space). Extended domain version of lsmelval 19595. (Contributed by NM, 28-Jan-2014.) (Revised by Mario Carneiro, 19-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (LSSumβπΊ) β β’ ((πΊ β π β§ π β π΅ β§ π β π΅) β (π β (π β π) β βπ¦ β π βπ§ β π π = (π¦ + π§))) | ||
Theorem | lsmelvalix 19587 | 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 19588 | 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 19589 | Subgroup sum is a subset of the base. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ β = (LSSumβπΊ) β β’ ((πΊ β Mnd β§ π β π΅ β§ π β π΅) β (π β π) β π΅) | ||
Theorem | lsmless1x 19590 | 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 19591 | 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 19592 | Subgroup sum is an upper bound of its arguments. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ π΅ = (BaseβπΊ) & β’ β = (LSSumβπΊ) β β’ ((π β π΅ β§ π β (SubMndβπΊ)) β π β (π β π)) | ||
Theorem | lsmub2x 19593 | 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 19594* | 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 19595* | 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 19596 | 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 19597* | Subgroup sum membership analogue of lsmelval 19595 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 19598 | 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 19599 | The sum of two commuting submonoids is a submonoid. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ β = (LSSumβπΊ) & β’ π = (CntzβπΊ) β β’ ((π β (SubMndβπΊ) β§ π β (SubMndβπΊ) β§ π β (πβπ)) β (π β π) β (SubMndβπΊ)) | ||
Theorem | lsmsubg 19600 | The sum of two commuting subgroups is a subgroup. (Contributed by Mario Carneiro, 19-Apr-2016.) |
β’ β = (LSSumβπΊ) & β’ π = (CntzβπΊ) β β’ ((π β (SubGrpβπΊ) β§ π β (SubGrpβπΊ) β§ π β (πβπ)) β (π β π) β (SubGrpβπΊ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |