![]() |
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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mulgnegnn 19001 | Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ผ = (invgโ๐บ) โ โข ((๐ โ โ โง ๐ โ ๐ต) โ (-๐ ยท ๐) = (๐ผโ(๐ ยท ๐))) | ||
Theorem | mulgnn0p1 19002 | 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 19003* | Closure of the group multiple (exponentiation) operation in a submagma. (Contributed by Mario Carneiro, 10-Jan-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) & โข (๐ โ ๐บ โ ๐) & โข (๐ โ ๐ โ ๐ต) & โข ((๐ โง ๐ฅ โ ๐ โง ๐ฆ โ ๐) โ (๐ฅ + ๐ฆ) โ ๐) โ โข ((๐ โง ๐ โ โ โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐) | ||
Theorem | mulgnn0subcl 19004* | 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 19005* | 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 19006 | 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 19007 | 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 19008 | Closure of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) | ||
Theorem | mulgneg 19009 | 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 19010 | 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 19011 | 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 19012 | Closure of the group multiple (exponentiation) operation for a nonnegative multiplier in a monoid. Deduction associated with mulgnn0cl 19007. (Contributed by SN, 1-Feb-2025.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข (๐ โ ๐บ โ Mnd) & โข (๐ โ ๐ โ โ0) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐ ยท ๐) โ ๐ต) | ||
Theorem | mulgcld 19013 | Deduction associated with mulgcl 19008. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ โ โค) & โข (๐ โ ๐ โ ๐ต) โ โข (๐ โ (๐ ยท ๐) โ ๐ต) | ||
Theorem | mulgaddcomlem 19014 | Lemma for mulgaddcom 19015. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 31-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข (((๐บ โ Grp โง ๐ฆ โ โค โง ๐ โ ๐ต) โง ((๐ฆ ยท ๐) + ๐) = (๐ + (๐ฆ ยท ๐))) โ ((-๐ฆ ยท ๐) + ๐) = (๐ + (-๐ฆ ยท ๐))) | ||
Theorem | mulgaddcom 19015 | 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 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 | mulginvinv 19017 | 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 19018 | 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 19019 | 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 19020 | 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 19021 | Sum of group multiples, generalized to โ0. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Mnd โง (๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) | ||
Theorem | mulgdirlem 19022 | Lemma for mulgdir 19023. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต) โง (๐ + ๐) โ โ0) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) | ||
Theorem | mulgdir 19023 | Sum of group multiples, generalized to โค. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) | ||
Theorem | mulgp1 19024 | Group multiple (exponentiation) operation at a successor, extended to โค. (Contributed by Mario Carneiro, 11-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ ((๐ + 1) ยท ๐) = ((๐ ยท ๐) + ๐)) | ||
Theorem | mulgneg2 19025 | Group multiple (exponentiation) operation at a negative integer. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ๐ผ = (invgโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ โค โง ๐ โ ๐ต) โ (-๐ ยท ๐) = (๐ ยท (๐ผโ๐))) | ||
Theorem | mulgnnass 19026 | 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 19027 | Product of group multiples, generalized to โ0. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Mnd โง (๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) | ||
Theorem | mulgass 19028 | Product of group multiples, generalized to โค. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) | ||
Theorem | mulgassr 19029 | Reversed product of group multiples. (Contributed by Paul Chapman, 17-Apr-2009.) (Revised by AV, 30-Aug-2021.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) | ||
Theorem | mulgmodid 19030 | 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 19031 | Distribution of group multiples over subtraction for group elements, subdir 11653 analog. (Contributed by Mario Carneiro, 13-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข โ = (-gโ๐บ) โ โข ((๐บ โ Grp โง (๐ โ โค โง ๐ โ โค โง ๐ โ ๐ต)) โ ((๐ โ ๐) ยท ๐) = ((๐ ยท ๐) โ (๐ ยท ๐))) | ||
Theorem | mhmmulg 19032 | A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ร = (.gโ๐ป) โ โข ((๐น โ (๐บ MndHom ๐ป) โง ๐ โ โ0 โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) | ||
Theorem | mulgpropd 19033* | 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 19034 | Closure of the group multiple (exponentiation) operation in a submonoid. (Contributed by Mario Carneiro, 13-Jan-2015.) |
โข โ = (.gโ๐บ) โ โข ((๐ โ (SubMndโ๐บ) โง ๐ โ โ0 โง ๐ โ ๐) โ (๐ โ ๐) โ ๐) | ||
Theorem | submmulg 19035 | 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 19036 | Value of a group multiple in a structure power. (Contributed by Mario Carneiro, 15-Jun-2015.) |
โข ๐ = (๐ โs ๐ผ) & โข ๐ต = (Baseโ๐) & โข โ = (.gโ๐) & โข ยท = (.gโ๐ ) โ โข (((๐ โ Mnd โง ๐ผ โ ๐) โง (๐ โ โ0 โง ๐ โ ๐ต โง ๐ด โ ๐ผ)) โ ((๐ โ ๐)โ๐ด) = (๐ ยท (๐โ๐ด))) | ||
Syntax | csubg 19037 | Extend class notation with all subgroups of a group. |
class SubGrp | ||
Syntax | cnsg 19038 | Extend class notation with all normal subgroups of a group. |
class NrmSGrp | ||
Syntax | cqg 19039 | Quotient group equivalence class. |
class ~QG | ||
Definition | df-subg 19040* | Define a subgroup of a group as a set of elements that is a group in its own right. Equivalently (issubg2 19058), a subgroup is a subset of the group that is closed for the group internal operation (see subgcl 19053), contains the neutral element of the group (see subg0 19049) and contains the inverses for all of its elements (see subginvcl 19052). (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข SubGrp = (๐ค โ Grp โฆ {๐ โ ๐ซ (Baseโ๐ค) โฃ (๐ค โพs ๐ ) โ Grp}) | ||
Definition | df-nsg 19041* | 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 19042* | 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 19043 | The subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) โ โข (๐ โ (SubGrpโ๐บ) โ (๐บ โ Grp โง ๐ โ ๐ต โง (๐บ โพs ๐) โ Grp)) | ||
Theorem | subgss 19044 | A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) โ โข (๐ โ (SubGrpโ๐บ) โ ๐ โ ๐ต) | ||
Theorem | subgid 19045 | A group is a subgroup of itself. (Contributed by Mario Carneiro, 7-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) โ โข (๐บ โ Grp โ ๐ต โ (SubGrpโ๐บ)) | ||
Theorem | subggrp 19046 | A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ป = (๐บ โพs ๐) โ โข (๐ โ (SubGrpโ๐บ) โ ๐ป โ Grp) | ||
Theorem | subgbas 19047 | The base of the restricted group in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ป = (๐บ โพs ๐) โ โข (๐ โ (SubGrpโ๐บ) โ ๐ = (Baseโ๐ป)) | ||
Theorem | subgrcl 19048 | Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข (๐ โ (SubGrpโ๐บ) โ ๐บ โ Grp) | ||
Theorem | subg0 19049 | 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 19050 | 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 19051 | The group identity is an element of any subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข 0 = (0gโ๐บ) โ โข (๐ โ (SubGrpโ๐บ) โ 0 โ ๐) | ||
Theorem | subginvcl 19052 | The inverse of an element is closed in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ผ = (invgโ๐บ) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ ๐) โ (๐ผโ๐) โ ๐) | ||
Theorem | subgcl 19053 | A subgroup is closed under group operation. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข + = (+gโ๐บ) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ + ๐) โ ๐) | ||
Theorem | subgsubcl 19054 | A subgroup is closed under group subtraction. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข โ = (-gโ๐บ) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ ๐ โง ๐ โ ๐) โ (๐ โ ๐) โ ๐) | ||
Theorem | subgsub 19055 | 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 19056 | Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.) |
โข ยท = (.gโ๐บ) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ โค โง ๐ โ ๐) โ (๐ ยท ๐) โ ๐) | ||
Theorem | subgmulg 19057 | A group multiple is the same if evaluated in a subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.) |
โข ยท = (.gโ๐บ) & โข ๐ป = (๐บ โพs ๐) & โข โ = (.gโ๐ป) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ โค โง ๐ โ ๐) โ (๐ ยท ๐) = (๐ โ ๐)) | ||
Theorem | issubg2 19058* | Characterize the subgroups of a group by closure properties. (Contributed by Mario Carneiro, 2-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข ๐ผ = (invgโ๐บ) โ โข (๐บ โ Grp โ (๐ โ (SubGrpโ๐บ) โ (๐ โ ๐ต โง ๐ โ โ โง โ๐ฅ โ ๐ (โ๐ฆ โ ๐ (๐ฅ + ๐ฆ) โ ๐ โง (๐ผโ๐ฅ) โ ๐)))) | ||
Theorem | issubgrpd2 19059* | 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 19060* | Prove a subgroup by closure. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
โข (๐ โ ๐ = (๐ผ โพs ๐ท)) & โข (๐ โ 0 = (0gโ๐ผ)) & โข (๐ โ + = (+gโ๐ผ)) & โข (๐ โ ๐ท โ (Baseโ๐ผ)) & โข (๐ โ 0 โ ๐ท) & โข ((๐ โง ๐ฅ โ ๐ท โง ๐ฆ โ ๐ท) โ (๐ฅ + ๐ฆ) โ ๐ท) & โข ((๐ โง ๐ฅ โ ๐ท) โ ((invgโ๐ผ)โ๐ฅ) โ ๐ท) & โข (๐ โ ๐ผ โ Grp) โ โข (๐ โ ๐ โ Grp) | ||
Theorem | issubg3 19061* | A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
โข ๐ผ = (invgโ๐บ) โ โข (๐บ โ Grp โ (๐ โ (SubGrpโ๐บ) โ (๐ โ (SubMndโ๐บ) โง โ๐ฅ โ ๐ (๐ผโ๐ฅ) โ ๐))) | ||
Theorem | issubg4 19062* | 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 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 (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 19064 | 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 19065 | A subgroup is a submonoid. (Contributed by Mario Carneiro, 18-Jun-2015.) |
โข (๐ โ (SubGrpโ๐บ) โ ๐ โ (SubMndโ๐บ)) | ||
Theorem | subsubg 19066 | A subgroup of a subgroup is a subgroup. (Contributed by Mario Carneiro, 19-Jan-2015.) |
โข ๐ป = (๐บ โพs ๐) โ โข (๐ โ (SubGrpโ๐บ) โ (๐ด โ (SubGrpโ๐ป) โ (๐ด โ (SubGrpโ๐บ) โง ๐ด โ ๐))) | ||
Theorem | subgint 19067 | The intersection of a nonempty collection of subgroups is a subgroup. (Contributed by Mario Carneiro, 7-Dec-2014.) |
โข ((๐ โ (SubGrpโ๐บ) โง ๐ โ โ ) โ โฉ ๐ โ (SubGrpโ๐บ)) | ||
Theorem | 0subg 19068 | 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 19069 | Obsolete version of 0subg 19068 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 19070 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ต = { 0 }) & โข (๐ โ ๐ด โ (SubGrpโ๐บ)) โ โข (๐ โ ๐ด = ๐ต) | ||
Theorem | trivsubgsnd 19071 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ต = { 0 }) โ โข (๐ โ (SubGrpโ๐บ) = {๐ต}) | ||
Theorem | isnsg 19072* | Property of being a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข (๐ โ (NrmSGrpโ๐บ) โ (๐ โ (SubGrpโ๐บ) โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐))) | ||
Theorem | isnsg2 19073* | Weaken the condition of isnsg 19072 to only one side of the implication. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข (๐ โ (NrmSGrpโ๐บ) โ (๐ โ (SubGrpโ๐บ) โง โ๐ฅ โ ๐ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐))) | ||
Theorem | nsgbi 19074 | Defining property of a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข ((๐ โ (NrmSGrpโ๐บ) โง ๐ด โ ๐ โง ๐ต โ ๐) โ ((๐ด + ๐ต) โ ๐ โ (๐ต + ๐ด) โ ๐)) | ||
Theorem | nsgsubg 19075 | A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข (๐ โ (NrmSGrpโ๐บ) โ ๐ โ (SubGrpโ๐บ)) | ||
Theorem | nsgconj 19076 | 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 19077* | 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 19078 | 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 19079 | Normal subgroups form an algebraic closure system. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
โข ๐ต = (Baseโ๐บ) โ โข (๐บ โ Grp โ (NrmSGrpโ๐บ) โ (ACSโ๐ต)) | ||
Theorem | elnmz 19080* | Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = {๐ฅ โ ๐ โฃ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐)} โ โข (๐ด โ ๐ โ (๐ด โ ๐ โง โ๐ง โ ๐ ((๐ด + ๐ง) โ ๐ โ (๐ง + ๐ด) โ ๐))) | ||
Theorem | nmzbi 19081* | Defining property of the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = {๐ฅ โ ๐ โฃ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐)} โ โข ((๐ด โ ๐ โง ๐ต โ ๐) โ ((๐ด + ๐ต) โ ๐ โ (๐ต + ๐ด) โ ๐)) | ||
Theorem | nmzsubg 19082* | 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 19083* | A subgroup is a subset of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = {๐ฅ โ ๐ โฃ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐)} & โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข (๐ โ (SubGrpโ๐บ) โ ๐ โ ๐) | ||
Theorem | isnsg4 19084* | A subgroup is normal iff its normalizer is the entire group. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = {๐ฅ โ ๐ โฃ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐)} & โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข (๐ โ (NrmSGrpโ๐บ) โ (๐ โ (SubGrpโ๐บ) โง ๐ = ๐)) | ||
Theorem | nmznsg 19085* | Any subgroup is a normal subgroup of its normalizer. (Contributed by Mario Carneiro, 19-Jan-2015.) |
โข ๐ = {๐ฅ โ ๐ โฃ โ๐ฆ โ ๐ ((๐ฅ + ๐ฆ) โ ๐ โ (๐ฆ + ๐ฅ) โ ๐)} & โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข ๐ป = (๐บ โพs ๐) โ โข (๐ โ (SubGrpโ๐บ) โ ๐ โ (NrmSGrpโ๐ป)) | ||
Theorem | 0nsg 19086 | The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015.) |
โข 0 = (0gโ๐บ) โ โข (๐บ โ Grp โ { 0 } โ (NrmSGrpโ๐บ)) | ||
Theorem | nsgid 19087 | The whole group is a normal subgroup of itself. (Contributed by Mario Carneiro, 4-Feb-2015.) |
โข ๐ต = (Baseโ๐บ) โ โข (๐บ โ Grp โ ๐ต โ (NrmSGrpโ๐บ)) | ||
Theorem | 0idnsgd 19088 | 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 19089 | 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 19090 | A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
โข ๐ต = (Baseโ๐บ) & โข 0 = (0gโ๐บ) & โข (๐ โ ๐บ โ Grp) & โข (๐ โ ๐ต = { 0 }) โ โข (๐ โ (NrmSGrpโ๐บ) โ 1o) | ||
Theorem | 1nsgtrivd 19091 | 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 19092 | The left coset equivalence relation is a relation. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข ๐ = (๐บ ~QG ๐) โ โข Rel ๐ | ||
Theorem | eqgfval 19093* | Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข ๐ = (invgโ๐บ) & โข + = (+gโ๐บ) & โข ๐ = (๐บ ~QG ๐) โ โข ((๐บ โ ๐ โง ๐ โ ๐) โ ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ({๐ฅ, ๐ฆ} โ ๐ โง ((๐โ๐ฅ) + ๐ฆ) โ ๐)}) | ||
Theorem | eqgval 19094 | 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 19095 | The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข โผ = (๐บ ~QG ๐) โ โข (๐ โ (SubGrpโ๐บ) โ โผ Er ๐) | ||
Theorem | eqglact 19096* | 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 19097 | 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 19098 | 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 19099 | 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 19100* | Membership in the base set of a quotient group. (Contributed by AV, 1-Mar-2025.) |
โข โผ = (๐บ ~QG ๐) & โข ๐ = (๐บ /s โผ ) & โข ๐ต = (Baseโ๐บ) โ โข ((๐บ โ ๐ โง ๐ โ ๐) โ (๐ โ (Baseโ๐) โ โ๐ฅ โ ๐ต ๐ = [๐ฅ] โผ )) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |