![]() |
Metamath
Proof Explorer Theorem List (p. 192 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | quseccl0 19101 | Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) Generalization of quseccl 19103 for arbitrary sets πΊ. (Revised by AV, 24-Feb-2025.) |
β’ βΌ = (πΊ ~QG π) & β’ π» = (πΊ /s βΌ ) & β’ πΆ = (BaseβπΊ) & β’ π΅ = (Baseβπ») β β’ ((πΊ β π β§ π β πΆ) β [π] βΌ β π΅) | ||
Theorem | qusgrp 19102 | 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 19103 | Closure of the quotient map for a quotient group. (Contributed by Mario Carneiro, 18-Sep-2015.) (Proof shortened by AV, 9-Mar-2025.) |
β’ π» = (πΊ /s (πΊ ~QG π)) & β’ π = (BaseβπΊ) & β’ π΅ = (Baseβπ») β β’ ((π β (NrmSGrpβπΊ) β§ π β π) β [π](πΊ ~QG π) β π΅) | ||
Theorem | qusadd 19104 | 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 19105 | 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 19106 | 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 19107 | 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 | ecqusaddd 19108 | Addition of equivalence classes in a quotient group. (Contributed by AV, 25-Feb-2025.) |
β’ (π β πΌ β (NrmSGrpβπ )) & β’ π΅ = (Baseβπ ) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) β β’ ((π β§ (π΄ β π΅ β§ πΆ β π΅)) β [(π΄(+gβπ )πΆ)] βΌ = ([π΄] βΌ (+gβπ)[πΆ] βΌ )) | ||
Theorem | ecqusaddcl 19109 | Closure of the addition in a quotient group. (Contributed by AV, 24-Feb-2025.) |
β’ (π β πΌ β (NrmSGrpβπ )) & β’ π΅ = (Baseβπ ) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) β β’ ((π β§ (π΄ β π΅ β§ πΆ β π΅)) β ([π΄] βΌ (+gβπ)[πΆ] βΌ ) β (Baseβπ)) | ||
Theorem | lagsubg2 19110 | 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 19111 | 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) β (β―βπ) β₯ (β―βπ)) | ||
Theorem | eqg0subg 19112 | The coset equivalence relation for the trivial (zero) subgroup of a group is the identity relation restricted to the base set of the group. (Contributed by AV, 25-Feb-2025.) |
β’ 0 = (0gβπΊ) & β’ π = { 0 } & β’ π΅ = (BaseβπΊ) & β’ π = (πΊ ~QG π) β β’ (πΊ β Grp β π = ( I βΎ π΅)) | ||
Theorem | eqg0subgecsn 19113 | The equivalence classes modulo the coset equivalence relation for the trivial (zero) subgroup of a group are singletons. (Contributed by AV, 26-Feb-2025.) |
β’ 0 = (0gβπΊ) & β’ π = { 0 } & β’ π΅ = (BaseβπΊ) & β’ π = (πΊ ~QG π) β β’ ((πΊ β Grp β§ π β π΅) β [π]π = {π}) | ||
Theorem | qus0subgbas 19114* | The base set of a quotient of a group by the trivial (zero) subgroup. (Contributed by AV, 26-Feb-2025.) |
β’ 0 = (0gβπΊ) & β’ π = { 0 } & β’ βΌ = (πΊ ~QG π) & β’ π = (πΊ /s βΌ ) & β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β (Baseβπ) = {π’ β£ βπ₯ β π΅ π’ = {π₯}}) | ||
Theorem | qus0subgadd 19115* | The addition in a quotient of a group by the trivial (zero) subgroup. (Contributed by AV, 26-Feb-2025.) |
β’ 0 = (0gβπΊ) & β’ π = { 0 } & β’ βΌ = (πΊ ~QG π) & β’ π = (πΊ /s βΌ ) & β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β βπ β π΅ βπ β π΅ ({π} (+gβπ){π}) = {(π(+gβπΊ)π)}) | ||
This section contains some preliminary results about cyclic monoids and groups before the class CycGrp of cyclic groups (see df-cyg 19788) is defined in the context of Abelian groups. | ||
Theorem | cycsubmel 19116* | 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 19117* | 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 19118* | The set of nonnegative integer powers of an element π΄ of a monoid forms a submonoid containing π΄ (see cycsubmcl 19117), 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 19119* | Condition for an operation to be commutative. Lemma for cycsubmcom 19120 and cygabl 19801. Formerly part of proof for cygabl 19801. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 20-Jan-2024.) |
β’ (π β βπ β πΆ βπ₯ β π π = (π₯ Β· π΄)) & β’ (π β βπ β π βπ β π ((π + π) Β· π΄) = ((π Β· π΄) + (π Β· π΄))) & β’ (π β π β πΆ) & β’ (π β π β πΆ) & β’ (π β π β β) β β’ (π β (π + π) = (π + π)) | ||
Theorem | cycsubmcom 19120* | 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 19121* | 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 19122* | 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 19123* | 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 19124* | The cyclic group generated by π΄ is the smallest subgroup containing π΄. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π₯ β β€ β¦ (π₯ Β· π΄)) β β’ ((πΊ β Grp β§ π΄ β π) β ran πΉ = β© {π β (SubGrpβπΊ) β£ π΄ β π }) | ||
Theorem | cycsubgcld 19125* | The cyclic subgroup generated by π΄ is a subgroup. Deduction related to cycsubgcl 19122. (Contributed by Rohan Ridenour, 3-Aug-2023.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ πΉ = (π β β€ β¦ (π Β· π΄)) & β’ (π β πΊ β Grp) & β’ (π β π΄ β π΅) β β’ (π β ran πΉ β (SubGrpβπΊ)) | ||
Theorem | cycsubg2 19126* | 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 19127 | 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 19128 | Extend class notation with the generator of group hom-sets. |
class GrpHom | ||
Definition | df-ghm 19129* | 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 19130 | Lemma for group homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ Rel dom GrpHom | ||
Theorem | isghm 19131* | Property of being a homomorphism of groups. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ (πΉ β (π GrpHom π) β ((π β Grp β§ π β Grp) β§ (πΉ:πβΆπ β§ βπ’ β π βπ£ β π (πΉβ(π’ + π£)) = ((πΉβπ’) ⨣ (πΉβπ£))))) | ||
Theorem | isghm3 19132* | Property of a group homomorphism, similar to ismhm 18708. (Contributed by Mario Carneiro, 7-Mar-2015.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ ((π β Grp β§ π β Grp) β (πΉ β (π GrpHom π) β (πΉ:πβΆπ β§ βπ’ β π βπ£ β π (πΉβ(π’ + π£)) = ((πΉβπ’) ⨣ (πΉβπ£))))) | ||
Theorem | ghmgrp1 19133 | A group homomorphism is only defined when the domain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ (πΉ β (π GrpHom π) β π β Grp) | ||
Theorem | ghmgrp2 19134 | A group homomorphism is only defined when the codomain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ (πΉ β (π GrpHom π) β π β Grp) | ||
Theorem | ghmf 19135 | A group homomorphism is a function. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) β β’ (πΉ β (π GrpHom π) β πΉ:πβΆπ) | ||
Theorem | ghmlin 19136 | A homomorphism of groups is linear. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) β β’ ((πΉ β (π GrpHom π) β§ π β π β§ π β π) β (πΉβ(π + π)) = ((πΉβπ) ⨣ (πΉβπ))) | ||
Theorem | ghmid 19137 | A homomorphism of groups preserves the identity. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (0gβπ) & β’ 0 = (0gβπ) β β’ (πΉ β (π GrpHom π) β (πΉβπ) = 0 ) | ||
Theorem | ghminv 19138 | A homomorphism of groups preserves inverses. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π΅ = (Baseβπ) & β’ π = (invgβπ) & β’ π = (invgβπ) β β’ ((πΉ β (π GrpHom π) β§ π β π΅) β (πΉβ(πβπ)) = (πβ(πΉβπ))) | ||
Theorem | ghmsub 19139 | Linearity of subtraction through a group homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π΅ = (Baseβπ) & β’ β = (-gβπ) & β’ π = (-gβπ) β β’ ((πΉ β (π GrpHom π) β§ π β π΅ β§ π β π΅) β (πΉβ(π β π)) = ((πΉβπ)π(πΉβπ))) | ||
Theorem | isghmd 19140* | Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ) & β’ (π β π β Grp) & β’ (π β π β Grp) & β’ (π β πΉ:πβΆπ) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (πΉβ(π₯ + π¦)) = ((πΉβπ₯) ⨣ (πΉβπ¦))) β β’ (π β πΉ β (π GrpHom π)) | ||
Theorem | ghmmhm 19141 | A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
β’ (πΉ β (π GrpHom π) β πΉ β (π MndHom π)) | ||
Theorem | ghmmhmb 19142 | 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 19143 | A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ Γ = (.gβπ») β β’ ((πΉ β (πΊ GrpHom π») β§ π β β€ β§ π β π΅) β (πΉβ(π Β· π)) = (π Γ (πΉβπ))) | ||
Theorem | ghmrn 19144 | The range of a homomorphism is a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ (πΉ β (π GrpHom π) β ran πΉ β (SubGrpβπ)) | ||
Theorem | 0ghm 19145 | 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 19146 | The identity homomorphism on a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β ( I βΎ π΅) β (πΊ GrpHom πΊ)) | ||
Theorem | resghm 19147 | Restriction of a homomorphism to a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π GrpHom π) β§ π β (SubGrpβπ)) β (πΉ βΎ π) β (π GrpHom π)) | ||
Theorem | resghm2 19148 | One direction of resghm2b 19149. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.) |
β’ π = (π βΎs π) β β’ ((πΉ β (π GrpHom π) β§ π β (SubGrpβπ)) β πΉ β (π GrpHom π)) | ||
Theorem | resghm2b 19149 | 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 19150 | 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 19151 | The composition of group homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
β’ ((πΉ β (π GrpHom π) β§ πΊ β (π GrpHom π)) β (πΉ β πΊ) β (π GrpHom π)) | ||
Theorem | ghmima 19152 | The image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ ((πΉ β (π GrpHom π) β§ π β (SubGrpβπ)) β (πΉ β π) β (SubGrpβπ)) | ||
Theorem | ghmpreima 19153 | The inverse image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
β’ ((πΉ β (π GrpHom π) β§ π β (SubGrpβπ)) β (β‘πΉ β π) β (SubGrpβπ)) | ||
Theorem | ghmeql 19154 | 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 19155 | 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 19156 | The inverse image of a normal subgroup under a homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ ((πΉ β (π GrpHom π) β§ π β (NrmSGrpβπ)) β (β‘πΉ β π) β (NrmSGrpβπ)) | ||
Theorem | ghmker 19157 | The kernel of a homomorphism is a normal subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.) |
β’ 0 = (0gβπ) β β’ (πΉ β (π GrpHom π) β (β‘πΉ β { 0 }) β (NrmSGrpβπ)) | ||
Theorem | ghmeqker 19158 | 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 19159* | Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ π = (π βs πΌ) & β’ π΅ = (Baseβπ ) & β’ πΉ = (π₯ β π΅ β¦ (πΌ Γ {π₯})) β β’ ((π β Grp β§ πΌ β π) β πΉ β (π GrpHom π)) | ||
Theorem | f1ghm0to0 19160 | If a group homomorphism πΉ is injective, it maps the zero of one group (and only the zero) to the zero of the other group. (Contributed by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 13-May-2023.) |
β’ π΄ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ ) & β’ 0 = (0gβπ) β β’ ((πΉ β (π GrpHom π) β§ πΉ:π΄β1-1βπ΅ β§ π β π΄) β ((πΉβπ) = 0 β π = π)) | ||
Theorem | ghmf1 19161* | 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.) (Proof shortened by AV, 4-Apr-2025.) |
β’ π΄ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ ) & β’ 0 = (0gβπ) β β’ (πΉ β (π GrpHom π) β (πΉ:π΄β1-1βπ΅ β βπ₯ β π΄ ((πΉβπ₯) = 0 β π₯ = π))) | ||
Theorem | kerf1ghm 19162 | A group homomorphism πΉ is injective if and only if its kernel is the singleton {π}. (Contributed by Thierry Arnoux, 27-Oct-2017.) (Proof shortened by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 13-May-2023.) |
β’ π΄ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ ) & β’ 0 = (0gβπ) β β’ (πΉ β (π GrpHom π) β (πΉ:π΄β1-1βπ΅ β (β‘πΉ β { 0 }) = {π})) | ||
Theorem | ghmf1o 19163 | A bijective group homomorphism is an isomorphism. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ π = (Baseβπ) & β’ π = (Baseβπ) β β’ (πΉ β (π GrpHom π) β (πΉ:πβ1-1-ontoβπ β β‘πΉ β (π GrpHom π))) | ||
Theorem | conjghm 19164* | Conjugation is an automorphism of the group. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ πΉ = (π₯ β π β¦ ((π΄ + π₯) β π΄)) β β’ ((πΊ β Grp β§ π΄ β π) β (πΉ β (πΊ GrpHom πΊ) β§ πΉ:πβ1-1-ontoβπ)) | ||
Theorem | conjsubg 19165* | A conjugated subgroup is also a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ πΉ = (π₯ β π β¦ ((π΄ + π₯) β π΄)) β β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β ran πΉ β (SubGrpβπΊ)) | ||
Theorem | conjsubgen 19166* | A conjugated subgroup is equinumerous to the original subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ πΉ = (π₯ β π β¦ ((π΄ + π₯) β π΄)) β β’ ((π β (SubGrpβπΊ) β§ π΄ β π) β π β ran πΉ) | ||
Theorem | conjnmz 19167* | 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 19168* | Alternative condition for elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ πΉ = (π₯ β π β¦ ((π΄ + π₯) β π΄)) & β’ π = {π¦ β π β£ βπ§ β π ((π¦ + π§) β π β (π§ + π¦) β π)} β β’ (π β (SubGrpβπΊ) β (π΄ β π β (π΄ β π β§ π = ran πΉ))) | ||
Theorem | conjnsg 19169* | A normal subgroup is unchanged under conjugation. (Contributed by Mario Carneiro, 18-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (-gβπΊ) & β’ πΉ = (π₯ β π β¦ ((π΄ + π₯) β π΄)) β β’ ((π β (NrmSGrpβπΊ) β§ π΄ β π) β π = ran πΉ) | ||
Theorem | qusghm 19170* | 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 19171* | 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 19172 | The class of group isomorphism sets. |
class GrpIso | ||
Syntax | cgic 19173 | The class of the group isomorphism relation. |
class βπ | ||
Definition | df-gim 19174* | 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 19175 | 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 19176 | The group isomorphism function is a well-defined function. (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ GrpIso Fn (Grp Γ Grp) | ||
Theorem | isgim 19177 | 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 19178 | 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 19179 | 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 19180 | A group isomorphism is a homomorphism whose converse is also a homomorphism. Characterization of isomorphisms similar to ishmeo 23484. (Contributed by Mario Carneiro, 6-May-2015.) |
β’ (πΉ β (π GrpIso π) β (πΉ β (π GrpHom π) β§ β‘πΉ β (π GrpHom π ))) | ||
Theorem | subggim 19181 | Behavior of subgroups under isomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
β’ π΅ = (Baseβπ ) β β’ ((πΉ β (π GrpIso π) β§ π΄ β π΅) β (π΄ β (SubGrpβπ ) β (πΉ β π΄) β (SubGrpβπ))) | ||
Theorem | gimcnv 19182 | 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 19183 | The composition of group isomorphisms is a group isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ ((πΉ β (π GrpIso π) β§ πΊ β (π GrpIso π)) β (πΉ β πΊ) β (π GrpIso π)) | ||
Theorem | gim0to0 19184 | A group isomorphism maps the zero of one group (and only the zero) to the zero of the other group. (Contributed by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 23-May-2023.) |
β’ π΄ = (Baseβπ ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ 0 = (0gβπ ) β β’ ((πΉ β (π GrpIso π) β§ π β π΄) β ((πΉβπ) = π β π = 0 )) | ||
Theorem | brgic 19185 | The relation "is isomorphic to" for groups. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β (π GrpIso π) β β ) | ||
Theorem | brgici 19186 | Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (πΉ β (π GrpIso π) β π βπ π) | ||
Theorem | gicref 19187 | Isomorphism is reflexive. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ (π β Grp β π βπ π ) | ||
Theorem | giclcl 19188 | Isomorphism implies the left side is a group. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β π β Grp) | ||
Theorem | gicrcl 19189 | Isomorphism implies the right side is a group. (Contributed by Mario Carneiro, 6-May-2015.) |
β’ (π βπ π β π β Grp) | ||
Theorem | gicsym 19190 | Isomorphism is symmetric. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ (π βπ π β π βπ π ) | ||
Theorem | gictr 19191 | Isomorphism is transitive. (Contributed by Mario Carneiro, 21-Apr-2016.) |
β’ ((π βπ π β§ π βπ π) β π βπ π) | ||
Theorem | gicer 19192 | 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 19193 | Isomorphic groups have equinumerous base sets. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ π΅ = (Baseβπ ) & β’ πΆ = (Baseβπ) β β’ (π βπ π β π΅ β πΆ) | ||
Theorem | gicsubgen 19194 | A less trivial example of a group invariant: cardinality of the subgroup lattice. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ (π βπ π β (SubGrpβπ ) β (SubGrpβπ)) | ||
Syntax | cga 19195 | Extend class definition to include the class of group actions. |
class GrpAct | ||
Definition | df-ga 19196* | Define the class of all group actions. A group πΊ acts on a set π if a permutation on π is associated with every element of πΊ in such a way that the identity permutation on π is associated with the neutral element of πΊ, and the composition of the permutations associated with two elements of πΊ is identical with the permutation associated with the composition of these two elements (in the same order) in the group πΊ. (Contributed by Jeff Hankins, 10-Aug-2009.) |
β’ GrpAct = (π β Grp, π β V β¦ β¦(Baseβπ) / πβ¦{π β (π βm (π Γ π )) β£ βπ₯ β π (((0gβπ)ππ₯) = π₯ β§ βπ¦ β π βπ§ β π ((π¦(+gβπ)π§)ππ₯) = (π¦π(π§ππ₯)))}) | ||
Theorem | isga 19197* | The predicate "is a (left) group action". The group πΊ is said to act on the base set π of the action, which is not assumed to have any special properties. There is a related notion of right group action, but as the Wikipedia article explains, it is not mathematically interesting. The way actions are usually thought of is that each element π of πΊ is a permutation of the elements of π (see gapm 19212). Since group theory was classically about symmetry groups, it is therefore likely that the notion of group action was useful even in early group theory. (Contributed by Jeff Hankins, 10-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ 0 = (0gβπΊ) β β’ ( β β (πΊ GrpAct π) β ((πΊ β Grp β§ π β V) β§ ( β :(π Γ π)βΆπ β§ βπ₯ β π (( 0 β π₯) = π₯ β§ βπ¦ β π βπ§ β π ((π¦ + π§) β π₯) = (π¦ β (π§ β π₯)))))) | ||
Theorem | gagrp 19198 | The left argument of a group action is a group. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ ( β β (πΊ GrpAct π) β πΊ β Grp) | ||
Theorem | gaset 19199 | The right argument of a group action is a set. (Contributed by Mario Carneiro, 30-Apr-2015.) |
β’ ( β β (πΊ GrpAct π) β π β V) | ||
Theorem | gagrpid 19200 | The identity of the group does not alter the base set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
β’ 0 = (0gβπΊ) β β’ (( β β (πΊ GrpAct π) β§ π΄ β π) β ( 0 β π΄) = π΄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |