![]() |
Metamath
Proof Explorer Theorem List (p. 192 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | isghmd 19101* | Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015.) |
โข ๐ = (Baseโ๐) & โข ๐ = (Baseโ๐) & โข + = (+gโ๐) & โข โจฃ = (+gโ๐) & โข (๐ โ ๐ โ Grp) & โข (๐ โ ๐ โ Grp) & โข (๐ โ ๐น:๐โถ๐) & โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (๐นโ(๐ฅ + ๐ฆ)) = ((๐นโ๐ฅ) โจฃ (๐นโ๐ฆ))) โ โข (๐ โ ๐น โ (๐ GrpHom ๐)) | ||
Theorem | ghmmhm 19102 | A group homomorphism is a monoid homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.) |
โข (๐น โ (๐ GrpHom ๐) โ ๐น โ (๐ MndHom ๐)) | ||
Theorem | ghmmhmb 19103 | 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 19104 | A homomorphism of monoids preserves group multiples. (Contributed by Mario Carneiro, 14-Jun-2015.) |
โข ๐ต = (Baseโ๐บ) & โข ยท = (.gโ๐บ) & โข ร = (.gโ๐ป) โ โข ((๐น โ (๐บ GrpHom ๐ป) โง ๐ โ โค โง ๐ โ ๐ต) โ (๐นโ(๐ ยท ๐)) = (๐ ร (๐นโ๐))) | ||
Theorem | ghmrn 19105 | The range of a homomorphism is a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
โข (๐น โ (๐ GrpHom ๐) โ ran ๐น โ (SubGrpโ๐)) | ||
Theorem | 0ghm 19106 | 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 19107 | The identity homomorphism on a group. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
โข ๐ต = (Baseโ๐บ) โ โข (๐บ โ Grp โ ( I โพ ๐ต) โ (๐บ GrpHom ๐บ)) | ||
Theorem | resghm 19108 | Restriction of a homomorphism to a subgroup. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
โข ๐ = (๐ โพs ๐) โ โข ((๐น โ (๐ GrpHom ๐) โง ๐ โ (SubGrpโ๐)) โ (๐น โพ ๐) โ (๐ GrpHom ๐)) | ||
Theorem | resghm2 19109 | One direction of resghm2b 19110. (Contributed by Mario Carneiro, 13-Jan-2015.) (Revised by Mario Carneiro, 18-Jun-2015.) |
โข ๐ = (๐ โพs ๐) โ โข ((๐น โ (๐ GrpHom ๐) โง ๐ โ (SubGrpโ๐)) โ ๐น โ (๐ GrpHom ๐)) | ||
Theorem | resghm2b 19110 | 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 19111 | 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 19112 | The composition of group homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.) |
โข ((๐น โ (๐ GrpHom ๐) โง ๐บ โ (๐ GrpHom ๐)) โ (๐น โ ๐บ) โ (๐ GrpHom ๐)) | ||
Theorem | ghmima 19113 | The image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
โข ((๐น โ (๐ GrpHom ๐) โง ๐ โ (SubGrpโ๐)) โ (๐น โ ๐) โ (SubGrpโ๐)) | ||
Theorem | ghmpreima 19114 | The inverse image of a subgroup under a homomorphism. (Contributed by Stefan O'Rear, 31-Dec-2014.) |
โข ((๐น โ (๐ GrpHom ๐) โง ๐ โ (SubGrpโ๐)) โ (โก๐น โ ๐) โ (SubGrpโ๐)) | ||
Theorem | ghmeql 19115 | 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 19116 | 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 19117 | The inverse image of a normal subgroup under a homomorphism is normal. (Contributed by Mario Carneiro, 4-Feb-2015.) |
โข ((๐น โ (๐ GrpHom ๐) โง ๐ โ (NrmSGrpโ๐)) โ (โก๐น โ ๐) โ (NrmSGrpโ๐)) | ||
Theorem | ghmker 19118 | The kernel of a homomorphism is a normal subgroup. (Contributed by Mario Carneiro, 4-Feb-2015.) |
โข 0 = (0gโ๐) โ โข (๐น โ (๐ GrpHom ๐) โ (โก๐น โ { 0 }) โ (NrmSGrpโ๐)) | ||
Theorem | ghmeqker 19119 | 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 19120* | Diagonal homomorphism into a structure power. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
โข ๐ = (๐ โs ๐ผ) & โข ๐ต = (Baseโ๐ ) & โข ๐น = (๐ฅ โ ๐ต โฆ (๐ผ ร {๐ฅ})) โ โข ((๐ โ Grp โง ๐ผ โ ๐) โ ๐น โ (๐ GrpHom ๐)) | ||
Theorem | ghmf1 19121* | 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 19122 | A bijective group homomorphism is an isomorphism. (Contributed by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐) & โข ๐ = (Baseโ๐) โ โข (๐น โ (๐ GrpHom ๐) โ (๐น:๐โ1-1-ontoโ๐ โ โก๐น โ (๐ GrpHom ๐))) | ||
Theorem | conjghm 19123* | Conjugation is an automorphism of the group. (Contributed by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) & โข ๐น = (๐ฅ โ ๐ โฆ ((๐ด + ๐ฅ) โ ๐ด)) โ โข ((๐บ โ Grp โง ๐ด โ ๐) โ (๐น โ (๐บ GrpHom ๐บ) โง ๐น:๐โ1-1-ontoโ๐)) | ||
Theorem | conjsubg 19124* | A conjugated subgroup is also a subgroup. (Contributed by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) & โข ๐น = (๐ฅ โ ๐ โฆ ((๐ด + ๐ฅ) โ ๐ด)) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ด โ ๐) โ ran ๐น โ (SubGrpโ๐บ)) | ||
Theorem | conjsubgen 19125* | A conjugated subgroup is equinumerous to the original subgroup. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) & โข ๐น = (๐ฅ โ ๐ โฆ ((๐ด + ๐ฅ) โ ๐ด)) โ โข ((๐ โ (SubGrpโ๐บ) โง ๐ด โ ๐) โ ๐ โ ran ๐น) | ||
Theorem | conjnmz 19126* | 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 19127* | Alternative condition for elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) & โข ๐น = (๐ฅ โ ๐ โฆ ((๐ด + ๐ฅ) โ ๐ด)) & โข ๐ = {๐ฆ โ ๐ โฃ โ๐ง โ ๐ ((๐ฆ + ๐ง) โ ๐ โ (๐ง + ๐ฆ) โ ๐)} โ โข (๐ โ (SubGrpโ๐บ) โ (๐ด โ ๐ โ (๐ด โ ๐ โง ๐ = ran ๐น))) | ||
Theorem | conjnsg 19128* | A normal subgroup is unchanged under conjugation. (Contributed by Mario Carneiro, 18-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข โ = (-gโ๐บ) & โข ๐น = (๐ฅ โ ๐ โฆ ((๐ด + ๐ฅ) โ ๐ด)) โ โข ((๐ โ (NrmSGrpโ๐บ) โง ๐ด โ ๐) โ ๐ = ran ๐น) | ||
Theorem | qusghm 19129* | 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 19130* | 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 19131 | The class of group isomorphism sets. |
class GrpIso | ||
Syntax | cgic 19132 | The class of the group isomorphism relation. |
class โ๐ | ||
Definition | df-gim 19133* | 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 19134 | 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 19135 | The group isomorphism function is a well-defined function. (Contributed by Mario Carneiro, 23-Aug-2015.) |
โข GrpIso Fn (Grp ร Grp) | ||
Theorem | isgim 19136 | 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 19137 | 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 19138 | 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 19139 | A group isomorphism is a homomorphism whose converse is also a homomorphism. Characterization of isomorphisms similar to ishmeo 23263. (Contributed by Mario Carneiro, 6-May-2015.) |
โข (๐น โ (๐ GrpIso ๐) โ (๐น โ (๐ GrpHom ๐) โง โก๐น โ (๐ GrpHom ๐ ))) | ||
Theorem | subggim 19140 | Behavior of subgroups under isomorphism. (Contributed by Stefan O'Rear, 21-Jan-2015.) |
โข ๐ต = (Baseโ๐ ) โ โข ((๐น โ (๐ GrpIso ๐) โง ๐ด โ ๐ต) โ (๐ด โ (SubGrpโ๐ ) โ (๐น โ ๐ด) โ (SubGrpโ๐))) | ||
Theorem | gimcnv 19141 | 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 19142 | The composition of group isomorphisms is a group isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ((๐น โ (๐ GrpIso ๐) โง ๐บ โ (๐ GrpIso ๐)) โ (๐น โ ๐บ) โ (๐ GrpIso ๐)) | ||
Theorem | brgic 19143 | The relation "is isomorphic to" for groups. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
โข (๐ โ๐ ๐ โ (๐ GrpIso ๐) โ โ ) | ||
Theorem | brgici 19144 | Prove isomorphic by an explicit isomorphism. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
โข (๐น โ (๐ GrpIso ๐) โ ๐ โ๐ ๐) | ||
Theorem | gicref 19145 | Isomorphism is reflexive. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข (๐ โ Grp โ ๐ โ๐ ๐ ) | ||
Theorem | giclcl 19146 | Isomorphism implies the left side is a group. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
โข (๐ โ๐ ๐ โ ๐ โ Grp) | ||
Theorem | gicrcl 19147 | Isomorphism implies the right side is a group. (Contributed by Mario Carneiro, 6-May-2015.) |
โข (๐ โ๐ ๐ โ ๐ โ Grp) | ||
Theorem | gicsym 19148 | Isomorphism is symmetric. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข (๐ โ๐ ๐ โ ๐ โ๐ ๐ ) | ||
Theorem | gictr 19149 | Isomorphism is transitive. (Contributed by Mario Carneiro, 21-Apr-2016.) |
โข ((๐ โ๐ ๐ โง ๐ โ๐ ๐) โ ๐ โ๐ ๐) | ||
Theorem | gicer 19150 | 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 19151 | Isomorphic groups have equinumerous base sets. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
โข ๐ต = (Baseโ๐ ) & โข ๐ถ = (Baseโ๐) โ โข (๐ โ๐ ๐ โ ๐ต โ ๐ถ) | ||
Theorem | gicsubgen 19152 | 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 19153 | Extend class definition to include the class of group actions. |
class GrpAct | ||
Definition | df-ga 19154* | 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 19155* | 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 19170). 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 19156 | 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 19157 | The right argument of a group action is a set. (Contributed by Mario Carneiro, 30-Apr-2015.) |
โข ( โ โ (๐บ GrpAct ๐) โ ๐ โ V) | ||
Theorem | gagrpid 19158 | 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 โ ๐ด) = ๐ด) | ||
Theorem | gaf 19159 | The mapping of the group action operation. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐บ) โ โข ( โ โ (๐บ GrpAct ๐) โ โ :(๐ ร ๐)โถ๐) | ||
Theorem | gafo 19160 | A group action is onto its base set. (Contributed by Jeff Hankins, 10-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐บ) โ โข ( โ โ (๐บ GrpAct ๐) โ โ :(๐ ร ๐)โontoโ๐) | ||
Theorem | gaass 19161 | An "associative" property for group actions. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) โ โข (( โ โ (๐บ GrpAct ๐) โง (๐ด โ ๐ โง ๐ต โ ๐ โง ๐ถ โ ๐)) โ ((๐ด + ๐ต) โ ๐ถ) = (๐ด โ (๐ต โ ๐ถ))) | ||
Theorem | ga0 19162 | The action of a group on the empty set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
โข (๐บ โ Grp โ โ โ (๐บ GrpAct โ )) | ||
Theorem | gaid 19163 | The trivial action of a group on any set. Each group element corresponds to the identity permutation. (Contributed by Jeff Hankins, 11-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐บ) โ โข ((๐บ โ Grp โง ๐ โ ๐) โ (2nd โพ (๐ ร ๐)) โ (๐บ GrpAct ๐)) | ||
Theorem | subgga 19164* | A subgroup acts on its parent group. (Contributed by Jeff Hankins, 13-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข ๐ป = (๐บ โพs ๐) & โข ๐น = (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ (๐ฅ + ๐ฆ)) โ โข (๐ โ (SubGrpโ๐บ) โ ๐น โ (๐ป GrpAct ๐)) | ||
Theorem | gass 19165* | A subset of a group action is a group action iff it is closed under the group action operation. (Contributed by Mario Carneiro, 17-Jan-2015.) |
โข ๐ = (Baseโ๐บ) โ โข (( โ โ (๐บ GrpAct ๐) โง ๐ โ ๐) โ (( โ โพ (๐ ร ๐)) โ (๐บ GrpAct ๐) โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ โ ๐ฆ) โ ๐)) | ||
Theorem | gasubg 19166 | The restriction of a group action to a subgroup is a group action. (Contributed by Mario Carneiro, 17-Jan-2015.) |
โข ๐ป = (๐บ โพs ๐) โ โข (( โ โ (๐บ GrpAct ๐) โง ๐ โ (SubGrpโ๐บ)) โ ( โ โพ (๐ ร ๐)) โ (๐ป GrpAct ๐)) | ||
Theorem | gaid2 19167* | A group operation is a left group action of the group on itself. (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข + = (+gโ๐บ) & โข ๐น = (๐ฅ โ ๐, ๐ฆ โ ๐ โฆ (๐ฅ + ๐ฆ)) โ โข (๐บ โ Grp โ ๐น โ (๐บ GrpAct ๐)) | ||
Theorem | galcan 19168 | The action of a particular group element is left-cancelable. (Contributed by FL, 17-May-2010.) (Revised by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐บ) โ โข (( โ โ (๐บ GrpAct ๐) โง (๐ด โ ๐ โง ๐ต โ ๐ โง ๐ถ โ ๐)) โ ((๐ด โ ๐ต) = (๐ด โ ๐ถ) โ ๐ต = ๐ถ)) | ||
Theorem | gacan 19169 | Group inverses cancel in a group action. (Contributed by Jeff Hankins, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข ๐ = (invgโ๐บ) โ โข (( โ โ (๐บ GrpAct ๐) โง (๐ด โ ๐ โง ๐ต โ ๐ โง ๐ถ โ ๐)) โ ((๐ด โ ๐ต) = ๐ถ โ ((๐โ๐ด) โ ๐ถ) = ๐ต)) | ||
Theorem | gapm 19170* | The action of a particular group element is a permutation of the base set. (Contributed by Jeff Hankins, 11-Aug-2009.) (Proof shortened by Mario Carneiro, 13-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข ๐น = (๐ฅ โ ๐ โฆ (๐ด โ ๐ฅ)) โ โข (( โ โ (๐บ GrpAct ๐) โง ๐ด โ ๐) โ ๐น:๐โ1-1-ontoโ๐) | ||
Theorem | gaorb 19171* | The orbit equivalence relation puts two points in the group action in the same equivalence class iff there is a group element that takes one element to the other. (Contributed by Mario Carneiro, 14-Jan-2015.) |
โข โผ = {โจ๐ฅ, ๐ฆโฉ โฃ ({๐ฅ, ๐ฆ} โ ๐ โง โ๐ โ ๐ (๐ โ ๐ฅ) = ๐ฆ)} โ โข (๐ด โผ ๐ต โ (๐ด โ ๐ โง ๐ต โ ๐ โง โโ โ ๐ (โ โ ๐ด) = ๐ต)) | ||
Theorem | gaorber 19172* | The orbit equivalence relation is an equivalence relation on the target set of the group action. (Contributed by NM, 11-Aug-2009.) (Revised by Mario Carneiro, 13-Jan-2015.) |
โข โผ = {โจ๐ฅ, ๐ฆโฉ โฃ ({๐ฅ, ๐ฆ} โ ๐ โง โ๐ โ ๐ (๐ โ ๐ฅ) = ๐ฆ)} & โข ๐ = (Baseโ๐บ) โ โข ( โ โ (๐บ GrpAct ๐) โ โผ Er ๐) | ||
Theorem | gastacl 19173* | The stabilizer subgroup in a group action. (Contributed by Mario Carneiro, 15-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข ๐ป = {๐ข โ ๐ โฃ (๐ข โ ๐ด) = ๐ด} โ โข (( โ โ (๐บ GrpAct ๐) โง ๐ด โ ๐) โ ๐ป โ (SubGrpโ๐บ)) | ||
Theorem | gastacos 19174* | Write the coset relation for the stabilizer subgroup. (Contributed by Mario Carneiro, 15-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข ๐ป = {๐ข โ ๐ โฃ (๐ข โ ๐ด) = ๐ด} & โข โผ = (๐บ ~QG ๐ป) โ โข ((( โ โ (๐บ GrpAct ๐) โง ๐ด โ ๐) โง (๐ต โ ๐ โง ๐ถ โ ๐)) โ (๐ต โผ ๐ถ โ (๐ต โ ๐ด) = (๐ถ โ ๐ด))) | ||
Theorem | orbstafun 19175* | Existence and uniqueness for the function of orbsta 19177. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
โข ๐ = (Baseโ๐บ) & โข ๐ป = {๐ข โ ๐ โฃ (๐ข โ ๐ด) = ๐ด} & โข โผ = (๐บ ~QG ๐ป) & โข ๐น = ran (๐ โ ๐ โฆ โจ[๐] โผ , (๐ โ ๐ด)โฉ) โ โข (( โ โ (๐บ GrpAct ๐) โง ๐ด โ ๐) โ Fun ๐น) | ||
Theorem | orbstaval 19176* | Value of the function at a given equivalence class element. (Contributed by Mario Carneiro, 15-Jan-2015.) (Proof shortened by Mario Carneiro, 23-Dec-2016.) |
โข ๐ = (Baseโ๐บ) & โข ๐ป = {๐ข โ ๐ โฃ (๐ข โ ๐ด) = ๐ด} & โข โผ = (๐บ ~QG ๐ป) & โข ๐น = ran (๐ โ ๐ โฆ โจ[๐] โผ , (๐ โ ๐ด)โฉ) โ โข ((( โ โ (๐บ GrpAct ๐) โง ๐ด โ ๐) โง ๐ต โ ๐) โ (๐นโ[๐ต] โผ ) = (๐ต โ ๐ด)) | ||
Theorem | orbsta 19177* | The Orbit-Stabilizer theorem. The mapping ๐น is a bijection from the cosets of the stabilizer subgroup of ๐ด to the orbit of ๐ด. (Contributed by Mario Carneiro, 15-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข ๐ป = {๐ข โ ๐ โฃ (๐ข โ ๐ด) = ๐ด} & โข โผ = (๐บ ~QG ๐ป) & โข ๐น = ran (๐ โ ๐ โฆ โจ[๐] โผ , (๐ โ ๐ด)โฉ) & โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ({๐ฅ, ๐ฆ} โ ๐ โง โ๐ โ ๐ (๐ โ ๐ฅ) = ๐ฆ)} โ โข (( โ โ (๐บ GrpAct ๐) โง ๐ด โ ๐) โ ๐น:(๐ / โผ )โ1-1-ontoโ[๐ด]๐) | ||
Theorem | orbsta2 19178* | Relation between the size of the orbit and the size of the stabilizer of a point in a finite group action. (Contributed by Mario Carneiro, 16-Jan-2015.) |
โข ๐ = (Baseโ๐บ) & โข ๐ป = {๐ข โ ๐ โฃ (๐ข โ ๐ด) = ๐ด} & โข โผ = (๐บ ~QG ๐ป) & โข ๐ = {โจ๐ฅ, ๐ฆโฉ โฃ ({๐ฅ, ๐ฆ} โ ๐ โง โ๐ โ ๐ (๐ โ ๐ฅ) = ๐ฆ)} โ โข ((( โ โ (๐บ GrpAct ๐) โง ๐ด โ ๐) โง ๐ โ Fin) โ (โฏโ๐) = ((โฏโ[๐ด]๐) ยท (โฏโ๐ป))) | ||
Syntax | ccntz 19179 | Syntax for the centralizer of a set in a monoid. |
class Cntz | ||
Syntax | ccntr 19180 | Syntax for the centralizer of a monoid. |
class Cntr | ||
Definition | df-cntz 19181* | Define the centralizer of a subset of a magma, which is the set of elements each of which commutes with each element of the given subset. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข Cntz = (๐ โ V โฆ (๐ โ ๐ซ (Baseโ๐) โฆ {๐ฅ โ (Baseโ๐) โฃ โ๐ฆ โ ๐ (๐ฅ(+gโ๐)๐ฆ) = (๐ฆ(+gโ๐)๐ฅ)})) | ||
Definition | df-cntr 19182 | Define the center of a magma, which is the elements that commute with all others. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข Cntr = (๐ โ V โฆ ((Cntzโ๐)โ(Baseโ๐))) | ||
Theorem | cntrval 19183 | Substitute definition of the center. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข ๐ = (Cntzโ๐) โ โข (๐โ๐ต) = (Cntrโ๐) | ||
Theorem | cntzfval 19184* | First level substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข ๐ = (Cntzโ๐) โ โข (๐ โ ๐ โ ๐ = (๐ โ ๐ซ ๐ต โฆ {๐ฅ โ ๐ต โฃ โ๐ฆ โ ๐ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)})) | ||
Theorem | cntzval 19185* | Definition substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข ๐ = (Cntzโ๐) โ โข (๐ โ ๐ต โ (๐โ๐) = {๐ฅ โ ๐ต โฃ โ๐ฆ โ ๐ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ)}) | ||
Theorem | elcntz 19186* | Elementhood in the centralizer. (Contributed by Mario Carneiro, 22-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข ๐ = (Cntzโ๐) โ โข (๐ โ ๐ต โ (๐ด โ (๐โ๐) โ (๐ด โ ๐ต โง โ๐ฆ โ ๐ (๐ด + ๐ฆ) = (๐ฆ + ๐ด)))) | ||
Theorem | cntzel 19187* | Membership in a centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข ๐ = (Cntzโ๐) โ โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ (๐โ๐) โ โ๐ฆ โ ๐ (๐ + ๐ฆ) = (๐ฆ + ๐))) | ||
Theorem | cntzsnval 19188* | Special substitution for the centralizer of a singleton. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข ๐ = (Cntzโ๐) โ โข (๐ โ ๐ต โ (๐โ{๐}) = {๐ฅ โ ๐ต โฃ (๐ฅ + ๐) = (๐ + ๐ฅ)}) | ||
Theorem | elcntzsn 19189 | Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข ๐ = (Cntzโ๐) โ โข (๐ โ ๐ต โ (๐ โ (๐โ{๐}) โ (๐ โ ๐ต โง (๐ + ๐) = (๐ + ๐)))) | ||
Theorem | sscntz 19190* | A centralizer expression for two sets elementwise commuting. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข ๐ = (Cntzโ๐) โ โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ (๐โ๐) โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ (๐ฅ + ๐ฆ) = (๐ฆ + ๐ฅ))) | ||
Theorem | cntzrcl 19191 | Reverse closure for elements of the centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข ๐ = (Cntzโ๐) โ โข (๐ โ (๐โ๐) โ (๐ โ V โง ๐ โ ๐ต)) | ||
Theorem | cntzssv 19192 | The centralizer is unconditionally a subset. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข ๐ = (Cntzโ๐) โ โข (๐โ๐) โ ๐ต | ||
Theorem | cntzi 19193 | Membership in a centralizer (inference). (Contributed by Stefan O'Rear, 6-Sep-2015.) (Revised by Mario Carneiro, 22-Sep-2015.) |
โข + = (+gโ๐) & โข ๐ = (Cntzโ๐) โ โข ((๐ โ (๐โ๐) โง ๐ โ ๐) โ (๐ + ๐) = (๐ + ๐)) | ||
Theorem | elcntr 19194* | Elementhood in the center of a magma. (Contributed by SN, 21-Mar-2025.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข ๐ = (Cntrโ๐) โ โข (๐ด โ ๐ โ (๐ด โ ๐ต โง โ๐ฆ โ ๐ต (๐ด + ๐ฆ) = (๐ฆ + ๐ด))) | ||
Theorem | cntrss 19195 | The center is a subset of the base field. (Contributed by Thierry Arnoux, 21-Aug-2023.) |
โข ๐ต = (Baseโ๐) โ โข (Cntrโ๐) โ ๐ต | ||
Theorem | cntri 19196 | Defining property of the center of a group. (Contributed by Mario Carneiro, 22-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข + = (+gโ๐) & โข ๐ = (Cntrโ๐) โ โข ((๐ โ ๐ โง ๐ โ ๐ต) โ (๐ + ๐) = (๐ + ๐)) | ||
Theorem | resscntz 19197 | Centralizer in a substructure. (Contributed by Mario Carneiro, 3-Oct-2015.) |
โข ๐ป = (๐บ โพs ๐ด) & โข ๐ = (Cntzโ๐บ) & โข ๐ = (Cntzโ๐ป) โ โข ((๐ด โ ๐ โง ๐ โ ๐ด) โ (๐โ๐) = ((๐โ๐) โฉ ๐ด)) | ||
Theorem | cntzsgrpcl 19198* | Centralizers are closed under the semigroup operation. (Contributed by AV, 17-Feb-2025.) |
โข ๐ต = (Baseโ๐) & โข ๐ = (Cntzโ๐) & โข ๐ถ = (๐โ๐) โ โข ((๐ โ Smgrp โง ๐ โ ๐ต) โ โ๐ฆ โ ๐ถ โ๐ง โ ๐ถ (๐ฆ(+gโ๐)๐ง) โ ๐ถ) | ||
Theorem | cntz2ss 19199 | Centralizers reverse the subset relation. (Contributed by Mario Carneiro, 3-Oct-2015.) |
โข ๐ต = (Baseโ๐) & โข ๐ = (Cntzโ๐) โ โข ((๐ โ ๐ต โง ๐ โ ๐) โ (๐โ๐) โ (๐โ๐)) | ||
Theorem | cntzrec 19200 | Reciprocity relationship for centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
โข ๐ต = (Baseโ๐) & โข ๐ = (Cntzโ๐) โ โข ((๐ โ ๐ต โง ๐ โ ๐ต) โ (๐ โ (๐โ๐) โ ๐ โ (๐โ๐))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |