![]() |
Metamath
Proof Explorer Theorem List (p. 201 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dmdprdsplit2lem 20001 | Lemma for dmdprdsplit 20003. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐:๐ผโถ(SubGrpโ๐บ)) & โข (๐ โ (๐ถ โฉ ๐ท) = โ ) & โข (๐ โ ๐ผ = (๐ถ โช ๐ท)) & โข ๐ = (Cntzโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บdom DProd (๐ โพ ๐ถ)) & โข (๐ โ ๐บdom DProd (๐ โพ ๐ท)) & โข (๐ โ (๐บ DProd (๐ โพ ๐ถ)) โ (๐โ(๐บ DProd (๐ โพ ๐ท)))) & โข (๐ โ ((๐บ DProd (๐ โพ ๐ถ)) โฉ (๐บ DProd (๐ โพ ๐ท))) = { 0 }) & โข ๐พ = (mrClsโ(SubGrpโ๐บ)) โ โข ((๐ โง ๐ โ ๐ถ) โ ((๐ โ ๐ผ โ (๐ โ ๐ โ (๐โ๐) โ (๐โ(๐โ๐)))) โง ((๐โ๐) โฉ (๐พโโช (๐ โ (๐ผ โ {๐})))) โ { 0 })) | ||
Theorem | dmdprdsplit2 20002 | The direct product splits into the direct product of any partition of the index set. (Contributed by Mario Carneiro, 25-Apr-2016.) |
โข (๐ โ ๐:๐ผโถ(SubGrpโ๐บ)) & โข (๐ โ (๐ถ โฉ ๐ท) = โ ) & โข (๐ โ ๐ผ = (๐ถ โช ๐ท)) & โข ๐ = (Cntzโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บdom DProd (๐ โพ ๐ถ)) & โข (๐ โ ๐บdom DProd (๐ โพ ๐ท)) & โข (๐ โ (๐บ DProd (๐ โพ ๐ถ)) โ (๐โ(๐บ DProd (๐ โพ ๐ท)))) & โข (๐ โ ((๐บ DProd (๐ โพ ๐ถ)) โฉ (๐บ DProd (๐ โพ ๐ท))) = { 0 }) โ โข (๐ โ ๐บdom DProd ๐) | ||
Theorem | dmdprdsplit 20003 | The direct product splits into the direct product of any partition of the index set. (Contributed by Mario Carneiro, 25-Apr-2016.) |
โข (๐ โ ๐:๐ผโถ(SubGrpโ๐บ)) & โข (๐ โ (๐ถ โฉ ๐ท) = โ ) & โข (๐ โ ๐ผ = (๐ถ โช ๐ท)) & โข ๐ = (Cntzโ๐บ) & โข 0 = (0gโ๐บ) โ โข (๐ โ (๐บdom DProd ๐ โ ((๐บdom DProd (๐ โพ ๐ถ) โง ๐บdom DProd (๐ โพ ๐ท)) โง (๐บ DProd (๐ โพ ๐ถ)) โ (๐โ(๐บ DProd (๐ โพ ๐ท))) โง ((๐บ DProd (๐ โพ ๐ถ)) โฉ (๐บ DProd (๐ โพ ๐ท))) = { 0 }))) | ||
Theorem | dprdsplit 20004 | The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 25-Apr-2016.) |
โข (๐ โ ๐:๐ผโถ(SubGrpโ๐บ)) & โข (๐ โ (๐ถ โฉ ๐ท) = โ ) & โข (๐ โ ๐ผ = (๐ถ โช ๐ท)) & โข โ = (LSSumโ๐บ) & โข (๐ โ ๐บdom DProd ๐) โ โข (๐ โ (๐บ DProd ๐) = ((๐บ DProd (๐ โพ ๐ถ)) โ (๐บ DProd (๐ โพ ๐ท)))) | ||
Theorem | dmdprdpr 20005 | A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 25-Apr-2016.) |
โข ๐ = (Cntzโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) โ โข (๐ โ (๐บdom DProd {โจโ , ๐โฉ, โจ1o, ๐โฉ} โ (๐ โ (๐โ๐) โง (๐ โฉ ๐) = { 0 }))) | ||
Theorem | dprdpr 20006 | A singleton family is an internal direct product, the product of which is the given subgroup. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข ๐ = (Cntzโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข โ = (LSSumโ๐บ) & โข (๐ โ ๐ โ (๐โ๐)) & โข (๐ โ (๐ โฉ ๐) = { 0 }) โ โข (๐ โ (๐บ DProd {โจโ , ๐โฉ, โจ1o, ๐โฉ}) = (๐ โ ๐)) | ||
Theorem | dpjlem 20007 | Lemma for theorems about direct product projection. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข (๐ โ ๐ โ ๐ผ) โ โข (๐ โ (๐บ DProd (๐ โพ {๐})) = (๐โ๐)) | ||
Theorem | dpjcntz 20008 | The two subgroups that appear in dpjval 20012 commute. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข (๐ โ ๐ โ ๐ผ) & โข ๐ = (Cntzโ๐บ) โ โข (๐ โ (๐โ๐) โ (๐โ(๐บ DProd (๐ โพ (๐ผ โ {๐}))))) | ||
Theorem | dpjdisj 20009 | The two subgroups that appear in dpjval 20012 are disjoint. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข (๐ โ ๐ โ ๐ผ) & โข 0 = (0gโ๐บ) โ โข (๐ โ ((๐โ๐) โฉ (๐บ DProd (๐ โพ (๐ผ โ {๐})))) = { 0 }) | ||
Theorem | dpjlsm 20010 | The two subgroups that appear in dpjval 20012 add to the full direct product. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข (๐ โ ๐ โ ๐ผ) & โข โ = (LSSumโ๐บ) โ โข (๐ โ (๐บ DProd ๐) = ((๐โ๐) โ (๐บ DProd (๐ โพ (๐ผ โ {๐}))))) | ||
Theorem | dpjfval 20011* | Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข ๐ = (๐บdProj๐) & โข ๐ = (proj1โ๐บ) โ โข (๐ โ ๐ = (๐ โ ๐ผ โฆ ((๐โ๐)๐(๐บ DProd (๐ โพ (๐ผ โ {๐})))))) | ||
Theorem | dpjval 20012 | Value of the direct product projection (defined in terms of binary projection). (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข ๐ = (๐บdProj๐) & โข ๐ = (proj1โ๐บ) & โข (๐ โ ๐ โ ๐ผ) โ โข (๐ โ (๐โ๐) = ((๐โ๐)๐(๐บ DProd (๐ โพ (๐ผ โ {๐}))))) | ||
Theorem | dpjf 20013 | The ๐-th index projection is a function from the direct product to the ๐-th factor. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข ๐ = (๐บdProj๐) & โข (๐ โ ๐ โ ๐ผ) โ โข (๐ โ (๐โ๐):(๐บ DProd ๐)โถ(๐โ๐)) | ||
Theorem | dpjidcl 20014* | The key property of projections: the sum of all the projections of ๐ด is ๐ด. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข ๐ = (๐บdProj๐) & โข (๐ โ ๐ด โ (๐บ DProd ๐)) & โข 0 = (0gโ๐บ) & โข ๐ = {โ โ X๐ โ ๐ผ (๐โ๐) โฃ โ finSupp 0 } โ โข (๐ โ ((๐ฅ โ ๐ผ โฆ ((๐โ๐ฅ)โ๐ด)) โ ๐ โง ๐ด = (๐บ ฮฃg (๐ฅ โ ๐ผ โฆ ((๐โ๐ฅ)โ๐ด))))) | ||
Theorem | dpjeq 20015* | Decompose a group sum into projections. (Contributed by Mario Carneiro, 26-Apr-2016.) (Revised by AV, 14-Jul-2019.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข ๐ = (๐บdProj๐) & โข (๐ โ ๐ด โ (๐บ DProd ๐)) & โข 0 = (0gโ๐บ) & โข ๐ = {โ โ X๐ โ ๐ผ (๐โ๐) โฃ โ finSupp 0 } & โข (๐ โ (๐ฅ โ ๐ผ โฆ ๐ถ) โ ๐) โ โข (๐ โ (๐ด = (๐บ ฮฃg (๐ฅ โ ๐ผ โฆ ๐ถ)) โ โ๐ฅ โ ๐ผ ((๐โ๐ฅ)โ๐ด) = ๐ถ)) | ||
Theorem | dpjid 20016* | The key property of projections: the sum of all the projections of ๐ด is ๐ด. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข ๐ = (๐บdProj๐) & โข (๐ โ ๐ด โ (๐บ DProd ๐)) โ โข (๐ โ ๐ด = (๐บ ฮฃg (๐ฅ โ ๐ผ โฆ ((๐โ๐ฅ)โ๐ด)))) | ||
Theorem | dpjlid 20017 | The ๐-th index projection acts as the identity on elements of the ๐-th factor. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข ๐ = (๐บdProj๐) & โข (๐ โ ๐ โ ๐ผ) & โข (๐ โ ๐ด โ (๐โ๐)) โ โข (๐ โ ((๐โ๐)โ๐ด) = ๐ด) | ||
Theorem | dpjrid 20018 | The ๐-th index projection annihilates elements of other factors. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข ๐ = (๐บdProj๐) & โข (๐ โ ๐ โ ๐ผ) & โข (๐ โ ๐ด โ (๐โ๐)) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐ โ ๐ผ) & โข (๐ โ ๐ โ ๐) โ โข (๐ โ ((๐โ๐)โ๐ด) = 0 ) | ||
Theorem | dpjghm 20019 | The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข ๐ = (๐บdProj๐) & โข (๐ โ ๐ โ ๐ผ) โ โข (๐ โ (๐โ๐) โ ((๐บ โพs (๐บ DProd ๐)) GrpHom ๐บ)) | ||
Theorem | dpjghm2 20020 | The direct product is the binary subgroup product ("sum") of the direct products of the partition. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข ๐ = (๐บdProj๐) & โข (๐ โ ๐ โ ๐ผ) โ โข (๐ โ (๐โ๐) โ ((๐บ โพs (๐บ DProd ๐)) GrpHom (๐บ โพs (๐โ๐)))) | ||
Theorem | ablfacrplem 20021* | Lemma for ablfacrp2 20023. (Contributed by Mario Carneiro, 19-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐พ = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} & โข ๐ฟ = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐ gcd ๐) = 1) & โข (๐ โ (โฏโ๐ต) = (๐ ยท ๐)) โ โข (๐ โ ((โฏโ๐พ) gcd ๐) = 1) | ||
Theorem | ablfacrp 20022* | A finite abelian group whose order factors into relatively prime integers, itself "factors" into two subgroups ๐พ, ๐ฟ that have trivial intersection and whose product is the whole group. Lemma 6.1C.2 of [Shapiro], p. 199. (Contributed by Mario Carneiro, 19-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐พ = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} & โข ๐ฟ = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐ gcd ๐) = 1) & โข (๐ โ (โฏโ๐ต) = (๐ ยท ๐)) & โข 0 = (0gโ๐บ) & โข โ = (LSSumโ๐บ) โ โข (๐ โ ((๐พ โฉ ๐ฟ) = { 0 } โง (๐พ โ ๐ฟ) = ๐ต)) | ||
Theorem | ablfacrp2 20023* | The factors ๐พ, ๐ฟ of ablfacrp 20022 have the expected orders (which allows for repeated application to decompose ๐บ into subgroups of prime-power order). Lemma 6.1C.2 of [Shapiro], p. 199. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐พ = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} & โข ๐ฟ = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐ gcd ๐) = 1) & โข (๐ โ (โฏโ๐ต) = (๐ ยท ๐)) โ โข (๐ โ ((โฏโ๐พ) = ๐ โง (โฏโ๐ฟ) = ๐)) | ||
Theorem | ablfac1lem 20024* | Lemma for ablfac1b 20026. Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ด โ โ) & โข ๐ = (๐โ(๐ pCnt (โฏโ๐ต))) & โข ๐ = ((โฏโ๐ต) / ๐) โ โข ((๐ โง ๐ โ ๐ด) โ ((๐ โ โ โง ๐ โ โ) โง (๐ gcd ๐) = 1 โง (โฏโ๐ต) = (๐ ยท ๐))) | ||
Theorem | ablfac1a 20025* | The factors of ablfac1b 20026 are of prime power order. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ด โ โ) โ โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) = (๐โ(๐ pCnt (โฏโ๐ต)))) | ||
Theorem | ablfac1b 20026* | Any abelian group is the direct product of factors of prime power order (with the exact order further matching the prime factorization of the group order). (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐บdom DProd ๐) | ||
Theorem | ablfac1c 20027* | The factors of ablfac1b 20026 cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ด โ โ) & โข ๐ท = {๐ค โ โ โฃ ๐ค โฅ (โฏโ๐ต)} & โข (๐ โ ๐ท โ ๐ด) โ โข (๐ โ (๐บ DProd ๐) = ๐ต) | ||
Theorem | ablfac1eulem 20028* | Lemma for ablfac1eu 20029. (Contributed by Mario Carneiro, 27-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ด โ โ) & โข ๐ท = {๐ค โ โ โฃ ๐ค โฅ (โฏโ๐ต)} & โข (๐ โ ๐ท โ ๐ด) & โข (๐ โ (๐บdom DProd ๐ โง (๐บ DProd ๐) = ๐ต)) & โข (๐ โ dom ๐ = ๐ด) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ0) & โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) = (๐โ๐ถ)) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ด โ Fin) โ โข (๐ โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ด โ {๐}))))) | ||
Theorem | ablfac1eu 20029* | The factorization of ablfac1b 20026 is unique, in that any other factorization into prime power factors (even if the exponents are different) must be equal to ๐. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ด โ โ) & โข ๐ท = {๐ค โ โ โฃ ๐ค โฅ (โฏโ๐ต)} & โข (๐ โ ๐ท โ ๐ด) & โข (๐ โ (๐บdom DProd ๐ โง (๐บ DProd ๐) = ๐ต)) & โข (๐ โ dom ๐ = ๐ด) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ0) & โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) = (๐โ๐ถ)) โ โข (๐ โ ๐ = ๐) | ||
Theorem | pgpfac1lem1 20030* | Lemma for pgpfac1 20036. (Contributed by Mario Carneiro, 27-Apr-2016.) |
โข ๐พ = (mrClsโ(SubGrpโ๐บ)) & โข ๐ = (๐พโ{๐ด}) & โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ธ = (gExโ๐บ) & โข 0 = (0gโ๐บ) & โข โ = (LSSumโ๐บ) & โข (๐ โ ๐ pGrp ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ (๐โ๐ด) = ๐ธ) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ (๐ โฉ ๐) = { 0 }) & โข (๐ โ (๐ โ ๐) โ ๐) & โข (๐ โ โ๐ค โ (SubGrpโ๐บ)((๐ค โ ๐ โง ๐ด โ ๐ค) โ ยฌ (๐ โ ๐) โ ๐ค)) โ โข ((๐ โง ๐ถ โ (๐ โ (๐ โ ๐))) โ ((๐ โ ๐) โ (๐พโ{๐ถ})) = ๐) | ||
Theorem | pgpfac1lem2 20031* | Lemma for pgpfac1 20036. (Contributed by Mario Carneiro, 27-Apr-2016.) |
โข ๐พ = (mrClsโ(SubGrpโ๐บ)) & โข ๐ = (๐พโ{๐ด}) & โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ธ = (gExโ๐บ) & โข 0 = (0gโ๐บ) & โข โ = (LSSumโ๐บ) & โข (๐ โ ๐ pGrp ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ (๐โ๐ด) = ๐ธ) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ (๐ โฉ ๐) = { 0 }) & โข (๐ โ (๐ โ ๐) โ ๐) & โข (๐ โ โ๐ค โ (SubGrpโ๐บ)((๐ค โ ๐ โง ๐ด โ ๐ค) โ ยฌ (๐ โ ๐) โ ๐ค)) & โข (๐ โ ๐ถ โ (๐ โ (๐ โ ๐))) & โข ยท = (.gโ๐บ) โ โข (๐ โ (๐ ยท ๐ถ) โ (๐ โ ๐)) | ||
Theorem | pgpfac1lem3a 20032* | Lemma for pgpfac1 20036. (Contributed by Mario Carneiro, 4-Jun-2016.) |
โข ๐พ = (mrClsโ(SubGrpโ๐บ)) & โข ๐ = (๐พโ{๐ด}) & โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ธ = (gExโ๐บ) & โข 0 = (0gโ๐บ) & โข โ = (LSSumโ๐บ) & โข (๐ โ ๐ pGrp ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ (๐โ๐ด) = ๐ธ) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ (๐ โฉ ๐) = { 0 }) & โข (๐ โ (๐ โ ๐) โ ๐) & โข (๐ โ โ๐ค โ (SubGrpโ๐บ)((๐ค โ ๐ โง ๐ด โ ๐ค) โ ยฌ (๐ โ ๐) โ ๐ค)) & โข (๐ โ ๐ถ โ (๐ โ (๐ โ ๐))) & โข ยท = (.gโ๐บ) & โข (๐ โ ๐ โ โค) & โข (๐ โ ((๐ ยท ๐ถ)(+gโ๐บ)(๐ ยท ๐ด)) โ ๐) โ โข (๐ โ (๐ โฅ ๐ธ โง ๐ โฅ ๐)) | ||
Theorem | pgpfac1lem3 20033* | Lemma for pgpfac1 20036. (Contributed by Mario Carneiro, 27-Apr-2016.) |
โข ๐พ = (mrClsโ(SubGrpโ๐บ)) & โข ๐ = (๐พโ{๐ด}) & โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ธ = (gExโ๐บ) & โข 0 = (0gโ๐บ) & โข โ = (LSSumโ๐บ) & โข (๐ โ ๐ pGrp ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ (๐โ๐ด) = ๐ธ) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ (๐ โฉ ๐) = { 0 }) & โข (๐ โ (๐ โ ๐) โ ๐) & โข (๐ โ โ๐ค โ (SubGrpโ๐บ)((๐ค โ ๐ โง ๐ด โ ๐ค) โ ยฌ (๐ โ ๐) โ ๐ค)) & โข (๐ โ ๐ถ โ (๐ โ (๐ โ ๐))) & โข ยท = (.gโ๐บ) & โข (๐ โ ๐ โ โค) & โข (๐ โ ((๐ ยท ๐ถ)(+gโ๐บ)(๐ ยท ๐ด)) โ ๐) & โข ๐ท = (๐ถ(+gโ๐บ)((๐ / ๐) ยท ๐ด)) โ โข (๐ โ โ๐ก โ (SubGrpโ๐บ)((๐ โฉ ๐ก) = { 0 } โง (๐ โ ๐ก) = ๐)) | ||
Theorem | pgpfac1lem4 20034* | Lemma for pgpfac1 20036. (Contributed by Mario Carneiro, 27-Apr-2016.) |
โข ๐พ = (mrClsโ(SubGrpโ๐บ)) & โข ๐ = (๐พโ{๐ด}) & โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ธ = (gExโ๐บ) & โข 0 = (0gโ๐บ) & โข โ = (LSSumโ๐บ) & โข (๐ โ ๐ pGrp ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ (๐โ๐ด) = ๐ธ) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ (๐ โฉ ๐) = { 0 }) & โข (๐ โ (๐ โ ๐) โ ๐) & โข (๐ โ โ๐ค โ (SubGrpโ๐บ)((๐ค โ ๐ โง ๐ด โ ๐ค) โ ยฌ (๐ โ ๐) โ ๐ค)) & โข (๐ โ ๐ถ โ (๐ โ (๐ โ ๐))) & โข ยท = (.gโ๐บ) โ โข (๐ โ โ๐ก โ (SubGrpโ๐บ)((๐ โฉ ๐ก) = { 0 } โง (๐ โ ๐ก) = ๐)) | ||
Theorem | pgpfac1lem5 20035* | Lemma for pgpfac1 20036. (Contributed by Mario Carneiro, 27-Apr-2016.) |
โข ๐พ = (mrClsโ(SubGrpโ๐บ)) & โข ๐ = (๐พโ{๐ด}) & โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ธ = (gExโ๐บ) & โข 0 = (0gโ๐บ) & โข โ = (LSSumโ๐บ) & โข (๐ โ ๐ pGrp ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ (๐โ๐ด) = ๐ธ) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ โ๐ โ (SubGrpโ๐บ)((๐ โ ๐ โง ๐ด โ ๐ ) โ โ๐ก โ (SubGrpโ๐บ)((๐ โฉ ๐ก) = { 0 } โง (๐ โ ๐ก) = ๐ ))) โ โข (๐ โ โ๐ก โ (SubGrpโ๐บ)((๐ โฉ ๐ก) = { 0 } โง (๐ โ ๐ก) = ๐)) | ||
Theorem | pgpfac1 20036* | Factorization of a finite abelian p-group. There is a direct product decomposition of any abelian group of prime-power order where one of the factors is cyclic and generated by an element of maximal order. (Contributed by Mario Carneiro, 27-Apr-2016.) |
โข ๐พ = (mrClsโ(SubGrpโ๐บ)) & โข ๐ = (๐พโ{๐ด}) & โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ธ = (gExโ๐บ) & โข 0 = (0gโ๐บ) & โข โ = (LSSumโ๐บ) & โข (๐ โ ๐ pGrp ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ (๐โ๐ด) = ๐ธ) & โข (๐ โ ๐ด โ ๐ต) โ โข (๐ โ โ๐ก โ (SubGrpโ๐บ)((๐ โฉ ๐ก) = { 0 } โง (๐ โ ๐ก) = ๐ต)) | ||
Theorem | pgpfaclem1 20037* | Lemma for pgpfac 20040. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ถ = {๐ โ (SubGrpโ๐บ) โฃ (๐บ โพs ๐) โ (CycGrp โฉ ran pGrp )} & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ pGrp ๐บ) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ โ๐ก โ (SubGrpโ๐บ)(๐ก โ ๐ โ โ๐ โ Word ๐ถ(๐บdom DProd ๐ โง (๐บ DProd ๐ ) = ๐ก))) & โข ๐ป = (๐บ โพs ๐) & โข ๐พ = (mrClsโ(SubGrpโ๐ป)) & โข ๐ = (odโ๐ป) & โข ๐ธ = (gExโ๐ป) & โข 0 = (0gโ๐ป) & โข โ = (LSSumโ๐ป) & โข (๐ โ ๐ธ โ 1) & โข (๐ โ ๐ โ ๐) & โข (๐ โ (๐โ๐) = ๐ธ) & โข (๐ โ ๐ โ (SubGrpโ๐ป)) & โข (๐ โ ((๐พโ{๐}) โฉ ๐) = { 0 }) & โข (๐ โ ((๐พโ{๐}) โ ๐) = ๐) & โข (๐ โ ๐ โ Word ๐ถ) & โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ (๐บ DProd ๐) = ๐) & โข ๐ = (๐ ++ โจโ(๐พโ{๐})โโฉ) โ โข (๐ โ โ๐ โ Word ๐ถ(๐บdom DProd ๐ โง (๐บ DProd ๐ ) = ๐)) | ||
Theorem | pgpfaclem2 20038* | Lemma for pgpfac 20040. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ถ = {๐ โ (SubGrpโ๐บ) โฃ (๐บ โพs ๐) โ (CycGrp โฉ ran pGrp )} & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ pGrp ๐บ) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ โ๐ก โ (SubGrpโ๐บ)(๐ก โ ๐ โ โ๐ โ Word ๐ถ(๐บdom DProd ๐ โง (๐บ DProd ๐ ) = ๐ก))) & โข ๐ป = (๐บ โพs ๐) & โข ๐พ = (mrClsโ(SubGrpโ๐ป)) & โข ๐ = (odโ๐ป) & โข ๐ธ = (gExโ๐ป) & โข 0 = (0gโ๐ป) & โข โ = (LSSumโ๐ป) & โข (๐ โ ๐ธ โ 1) & โข (๐ โ ๐ โ ๐) & โข (๐ โ (๐โ๐) = ๐ธ) & โข (๐ โ ๐ โ (SubGrpโ๐ป)) & โข (๐ โ ((๐พโ{๐}) โฉ ๐) = { 0 }) & โข (๐ โ ((๐พโ{๐}) โ ๐) = ๐) โ โข (๐ โ โ๐ โ Word ๐ถ(๐บdom DProd ๐ โง (๐บ DProd ๐ ) = ๐)) | ||
Theorem | pgpfaclem3 20039* | Lemma for pgpfac 20040. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ถ = {๐ โ (SubGrpโ๐บ) โฃ (๐บ โพs ๐) โ (CycGrp โฉ ran pGrp )} & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ pGrp ๐บ) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ โ๐ก โ (SubGrpโ๐บ)(๐ก โ ๐ โ โ๐ โ Word ๐ถ(๐บdom DProd ๐ โง (๐บ DProd ๐ ) = ๐ก))) โ โข (๐ โ โ๐ โ Word ๐ถ(๐บdom DProd ๐ โง (๐บ DProd ๐ ) = ๐)) | ||
Theorem | pgpfac 20040* | Full factorization of a finite abelian p-group, by iterating pgpfac1 20036. There is a direct product decomposition of any abelian group of prime-power order into cyclic subgroups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ถ = {๐ โ (SubGrpโ๐บ) โฃ (๐บ โพs ๐) โ (CycGrp โฉ ran pGrp )} & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ pGrp ๐บ) & โข (๐ โ ๐ต โ Fin) โ โข (๐ โ โ๐ โ Word ๐ถ(๐บdom DProd ๐ โง (๐บ DProd ๐ ) = ๐ต)) | ||
Theorem | ablfaclem1 20041* | Lemma for ablfac 20044. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ถ = {๐ โ (SubGrpโ๐บ) โฃ (๐บ โพs ๐) โ (CycGrp โฉ ran pGrp )} & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข ๐ = (odโ๐บ) & โข ๐ด = {๐ค โ โ โฃ ๐ค โฅ (โฏโ๐ต)} & โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) & โข ๐ = (๐ โ (SubGrpโ๐บ) โฆ {๐ โ Word ๐ถ โฃ (๐บdom DProd ๐ โง (๐บ DProd ๐ ) = ๐)}) โ โข (๐ โ (SubGrpโ๐บ) โ (๐โ๐) = {๐ โ Word ๐ถ โฃ (๐บdom DProd ๐ โง (๐บ DProd ๐ ) = ๐)}) | ||
Theorem | ablfaclem2 20042* | Lemma for ablfac 20044. (Contributed by Mario Carneiro, 27-Apr-2016.) (Proof shortened by Mario Carneiro, 3-May-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ถ = {๐ โ (SubGrpโ๐บ) โฃ (๐บ โพs ๐) โ (CycGrp โฉ ran pGrp )} & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข ๐ = (odโ๐บ) & โข ๐ด = {๐ค โ โ โฃ ๐ค โฅ (โฏโ๐ต)} & โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) & โข ๐ = (๐ โ (SubGrpโ๐บ) โฆ {๐ โ Word ๐ถ โฃ (๐บdom DProd ๐ โง (๐บ DProd ๐ ) = ๐)}) & โข (๐ โ ๐น:๐ดโถWord ๐ถ) & โข (๐ โ โ๐ฆ โ ๐ด (๐นโ๐ฆ) โ (๐โ(๐โ๐ฆ))) & โข ๐ฟ = โช ๐ฆ โ ๐ด ({๐ฆ} ร dom (๐นโ๐ฆ)) & โข (๐ โ ๐ป:(0..^(โฏโ๐ฟ))โ1-1-ontoโ๐ฟ) โ โข (๐ โ (๐โ๐ต) โ โ ) | ||
Theorem | ablfaclem3 20043* | Lemma for ablfac 20044. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ถ = {๐ โ (SubGrpโ๐บ) โฃ (๐บ โพs ๐) โ (CycGrp โฉ ran pGrp )} & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข ๐ = (odโ๐บ) & โข ๐ด = {๐ค โ โ โฃ ๐ค โฅ (โฏโ๐ต)} & โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) & โข ๐ = (๐ โ (SubGrpโ๐บ) โฆ {๐ โ Word ๐ถ โฃ (๐บdom DProd ๐ โง (๐บ DProd ๐ ) = ๐)}) โ โข (๐ โ (๐โ๐ต) โ โ ) | ||
Theorem | ablfac 20044* | The Fundamental Theorem of (finite) Abelian Groups. Any finite abelian group is a direct product of cyclic p-groups. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ถ = {๐ โ (SubGrpโ๐บ) โฃ (๐บ โพs ๐) โ (CycGrp โฉ ran pGrp )} & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) โ โข (๐ โ โ๐ โ Word ๐ถ(๐บdom DProd ๐ โง (๐บ DProd ๐ ) = ๐ต)) | ||
Theorem | ablfac2 20045* | Choose generators for each cyclic group in ablfac 20044. (Contributed by Mario Carneiro, 28-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ถ = {๐ โ (SubGrpโ๐บ) โฃ (๐บ โพs ๐) โ (CycGrp โฉ ran pGrp )} & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข ยท = (.gโ๐บ) & โข ๐ = (๐ โ dom ๐ค โฆ ran (๐ โ โค โฆ (๐ ยท (๐คโ๐)))) โ โข (๐ โ โ๐ค โ Word ๐ต(๐:dom ๐คโถ๐ถ โง ๐บdom DProd ๐ โง (๐บ DProd ๐) = ๐ต)) | ||
Syntax | csimpg 20046 | Extend class notation with the class of simple groups. |
class SimpGrp | ||
Definition | df-simpg 20047 | Define class of all simple groups. A simple group is a group (df-grp 18892) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 20059). (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข SimpGrp = {๐ โ Grp โฃ (NrmSGrpโ๐) โ 2o} | ||
Theorem | issimpg 20048 | The predicate "is a simple group". (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข (๐บ โ SimpGrp โ (๐บ โ Grp โง (NrmSGrpโ๐บ) โ 2o)) | ||
Theorem | issimpgd 20049 | Deduce a simple group from its properties. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข (๐ โ ๐บ โ Grp) & โข (๐ โ (NrmSGrpโ๐บ) โ 2o) โ โข (๐ โ ๐บ โ SimpGrp) | ||
Theorem | simpggrp 20050 | A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข (๐บ โ SimpGrp โ ๐บ โ Grp) | ||
Theorem | simpggrpd 20051 | A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข (๐ โ ๐บ โ SimpGrp) โ โข (๐ โ ๐บ โ Grp) | ||
Theorem | simpg2nsg 20052 | A simple group has two normal subgroups. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข (๐บ โ SimpGrp โ (NrmSGrpโ๐บ) โ 2o) | ||
Theorem | trivnsimpgd 20053 | Trivial groups are not simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ต = { 0 }) โ โข (๐ โ ยฌ ๐บ โ SimpGrp) | ||
Theorem | simpgntrivd 20054 | Simple groups are nontrivial. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ SimpGrp) โ โข (๐ โ ยฌ ๐ต = { 0 }) | ||
Theorem | simpgnideld 20055* | A simple group contains a nonidentity element. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ SimpGrp) โ โข (๐ โ โ๐ฅ โ ๐ต ยฌ ๐ฅ = 0 ) | ||
Theorem | simpgnsgd 20056 | The only normal subgroups of a simple group are the group itself and the trivial group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ SimpGrp) โ โข (๐ โ (NrmSGrpโ๐บ) = {{ 0 }, ๐ต}) | ||
Theorem | simpgnsgeqd 20057 | A normal subgroup of a simple group is either the whole group or the trivial subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ SimpGrp) & โข (๐ โ ๐ด โ (NrmSGrpโ๐บ)) โ โข (๐ โ (๐ด = { 0 } โจ ๐ด = ๐ต)) | ||
Theorem | 2nsgsimpgd 20058* | If any normal subgroup of a nontrivial group is either the trivial subgroup or the whole group, the group is simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ยฌ { 0 } = ๐ต) & โข ((๐ โง ๐ฅ โ (NrmSGrpโ๐บ)) โ (๐ฅ = { 0 } โจ ๐ฅ = ๐ต)) โ โข (๐ โ ๐บ โ SimpGrp) | ||
Theorem | simpgnsgbid 20059 | A nontrivial group is simple if and only if its normal subgroups are exactly the group itself and the trivial subgroup. (Contributed by Rohan Ridenour, 4-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ยฌ { 0 } = ๐ต) โ โข (๐ โ (๐บ โ SimpGrp โ (NrmSGrpโ๐บ) = {{ 0 }, ๐ต})) | ||
Theorem | ablsimpnosubgd 20060 | A subgroup of an abelian simple group containing a nonidentity element is the whole group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐บ โ SimpGrp) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ยฌ ๐ด = 0 ) โ โข (๐ โ ๐ = ๐ต) | ||
Theorem | ablsimpg1gend 20061* | An abelian simple group is generated by any non-identity element. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข ยท = (.gโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐บ โ SimpGrp) & โข (๐ โ ๐ด โ ๐ต) & โข (๐ โ ยฌ ๐ด = 0 ) & โข (๐ โ ๐ถ โ ๐ต) โ โข (๐ โ โ๐ โ โค ๐ถ = (๐ ยท ๐ด)) | ||
Theorem | ablsimpgcygd 20062 | An abelian simple group is cyclic. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof shortened by Rohan Ridenour, 31-Oct-2023.) |
โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐บ โ SimpGrp) โ โข (๐ โ ๐บ โ CycGrp) | ||
Theorem | ablsimpgfindlem1 20063* | Lemma for ablsimpgfind 20066. An element of an abelian finite simple group which doesn't square to the identity has finite order. (Contributed by Rohan Ridenour, 3-Aug-2023.) (Proof shortened by Rohan Ridenour, 31-Oct-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ = (odโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐บ โ SimpGrp) โ โข (((๐ โง ๐ฅ โ ๐ต) โง (2 ยท ๐ฅ) โ 0 ) โ (๐โ๐ฅ) โ 0) | ||
Theorem | ablsimpgfindlem2 20064* | Lemma for ablsimpgfind 20066. An element of an abelian finite simple group which squares to the identity has finite order. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ = (odโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐บ โ SimpGrp) โ โข (((๐ โง ๐ฅ โ ๐ต) โง (2 ยท ๐ฅ) = 0 ) โ (๐โ๐ฅ) โ 0) | ||
Theorem | cycsubggenodd 20065* | Relationship between the order of a subgroup and the order of a generator of the subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ = (odโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ด โ ๐ต) & โข (๐ โ ๐ถ = ran (๐ โ โค โฆ (๐ ยท ๐ด))) โ โข (๐ โ (๐โ๐ด) = if(๐ถ โ Fin, (โฏโ๐ถ), 0)) | ||
Theorem | ablsimpgfind 20066 | An abelian simple group is finite. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐บ โ SimpGrp) โ โข (๐ โ ๐ต โ Fin) | ||
Theorem | fincygsubgd 20067* | The subgroup referenced in fincygsubgodd 20068 is a subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ป = (๐ โ โค โฆ (๐ ยท (๐ถ ยท ๐ด))) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ด โ ๐ต) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ ran ๐ป โ (SubGrpโ๐บ)) | ||
Theorem | fincygsubgodd 20068* | Calculate the order of a subgroup of a finite cyclic group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ท = ((โฏโ๐ต) / ๐ถ) & โข ๐น = (๐ โ โค โฆ (๐ ยท ๐ด)) & โข ๐ป = (๐ โ โค โฆ (๐ ยท (๐ถ ยท ๐ด))) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ด โ ๐ต) & โข (๐ โ ran ๐น = ๐ต) & โข (๐ โ ๐ถ โฅ (โฏโ๐ต)) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ (โฏโran ๐ป) = ๐ท) | ||
Theorem | fincygsubgodexd 20069* | A finite cyclic group has subgroups of every possible order. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข (๐ โ ๐บ โ CycGrp) & โข (๐ โ ๐ถ โฅ (โฏโ๐ต)) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ โ๐ฅ โ (SubGrpโ๐บ)(โฏโ๐ฅ) = ๐ถ) | ||
Theorem | prmgrpsimpgd 20070 | A group of prime order is simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ (โฏโ๐ต) โ โ) โ โข (๐ โ ๐บ โ SimpGrp) | ||
Theorem | ablsimpgprmd 20071 | An abelian simple group has prime order. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐บ โ SimpGrp) โ โข (๐ โ (โฏโ๐ต) โ โ) | ||
Theorem | ablsimpgd 20072 | An abelian group is simple if and only if its order is prime. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข (๐ โ ๐บ โ Abel) โ โข (๐ โ (๐บ โ SimpGrp โ (โฏโ๐ต) โ โ)) | ||
Syntax | cmgp 20073 | Multiplicative group. |
class mulGrp | ||
Definition | df-mgp 20074 | Define a structure that puts the multiplication operation of a ring in the addition slot. Note that this will not actually be a group for the average ring, or even for a field, but it will be a monoid, and unitgrp 20321 shows that we get a group if we restrict to the elements that have inverses. This allows to formalize such notions as "the multiplication operation of a ring is a monoid" (ringmgp 20178) or "the multiplicative identity" in terms of the identity of a monoid (df-ur 20121). (Contributed by Mario Carneiro, 21-Dec-2014.) |
โข mulGrp = (๐ค โ V โฆ (๐ค sSet โจ(+gโndx), (.rโ๐ค)โฉ)) | ||
Theorem | fnmgp 20075 | The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.) |
โข mulGrp Fn V | ||
Theorem | mgpval 20076 | Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014.) |
โข ๐ = (mulGrpโ๐ ) & โข ยท = (.rโ๐ ) โ โข ๐ = (๐ sSet โจ(+gโndx), ยท โฉ) | ||
Theorem | mgpplusg 20077 | Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) |
โข ๐ = (mulGrpโ๐ ) & โข ยท = (.rโ๐ ) โ โข ยท = (+gโ๐) | ||
Theorem | mgplemOLD 20078 | Obsolete version of setsplusg 19300 as of 18-Oct-2024. Lemma for mgpbas 20079. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ๐ = (mulGrpโ๐ ) & โข ๐ธ = Slot ๐ & โข ๐ โ โ & โข ๐ โ 2 โ โข (๐ธโ๐ ) = (๐ธโ๐) | ||
Theorem | mgpbas 20079 | Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.) |
โข ๐ = (mulGrpโ๐ ) & โข ๐ต = (Baseโ๐ ) โ โข ๐ต = (Baseโ๐) | ||
Theorem | mgpbasOLD 20080 | Obsolete version of mgpbas 20079 as of 18-Oct-2024. Base set of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) (Revised by Mario Carneiro, 5-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ๐ = (mulGrpโ๐ ) & โข ๐ต = (Baseโ๐ ) โ โข ๐ต = (Baseโ๐) | ||
Theorem | mgpsca 20081 | The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 20262. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
โข ๐ = (mulGrpโ๐ ) & โข ๐ = (Scalarโ๐ ) โ โข ๐ = (Scalarโ๐) | ||
Theorem | mgpscaOLD 20082 | Obsolete version of mgpsca 20081 as of 18-Oct-2024. The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 20262. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ๐ = (mulGrpโ๐ ) & โข ๐ = (Scalarโ๐ ) โ โข ๐ = (Scalarโ๐) | ||
Theorem | mgptset 20083 | Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
โข ๐ = (mulGrpโ๐ ) โ โข (TopSetโ๐ ) = (TopSetโ๐) | ||
Theorem | mgptsetOLD 20084 | Obsolete version of mgptset 20083 as of 18-Oct-2024. Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ๐ = (mulGrpโ๐ ) โ โข (TopSetโ๐ ) = (TopSetโ๐) | ||
Theorem | mgptopn 20085 | Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
โข ๐ = (mulGrpโ๐ ) & โข ๐ฝ = (TopOpenโ๐ ) โ โข ๐ฝ = (TopOpenโ๐) | ||
Theorem | mgpds 20086 | Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
โข ๐ = (mulGrpโ๐ ) & โข ๐ต = (distโ๐ ) โ โข ๐ต = (distโ๐) | ||
Theorem | mgpdsOLD 20087 | Obsolete version of mgpds 20086 as of 18-Oct-2024. Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ๐ = (mulGrpโ๐ ) & โข ๐ต = (distโ๐ ) โ โข ๐ต = (distโ๐) | ||
Theorem | mgpress 20088 | Subgroup commutes with the multiplicative group operator. (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof shortened by AV, 18-Oct-2024.) |
โข ๐ = (๐ โพs ๐ด) & โข ๐ = (mulGrpโ๐ ) โ โข ((๐ โ ๐ โง ๐ด โ ๐) โ (๐ โพs ๐ด) = (mulGrpโ๐)) | ||
Theorem | mgpressOLD 20089 | Obsolete version of mgpress 20088 as of 18-Oct-2024. Subgroup commutes with the multiplication group operator. (Contributed by Mario Carneiro, 10-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ๐ = (๐ โพs ๐ด) & โข ๐ = (mulGrpโ๐ ) โ โข ((๐ โ ๐ โง ๐ด โ ๐) โ (๐ โพs ๐ด) = (mulGrpโ๐)) | ||
Theorem | prdsmgp 20090 | The multiplicative monoid of a product is the product of the multiplicative monoids of the factors. (Contributed by Mario Carneiro, 11-Mar-2015.) |
โข ๐ = (๐Xs๐ ) & โข ๐ = (mulGrpโ๐) & โข ๐ = (๐Xs(mulGrp โ ๐ )) & โข (๐ โ ๐ผ โ ๐) & โข (๐ โ ๐ โ ๐) & โข (๐ โ ๐ Fn ๐ผ) โ โข (๐ โ ((Baseโ๐) = (Baseโ๐) โง (+gโ๐) = (+gโ๐))) | ||
According to Wikipedia, "... in abstract algebra, a rng (or non-unital ring or pseudo-ring) is an algebraic structure satisfying the same properties as a [unital] ring, without assuming the existence of a multiplicative identity. The term "rng" (pronounced rung) is meant to suggest that it is a "ring" without "i", i.e. without the requirement for an "identity element"." (see https://en.wikipedia.org/wiki/Rng_(algebra), 28-Mar-2025). | ||
Syntax | crng 20091 | Extend class notation with class of all non-unital rings. |
class Rng | ||
Definition | df-rng 20092* | Define the class of all non-unital rings. A non-unital ring (or rng, or pseudoring) is a set equipped with two everywhere-defined internal operations, whose first one is an additive abelian group operation and the second one is a multiplicative semigroup operation, and where the addition is left- and right-distributive for the multiplication. Definition of a pseudo-ring in section I.8.1 of [BourbakiAlg1] p. 93 or the definition of a ring in part Preliminaries of [Roman] p. 18. As almost always in mathematics, "non-unital" means "not necessarily unital". Therefore, by talking about a ring (in general) or a non-unital ring the "unital" case is always included. In contrast to a unital ring, the commutativity of addition must be postulated and cannot be proven from the other conditions. (Contributed by AV, 6-Jan-2020.) |
โข Rng = {๐ โ Abel โฃ ((mulGrpโ๐) โ Smgrp โง [(Baseโ๐) / ๐][(+gโ๐) / ๐][(.rโ๐) / ๐ก]โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐ ((๐ฅ๐ก(๐ฆ๐๐ง)) = ((๐ฅ๐ก๐ฆ)๐(๐ฅ๐ก๐ง)) โง ((๐ฅ๐๐ฆ)๐ก๐ง) = ((๐ฅ๐ก๐ง)๐(๐ฆ๐ก๐ง))))} | ||
Theorem | isrng 20093* | The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020.) |
โข ๐ต = (Baseโ๐ ) & โข ๐บ = (mulGrpโ๐ ) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) โ โข (๐ โ Rng โ (๐ โ Abel โง ๐บ โ Smgrp โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) | ||
Theorem | rngabl 20094 | A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.) |
โข (๐ โ Rng โ ๐ โ Abel) | ||
Theorem | rngmgp 20095 | A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020.) |
โข ๐บ = (mulGrpโ๐ ) โ โข (๐ โ Rng โ ๐บ โ Smgrp) | ||
Theorem | rngmgpf 20096 | Restricted functionality of the multiplicative group on non-unital rings (mgpf 20187 analog). (Contributed by AV, 22-Feb-2025.) |
โข (mulGrp โพ Rng):RngโถSmgrp | ||
Theorem | rnggrp 20097 | A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.) |
โข (๐ โ Rng โ ๐ โ Grp) | ||
Theorem | rngass 20098 | Associative law for the multiplication operation of a non-unital ring. (Contributed by NM, 27-Aug-2011.) (Revised by AV, 13-Feb-2025.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) โ โข ((๐ โ Rng โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) | ||
Theorem | rngdi 20099 | Distributive law for the multiplication operation of a non-unital ring (left-distributivity). (Contributed by AV, 14-Feb-2025.) |
โข ๐ต = (Baseโ๐ ) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) โ โข ((๐ โ Rng โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) | ||
Theorem | rngdir 20100 | Distributive law for the multiplication operation of a non-unital ring (right-distributivity). (Contributed by AV, 17-Apr-2020.) |
โข ๐ต = (Baseโ๐ ) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) โ โข ((๐ โ Rng โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |