![]() |
Metamath
Proof Explorer Theorem List (p. 201 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 | dpjdisj 20001 | The two subgroups that appear in dpjval 20004 are disjoint. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข (๐ โ ๐ โ ๐ผ) & โข 0 = (0gโ๐บ) โ โข (๐ โ ((๐โ๐) โฉ (๐บ DProd (๐ โพ (๐ผ โ {๐})))) = { 0 }) | ||
Theorem | dpjlsm 20002 | The two subgroups that appear in dpjval 20004 add to the full direct product. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข (๐ โ ๐บdom DProd ๐) & โข (๐ โ dom ๐ = ๐ผ) & โข (๐ โ ๐ โ ๐ผ) & โข โ = (LSSumโ๐บ) โ โข (๐ โ (๐บ DProd ๐) = ((๐โ๐) โ (๐บ DProd (๐ โพ (๐ผ โ {๐}))))) | ||
Theorem | dpjfval 20003* | 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 20004 | 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 20005 | 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 20006* | 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 20007* | 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 20008* | 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 20009 | 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 20010 | 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 20011 | 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 20012 | 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 20013* | Lemma for ablfacrp2 20015. (Contributed by Mario Carneiro, 19-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐พ = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} & โข ๐ฟ = {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ ๐} & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ โ โ) & โข (๐ โ (๐ gcd ๐) = 1) & โข (๐ โ (โฏโ๐ต) = (๐ ยท ๐)) โ โข (๐ โ ((โฏโ๐พ) gcd ๐) = 1) | ||
Theorem | ablfacrp 20014* | 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 20015* | The factors ๐พ, ๐ฟ of ablfacrp 20014 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 20016* | Lemma for ablfac1b 20018. Satisfy the assumptions of ablfacrp. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ด โ โ) & โข ๐ = (๐โ(๐ pCnt (โฏโ๐ต))) & โข ๐ = ((โฏโ๐ต) / ๐) โ โข ((๐ โง ๐ โ ๐ด) โ ((๐ โ โ โง ๐ โ โ) โง (๐ gcd ๐) = 1 โง (โฏโ๐ต) = (๐ ยท ๐))) | ||
Theorem | ablfac1a 20017* | The factors of ablfac1b 20018 are of prime power order. (Contributed by Mario Carneiro, 26-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ด โ โ) โ โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) = (๐โ(๐ pCnt (โฏโ๐ต)))) | ||
Theorem | ablfac1b 20018* | 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 20019* | The factors of ablfac1b 20018 cover the entire group. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ด โ โ) & โข ๐ท = {๐ค โ โ โฃ ๐ค โฅ (โฏโ๐ต)} & โข (๐ โ ๐ท โ ๐ด) โ โข (๐ โ (๐บ DProd ๐) = ๐ต) | ||
Theorem | ablfac1eulem 20020* | Lemma for ablfac1eu 20021. (Contributed by Mario Carneiro, 27-Apr-2016.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ = (๐ โ ๐ด โฆ {๐ฅ โ ๐ต โฃ (๐โ๐ฅ) โฅ (๐โ(๐ pCnt (โฏโ๐ต)))}) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ด โ โ) & โข ๐ท = {๐ค โ โ โฃ ๐ค โฅ (โฏโ๐ต)} & โข (๐ โ ๐ท โ ๐ด) & โข (๐ โ (๐บdom DProd ๐ โง (๐บ DProd ๐) = ๐ต)) & โข (๐ โ dom ๐ = ๐ด) & โข ((๐ โง ๐ โ ๐ด) โ ๐ถ โ โ0) & โข ((๐ โง ๐ โ ๐ด) โ (โฏโ(๐โ๐)) = (๐โ๐ถ)) & โข (๐ โ ๐ โ โ) & โข (๐ โ ๐ด โ Fin) โ โข (๐ โ ยฌ ๐ โฅ (โฏโ(๐บ DProd (๐ โพ (๐ด โ {๐}))))) | ||
Theorem | ablfac1eu 20021* | The factorization of ablfac1b 20018 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 20022* | Lemma for pgpfac1 20028. (Contributed by Mario Carneiro, 27-Apr-2016.) |
โข ๐พ = (mrClsโ(SubGrpโ๐บ)) & โข ๐ = (๐พโ{๐ด}) & โข ๐ต = (Baseโ๐บ) & โข ๐ = (odโ๐บ) & โข ๐ธ = (gExโ๐บ) & โข 0 = (0gโ๐บ) & โข โ = (LSSumโ๐บ) & โข (๐ โ ๐ pGrp ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ (๐โ๐ด) = ๐ธ) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ ๐ด โ ๐) & โข (๐ โ ๐ โ (SubGrpโ๐บ)) & โข (๐ โ (๐ โฉ ๐) = { 0 }) & โข (๐ โ (๐ โ ๐) โ ๐) & โข (๐ โ โ๐ค โ (SubGrpโ๐บ)((๐ค โ ๐ โง ๐ด โ ๐ค) โ ยฌ (๐ โ ๐) โ ๐ค)) โ โข ((๐ โง ๐ถ โ (๐ โ (๐ โ ๐))) โ ((๐ โ ๐) โ (๐พโ{๐ถ})) = ๐) | ||
Theorem | pgpfac1lem2 20023* | Lemma for pgpfac1 20028. (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 20024* | Lemma for pgpfac1 20028. (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 20025* | Lemma for pgpfac1 20028. (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 20026* | Lemma for pgpfac1 20028. (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 20027* | Lemma for pgpfac1 20028. (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 20028* | 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 20029* | Lemma for pgpfac 20032. (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 20030* | Lemma for pgpfac 20032. (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 20031* | Lemma for pgpfac 20032. (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 20032* | Full factorization of a finite abelian p-group, by iterating pgpfac1 20028. 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 20033* | Lemma for ablfac 20036. (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 20034* | Lemma for ablfac 20036. (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 20035* | Lemma for ablfac 20036. (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 20036* | 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 20037* | Choose generators for each cyclic group in ablfac 20036. (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 20038 | Extend class notation with the class of simple groups. |
class SimpGrp | ||
Definition | df-simpg 20039 | Define class of all simple groups. A simple group is a group (df-grp 18884) with exactly two normal subgroups. These are always the subgroup of all elements and the subgroup containing only the identity (simpgnsgbid 20051). (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข SimpGrp = {๐ โ Grp โฃ (NrmSGrpโ๐) โ 2o} | ||
Theorem | issimpg 20040 | The predicate "is a simple group". (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข (๐บ โ SimpGrp โ (๐บ โ Grp โง (NrmSGrpโ๐บ) โ 2o)) | ||
Theorem | issimpgd 20041 | Deduce a simple group from its properties. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข (๐ โ ๐บ โ Grp) & โข (๐ โ (NrmSGrpโ๐บ) โ 2o) โ โข (๐ โ ๐บ โ SimpGrp) | ||
Theorem | simpggrp 20042 | A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข (๐บ โ SimpGrp โ ๐บ โ Grp) | ||
Theorem | simpggrpd 20043 | A simple group is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข (๐ โ ๐บ โ SimpGrp) โ โข (๐ โ ๐บ โ Grp) | ||
Theorem | simpg2nsg 20044 | A simple group has two normal subgroups. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข (๐บ โ SimpGrp โ (NrmSGrpโ๐บ) โ 2o) | ||
Theorem | trivnsimpgd 20045 | Trivial groups are not simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ต = { 0 }) โ โข (๐ โ ยฌ ๐บ โ SimpGrp) | ||
Theorem | simpgntrivd 20046 | Simple groups are nontrivial. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ SimpGrp) โ โข (๐ โ ยฌ ๐ต = { 0 }) | ||
Theorem | simpgnideld 20047* | A simple group contains a nonidentity element. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ SimpGrp) โ โข (๐ โ โ๐ฅ โ ๐ต ยฌ ๐ฅ = 0 ) | ||
Theorem | simpgnsgd 20048 | 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 20049 | 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 20050* | 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 20051 | 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 20052 | 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 20053* | 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 20054 | 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 20055* | Lemma for ablsimpgfind 20058. 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 20056* | Lemma for ablsimpgfind 20058. 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 20057* | 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 20058 | An abelian simple group is finite. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐บ โ SimpGrp) โ โข (๐ โ ๐ต โ Fin) | ||
Theorem | fincygsubgd 20059* | The subgroup referenced in fincygsubgodd 20060 is a subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ป = (๐ โ โค โฆ (๐ ยท (๐ถ ยท ๐ด))) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ด โ ๐ต) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ ran ๐ป โ (SubGrpโ๐บ)) | ||
Theorem | fincygsubgodd 20060* | 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 20061* | A finite cyclic group has subgroups of every possible order. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข (๐ โ ๐บ โ CycGrp) & โข (๐ โ ๐ถ โฅ (โฏโ๐ต)) & โข (๐ โ ๐ต โ Fin) & โข (๐ โ ๐ถ โ โ) โ โข (๐ โ โ๐ฅ โ (SubGrpโ๐บ)(โฏโ๐ฅ) = ๐ถ) | ||
Theorem | prmgrpsimpgd 20062 | A group of prime order is simple. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ (โฏโ๐ต) โ โ) โ โข (๐ โ ๐บ โ SimpGrp) | ||
Theorem | ablsimpgprmd 20063 | An abelian simple group has prime order. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข (๐ โ ๐บ โ Abel) & โข (๐ โ ๐บ โ SimpGrp) โ โข (๐ โ (โฏโ๐ต) โ โ) | ||
Theorem | ablsimpgd 20064 | 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 20065 | Multiplicative group. |
class mulGrp | ||
Definition | df-mgp 20066 | 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 20311 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 20170) or "the multiplicative identity" in terms of the identity of a monoid (df-ur 20113). (Contributed by Mario Carneiro, 21-Dec-2014.) |
โข mulGrp = (๐ค โ V โฆ (๐ค sSet โจ(+gโndx), (.rโ๐ค)โฉ)) | ||
Theorem | fnmgp 20067 | The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015.) |
โข mulGrp Fn V | ||
Theorem | mgpval 20068 | Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014.) |
โข ๐ = (mulGrpโ๐ ) & โข ยท = (.rโ๐ ) โ โข ๐ = (๐ sSet โจ(+gโndx), ยท โฉ) | ||
Theorem | mgpplusg 20069 | Value of the group operation of the multiplication group. (Contributed by Mario Carneiro, 21-Dec-2014.) |
โข ๐ = (mulGrpโ๐ ) & โข ยท = (.rโ๐ ) โ โข ยท = (+gโ๐) | ||
Theorem | mgplemOLD 20070 | Obsolete version of setsplusg 19292 as of 18-Oct-2024. Lemma for mgpbas 20071. (Contributed by Mario Carneiro, 5-Oct-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข ๐ = (mulGrpโ๐ ) & โข ๐ธ = Slot ๐ & โข ๐ โ โ & โข ๐ โ 2 โ โข (๐ธโ๐ ) = (๐ธโ๐) | ||
Theorem | mgpbas 20071 | 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 20072 | Obsolete version of mgpbas 20071 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 20073 | The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 20252. (Contributed by Mario Carneiro, 12-Mar-2015.) (Revised by Mario Carneiro, 5-May-2015.) |
โข ๐ = (mulGrpโ๐ ) & โข ๐ = (Scalarโ๐ ) โ โข ๐ = (Scalarโ๐) | ||
Theorem | mgpscaOLD 20074 | Obsolete version of mgpsca 20073 as of 18-Oct-2024. The multiplication monoid has the same (if any) scalars as the original ring. Mostly to simplify pwsmgp 20252. (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 20075 | Topology component of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
โข ๐ = (mulGrpโ๐ ) โ โข (TopSetโ๐ ) = (TopSetโ๐) | ||
Theorem | mgptsetOLD 20076 | Obsolete version of mgptset 20075 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 20077 | Topology of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
โข ๐ = (mulGrpโ๐ ) & โข ๐ฝ = (TopOpenโ๐ ) โ โข ๐ฝ = (TopOpenโ๐) | ||
Theorem | mgpds 20078 | Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015.) |
โข ๐ = (mulGrpโ๐ ) & โข ๐ต = (distโ๐ ) โ โข ๐ต = (distโ๐) | ||
Theorem | mgpdsOLD 20079 | Obsolete version of mgpds 20078 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 20080 | 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 20081 | Obsolete version of mgpress 20080 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 20082 | 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 20083 | Extend class notation with class of all non-unital rings. |
class Rng | ||
Definition | df-rng 20084* | 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 20085* | The predicate "is a non-unital ring." (Contributed by AV, 6-Jan-2020.) |
โข ๐ต = (Baseโ๐ ) & โข ๐บ = (mulGrpโ๐ ) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) โ โข (๐ โ Rng โ (๐ โ Abel โง ๐บ โ Smgrp โง โ๐ฅ โ ๐ต โ๐ฆ โ ๐ต โ๐ง โ ๐ต ((๐ฅ ยท (๐ฆ + ๐ง)) = ((๐ฅ ยท ๐ฆ) + (๐ฅ ยท ๐ง)) โง ((๐ฅ + ๐ฆ) ยท ๐ง) = ((๐ฅ ยท ๐ง) + (๐ฆ ยท ๐ง))))) | ||
Theorem | rngabl 20086 | A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.) |
โข (๐ โ Rng โ ๐ โ Abel) | ||
Theorem | rngmgp 20087 | A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020.) |
โข ๐บ = (mulGrpโ๐ ) โ โข (๐ โ Rng โ ๐บ โ Smgrp) | ||
Theorem | rngmgpf 20088 | Restricted functionality of the multiplicative group on non-unital rings (mgpf 20179 analog). (Contributed by AV, 22-Feb-2025.) |
โข (mulGrp โพ Rng):RngโถSmgrp | ||
Theorem | rnggrp 20089 | A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.) |
โข (๐ โ Rng โ ๐ โ Grp) | ||
Theorem | rngass 20090 | 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 20091 | 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 20092 | Distributive law for the multiplication operation of a non-unital ring (right-distributivity). (Contributed by AV, 17-Apr-2020.) |
โข ๐ต = (Baseโ๐ ) & โข + = (+gโ๐ ) & โข ยท = (.rโ๐ ) โ โข ((๐ โ Rng โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) | ||
Theorem | rngacl 20093 | Closure of the addition operation of a non-unital ring. (Contributed by AV, 16-Feb-2025.) |
โข ๐ต = (Baseโ๐ ) & โข + = (+gโ๐ ) โ โข ((๐ โ Rng โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ + ๐) โ ๐ต) | ||
Theorem | rng0cl 20094 | The zero element of a non-unital ring belongs to its base set. (Contributed by AV, 16-Feb-2025.) |
โข ๐ต = (Baseโ๐ ) & โข 0 = (0gโ๐ ) โ โข (๐ โ Rng โ 0 โ ๐ต) | ||
Theorem | rngcl 20095 | Closure of the multiplication operation of a non-unital ring. (Contributed by AV, 17-Apr-2020.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) โ โข ((๐ โ Rng โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) | ||
Theorem | rnglz 20096 | The zero of a non-unital ring is a left-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringlz 20218. (Revised by AV, 17-Apr-2020.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข 0 = (0gโ๐ ) โ โข ((๐ โ Rng โง ๐ โ ๐ต) โ ( 0 ยท ๐) = 0 ) | ||
Theorem | rngrz 20097 | The zero of a non-unital ring is a right-absorbing element. (Contributed by FL, 31-Aug-2009.) Generalization of ringrz 20219. (Revised by AV, 16-Feb-2025.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข 0 = (0gโ๐ ) โ โข ((๐ โ Rng โง ๐ โ ๐ต) โ (๐ ยท 0 ) = 0 ) | ||
Theorem | rngmneg1 20098 | Negation of a product in a non-unital ring (mulneg1 11672 analog). In contrast to ringmneg1 20229, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข ๐ = (invgโ๐ ) & โข (๐ โ ๐ โ Rng) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐โ๐) ยท ๐) = (๐โ(๐ ยท ๐))) | ||
Theorem | rngmneg2 20099 | Negation of a product in a non-unital ring (mulneg2 11673 analog). In contrast to ringmneg2 20230, the proof does not (and cannot) make use of the existence of a ring unity. (Contributed by AV, 17-Feb-2025.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข ๐ = (invgโ๐ ) & โข (๐ โ ๐ โ Rng) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐ ยท (๐โ๐)) = (๐โ(๐ ยท ๐))) | ||
Theorem | rngm2neg 20100 | Double negation of a product in a non-unital ring (mul2neg 11675 analog). (Contributed by Mario Carneiro, 4-Dec-2014.) Generalization of ringm2neg 20231. (Revised by AV, 17-Feb-2025.) |
โข ๐ต = (Baseโ๐ ) & โข ยท = (.rโ๐ ) & โข ๐ = (invgโ๐ ) & โข (๐ โ ๐ โ Rng) & โข (๐ โ ๐ โ ๐ต) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ ((๐โ๐) ยท (๐โ๐)) = (๐ ยท ๐)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |