Home | Metamath
Proof Explorer Theorem List (p. 190 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isnsg4 18901* | A subgroup is normal iff its normalizer is the entire group. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = {π₯ β π β£ βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π)} & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) β β’ (π β (NrmSGrpβπΊ) β (π β (SubGrpβπΊ) β§ π = π)) | ||
Theorem | nmznsg 18902* | Any subgroup is a normal subgroup of its normalizer. (Contributed by Mario Carneiro, 19-Jan-2015.) |
β’ π = {π₯ β π β£ βπ¦ β π ((π₯ + π¦) β π β (π¦ + π₯) β π)} & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π» = (πΊ βΎs π) β β’ (π β (SubGrpβπΊ) β π β (NrmSGrpβπ»)) | ||
Theorem | 0nsg 18903 | The zero subgroup is normal. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ 0 = (0gβπΊ) β β’ (πΊ β Grp β { 0 } β (NrmSGrpβπΊ)) | ||
Theorem | nsgid 18904 | The whole group is a normal subgroup of itself. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β π΅ β (NrmSGrpβπΊ)) | ||
Theorem | 0idnsgd 18905 | 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 18906 | 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 18907 | A trivial group has exactly one normal subgroup. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ (π β πΊ β Grp) & β’ (π β π΅ = { 0 }) β β’ (π β (NrmSGrpβπΊ) β 1o) | ||
Theorem | 1nsgtrivd 18908 | 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 18909 | The left coset equivalence relation is a relation. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π = (πΊ ~QG π) β β’ Rel π | ||
Theorem | eqgfval 18910* | Value of the subgroup left coset equivalence relation. (Contributed by Mario Carneiro, 15-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ π = (invgβπΊ) & β’ + = (+gβπΊ) & β’ π = (πΊ ~QG π) β β’ ((πΊ β π β§ π β π) β π = {β¨π₯, π¦β© β£ ({π₯, π¦} β π β§ ((πβπ₯) + π¦) β π)}) | ||
Theorem | eqgval 18911 | 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 18912 | The subgroup coset equivalence relation is an equivalence relation. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ βΌ = (πΊ ~QG π) β β’ (π β (SubGrpβπΊ) β βΌ Er π) | ||
Theorem | eqglact 18913* | 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 18914 | 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 18915 | 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 18916 | 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 18917 | 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 18918 | Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) & β’ π = (BaseβπΊ) & β’ π΅ = (Baseβπ») β β’ ((π β (NrmSGrpβπΊ) β§ π β π) β [π](πΊ ~QG π) β π΅) | ||
Theorem | qusadd 18919 | 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 18920 | 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 18921 | 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 18922 | 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 18923 | 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 18924 | 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 19584) is defined in the context of Abelian groups. | ||
Theorem | cycsubmel 18925* | 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 18926* | 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 18927* | The set of nonnegative integer powers of an element π΄ of a monoid forms a submonoid containing π΄ (see cycsubmcl 18926), 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 18928* | Condition for an operation to be commutative. Lemma for cycsubmcom 18929 and cygabl 19597. Formerly part of proof for cygabl 19597. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 20-Jan-2024.) |
β’ (π β βπ β πΆ βπ₯ β π π = (π₯ Β· π΄)) & β’ (π β βπ β π βπ β π ((π + π) Β· π΄) = ((π Β· π΄) + (π Β· π΄))) & β’ (π β π β πΆ) & β’ (π β π β πΆ) & β’ (π β π β β) β β’ (π β (π + π) = (π + π)) | ||
Theorem | cycsubmcom 18929* | 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 18930* | 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 18931* | 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 18932* | 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 18933* | The cyclic group generated by π΄ is the smallest subgroup containing π΄. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π₯ β β€ β¦ (π₯ Β· π΄)) β β’ ((πΊ β Grp β§ π΄ β π) β ran πΉ = β© {π β (SubGrpβπΊ) β£ π΄ β π }) | ||
Theorem | cycsubgcld 18934* | The cyclic subgroup generated by π΄ is a subgroup. Deduction related to cycsubgcl 18931. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π β β€ β¦ (π Β· π΄)) & β’ (π β πΊ β Grp) & β’ (π β π΄ β π΅) β β’ (π β ran πΉ β (SubGrpβπΊ)) | ||
Theorem | cycsubg2 18935* | 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 18936 | 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 18937 | Extend class notation with the generator of group hom-sets. |
class GrpHom | ||
Definition | df-ghm 18938* | 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 18939 | Lemma for group homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ Rel dom GrpHom | ||
Theorem | isghm 18940* | Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ (πΉ β (π GrpHom π) β ((π β Grp β§ π β Grp) β§ (πΉ:πβΆπ β§ βπ’ β π βπ£ β π (πΉβ(π’ + π£)) = ((πΉβπ’) ⨣ (πΉβπ£))))) | ||
Theorem | isghm3 18941* | Property of a group homomorphism, similar to ismhm 18538. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ ((π β Grp β§ π β Grp) β (πΉ β (π GrpHom π) β (πΉ:πβΆπ β§ βπ’ β π βπ£ β π (πΉβ(π’ + π£)) = ((πΉβπ’) ⨣ (πΉβπ£))))) | ||
Theorem | ghmgrp1 18942 | A group homomorphism is only defined when the domain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ (πΉ β (π GrpHom π) β π β Grp) | ||
Theorem | ghmgrp2 18943 | A group homomorphism is only defined when the codomain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ (πΉ β (π GrpHom π) β π β Grp) | ||
Theorem | ghmf 18944 | A group homomorphism is a function. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) β β’ (πΉ β (π GrpHom π) β πΉ:πβΆπ) | ||
Theorem | ghmlin 18945 | A homomorphism of groups is linear. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ ((πΉ β (π GrpHom π) β§ π β π β§ π β π) β (πΉβ(π + π)) = ((πΉβπ) ⨣ (πΉβπ))) | ||
Theorem | ghmid 18946 | A homomorphism of groups preserves the identity. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (0gβπ) & β’ 0 = (0gβπ) β β’ (πΉ β (π GrpHom π) β (πΉβπ) = 0 ) | ||
Theorem | ghminv 18947 | A homomorphism of groups preserves inverses. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π΅ = (Baseβπ) & β’ π = (invgβπ) & β’ π = (invgβπ) β β’ ((πΉ β (π GrpHom π) β§ π β π΅) β (πΉβ(πβπ)) = (πβ(πΉβπ))) | ||
Theorem | ghmsub 18948 | Linearity of subtraction through a group homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ π = (-gβπ) β β’ ((πΉ β (π GrpHom π) β§ π β π΅ β§ π β π΅) β (πΉβ(π β π)) = ((πΉβπ)π(πΉβπ))) | ||
Theorem | isghmd 18949* | Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) & β’ (π β π β Grp) & β’ (π β π β Grp) & β’ (π β πΉ:πβΆπ) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) ⨣ (πΉβπ¦))) β β’ (π β πΉ β (π GrpHom π)) | ||
Theorem | ghmmhm 18950 | A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ (πΉ β (π GrpHom π) β πΉ β (π MndHom π)) | ||
Theorem | ghmmhmb 18951 | 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 18952 | A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ Γ = (.gβπ») β β’ ((πΉ β (πΊ GrpHom π») β§ π β β€ β§ π β π΅) β (πΉβ(π Β· π)) = (π Γ (πΉβπ))) | ||
Theorem | ghmrn 18953 | The range of a homomorphism is a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ (πΉ β (π GrpHom π) β ran πΉ β (SubGrpβπ)) | ||
Theorem | 0ghm 18954 | 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 18955 | The identity homomorphism on a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β ( I βΎ π΅) β (πΊ GrpHom πΊ)) | ||
Theorem | resghm 18956 | Restriction of a homomorphism to a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π GrpHom π) β§ π β (SubGrpβπ)) β (πΉ βΎ π) β (π GrpHom π)) | ||
Theorem | resghm2 18957 | One direction of resghm2b 18958. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π GrpHom π) β§ π β (SubGrpβπ)) β πΉ β (π GrpHom π)) | ||
Theorem | resghm2b 18958 | Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.) |
β’ π = (π βΎs π) β β’ ((π β (SubGrpβπ) β§ ran πΉ β π) β (πΉ β (π GrpHom π) β πΉ β (π GrpHom π))) | ||
Theorem | ghmghmrn 18959 | A group homomorphism from πΊ to π» is also a group homomorphism from πΊ to its image in π». (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by AV, 26-Aug-2021.) |
β’ π = (π βΎs ran πΉ) β β’ (πΉ β (π GrpHom π) β πΉ β (π GrpHom π)) | ||
Theorem | ghmco 18960 | The composition of group homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ ((πΉ β (π GrpHom π) β§ πΊ β (π GrpHom π)) β (πΉ β πΊ) β (π GrpHom π)) | ||
Theorem | ghmima 18961 | The image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ ((πΉ β (π GrpHom π) β§ π β (SubGrpβπ)) β (πΉ β π) β (SubGrpβπ)) | ||
Theorem | ghmpreima 18962 | The inverse image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ ((πΉ β (π GrpHom π) β§ π β (SubGrpβπ)) β (β‘πΉ β π) β (SubGrpβπ)) | ||
Theorem | ghmeql 18963 | The equalizer of two group homomorphisms is a subgroup. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ ((πΉ β (π GrpHom π) β§ πΊ β (π GrpHom π)) β dom (πΉ β© πΊ) β (SubGrpβπ)) | ||
Theorem | ghmnsgima 18964 | The image of a normal subgroup under a surjective homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ π = (Baseβπ) β β’ ((πΉ β (π GrpHom π) β§ π β (NrmSGrpβπ) β§ ran πΉ = π) β (πΉ β π) β (NrmSGrpβπ)) | ||
Theorem | ghmnsgpreima 18965 | The inverse image of a normal subgroup under a homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ ((πΉ β (π GrpHom π) β§ π β (NrmSGrpβπ)) β (β‘πΉ β π) β (NrmSGrpβπ)) | ||
Theorem | ghmker 18966 | The kernel of a homomorphism is a normal subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ 0 = (0gβπ) β β’ (πΉ β (π GrpHom π) β (β‘πΉ β { 0 }) β (NrmSGrpβπ)) | ||
Theorem | ghmeqker 18967 | Two source points map to the same destination point under a group homomorphism iff their difference belongs to the kernel. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΎ = (β‘πΉ β { 0 }) & β’ β = (-gβπ) β β’ ((πΉ β (π GrpHom π) β§ π β π΅ β§ π β π΅) β ((πΉβπ) = (πΉβπ) β (π β π) β πΎ)) | ||
Theorem | pwsdiagghm 18968* | Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ πΉ = (π₯ β π΅ β¦ (πΌ Γ {π₯})) β β’ ((π β Grp β§ πΌ β π) β πΉ β (π GrpHom π)) | ||
Theorem | ghmf1 18969* | Two ways of saying a group homomorphism is 1-1 into its codomain. (Contributed by Paul Chapman, 3-Mar-2008.) (Revised by Mario Carneiro, 13-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (0gβπ) β β’ (πΉ β (π GrpHom π) β (πΉ:πβ1-1βπ β βπ₯ β π ((πΉβπ₯) = π β π₯ = 0 ))) | ||
Theorem | ghmf1o 18970 | A bijective group homomorphism is an isomorphism. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) β β’ (πΉ β (π GrpHom π) β (πΉ:πβ1-1-ontoβπ β β‘πΉ β (π GrpHom π))) | ||
Theorem | conjghm 18971* | Conjugation is an automorphism of the group. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ πΉ = (π₯ β π β¦ ((π΄ + π₯) β π΄)) β β’ ((πΊ β Grp β§ π΄ β π) β (πΉ β (πΊ GrpHom πΊ) β§ πΉ:πβ1-1-ontoβπ)) | ||
Theorem | conjsubg 18972* | A conjugated subgroup is also a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ πΉ = (π₯ β π β¦ ((π΄ + π₯) β π΄)) β β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β ran πΉ β (SubGrpβπΊ)) | ||
Theorem | conjsubgen 18973* | A conjugated subgroup is equinumerous to the original subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ πΉ = (π₯ β π β¦ ((π΄ + π₯) β π΄)) β β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β π β ran πΉ) | ||
Theorem | conjnmz 18974* | A subgroup is unchanged under conjugation by an element of its normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ πΉ = (π₯ β π β¦ ((π΄ + π₯) β π΄)) & β’ π = {π¦ β π β£ βπ§ β π ((π¦ + π§) β π β (π§ + π¦) β π)} β β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β π = ran πΉ) | ||
Theorem | conjnmzb 18975* | Alternative condition for elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ πΉ = (π₯ β π β¦ ((π΄ + π₯) β π΄)) & β’ π = {π¦ β π β£ βπ§ β π ((π¦ + π§) β π β (π§ + π¦) β π)} β β’ (π β (SubGrpβπΊ) β (π΄ β π β (π΄ β π β§ π = ran πΉ))) | ||
Theorem | conjnsg 18976* | A normal subgroup is unchanged under conjugation. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ πΉ = (π₯ β π β¦ ((π΄ + π₯) β π΄)) β β’ ((π β (NrmSGrpβπΊ) β§ π΄ β π) β π = ran πΉ) | ||
Theorem | qusghm 18977* | If π is a normal subgroup of πΊ, then the "natural map" from elements to their cosets is a group homomorphism from πΊ to πΊ / π. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by Mario Carneiro, 18-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ π» = (πΊ /s (πΊ ~QG π)) & β’ πΉ = (π₯ β π β¦ [π₯](πΊ ~QG π)) β β’ (π β (NrmSGrpβπΊ) β πΉ β (πΊ GrpHom π»)) | ||
Theorem | ghmpropd 18978* | Group homomorphism depends only on the group attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ (π β π΅ = (Baseβπ½)) & β’ (π β πΆ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β πΆ = (Baseβπ)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ½)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπ)π¦)) β β’ (π β (π½ GrpHom πΎ) = (πΏ GrpHom π)) | ||
Syntax | cgim 18979 | The class of group isomorphism sets. |
class GrpIso | ||
Syntax | cgic 18980 | The class of the group isomorphism relation. |
class βπ | ||
Definition | df-gim 18981* | An isomorphism of groups is a homomorphism which is also a bijection, i.e. it preserves equality as well as the group operation. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
β’ GrpIso = (π β Grp, π‘ β Grp β¦ {π β (π GrpHom π‘) β£ π:(Baseβπ )β1-1-ontoβ(Baseβπ‘)}) | ||
Definition | df-gic 18982 | Two groups are said to be isomorphic iff they are connected by at least one isomorphism. Isomorphic groups share all global group properties, but to relate local properties requires knowledge of a specific isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ βπ = (β‘ GrpIso β (V β 1o)) | ||
Theorem | gimfn 18983 | The group isomorphism function is a well-defined function. (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ GrpIso Fn (Grp Γ Grp) | ||
Theorem | isgim 18984 | An isomorphism of groups is a bijective homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π GrpIso π) β (πΉ β (π GrpHom π) β§ πΉ:π΅β1-1-ontoβπΆ)) | ||
Theorem | gimf1o 18985 | An isomorphism of groups is a bijection. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (πΉ β (π GrpIso π) β πΉ:π΅β1-1-ontoβπΆ) | ||
Theorem | gimghm 18986 | An isomorphism of groups is a homomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ (πΉ β (π GrpIso π) β πΉ β (π GrpHom π)) | ||
Theorem | isgim2 18987 | A group isomorphism is a homomorphism whose converse is also a homomorphism. Characterization of isomorphisms similar to ishmeo 23032. (Contributed by Mario Carneiro, 6-May-2015.) |
β’ (πΉ β (π GrpIso π) β (πΉ β (π GrpHom π) β§ β‘πΉ β (π GrpHom π ))) | ||
Theorem | subggim 18988 | Behavior of subgroups under isomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
β’ π΅ = (Baseβπ ) β β’ ((πΉ β (π GrpIso π) β§ π΄ β π΅) β (π΄ β (SubGrpβπ ) β (πΉ β π΄) β (SubGrpβπ))) | ||
Theorem | gimcnv 18989 | The converse of a bijective group homomorphism is a bijective group homomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ (πΉ β (π GrpIso π) β β‘πΉ β (π GrpIso π)) | ||
Theorem | gimco 18990 | The composition of group isomorphisms is a group isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ ((πΉ β (π GrpIso π) β§ πΊ β (π GrpIso π)) β (πΉ β πΊ) β (π GrpIso π)) | ||
Theorem | brgic 18991 | The relation "is isomorphic to" for groups. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β (π GrpIso π) β β ) | ||
Theorem | brgici 18992 | Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ β (π GrpIso π) β π βπ π) | ||
Theorem | gicref 18993 | Isomorphism is reflexive. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ (π β Grp β π βπ π ) | ||
Theorem | giclcl 18994 | Isomorphism implies the left side is a group. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β π β Grp) | ||
Theorem | gicrcl 18995 | Isomorphism implies the right side is a group. (Contributed by Mario Carneiro, 6-May-2015.) |
β’ (π βπ π β π β Grp) | ||
Theorem | gicsym 18996 | Isomorphism is symmetric. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ (π βπ π β π βπ π ) | ||
Theorem | gictr 18997 | Isomorphism is transitive. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ ((π βπ π β§ π βπ π) β π βπ π) | ||
Theorem | gicer 18998 | Isomorphism is an equivalence relation on groups. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 1-May-2021.) |
β’ βπ Er Grp | ||
Theorem | gicen 18999 | Isomorphic groups have equinumerous base sets. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (π βπ π β π΅ β πΆ) | ||
Theorem | gicsubgen 19000 | A less trivial example of a group invariant: cardinality of the subgroup lattice. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β (SubGrpβπ ) β (SubGrpβπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |