Home | Metamath
Proof Explorer Theorem List (p. 189 of 468) | < 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: | Metamath Proof Explorer
(1-29329) |
Hilbert Space Explorer
(29330-30852) |
Users' Mathboxes
(30853-46765) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-subg 18801* | Define a subgroup of a group as a set of elements that is a group in its own right. Equivalently (issubg2 18819), a subgroup is a subset of the group that is closed for the group internal operation (see subgcl 18814), contains the neutral element of the group (see subg0 18810) and contains the inverses for all of its elements (see subginvcl 18813). (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ SubGrp = (π€ β Grp β¦ {π β π« (Baseβπ€) β£ (π€ βΎs π ) β Grp}) | ||
Definition | df-nsg 18802* | 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 18803* | 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 18804 | The subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (BaseβπΊ) β β’ (π β (SubGrpβπΊ) β (πΊ β Grp β§ π β π΅ β§ (πΊ βΎs π) β Grp)) | ||
Theorem | subgss 18805 | A subgroup is a subset. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (BaseβπΊ) β β’ (π β (SubGrpβπΊ) β π β π΅) | ||
Theorem | subgid 18806 | A group is a subgroup of itself. (Contributed by Mario Carneiro, 7-Dec-2014.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β π΅ β (SubGrpβπΊ)) | ||
Theorem | subggrp 18807 | A subgroup is a group. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π» = (πΊ βΎs π) β β’ (π β (SubGrpβπΊ) β π» β Grp) | ||
Theorem | subgbas 18808 | The base of the restricted group in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π» = (πΊ βΎs π) β β’ (π β (SubGrpβπΊ) β π = (Baseβπ»)) | ||
Theorem | subgrcl 18809 | Reverse closure for the subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ (π β (SubGrpβπΊ) β πΊ β Grp) | ||
Theorem | subg0 18810 | 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 18811 | 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 18812 | The group identity is an element of any subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ 0 = (0gβπΊ) β β’ (π β (SubGrpβπΊ) β 0 β π) | ||
Theorem | subginvcl 18813 | The inverse of an element is closed in a subgroup. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ πΌ = (invgβπΊ) β β’ ((π β (SubGrpβπΊ) β§ π β π) β (πΌβπ) β π) | ||
Theorem | subgcl 18814 | A subgroup is closed under group operation. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ + = (+gβπΊ) β β’ ((π β (SubGrpβπΊ) β§ π β π β§ π β π) β (π + π) β π) | ||
Theorem | subgsubcl 18815 | A subgroup is closed under group subtraction. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ β = (-gβπΊ) β β’ ((π β (SubGrpβπΊ) β§ π β π β§ π β π) β (π β π) β π) | ||
Theorem | subgsub 18816 | 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 18817 | Closure of the group multiple (exponentiation) operation in a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ Β· = (.gβπΊ) β β’ ((π β (SubGrpβπΊ) β§ π β β€ β§ π β π) β (π Β· π) β π) | ||
Theorem | subgmulg 18818 | A group multiple is the same if evaluated in a subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.) |
β’ Β· = (.gβπΊ) & β’ π» = (πΊ βΎs π) & β’ β = (.gβπ») β β’ ((π β (SubGrpβπΊ) β§ π β β€ β§ π β π) β (π Β· π) = (π β π)) | ||
Theorem | issubg2 18819* | Characterize the subgroups of a group by closure properties. (Contributed by Mario Carneiro, 2-Dec-2014.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ πΌ = (invgβπΊ) β β’ (πΊ β Grp β (π β (SubGrpβπΊ) β (π β π΅ β§ π β β β§ βπ₯ β π (βπ¦ β π (π₯ + π¦) β π β§ (πΌβπ₯) β π)))) | ||
Theorem | issubgrpd2 18820* | 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 18821* | Prove a subgroup by closure. (Contributed by Stefan O'Rear, 7-Dec-2014.) |
β’ (π β π = (πΌ βΎs π·)) & β’ (π β 0 = (0gβπΌ)) & β’ (π β + = (+gβπΌ)) & β’ (π β π· β (BaseβπΌ)) & β’ (π β 0 β π·) & β’ ((π β§ π₯ β π· β§ π¦ β π·) β (π₯ + π¦) β π·) & β’ ((π β§ π₯ β π·) β ((invgβπΌ)βπ₯) β π·) & β’ (π β πΌ β Grp) β β’ (π β π β Grp) | ||
Theorem | issubg3 18822* | A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ πΌ = (invgβπΊ) β β’ (πΊ β Grp β (π β (SubGrpβπΊ) β (π β (SubMndβπΊ) β§ βπ₯ β π (πΌβπ₯) β π))) | ||
Theorem | issubg4 18823* | 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 18824 | 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 18825 | 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 18826 | A subgroup is a submonoid. (Contributed by Mario Carneiro, 18-Jun-2015.) |
β’ (π β (SubGrpβπΊ) β π β (SubMndβπΊ)) | ||
Theorem | subsubg 18827 | A subgroup of a subgroup is a subgroup. (Contributed by Mario Carneiro, 19-Jan-2015.) |
β’ π» = (πΊ βΎs π) β β’ (π β (SubGrpβπΊ) β (π΄ β (SubGrpβπ») β (π΄ β (SubGrpβπΊ) β§ π΄ β π))) | ||
Theorem | subgint 18828 | The intersection of a nonempty collection of subgroups is a subgroup. (Contributed by Mario Carneiro, 7-Dec-2014.) |
β’ ((π β (SubGrpβπΊ) β§ π β β ) β β© π β (SubGrpβπΊ)) | ||
Theorem | 0subg 18829 | The zero subgroup of an arbitrary group. (Contributed by Stefan O'Rear, 10-Dec-2014.) |
β’ 0 = (0gβπΊ) β β’ (πΊ β Grp β { 0 } β (SubGrpβπΊ)) | ||
Theorem | trivsubgd 18830 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π΅ = { 0 }) & β’ (π β π΄ β (SubGrpβπΊ)) β β’ (π β π΄ = π΅) | ||
Theorem | trivsubgsnd 18831 | The only subgroup of a trivial group is itself. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π΅ = { 0 }) β β’ (π β (SubGrpβπΊ) = {π΅}) | ||
Theorem | isnsg 18832* | Property of being a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (π β (NrmSGrpβπΊ) β (π β (SubGrpβπΊ) β§ βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π))) | ||
Theorem | isnsg2 18833* | Weaken the condition of isnsg 18832 to only one side of the implication. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (π β (NrmSGrpβπΊ) β (π β (SubGrpβπΊ) β§ βπ₯ β π βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π))) | ||
Theorem | nsgbi 18834 | Defining property of a normal subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ ((π β (NrmSGrpβπΊ) β§ π΄ β π β§ π΅ β π) β ((π΄ + π΅) β π β (π΅ + π΄) β π)) | ||
Theorem | nsgsubg 18835 | A normal subgroup is a subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ (π β (NrmSGrpβπΊ) β π β (SubGrpβπΊ)) | ||
Theorem | nsgconj 18836 | 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 18837* | 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 18838 | 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 18839 | Normal subgroups form an algebraic closure system. (Contributed by Stefan O'Rear, 4-Sep-2015.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β (NrmSGrpβπΊ) β (ACSβπ΅)) | ||
Theorem | elnmz 18840* | Elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = {π₯ β π β£ βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π)} β β’ (π΄ β π β (π΄ β π β§ βπ§ β π ((π΄ + π§) β π β (π§ + π΄) β π))) | ||
Theorem | nmzbi 18841* | Defining property of the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = {π₯ β π β£ βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π)} β β’ ((π΄ β π β§ π΅ β π) β ((π΄ + π΅) β π β (π΅ + π΄) β π)) | ||
Theorem | nmzsubg 18842* | 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 18843* | A subgroup is a subset of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = {π₯ β π β£ βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π)} & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (π β (SubGrpβπΊ) β π β π) | ||
Theorem | isnsg4 18844* | A subgroup is normal iff its normalizer is the entire group. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = {π₯ β π β£ βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π)} & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (π β (NrmSGrpβπΊ) β (π β (SubGrpβπΊ) β§ π = π)) | ||
Theorem | nmznsg 18845* | Any subgroup is a normal subgroup of its normalizer. (Contributed by Mario Carneiro, 19-Jan-2015.) |
β’ π = {π₯ β π β£ βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π)} & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π» = (πΊ βΎs π) β β’ (π β (SubGrpβπΊ) β π β (NrmSGrpβπ»)) | ||
Theorem | 0nsg 18846 | The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ 0 = (0gβπΊ) β β’ (πΊ β Grp β { 0 } β (NrmSGrpβπΊ)) | ||
Theorem | nsgid 18847 | The whole group is a normal subgroup of itself. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β π΅ β (NrmSGrpβπΊ)) | ||
Theorem | 0idnsgd 18848 | 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 18849 | 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 18850 | A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π΅ = { 0 }) β β’ (π β (NrmSGrpβπΊ) β 1o) | ||
Theorem | 1nsgtrivd 18851 | 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 18852 | The left coset equivalence relation is a relation. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π = (πΊ ~QG π) β β’ Rel π | ||
Theorem | eqgfval 18853* | Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ π = (invgβπΊ) & β’ + = (+gβπΊ) & β’ π = (πΊ ~QG π) β β’ ((πΊ β π β§ π β π) β π = {β¨π₯, π¦β© β£ ({π₯, π¦} β π β§ ((πβπ₯) + π¦) β π)}) | ||
Theorem | eqgval 18854 | 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 18855 | The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ βΌ = (πΊ ~QG π) β β’ (π β (SubGrpβπΊ) β βΌ Er π) | ||
Theorem | eqglact 18856* | 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 18857 | 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 18858 | 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 18859 | 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 | qusgrp 18860 | If π is a normal subgroup of πΊ, then π» = πΊ / π is a group, called the quotient of πΊ by π. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 12-Aug-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) β β’ (π β (NrmSGrpβπΊ) β π» β Grp) | ||
Theorem | quseccl 18861 | Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) & β’ π = (BaseβπΊ) & β’ π΅ = (Baseβπ») β β’ ((π β (NrmSGrpβπΊ) β§ π β π) β [π](πΊ ~QG π) β π΅) | ||
Theorem | qusadd 18862 | Value of the group operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (+gβπ») β β’ ((π β (NrmSGrpβπΊ) β§ π β π β§ π β π) β ([π](πΊ ~QG π) β [π](πΊ ~QG π)) = [(π + π)](πΊ ~QG π)) | ||
Theorem | qus0 18863 | Value of the group identity operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) & β’ 0 = (0gβπΊ) β β’ (π β (NrmSGrpβπΊ) β [ 0 ](πΊ ~QG π) = (0gβπ»)) | ||
Theorem | qusinv 18864 | Value of the group inverse operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) & β’ π = (BaseβπΊ) & β’ πΌ = (invgβπΊ) & β’ π = (invgβπ») β β’ ((π β (NrmSGrpβπΊ) β§ π β π) β (πβ[π](πΊ ~QG π)) = [(πΌβπ)](πΊ ~QG π)) | ||
Theorem | qussub 18865 | Value of the group subtraction operation in a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) & β’ π = (BaseβπΊ) & β’ β = (-gβπΊ) & β’ π = (-gβπ») β β’ ((π β (NrmSGrpβπΊ) β§ π β π β§ π β π) β ([π](πΊ ~QG π)π[π](πΊ ~QG π)) = [(π β π)](πΊ ~QG π)) | ||
Theorem | lagsubg2 18866 | Lagrange's theorem for finite groups. Call the "order" of a group the cardinal number of the basic set of the group, and "index of a subgroup" the cardinal number of the set of left (or right, this is the same) cosets of this subgroup. Then the order of the group is the (cardinal) product of the order of any of its subgroups by the index of this subgroup. (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.) |
β’ π = (BaseβπΊ) & β’ βΌ = (πΊ ~QG π) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π β Fin) β β’ (π β (β―βπ) = ((β―β(π / βΌ )) Β· (β―βπ))) | ||
Theorem | lagsubg 18867 | Lagrange's theorem for Groups: the order of any subgroup of a finite group is a divisor of the order of the group. This is Metamath 100 proof #71. (Contributed by Mario Carneiro, 11-Jul-2014.) (Revised by Mario Carneiro, 12-Aug-2015.) |
β’ π = (BaseβπΊ) β β’ ((π β (SubGrpβπΊ) β§ π β Fin) β (β―βπ) β₯ (β―βπ)) | ||
This section contains some preliminary results about cyclic monoids and groups before the class CycGrp of cyclic groups (see df-cyg 19527) is defined in the context of Abelian groups. | ||
Theorem | cycsubmel 18868* | Characterization of an element of the set of nonnegative integer powers of an element π΄. Although this theorem holds for any class πΊ, the definition of πΉ is only meaningful if πΊ is a monoid or at least a unital magma. (Contributed by AV, 28-Dec-2023.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π₯ β β0 β¦ (π₯ Β· π΄)) & β’ πΆ = ran πΉ β β’ (π β πΆ β βπ β β0 π = (π Β· π΄)) | ||
Theorem | cycsubmcl 18869* | The set of nonnegative integer powers of an element π΄ contains π΄. Although this theorem holds for any class πΊ, the definition of πΉ is only meaningful if πΊ is a monoid or at least a unital magma. (Contributed by AV, 28-Dec-2023.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π₯ β β0 β¦ (π₯ Β· π΄)) & β’ πΆ = ran πΉ β β’ (π΄ β π΅ β π΄ β πΆ) | ||
Theorem | cycsubm 18870* | The set of nonnegative integer powers of an element π΄ of a monoid forms a submonoid containing π΄ (see cycsubmcl 18869), called the cyclic monoid generated by the element π΄. This corresponds to the statement in [Lang] p. 6. (Contributed by AV, 28-Dec-2023.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π₯ β β0 β¦ (π₯ Β· π΄)) & β’ πΆ = ran πΉ β β’ ((πΊ β Mnd β§ π΄ β π΅) β πΆ β (SubMndβπΊ)) | ||
Theorem | cyccom 18871* | Condition for an operation to be commutative. Lemma for cycsubmcom 18872 and cygabl 19540. Formerly part of proof for cygabl 19540. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 20-Jan-2024.) |
β’ (π β βπ β πΆ βπ₯ β π π = (π₯ Β· π΄)) & β’ (π β βπ β π βπ β π ((π + π) Β· π΄) = ((π Β· π΄) + (π Β· π΄))) & β’ (π β π β πΆ) & β’ (π β π β πΆ) & β’ (π β π β β) β β’ (π β (π + π) = (π + π)) | ||
Theorem | cycsubmcom 18872* | The operation of a monoid is commutative over the set of nonnegative integer powers of an element π΄ of the monoid. (Contributed by AV, 20-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π₯ β β0 β¦ (π₯ Β· π΄)) & β’ πΆ = ran πΉ & β’ + = (+gβπΊ) β β’ (((πΊ β Mnd β§ π΄ β π΅) β§ (π β πΆ β§ π β πΆ)) β (π + π) = (π + π)) | ||
Theorem | cycsubggend 18873* | The cyclic subgroup generated by π΄ includes its generator. Although this theorem holds for any class πΊ, the definition of πΉ is only meaningful if πΊ is a group. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π β β€ β¦ (π Β· π΄)) & β’ (π β π΄ β π΅) β β’ (π β π΄ β ran πΉ) | ||
Theorem | cycsubgcl 18874* | The set of integer powers of an element π΄ of a group forms a subgroup containing π΄, called the cyclic group generated by the element π΄. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π₯ β β€ β¦ (π₯ Β· π΄)) β β’ ((πΊ β Grp β§ π΄ β π) β (ran πΉ β (SubGrpβπΊ) β§ π΄ β ran πΉ)) | ||
Theorem | cycsubgss 18875* | The cyclic subgroup generated by an element π΄ is a subset of any subgroup containing π΄. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π₯ β β€ β¦ (π₯ Β· π΄)) β β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β ran πΉ β π) | ||
Theorem | cycsubg 18876* | The cyclic group generated by π΄ is the smallest subgroup containing π΄. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π₯ β β€ β¦ (π₯ Β· π΄)) β β’ ((πΊ β Grp β§ π΄ β π) β ran πΉ = β© {π β (SubGrpβπΊ) β£ π΄ β π }) | ||
Theorem | cycsubgcld 18877* | The cyclic subgroup generated by π΄ is a subgroup. Deduction related to cycsubgcl 18874. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π β β€ β¦ (π Β· π΄)) & β’ (π β πΊ β Grp) & β’ (π β π΄ β π΅) β β’ (π β ran πΉ β (SubGrpβπΊ)) | ||
Theorem | cycsubg2 18878* | The subgroup generated by an element is exhausted by its multiples. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π₯ β β€ β¦ (π₯ Β· π΄)) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ ((πΊ β Grp β§ π΄ β π) β (πΎβ{π΄}) = ran πΉ) | ||
Theorem | cycsubg2cl 18879 | Any multiple of an element is contained in the generated cyclic subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΎ = (mrClsβ(SubGrpβπΊ)) β β’ ((πΊ β Grp β§ π΄ β π β§ π β β€) β (π Β· π΄) β (πΎβ{π΄})) | ||
Syntax | cghm 18880 | Extend class notation with the generator of group hom-sets. |
class GrpHom | ||
Definition | df-ghm 18881* | A homomorphism of groups is a map between two structures which preserves the group operation. Requiring both sides to be groups simplifies most theorems at the cost of complicating the theorem which pushes forward a group structure. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ GrpHom = (π β Grp, π‘ β Grp β¦ {π β£ [(Baseβπ ) / π€](π:π€βΆ(Baseβπ‘) β§ βπ₯ β π€ βπ¦ β π€ (πβ(π₯(+gβπ )π¦)) = ((πβπ₯)(+gβπ‘)(πβπ¦)))}) | ||
Theorem | reldmghm 18882 | Lemma for group homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ Rel dom GrpHom | ||
Theorem | isghm 18883* | Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ (πΉ β (π GrpHom π) β ((π β Grp β§ π β Grp) β§ (πΉ:πβΆπ β§ βπ’ β π βπ£ β π (πΉβ(π’ + π£)) = ((πΉβπ’) ⨣ (πΉβπ£))))) | ||
Theorem | isghm3 18884* | Property of a group homomorphism, similar to ismhm 18481. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ ((π β Grp β§ π β Grp) β (πΉ β (π GrpHom π) β (πΉ:πβΆπ β§ βπ’ β π βπ£ β π (πΉβ(π’ + π£)) = ((πΉβπ’) ⨣ (πΉβπ£))))) | ||
Theorem | ghmgrp1 18885 | A group homomorphism is only defined when the domain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ (πΉ β (π GrpHom π) β π β Grp) | ||
Theorem | ghmgrp2 18886 | A group homomorphism is only defined when the codomain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ (πΉ β (π GrpHom π) β π β Grp) | ||
Theorem | ghmf 18887 | A group homomorphism is a function. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) β β’ (πΉ β (π GrpHom π) β πΉ:πβΆπ) | ||
Theorem | ghmlin 18888 | A homomorphism of groups is linear. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ ((πΉ β (π GrpHom π) β§ π β π β§ π β π) β (πΉβ(π + π)) = ((πΉβπ) ⨣ (πΉβπ))) | ||
Theorem | ghmid 18889 | A homomorphism of groups preserves the identity. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (0gβπ) & β’ 0 = (0gβπ) β β’ (πΉ β (π GrpHom π) β (πΉβπ) = 0 ) | ||
Theorem | ghminv 18890 | A homomorphism of groups preserves inverses. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π΅ = (Baseβπ) & β’ π = (invgβπ) & β’ π = (invgβπ) β β’ ((πΉ β (π GrpHom π) β§ π β π΅) β (πΉβ(πβπ)) = (πβ(πΉβπ))) | ||
Theorem | ghmsub 18891 | Linearity of subtraction through a group homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ π = (-gβπ) β β’ ((πΉ β (π GrpHom π) β§ π β π΅ β§ π β π΅) β (πΉβ(π β π)) = ((πΉβπ)π(πΉβπ))) | ||
Theorem | isghmd 18892* | Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) & β’ (π β π β Grp) & β’ (π β π β Grp) & β’ (π β πΉ:πβΆπ) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) ⨣ (πΉβπ¦))) β β’ (π β πΉ β (π GrpHom π)) | ||
Theorem | ghmmhm 18893 | A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ (πΉ β (π GrpHom π) β πΉ β (π MndHom π)) | ||
Theorem | ghmmhmb 18894 | Group homomorphisms and monoid homomorphisms coincide. (Thus, GrpHom is somewhat redundant, although its stronger reverse closure properties are sometimes useful.) (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ ((π β Grp β§ π β Grp) β (π GrpHom π) = (π MndHom π)) | ||
Theorem | ghmmulg 18895 | A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ Γ = (.gβπ») β β’ ((πΉ β (πΊ GrpHom π») β§ π β β€ β§ π β π΅) β (πΉβ(π Β· π)) = (π Γ (πΉβπ))) | ||
Theorem | ghmrn 18896 | The range of a homomorphism is a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ (πΉ β (π GrpHom π) β ran πΉ β (SubGrpβπ)) | ||
Theorem | 0ghm 18897 | The constant zero linear function between two groups. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) β β’ ((π β Grp β§ π β Grp) β (π΅ Γ { 0 }) β (π GrpHom π)) | ||
Theorem | idghm 18898 | The identity homomorphism on a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β ( I βΎ π΅) β (πΊ GrpHom πΊ)) | ||
Theorem | resghm 18899 | Restriction of a homomorphism to a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π GrpHom π) β§ π β (SubGrpβπ)) β (πΉ βΎ π) β (π GrpHom π)) | ||
Theorem | resghm2 18900 | One direction of resghm2b 18901. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π GrpHom π) β§ π β (SubGrpβπ)) β πΉ β (π GrpHom π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |