Home | Metamath
Proof Explorer Theorem List (p. 180 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pmtrdifwrdellem1 17901* | Lemma 1 for pmtrdifwrdel 17905. (Contributed by AV, 15-Jan-2019.) |
pmTrsp pmTrsp ..^ pmTrsp Word Word | ||
Theorem | pmtrdifwrdellem2 17902* | Lemma 2 for pmtrdifwrdel 17905. (Contributed by AV, 15-Jan-2019.) |
pmTrsp pmTrsp ..^ pmTrsp Word | ||
Theorem | pmtrdifwrdellem3 17903* | Lemma 3 for pmtrdifwrdel 17905. (Contributed by AV, 15-Jan-2019.) |
pmTrsp pmTrsp ..^ pmTrsp Word ..^ | ||
Theorem | pmtrdifwrdel2lem1 17904* | Lemma 1 for pmtrdifwrdel2 17906. (Contributed by AV, 31-Jan-2019.) |
pmTrsp pmTrsp ..^ pmTrsp Word ..^ | ||
Theorem | pmtrdifwrdel 17905* | A sequence of transpositions of elements of a set without a special element corresponds to a sequence of transpositions of elements of the set. (Contributed by AV, 15-Jan-2019.) |
pmTrsp pmTrsp Word Word ..^ | ||
Theorem | pmtrdifwrdel2 17906* | A sequence of transpositions of elements of a set without a special element corresponds to a sequence of transpositions of elements of the set not moving the special element. (Contributed by AV, 31-Jan-2019.) |
pmTrsp pmTrsp Word Word ..^ | ||
Theorem | pmtrprfval 17907* | The transpositions on a pair. (Contributed by AV, 9-Dec-2018.) |
pmTrsp | ||
Theorem | pmtrprfvalrn 17908 | The range of the transpositions on a pair is actually a singleton: the transposition of the two elements of the pair. (Contributed by AV, 9-Dec-2018.) |
pmTrsp | ||
Syntax | cpsgn 17909 | Syntax for the sign of a permutation. |
pmSgn | ||
Syntax | cevpm 17910 | Syntax for even permutations. |
pmEven | ||
Definition | df-psgn 17911* | Define a function which takes the value for even permutations and for odd. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
pmSgn Word pmTrsp g | ||
Definition | df-evpm 17912 | Define the set of even permutations on a given set. (Contributed by Stefan O'Rear, 9-Jul-2018.) |
pmEven pmSgn | ||
Theorem | psgnunilem1 17913* | Lemma for psgnuni 17919. Given two consequtive transpositions in a representation of a permutation, either they are equal and therefore equivalent to the identity, or they are not and it is possible to commute them such that a chosen point in the left transposition is preserved in the right. By repeating this process, a point can be removed from a representation of the identity. (Contributed by Stefan O'Rear, 22-Aug-2015.) |
pmTrsp | ||
Theorem | psgnunilem5 17914* | Lemma for psgnuni 17919. It is impossible to shift a transposition off the end because if the active transposition is at the right end, it is the only transposition moving in contradiction to this being a representation of the identity. (Contributed by Stefan O'Rear, 25-Aug-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
pmTrsp Word g ..^ ..^ ..^ | ||
Theorem | psgnunilem2 17915* | Lemma for psgnuni 17919. Induction step for moving a transposition as far to the right as possible. (Contributed by Stefan O'Rear, 24-Aug-2015.) (Revised by Mario Carneiro, 28-Feb-2016.) |
pmTrsp Word g ..^ ..^ Word g Word g ..^ ..^ | ||
Theorem | psgnunilem3 17916* | Lemma for psgnuni 17919. Any nonempty representation of the identity can be incrementally transformed into a representation two shorter. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
pmTrsp Word g Word g | ||
Theorem | psgnunilem4 17917 | Lemma for psgnuni 17919. An odd-length representation of the identity is impossible, as it could be repeatedly shortened to a length of 1, but a length 1 permutation must be a transposition. (Contributed by Stefan O'Rear, 25-Aug-2015.) |
pmTrsp Word g | ||
Theorem | m1expaddsub 17918 | Addition and subtraction of parities are the same. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
Theorem | psgnuni 17919 | If the same permutation can be written in more than one way as a product of transpositions, the parity of those products must agree; otherwise the product of one with the inverse of the other would be an odd representation of the identity. (Contributed by Stefan O'Rear, 27-Aug-2015.) |
pmTrsp Word Word g g | ||
Theorem | psgnfval 17920* | Function definition of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
pmTrsp pmSgn Word g | ||
Theorem | psgnfn 17921* | Functionality and domain of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
pmSgn | ||
Theorem | psgndmsubg 17922 | The finitary permutations are a subgroup. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
pmSgn SubGrp | ||
Theorem | psgneldm 17923 | Property of being a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
pmSgn | ||
Theorem | psgneldm2 17924* | The finitary permutations are the span of the transpositions. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
pmTrsp pmSgn Word g | ||
Theorem | psgneldm2i 17925 | A sequence of transpositions describes a finitary permutation. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
pmTrsp pmSgn Word g | ||
Theorem | psgneu 17926* | A finitary permutation has exactly one parity. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
pmTrsp pmSgn Word g | ||
Theorem | psgnval 17927* | Value of the permutation sign function. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
pmTrsp pmSgn Word g | ||
Theorem | psgnvali 17928* | A finitary permutation has at least one representation for its parity. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
pmTrsp pmSgn Word g | ||
Theorem | psgnvalii 17929 | Any representation of a permutation is length matching the permutation sign. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
pmTrsp pmSgn Word g | ||
Theorem | psgnpmtr 17930 | All transpositions are odd. (Contributed by Stefan O'Rear, 29-Aug-2015.) |
pmTrsp pmSgn | ||
Theorem | psgn0fv0 17931 | The permutation sign function for an empty set at an empty set is 1. (Contributed by AV, 27-Feb-2019.) |
pmSgn | ||
Theorem | sygbasnfpfi 17932 | The class of non-fixed points of a permutation of a finite set is finite. (Contributed by AV, 13-Jan-2019.) |
Theorem | psgnfvalfi 17933* | Function definition of the permutation sign function for permutations of finite sets. (Contributed by AV, 13-Jan-2019.) |
pmTrsp pmSgn Word g | ||
Theorem | psgnvalfi 17934* | Value of the permutation sign function for permutations of finite sets. (Contributed by AV, 13-Jan-2019.) |
pmTrsp pmSgn Word g | ||
Theorem | psgnran 17935 | The range of the permutation sign function for finite permutations. (Contributed by AV, 1-Jan-2019.) |
pmSgn | ||
Theorem | gsmtrcl 17936 | The group sum of transpositions of a finite set is a permutation, see also psgneldm2i 17925. (Contributed by AV, 19-Jan-2019.) |
pmTrsp Word g | ||
Theorem | psgnfitr 17937* | A permutation of a finite set is generated by transpositions. (Contributed by AV, 13-Jan-2019.) |
pmTrsp Word g | ||
Theorem | psgnfieu 17938* | A permutation of a finite set has exactly one parity. (Contributed by AV, 13-Jan-2019.) |
pmTrsp Word g | ||
Theorem | pmtrsn 17939 | The value of the transposition generator function for a singleton is empty, i.e. there is no transposition for a singleton. This also holds for , i.e. for the empty set resulting in pmTrsp . (Contributed by AV, 6-Aug-2019.) |
pmTrsp | ||
Theorem | psgnsn 17940 | The permutation sign function for a singleton. (Contributed by AV, 6-Aug-2019.) |
pmSgn | ||
Theorem | psgnprfval 17941* | The permutation sign function for a pair. (Contributed by AV, 10-Dec-2018.) |
pmTrsp pmSgn Word g | ||
Theorem | psgnprfval1 17942 | The permutation sign of the identity for a pair. (Contributed by AV, 11-Dec-2018.) |
pmTrsp pmSgn | ||
Theorem | psgnprfval2 17943 | The permutation sign of the transposition for a pair. (Contributed by AV, 10-Dec-2018.) |
pmTrsp pmSgn | ||
Syntax | cod 17944 | Extend class notation to include the order function on the elements of a group. |
Syntax | cgex 17945 | Extend class notation to include the order function on the elements of a group. |
gEx | ||
Syntax | cpgp 17946 | Extend class notation to include the class of all p-groups. |
pGrp | ||
Syntax | cslw 17947 | Extend class notation to include the class of all Sylow p-subgroups of a group. |
pSyl | ||
Definition | df-od 17948* | Define the order of an element in a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.) (Revised by AV, 5-Oct-2020.) |
.g inf | ||
Definition | df-gex 17949* | Define the exponent of a group. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 4-Sep-2015.) (Revised by AV, 26-Sep-2020.) |
gEx .g inf | ||
Definition | df-pgp 17950* | Define the set of p-groups, which are groups such that every element has a power of as its order. (Contributed by Mario Carneiro, 15-Jan-2015.) (Revised by AV, 5-Oct-2020.) |
pGrp | ||
Definition | df-slw 17951* | Define the set of Sylow p-subgroups of a group . A Sylow p-subgroup is a p-group that is not a subgroup of any other p-groups in . (Contributed by Mario Carneiro, 16-Jan-2015.) |
pSyl SubGrp SubGrp pGrp ↾s | ||
Theorem | odfval 17952* | Value of the order function. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by AV, 5-Oct-2020.) |
.g inf | ||
Theorem | odval 17953* | Second substitution for the group order definition. (Contributed by Mario Carneiro, 13-Jul-2014.) (Revised by Stefan O'Rear, 5-Sep-2015.) (Revised by AV, 5-Oct-2020.) |
.g inf | ||
Theorem | odlem1 17954* | The group element order is either zero or a nonzero multiplier that annihilates the element. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.) (Revised by AV, 5-Oct-2020.) |
.g | ||
Theorem | odcl 17955 | The order of a group element is always a nonnegative integer. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.) |
Theorem | odf 17956 | Functionality of the group element order. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 5-Oct-2020.) |
Theorem | odid 17957 | Any element to the power of its order is the identity. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.) |
.g | ||
Theorem | odlem2 17958 | Any positive annihilator of a group element is an upper bound on the (positive) order of the element. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Stefan O'Rear, 5-Sep-2015.) (Proof shortened by AV, 5-Oct-2020.) |
.g | ||
Theorem | odmodnn0 17959 | Reduce the argument of a group multiple by modding out the order of the element. (Contributed by Mario Carneiro, 23-Sep-2015.) |
.g | ||
Theorem | mndodconglem 17960 | Lemma for mndodcong 17961. (Contributed by Mario Carneiro, 23-Sep-2015.) |
.g | ||
Theorem | mndodcong 17961 | If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. (Contributed by Mario Carneiro, 23-Sep-2015.) |
.g | ||
Theorem | mndodcongi 17962 | If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. For monoids, the reverse implication is false for elements with infinite order. For example, the powers of are 1,2,4,8,6,2,4,8,6,... so that the identity 1 never repeats, which is infinite order by our definition, yet other numbers like 6 appear many times in the sequence. (Contributed by Mario Carneiro, 23-Sep-2015.) |
.g | ||
Theorem | oddvdsnn0 17963 | The only multiples of that are equal to the identity are the multiples of the order of . (Contributed by Mario Carneiro, 23-Sep-2015.) |
.g | ||
Theorem | odnncl 17964 | If a nonzero multiple of an element is zero, the element has positive order. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 22-Sep-2015.) |
.g | ||
Theorem | odmod 17965 | Reduce the argument of a group multiple by modding out the order of the element. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 6-Sep-2015.) |
.g | ||
Theorem | oddvds 17966 | The only multiples of that are equal to the identity are the multiples of the order of . (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.) |
.g | ||
Theorem | oddvdsi 17967 | Any group element is annihilated by any multiple of its order. (Contributed by Stefan O'Rear, 5-Sep-2015.) (Revised by Mario Carneiro, 23-Sep-2015.) |
.g | ||
Theorem | odcong 17968 | If two multipliers are congruent relative to the base point's order, the corresponding multiples are the same. (Contributed by Stefan O'Rear, 5-Sep-2015.) |
.g | ||
Theorem | odeq 17969* | The oddvds 17966 property uniquely defines the group order. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
.g | ||
Theorem | odval2 17970* | A non-conditional definition of the group order. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
.g | ||
Theorem | odmulgid 17971 | A relationship between the order of a multiple and the order of the basepoint. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
.g | ||
Theorem | odmulg2 17972 | The order of a multiple divides the order of the base point. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
.g | ||
Theorem | odmulg 17973 | Relationship between the order of an element and that of a multiple. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
.g | ||
Theorem | odmulgeq 17974 | A multiple of a point of finite order only has the same order if the multiplier is relatively prime. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
.g | ||
Theorem | odbezout 17975* | If is coprime to the order of , there is a modular inverse to cancel multiplication by . (Contributed by Mario Carneiro, 27-Apr-2016.) |
.g | ||
Theorem | od1 17976 | The order of the group identity is one. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.) |
Theorem | odeq1 17977 | The group identity is the unique element of a group with order one. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.) |
Theorem | odinv 17978 | The order of the inverse of a group element. (Contributed by Mario Carneiro, 20-Oct-2015.) |
Theorem | odf1 17979* | The multiples of an element with infinite order form an infinite cyclic subgroup of . (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 23-Sep-2015.) |
.g | ||
Theorem | odinf 17980* | The multiples of an element with infinite order form an infinite cyclic subgroup of . (Contributed by Mario Carneiro, 14-Jan-2015.) |
.g | ||
Theorem | dfod2 17981* | An alternative definition of the order of a group element is as the cardinality of the cyclic subgroup generated by the element. (Contributed by Mario Carneiro, 14-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.) |
.g | ||
Theorem | odcl2 17982 | The order of an element of a finite group is finite. (Contributed by Mario Carneiro, 14-Jan-2015.) |
Theorem | oddvds2 17983 | The order of an element of a finite group divides the order (cardinality) of the group. Corollary of Lagrange's theorem for the order of a subgroup. (Contributed by Mario Carneiro, 14-Jan-2015.) |
Theorem | submod 17984 | The order of an element is the same in a subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.) (Proof shortened by AV, 5-Oct-2020.) |
↾s SubMnd | ||
Theorem | subgod 17985 | The order of an element is the same in a subgroup. (Contributed by Mario Carneiro, 14-Jan-2015.) (Proof shortened by Stefan O'Rear, 12-Sep-2015.) |
↾s SubGrp | ||
Theorem | odsubdvds 17986 | The order of an element of a subgroup divides the order of the subgroup. (Contributed by Mario Carneiro, 16-Jan-2015.) |
SubGrp | ||
Theorem | odf1o1 17987* | An element with zero order has infinitely many multiples. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
.g mrClsSubGrp | ||
Theorem | odf1o2 17988* | An element with nonzero order has as many multiples as its order. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
.g mrClsSubGrp ..^ ..^ | ||
Theorem | odhash 17989 | An element of zero order generates an infinite subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
mrClsSubGrp | ||
Theorem | odhash2 17990 | If an element has nonzero order, it generates a subgroup with size equal to the order. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
mrClsSubGrp | ||
Theorem | odhash3 17991 | An element which generates a finite subgroup has order the size of that subgroup. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
mrClsSubGrp | ||
Theorem | odngen 17992* | A cyclic subgroup of size has generators. (Contributed by Stefan O'Rear, 12-Sep-2015.) |
mrClsSubGrp | ||
Theorem | gexval 17993* | Value of the exponent of a group. (Contributed by Mario Carneiro, 23-Apr-2016.) (Revised by AV, 26-Sep-2020.) |
.g gEx inf | ||
Theorem | gexlem1 17994* | The group element order is either zero or a nonzero multiplier that annihilates the element. (Contributed by Mario Carneiro, 23-Apr-2016.) (Proof shortened by AV, 26-Sep-2020.) |
.g gEx | ||
Theorem | gexcl 17995 | The exponent of a group is a nonnegative integer. (Contributed by Mario Carneiro, 23-Apr-2016.) |
gEx | ||
Theorem | gexid 17996 | Any element to the power of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.) |
gEx .g | ||
Theorem | gexlem2 17997* | Any positive annihilator of all the group elements is an upper bound on the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.) (Proof shortened by AV, 26-Sep-2020.) |
gEx .g | ||
Theorem | gexdvdsi 17998 | Any group element is annihilated by any multiple of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.) |
gEx .g | ||
Theorem | gexdvds 17999* | The only that annihilate all the elements of the group are the multiples of the group exponent. (Contributed by Mario Carneiro, 24-Apr-2016.) |
gEx .g | ||
Theorem | gexdvds2 18000* | An integer divides the group exponent iff it divides all the group orders. In other words, the group exponent is the LCM of the orders of all the elements. (Contributed by Mario Carneiro, 24-Apr-2016.) |
gEx |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |