![]() |
Metamath
Proof Explorer Theorem List (p. 191 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mulgnn0p1 19001 | Group multiple (exponentiation) operation at a successor, extended to โ0. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Mnd โง ๐ โ โ0 โง ๐ โ ๐ต) โ ((๐ + 1) ยท ๐) = ((๐ ยท ๐) + ๐)) | ||
Theorem | mulgnnsubcl 19002* | Closure of the group multiple (exponentiation) operation in a submagma. (Contributed by Mario Carneiro, 10-Jan-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) & โข (๐ โ ๐บ โ ๐) & โข (๐ โ ๐ โ ๐ต) & โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ฅ + ๐ฆ) โ ๐) โ โข ((๐ โง ๐ โ โ โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐) | ||
Theorem | mulgnn0subcl 19003* | Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 10-Jan-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) & โข (๐ โ ๐บ โ ๐) & โข (๐ โ ๐ โ ๐ต) & โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ฅ + ๐ฆ) โ ๐) & โข 0 = (0gโ๐บ) & โข (๐ โ 0 โ ๐) โ โข ((๐ โง ๐ โ โ0 โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐) | ||
Theorem | mulgsubcl 19004* | Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 10-Jan-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) & โข (๐ โ ๐บ โ ๐) & โข (๐ โ ๐ โ ๐ต) & โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ฅ + ๐ฆ) โ ๐) & โข 0 = (0gโ๐บ) & โข (๐ โ 0 โ ๐) & โข ๐ผ = (invgโ๐บ) & โข ((๐ โง ๐ฅ โ ๐) โ (๐ผโ๐ฅ) โ ๐) โ โข ((๐ โง ๐ โ โค โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐) | ||
Theorem | mulgnncl 19005 | Closure of the group multiple (exponentiation) operation for a positive multiplier in a magma. (Contributed by Mario Carneiro, 11-Dec-2014.) (Revised by AV, 29-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Mgm โง ๐ โ โ โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) | ||
Theorem | mulgnn0cl 19006 | Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Mnd โง ๐ โ โ0 โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) | ||
Theorem | mulgcl 19007 | Closure of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) | ||
Theorem | mulgneg 19008 | Group multiple (exponentiation) operation at a negative integer. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ผ = (invgโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (-๐ ยท ๐) = (๐ผโ(๐ ยท ๐))) | ||
Theorem | mulgnegneg 19009 | The inverse of a negative group multiple is the positive group multiple. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ผ = (invgโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ผโ(-๐ ยท ๐)) = (๐ ยท ๐)) | ||
Theorem | mulgm1 19010 | Group multiple (exponentiation) operation at negative one. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by Mario Carneiro, 20-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ผ = (invgโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ต) โ (-1 ยท ๐) = (๐ผโ๐)) | ||
Theorem | mulgnn0cld 19011 | Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 19006. (Contributed by SN, 1-Feb-2025.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข (๐ โ ๐บ โ Mnd) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐ ยท ๐) โ ๐ต) | ||
Theorem | mulgcld 19012 | Deduction associated with mulgcl 19007. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐ ยท ๐) โ ๐ต) | ||
Theorem | mulgaddcomlem 19013 | Lemma for mulgaddcom 19014. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ((-๐ฆ ยท ๐) + ๐) = (๐ + (-๐ฆ ยท ๐))) | ||
Theorem | mulgaddcom 19014 | The group multiple operator commutes with the group operation. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ ((๐ ยท ๐) + ๐) = (๐ + (๐ ยท ๐))) | ||
Theorem | mulginvcom 19015 | The group multiple operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ผ = (invgโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท (๐ผโ๐)) = (๐ผโ(๐ ยท ๐))) | ||
Theorem | mulginvinv 19016 | The group multiple operator commutes with the group inverse function. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ผ = (invgโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ผโ(๐ ยท (๐ผโ๐))) = (๐ ยท ๐)) | ||
Theorem | mulgnn0z 19017 | A group multiple of the identity, for nonnegative multiple. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข 0 = (0gโ๐บ) โ โข ((๐บ โ Mnd โง ๐ โ โ0) โ (๐ ยท 0 ) = 0 ) | ||
Theorem | mulgz 19018 | A group multiple of the identity, for integer multiple. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข 0 = (0gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ โค) โ (๐ ยท 0 ) = 0 ) | ||
Theorem | mulgnndir 19019 | Sum of group multiples, for positive multiples. (Contributed by Mario Carneiro, 11-Dec-2014.) (Revised by AV, 29-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Smgrp โง (๐ โ โ โง ๐ โ โ โง ๐ โ ๐ต)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) | ||
Theorem | mulgnn0dir 19020 | Sum of group multiples, generalized to โ0. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Mnd โง (๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) | ||
Theorem | mulgdirlem 19021 | Lemma for mulgdir 19022. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) | ||
Theorem | mulgdir 19022 | Sum of group multiples, generalized to โค. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) | ||
Theorem | mulgp1 19023 | Group multiple (exponentiation) operation at a successor, extended to โค. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ ((๐ + 1) ยท ๐) = ((๐ ยท ๐) + ๐)) | ||
Theorem | mulgneg2 19024 | Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ผ = (invgโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (-๐ ยท ๐) = (๐ ยท (๐ผโ๐))) | ||
Theorem | mulgnnass 19025 | Product of group multiples, for positive multiples in a semigroup. (Contributed by Mario Carneiro, 13-Dec-2014.) (Revised by AV, 29-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Smgrp โง (๐ โ โ โง ๐ โ โ โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) | ||
Theorem | mulgnn0ass 19026 | Product of group multiples, generalized to โ0. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Mnd โง (๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) | ||
Theorem | mulgass 19027 | Product of group multiples, generalized to โค. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) | ||
Theorem | mulgassr 19028 | Reversed product of group multiples. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) | ||
Theorem | mulgmodid 19029 | Casting out multiples of the identity element leaves the group multiple unchanged. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โ) โง (๐ โ ๐ต โง (๐ ยท ๐) = 0 )) โ ((๐ mod ๐) ยท ๐) = (๐ ยท ๐)) | ||
Theorem | mulgsubdir 19030 | Distribution of group multiples over subtraction for group elements, subdir 11652 analog. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ โ ๐) ยท ๐) = ((๐ ยท ๐) โ (๐ ยท ๐))) | ||
Theorem | mhmmulg 19031 | A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ร = (.gโ๐ป) โ โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ โ0 โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) | ||
Theorem | mulgpropd 19032* | Two structures with the same group-nature have the same group multiple function. ๐พ is expected to either be V (when strong equality is available) or ๐ต (when closure is available). (Contributed by Stefan O'Rear, 21-Mar-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
โข ยท = (.gโ๐บ) & โข ร = (.gโ๐ป) & โข (๐ โ ๐ต = (Baseโ๐บ)) & โข (๐ โ ๐ต = (Baseโ๐ป)) & โข (๐ โ ๐ต โ ๐พ) & โข ((๐ โง (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ)) โ (๐ฅ(+gโ๐บ)๐ฆ) โ ๐พ) & โข ((๐ โง (๐ฅ โ ๐พ โง ๐ฆ โ ๐พ)) โ (๐ฅ(+gโ๐บ)๐ฆ) = (๐ฅ(+gโ๐ป)๐ฆ)) โ โข (๐ โ ยท = ร ) | ||
Theorem | submmulgcl 19033 | Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 13-Jan-2015.) |
โข โ = (.gโ๐บ) โ โข ((๐ โ (SubMndโ๐บ) โง ๐ โ โ0 โง ๐ โ ๐) โ (๐ โ ๐) โ ๐) | ||
Theorem | submmulg 19034 | A group multiple is the same if evaluated in a submonoid. (Contributed by Mario Carneiro, 15-Jun-2015.) |
โข โ = (.gโ๐บ) & โข ๐ป = (๐บ โพs ๐) & โข ยท = (.gโ๐ป) โ โข ((๐ โ (SubMndโ๐บ) โง ๐ โ โ0 โง ๐ โ ๐) โ (๐ โ ๐) = (๐ ยท ๐)) | ||
Theorem | pwsmulg 19035 | Value of a group multiple in a structure power. (Contributed by Mario Carneiro, 15-Jun-2015.) |
โข ๐ = (๐ โs ๐ผ) & โข ๐ต = (Baseโ๐) & โข โ = (.gโ๐) & โข ยท = (.gโ๐ ) โ โข (((๐ โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ ((๐ โ ๐)โ๐ด) = (๐ ยท (๐โ๐ด))) | ||
Syntax | csubg 19036 | Extend class notation with all subgroups of a group. |
class SubGrp | ||
Syntax | cnsg 19037 | Extend class notation with all normal subgroups of a group. |
class NrmSGrp | ||
Syntax | cqg 19038 | Quotient group equivalence class. |
class ~QG | ||
Definition | df-subg 19039* | Define a subgroup of a group as a set of elements that is a group in its own right. Equivalently (issubg2 19057), a subgroup is a subset of the group that is closed for the group internal operation (see subgcl 19052), contains the neutral element of the group (see subg0 19048) and contains the inverses for all of its elements (see subginvcl 19051). (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข SubGrp = (๐ค โ Grp โฆ {๐ โ ๐ซ (Baseโ๐ค) โฃ (๐ค โพs ๐ ) โ Grp}) | ||
Definition | df-nsg 19040* | Define the equivalence relation in a quotient ring or quotient group (where ๐ is a two-sided ideal or a normal subgroup). For non-normal subgroups this generates the left cosets. (Contributed by Mario Carneiro, 15-Jun-2015.) |
โข NrmSGrp = (๐ค โ Grp โฆ {๐ โ (SubGrpโ๐ค) โฃ [(Baseโ๐ค) / ๐][(+gโ๐ค) / ๐]โ๐ฅ โ ๐ โ๐ฆ โ ๐ ((๐ฅ๐๐ฆ) โ ๐ โ (๐ฆ๐๐ฅ) โ ๐ )}) | ||
Definition | df-eqg 19041* | Define the equivalence relation in a group generated by a subgroup. More precisely, if ๐บ is a group and ๐ป is a subgroup, then ๐บ ~QG ๐ป is the equivalence relation on ๐บ associated with the left cosets of ๐ป. A typical application of this definition is the construction of the quotient group (resp. ring) of a group (resp. ring) by a normal subgroup (resp. two-sided ideal). (Contributed by Mario Carneiro, 15-Jun-2015.) |
โข ~QG = (๐ โ V, ๐ โ V โฆ {โจ๐ฅ, ๐ฆโฉ โฃ ({๐ฅ, ๐ฆ} โ (Baseโ๐) โง (((invgโ๐)โ๐ฅ)(+gโ๐)๐ฆ) โ ๐)}) | ||
Theorem | issubg 19042 | The subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) โ โข (๐ โ (SubGrpโ๐บ) โ (๐บ โ Grp โง ๐ โ ๐ต โง (๐บ โพs ๐) โ Grp)) | ||
Theorem | subgss 19043 | A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) โ โข (๐ โ (SubGrpโ๐บ) โ ๐ โ ๐ต) | ||
Theorem | subgid 19044 | A group is a subgroup of itself. (Contributed by Mario Carneiro, 7-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) โ โข (๐บ โ Grp โ ๐ต โ (SubGrpโ๐บ)) | ||
Theorem | subggrp 19045 | A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ป = (๐บ โพs ๐) โ โข (๐ โ (SubGrpโ๐บ) โ ๐ป โ Grp) | ||
Theorem | subgbas 19046 | The base of the restricted group in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ป = (๐บ โพs ๐) โ โข (๐ โ (SubGrpโ๐บ) โ ๐ = (Baseโ๐ป)) | ||
Theorem | subgrcl 19047 | Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข (๐ โ (SubGrpโ๐บ) โ ๐บ โ Grp) | ||
Theorem | subg0 19048 | A subgroup of a group must have the same identity as the group. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 30-Apr-2015.) |
โข ๐ป = (๐บ โพs ๐) & โข 0 = (0gโ๐บ) โ โข (๐ โ (SubGrpโ๐บ) โ 0 = (0gโ๐ป)) | ||
Theorem | subginv 19049 | The inverse of an element in a subgroup is the same as the inverse in the larger group. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ป = (๐บ โพs ๐) & โข ๐ผ = (invgโ๐บ) & โข ๐ฝ = (invgโ๐ป) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ ๐) โ (๐ผโ๐) = (๐ฝโ๐)) | ||
Theorem | subg0cl 19050 | The group identity is an element of any subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข 0 = (0gโ๐บ) โ โข (๐ โ (SubGrpโ๐บ) โ 0 โ ๐) | ||
Theorem | subginvcl 19051 | The inverse of an element is closed in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ผ = (invgโ๐บ) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ ๐) โ (๐ผโ๐) โ ๐) | ||
Theorem | subgcl 19052 | A subgroup is closed under group operation. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข + = (+gโ๐บ) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ + ๐) โ ๐) | ||
Theorem | subgsubcl 19053 | A subgroup is closed under group subtraction. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข โ = (-gโ๐บ) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ โ ๐) โ ๐) | ||
Theorem | subgsub 19054 | The subtraction of elements in a subgroup is the same as subtraction in the group. (Contributed by Mario Carneiro, 15-Jun-2015.) |
โข โ = (-gโ๐บ) & โข ๐ป = (๐บ โพs ๐) & โข ๐ = (-gโ๐ป) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ โ ๐) = (๐๐๐)) | ||
Theorem | subgmulgcl 19055 | Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.) |
โข ยท = (.gโ๐บ) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ โค โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐) | ||
Theorem | subgmulg 19056 | A group multiple is the same if evaluated in a subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.) |
โข ยท = (.gโ๐บ) & โข ๐ป = (๐บ โพs ๐) & โข โ = (.gโ๐ป) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ โค โง ๐ โ ๐) โ (๐ ยท ๐) = (๐ โ ๐)) | ||
Theorem | issubg2 19057* | Characterize the subgroups of a group by closure properties. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข ๐ผ = (invgโ๐บ) โ โข (๐บ โ Grp โ (๐ โ (SubGrpโ๐บ) โ (๐ โ ๐ต โง ๐ โ โ โง โ๐ฅ โ ๐ (โ๐ฆ โ ๐ (๐ฅ + ๐ฆ) โ ๐ โง (๐ผโ๐ฅ) โ ๐)))) | ||
Theorem | issubgrpd2 19058* | Prove a subgroup by closure (definition version). (Contributed by Stefan O'Rear, 7-Dec-2014.) |
โข (๐ โ ๐ = (๐ผ โพs ๐ท)) & โข (๐ โ 0 = (0gโ๐ผ)) & โข (๐ โ + = (+gโ๐ผ)) & โข (๐ โ ๐ท โ (Baseโ๐ผ)) & โข (๐ โ 0 โ ๐ท) & โข ((๐ โง ๐ฅ โ ๐ท โง ๐ฆ โ ๐ท) โ (๐ฅ + ๐ฆ) โ ๐ท) & โข ((๐ โง ๐ฅ โ ๐ท) โ ((invgโ๐ผ)โ๐ฅ) โ ๐ท) & โข (๐ โ ๐ผ โ Grp) โ โข (๐ โ ๐ท โ (SubGrpโ๐ผ)) | ||
Theorem | issubgrpd 19059* | Prove a subgroup by closure. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
โข (๐ โ ๐ = (๐ผ โพs ๐ท)) & โข (๐ โ 0 = (0gโ๐ผ)) & โข (๐ โ + = (+gโ๐ผ)) & โข (๐ โ ๐ท โ (Baseโ๐ผ)) & โข (๐ โ 0 โ ๐ท) & โข ((๐ โง ๐ฅ โ ๐ท โง ๐ฆ โ ๐ท) โ (๐ฅ + ๐ฆ) โ ๐ท) & โข ((๐ โง ๐ฅ โ ๐ท) โ ((invgโ๐ผ)โ๐ฅ) โ ๐ท) & โข (๐ โ ๐ผ โ Grp) โ โข (๐ โ ๐ โ Grp) | ||
Theorem | issubg3 19060* | A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
โข ๐ผ = (invgโ๐บ) โ โข (๐บ โ Grp โ (๐ โ (SubGrpโ๐บ) โ (๐ โ (SubMndโ๐บ) โง โ๐ฅ โ ๐ (๐ผโ๐ฅ) โ ๐))) | ||
Theorem | issubg4 19061* | A subgroup is a nonempty subset of the group closed under subtraction. (Contributed by Mario Carneiro, 17-Sep-2015.) |
โข ๐ต = (Baseโ๐บ) & โข โ = (-gโ๐บ) โ โข (๐บ โ Grp โ (๐ โ (SubGrpโ๐บ) โ (๐ โ ๐ต โง ๐ โ โ โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ โ ๐ฆ) โ ๐))) | ||
Theorem | grpissubg 19062 | If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then the (base set of the) group is subgroup of the other group. (Contributed by AV, 14-Mar-2019.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (Baseโ๐ป) โ โข ((๐บ โ Grp โง ๐ป โ Grp) โ ((๐ โ ๐ต โง (+gโ๐ป) = ((+gโ๐บ) โพ (๐ ร ๐))) โ ๐ โ (SubGrpโ๐บ))) | ||
Theorem | resgrpisgrp 19063 | If the base set of a group is contained in the base set of another group, and the group operation of the group is the restriction of the group operation of the other group to its base set, then the other group restricted to the base set of the group is a group. (Contributed by AV, 14-Mar-2019.) |
โข ๐ต = (Baseโ๐บ) & โข ๐ = (Baseโ๐ป) โ โข ((๐บ โ Grp โง ๐ป โ Grp) โ ((๐ โ ๐ต โง (+gโ๐ป) = ((+gโ๐บ) โพ (๐ ร ๐))) โ (๐บ โพs ๐) โ Grp)) | ||
Theorem | subgsubm 19064 | A subgroup is a submonoid. (Contributed by Mario Carneiro, 18-Jun-2015.) |
โข (๐ โ (SubGrpโ๐บ) โ ๐ โ (SubMndโ๐บ)) | ||
Theorem | subsubg 19065 | A subgroup of a subgroup is a subgroup. (Contributed by Mario Carneiro, 19-Jan-2015.) |
โข ๐ป = (๐บ โพs ๐) โ โข (๐ โ (SubGrpโ๐บ) โ (๐ด โ (SubGrpโ๐ป) โ (๐ด โ (SubGrpโ๐บ) โง ๐ด โ ๐))) | ||
Theorem | subgint 19066 | The intersection of a nonempty collection of subgroups is a subgroup. (Contributed by Mario Carneiro, 7-Dec-2014.) |
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ โ ) โ โฉ ๐ โ (SubGrpโ๐บ)) | ||
Theorem | 0subg 19067 | The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014.) (Proof shortened by SN, 31-Jan-2025.) |
โข 0 = (0gโ๐บ) โ โข (๐บ โ Grp โ { 0 } โ (SubGrpโ๐บ)) | ||
Theorem | 0subgOLD 19068 | Obsolete version of 0subg 19067 as of 31-Jan-2025. (Contributed by Stefan O'Rear, 10-Dec-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข 0 = (0gโ๐บ) โ โข (๐บ โ Grp โ { 0 } โ (SubGrpโ๐บ)) | ||
Theorem | trivsubgd 19069 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ต = { 0 }) & โข (๐ โ ๐ด โ (SubGrpโ๐บ)) โ โข (๐ โ ๐ด = ๐ต) | ||
Theorem | trivsubgsnd 19070 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ต = { 0 }) โ โข (๐ โ (SubGrpโ๐บ) = {๐ต}) | ||
Theorem | isnsg 19071* | Property of being a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข (๐ โ (NrmSGrpโ๐บ) โ (๐ โ (SubGrpโ๐บ) โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐))) | ||
Theorem | isnsg2 19072* | Weaken the condition of isnsg 19071 to only one side of the implication. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข (๐ โ (NrmSGrpโ๐บ) โ (๐ โ (SubGrpโ๐บ) โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐))) | ||
Theorem | nsgbi 19073 | Defining property of a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐ โ (NrmSGrpโ๐บ) โง ๐ด โ ๐ โง ๐ต โ ๐) โ ((๐ด + ๐ต) โ ๐ โ (๐ต + ๐ด) โ ๐)) | ||
Theorem | nsgsubg 19074 | A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข (๐ โ (NrmSGrpโ๐บ) โ ๐ โ (SubGrpโ๐บ)) | ||
Theorem | nsgconj 19075 | The conjugation of an element of a normal subgroup is in the subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐ โ (NrmSGrpโ๐บ) โง ๐ด โ ๐ โง ๐ต โ ๐) โ ((๐ด + ๐ต) โ ๐ด) โ ๐) | ||
Theorem | isnsg3 19076* | A subgroup is normal iff the conjugation of all the elements of the subgroup is in the subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) โ โข (๐ โ (NrmSGrpโ๐บ) โ (๐ โ (SubGrpโ๐บ) โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ฅ) โ ๐)) | ||
Theorem | subgacs 19077 | Subgroups are an algebraic closure system. (Contributed by Stefan O'Rear, 4-Apr-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
โข ๐ต = (Baseโ๐บ) โ โข (๐บ โ Grp โ (SubGrpโ๐บ) โ (ACSโ๐ต)) | ||
Theorem | nsgacs 19078 | Normal subgroups form an algebraic closure system. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
โข ๐ต = (Baseโ๐บ) โ โข (๐บ โ Grp โ (NrmSGrpโ๐บ) โ (ACSโ๐ต)) | ||
Theorem | elnmz 19079* | Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = {๐ฅ โ ๐ โฃ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐)} โ โข (๐ด โ ๐ โ (๐ด โ ๐ โง โ๐ง โ ๐ ((๐ด + ๐ง) โ ๐ โ (๐ง + ๐ด) โ ๐))) | ||
Theorem | nmzbi 19080* | Defining property of the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = {๐ฅ โ ๐ โฃ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐)} โ โข ((๐ด โ ๐ โง ๐ต โ ๐) โ ((๐ด + ๐ต) โ ๐ โ (๐ต + ๐ด) โ ๐)) | ||
Theorem | nmzsubg 19081* | The normalizer NG(S) of a subset ๐ of the group is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = {๐ฅ โ ๐ โฃ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐)} & โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข (๐บ โ Grp โ ๐ โ (SubGrpโ๐บ)) | ||
Theorem | ssnmz 19082* | A subgroup is a subset of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = {๐ฅ โ ๐ โฃ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐)} & โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข (๐ โ (SubGrpโ๐บ) โ ๐ โ ๐) | ||
Theorem | isnsg4 19083* | A subgroup is normal iff its normalizer is the entire group. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = {๐ฅ โ ๐ โฃ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐)} & โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข (๐ โ (NrmSGrpโ๐บ) โ (๐ โ (SubGrpโ๐บ) โง ๐ = ๐)) | ||
Theorem | nmznsg 19084* | Any subgroup is a normal subgroup of its normalizer. (Contributed by Mario Carneiro, 19-Jan-2015.) |
โข ๐ = {๐ฅ โ ๐ โฃ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐)} & โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข ๐ป = (๐บ โพs ๐) โ โข (๐ โ (SubGrpโ๐บ) โ ๐ โ (NrmSGrpโ๐ป)) | ||
Theorem | 0nsg 19085 | The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015.) |
โข 0 = (0gโ๐บ) โ โข (๐บ โ Grp โ { 0 } โ (NrmSGrpโ๐บ)) | ||
Theorem | nsgid 19086 | The whole group is a normal subgroup of itself. (Contributed by Mario Carneiro, 4-Feb-2015.) |
โข ๐ต = (Baseโ๐บ) โ โข (๐บ โ Grp โ ๐ต โ (NrmSGrpโ๐บ)) | ||
Theorem | 0idnsgd 19087 | The whole group and the zero subgroup are normal subgroups of a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Grp) โ โข (๐ โ {{ 0 }, ๐ต} โ (NrmSGrpโ๐บ)) | ||
Theorem | trivnsgd 19088 | The only normal subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ต = { 0 }) โ โข (๐ โ (NrmSGrpโ๐บ) = {๐ต}) | ||
Theorem | triv1nsgd 19089 | A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ต = { 0 }) โ โข (๐ โ (NrmSGrpโ๐บ) โ 1o) | ||
Theorem | 1nsgtrivd 19090 | A group with exactly one normal subgroup is trivial. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ (NrmSGrpโ๐บ) โ 1o) โ โข (๐ โ ๐ต = { 0 }) | ||
Theorem | releqg 19091 | The left coset equivalence relation is a relation. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข ๐ = (๐บ ~QG ๐) โ โข Rel ๐ | ||
Theorem | eqgfval 19092* | Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข ๐ = (invgโ๐บ) & โข + = (+gโ๐บ) & โข ๐ = (๐บ ~QG ๐) โ โข ((๐บ โ ๐ โง ๐ โ ๐) โ ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ({๐ฅ, ๐ฆ} โ ๐ โง ((๐โ๐ฅ) + ๐ฆ) โ ๐)}) | ||
Theorem | eqgval 19093 | Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) |
โข ๐ = (Baseโ๐บ) & โข ๐ = (invgโ๐บ) & โข + = (+gโ๐บ) & โข ๐ = (๐บ ~QG ๐) โ โข ((๐บ โ ๐ โง ๐ โ ๐) โ (๐ด๐ ๐ต โ (๐ด โ ๐ โง ๐ต โ ๐ โง ((๐โ๐ด) + ๐ต) โ ๐))) | ||
Theorem | eqger 19094 | The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข โผ = (๐บ ~QG ๐) โ โข (๐ โ (SubGrpโ๐บ) โ โผ Er ๐) | ||
Theorem | eqglact 19095* | A left coset can be expressed as the image of a left action. (Contributed by Mario Carneiro, 20-Sep-2015.) |
โข ๐ = (Baseโ๐บ) & โข โผ = (๐บ ~QG ๐) & โข + = (+gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐ โง ๐ด โ ๐) โ [๐ด] โผ = ((๐ฅ โ ๐ โฆ (๐ด + ๐ฅ)) โ ๐)) | ||
Theorem | eqgid 19096 | The left coset containing the identity is the original subgroup. (Contributed by Mario Carneiro, 20-Sep-2015.) |
โข ๐ = (Baseโ๐บ) & โข โผ = (๐บ ~QG ๐) & โข 0 = (0gโ๐บ) โ โข (๐ โ (SubGrpโ๐บ) โ [ 0 ] โผ = ๐) | ||
Theorem | eqgen 19097 | Each coset is equipotent to the subgroup itself (which is also the coset containing the identity). (Contributed by Mario Carneiro, 20-Sep-2015.) |
โข ๐ = (Baseโ๐บ) & โข โผ = (๐บ ~QG ๐) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ด โ (๐ / โผ )) โ ๐ โ ๐ด) | ||
Theorem | eqgcpbl 19098 | The subgroup coset equivalence relation is compatible with addition when the subgroup is normal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข ๐ = (Baseโ๐บ) & โข โผ = (๐บ ~QG ๐) & โข + = (+gโ๐บ) โ โข (๐ โ (NrmSGrpโ๐บ) โ ((๐ด โผ ๐ถ โง ๐ต โผ ๐ท) โ (๐ด + ๐ต) โผ (๐ถ + ๐ท))) | ||
Theorem | quselbas 19099* | Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025.) |
โข โผ = (๐บ ~QG ๐) & โข ๐ = (๐บ /s โผ ) & โข ๐ต = (Baseโ๐บ) โ โข ((๐บ โ ๐ โง ๐ โ ๐) โ (๐ โ (Baseโ๐) โ โ๐ฅ โ ๐ต ๐ = [๐ฅ] โผ )) | ||
Theorem | quseccl0 19100 | Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) Generalization of quseccl 19102 for arbitrary sets ๐บ. (Revised by AV, 24-Feb-2025.) |
โข โผ = (๐บ ~QG ๐) & โข ๐ป = (๐บ /s โผ ) & โข ๐ถ = (Baseโ๐บ) & โข ๐ต = (Baseโ๐ป) โ โข ((๐บ โ ๐ โง ๐ โ ๐ถ) โ [๐] โผ โ ๐ต) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |