Home | Metamath
Proof Explorer Theorem List (p. 200 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 | zzngim 19901 | The ring homomorphism is an isomorphism for . (We only show group isomorphism here, but ring isomorphism follows, since it is a bijective ring homomorphism.) (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by AV, 13-Jun-2019.) |
ℤ/nℤ RHom ℤring GrpIso | ||
Theorem | znle2 19902 | The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
ℤ/nℤ RHom ..^ | ||
Theorem | znleval 19903 | The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
ℤ/nℤ RHom ..^ | ||
Theorem | znleval2 19904 | The ordering of the ℤ/nℤ structure. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
ℤ/nℤ RHom ..^ | ||
Theorem | zntoslem 19905 | Lemma for zntos 19906. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 13-Jun-2019.) |
ℤ/nℤ RHom ..^ Toset | ||
Theorem | zntos 19906 | The ℤ/nℤ structure is a totally ordered set. (The order is not respected by the operations, except in the case when it coincides with the ordering on .) (Contributed by Mario Carneiro, 15-Jun-2015.) |
ℤ/nℤ Toset | ||
Theorem | znhash 19907 | The ℤ/nℤ structure has elements. (Contributed by Mario Carneiro, 15-Jun-2015.) |
ℤ/nℤ | ||
Theorem | znfi 19908 | The ℤ/nℤ structure is a finite ring. (Contributed by Mario Carneiro, 2-May-2016.) |
ℤ/nℤ | ||
Theorem | znfld 19909 | The ℤ/nℤ structure is a finite field when is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) |
ℤ/nℤ Field | ||
Theorem | znidomb 19910 | The ℤ/nℤ structure is a domain (and hence a field) precisely when is prime. (Contributed by Mario Carneiro, 15-Jun-2015.) |
ℤ/nℤ IDomn | ||
Theorem | znchr 19911 | Cyclic rings are defined by their characteristic. (Contributed by Stefan O'Rear, 6-Sep-2015.) |
ℤ/nℤ chr | ||
Theorem | znunit 19912 | The units of ℤ/nℤ are the integers coprime to the base. (Contributed by Mario Carneiro, 18-Apr-2016.) |
ℤ/nℤ Unit RHom | ||
Theorem | znunithash 19913 | The size of the unit group of ℤ/nℤ. (Contributed by Mario Carneiro, 19-Apr-2016.) |
ℤ/nℤ Unit | ||
Theorem | znrrg 19914 | The regular elements of ℤ/nℤ are exactly the units. (This theorem fails for , where all nonzero integers are regular, but only are units.) (Contributed by Mario Carneiro, 18-Apr-2016.) |
ℤ/nℤ Unit RLReg | ||
Theorem | cygznlem1 19915* | Lemma for cygzn 19919. (Contributed by Mario Carneiro, 21-Apr-2016.) |
ℤ/nℤ .g RHom CycGrp | ||
Theorem | cygznlem2a 19916* | Lemma for cygzn 19919. (Contributed by Mario Carneiro, 23-Dec-2016.) |
ℤ/nℤ .g RHom CycGrp | ||
Theorem | cygznlem2 19917* | Lemma for cygzn 19919. (Contributed by Mario Carneiro, 21-Apr-2016.) (Revised by Mario Carneiro, 23-Dec-2016.) |
ℤ/nℤ .g RHom CycGrp | ||
Theorem | cygznlem3 19918* | A cyclic group with elements is isomorphic to . (Contributed by Mario Carneiro, 21-Apr-2016.) |
ℤ/nℤ .g RHom CycGrp 𝑔 | ||
Theorem | cygzn 19919 | A cyclic group with elements is isomorphic to , and an infinite cyclic group is isomorphic to . (Contributed by Mario Carneiro, 21-Apr-2016.) |
ℤ/nℤ CycGrp 𝑔 | ||
Theorem | cygth 19920* | The "fundamental theorem of cyclic groups". Cyclic groups are exactly the additive groups , for (where is the infinite cyclic group ), up to isomorphism. (Contributed by Mario Carneiro, 21-Apr-2016.) |
CycGrp 𝑔 ℤ/nℤ | ||
Theorem | cyggic 19921 | Cyclic groups are isomorphic precisely when they have the same order. (Contributed by Mario Carneiro, 21-Apr-2016.) |
CycGrp CycGrp 𝑔 | ||
Theorem | frgpcyg 19922 | A free group is cyclic iff it has zero or one generator. (Contributed by Mario Carneiro, 21-Apr-2016.) (Proof shortened by AV, 18-Apr-2021.) |
freeGrp CycGrp | ||
Theorem | cnmsgnsubg 19923 | The signs form a multiplicative subgroup of the complex numbers. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
mulGrpℂfld ↾s SubGrp | ||
Theorem | cnmsgnbas 19924 | The base set of the sign subgroup of the complex numbers. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
mulGrpℂfld ↾s | ||
Theorem | cnmsgngrp 19925 | The group of signs under multiplication. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
mulGrpℂfld ↾s | ||
Theorem | psgnghm 19926 | The sign is a homomorphism from the finitary permutation group to the numeric signs. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
pmSgn ↾s mulGrpℂfld ↾s | ||
Theorem | psgnghm2 19927 | The sign is a homomorphism from the finite symmetric group to the numeric signs. (Contributed by Stefan O'Rear, 28-Aug-2015.) |
pmSgn mulGrpℂfld ↾s | ||
Theorem | psgninv 19928 | The sign of a permutation equals the sign of the inverse of the permutation. (Contributed by SO, 9-Jul-2018.) |
pmSgn | ||
Theorem | psgnco 19929 | Multiplicativity of the permutation sign function. (Contributed by SO, 9-Jul-2018.) |
pmSgn | ||
Theorem | zrhpsgnmhm 19930 | Embedding of permutation signs into an arbitrary ring is a homomorphism. (Contributed by SO, 9-Jul-2018.) |
RHom pmSgn MndHom mulGrp | ||
Theorem | zrhpsgninv 19931 | The embedded sign of a permutation equals the embedded sign of the inverse of the permutation. (Contributed by SO, 9-Jul-2018.) |
RHom pmSgn | ||
Theorem | evpmss 19932 | Even permutations are permutations. (Contributed by SO, 9-Jul-2018.) |
pmEven | ||
Theorem | psgnevpmb 19933 | A class is an even permutation if it is a permutation with sign 1. (Contributed by SO, 9-Jul-2018.) |
pmSgn pmEven | ||
Theorem | psgnodpm 19934 | A permutation which is odd (i.e. not even) has sign -1. (Contributed by SO, 9-Jul-2018.) |
pmSgn pmEven | ||
Theorem | psgnevpm 19935 | A permutation which is even has sign 1. (Contributed by SO, 9-Jul-2018.) |
pmSgn pmEven | ||
Theorem | psgnodpmr 19936 | If a permutation has sign -1 it is odd (not even). (Contributed by SO, 9-Jul-2018.) |
pmSgn pmEven | ||
Theorem | zrhpsgnevpm 19937 | The sign of an even permutation embedded into a ring is the multiplicative neutral element of the ring. (Contributed by SO, 9-Jul-2018.) |
RHom pmSgn pmEven | ||
Theorem | zrhpsgnodpm 19938 | The sign of an odd permutation embedded into a ring is the additive inverse of the multiplicative neutral element of the ring. (Contributed by SO, 9-Jul-2018.) |
RHom pmSgn pmEven | ||
Theorem | zrhcofipsgn 19939 | Composition of a RHom homomorphism and the sign function for a finite permutation. (Contributed by AV, 27-Dec-2018.) |
RHom pmSgn | ||
Theorem | zrhpsgnelbas 19940 | Embedding of permutation signs into a ring results in an element of the ring. (Contributed by AV, 1-Jan-2019.) |
pmSgn RHom | ||
Theorem | zrhcopsgnelbas 19941 | Embedding of permutation signs into a ring results in an element of the ring. (Contributed by AV, 1-Jan-2019.) |
pmSgn RHom | ||
Theorem | evpmodpmf1o 19942* | The function for performing an even permutation after a fixed odd permutation is one to one onto all odd permutations. (Contributed by SO, 9-Jul-2018.) |
pmEven pmEven pmEven pmEven | ||
Theorem | pmtrodpm 19943 | A transposition is an odd permutation. (Contributed by SO, 9-Jul-2018.) |
pmTrsp pmEven | ||
Theorem | psgnfix1 19944* | A permutation of a finite set fixing one element is generated by transpositions not involving the fixed element. (Contributed by AV, 13-Jan-2019.) |
pmTrsp Word g | ||
Theorem | psgnfix2 19945* | A permutation of a finite set fixing one element is generated by transpositions not involving the fixed element. (Contributed by AV, 17-Jan-2019.) |
pmTrsp pmTrsp Word g | ||
Theorem | psgndiflemB 19946* | Lemma 1 for psgndif 19948. (Contributed by AV, 27-Jan-2019.) |
pmTrsp pmTrsp Word g Word ..^ g | ||
Theorem | psgndiflemA 19947* | Lemma 2 for psgndif 19948. (Contributed by AV, 31-Jan-2019.) |
pmTrsp pmTrsp Word g Word g | ||
Theorem | psgndif 19948* | Embedding of permutation signs restricted to a set without a single element into a ring. (Contributed by AV, 31-Jan-2019.) |
pmSgn pmSgn | ||
Theorem | zrhcopsgndif 19949* | Embedding of permutation signs restricted to a set without a single element into a ring. (Contributed by AV, 31-Jan-2019.) |
pmSgn pmSgn RHom | ||
Syntax | crefld 19950 | Extend class notation with the field of real numbers. |
RRfld | ||
Definition | df-refld 19951 | The field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
RRfld ℂfld ↾s | ||
Theorem | rebase 19952 | The base of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
RRfld | ||
Theorem | remulg 19953 | The multiplication (group power) operation of the group of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
.gRRfld | ||
Theorem | resubdrg 19954 | The real numbers form a division subring of the complex numbers. (Contributed by Mario Carneiro, 4-Dec-2014.) (Revised by Thierry Arnoux, 30-Jun-2019.) |
SubRingℂfld RRfld | ||
Theorem | resubgval 19955 | Subtraction in the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
RRfld | ||
Theorem | replusg 19956 | The addition operation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
RRfld | ||
Theorem | remulr 19957 | The multiplication operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
RRfld | ||
Theorem | re0g 19958 | The neutral element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
RRfld | ||
Theorem | re1r 19959 | The multiplicative neutral element of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
RRfld | ||
Theorem | rele2 19960 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
RRfld | ||
Theorem | relt 19961 | The ordering relation of the field of reals. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
RRfld | ||
Theorem | reds 19962 | The distance of the field of reals. (Contributed by Thierry Arnoux, 20-Jun-2019.) |
RRfld | ||
Theorem | redvr 19963 | The division operation of the field of reals. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
/rRRfld | ||
Theorem | retos 19964 | The real numbers are a totally ordered set. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
RRfld Toset | ||
Theorem | refld 19965 | The real numbers form a field. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
RRfld Field | ||
Theorem | refldcj 19966 | The conjugation operation of the field of real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
RRfld | ||
Theorem | recrng 19967 | The real numbers form a star ring. (Contributed by Thierry Arnoux, 19-Apr-2019.) |
RRfld | ||
Theorem | regsumsupp 19968* | The group sum over the real numbers, expressed as a finite sum. (Contributed by Thierry Arnoux, 22-Jun-2019.) (Proof shortened by AV, 19-Jul-2019.) |
finSupp RRfld g supp | ||
Syntax | cphl 19969 | Extend class notation with class of all pre-Hilbert spaces. |
Syntax | cipf 19970 | Extend class notation with inner product function. |
Definition | df-phl 19971* | Define the class of all pre-Hilbert spaces (inner product spaces) over arbitrary fields with involution. (Some textbook definitions are more restrictive and require the field of scalars to be the field of real or complex numbers). (Contributed by NM, 22-Sep-2011.) |
Scalar LMHom ringLMod | ||
Definition | df-ipf 19972* | Define the inner product function. Usually we will use directly instead of , and they have the same behavior in most cases. The main advantage of is that it is a guaranteed function (ipffn 19996), while only has closure (ipcl 19978). (Contributed by Mario Carneiro, 12-Aug-2015.) |
Theorem | isphl 19973* | The predicate "is a generalized pre-Hilbert (inner product) space". (Contributed by NM, 22-Sep-2011.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar LMHom ringLMod | ||
Theorem | phllvec 19974 | A pre-Hilbert space is a left vector space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
Theorem | phllmod 19975 | A pre-Hilbert space is a left module. (Contributed by Mario Carneiro, 7-Oct-2015.) |
Theorem | phlsrng 19976 | The scalar ring of a pre-Hilbert space is a star ring. (Contributed by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | phllmhm 19977* | The inner product of a pre-Hilbert space is linear in its left argument. (Contributed by Mario Carneiro, 7-Oct-2015.) |
Scalar LMHom ringLMod | ||
Theorem | ipcl 19978 | Closure of the inner product operation in a pre-Hilbert space. (Contributed by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | ipcj 19979 | Conjugate of an inner product in a pre-Hilbert space. Equation I1 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | iporthcom 19980 | Orthogonality (meaning inner product is 0) is commutative. (Contributed by NM, 17-Apr-2008.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | ip0l 19981 | Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. (Contributed by NM, 5-Feb-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | ip0r 19982 | Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | ipeq0 19983 | The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of [Kreyszig] p. 129. (Contributed by NM, 24-Jan-2008.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | ipdir 19984 | Distributive law for inner product (right-distributivity). Equation I3 of [Ponnusamy] p. 362. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | ipdi 19985 | Distributive law for inner product (left-distributivity). (Contributed by NM, 20-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | ip2di 19986 | Distributive law for inner product. (Contributed by NM, 17-Apr-2008.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | ipsubdir 19987 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | ipsubdi 19988 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | ip2subdi 19989 | Distributive law for inner product subtraction. (Contributed by Mario Carneiro, 8-Oct-2015.) |
Scalar | ||
Theorem | ipass 19990 | Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | ipassr 19991 | "Associative" law for second argument of inner product (compare ipass 19990). (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | ipassr2 19992 | "Associative" law for inner product. Conjugate version of ipassr 19991. (Contributed by NM, 25-Aug-2007.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | ipffval 19993* | The inner product operation as a function. (Contributed by Mario Carneiro, 12-Oct-2015.) |
Theorem | ipfval 19994 | The inner product operation as a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
Theorem | ipfeq 19995 | If the inner product operation is already a function, the functionalization of it is equal to the original operation. (Contributed by Mario Carneiro, 14-Aug-2015.) |
Theorem | ipffn 19996 | The inner product operation is a function. (Contributed by Mario Carneiro, 20-Sep-2015.) |
Theorem | phlipf 19997 | The inner product operation is a function. (Contributed by Mario Carneiro, 14-Aug-2015.) |
Scalar | ||
Theorem | ip2eq 19998* | Two vectors are equal iff their inner products with all other vectors are equal. (Contributed by NM, 24-Jan-2008.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Theorem | isphld 19999* | Properties that determine a pre-Hilbert (inner product) space. (Contributed by Mario Carneiro, 18-Nov-2013.) (Revised by Mario Carneiro, 7-Oct-2015.) |
Scalar | ||
Theorem | phlpropd 20000* | If two structures have the same components (properties), one is a pre-Hilbert space iff the other one is. (Contributed by Mario Carneiro, 8-Oct-2015.) |
Scalar Scalar |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |