Home | Metamath
Proof Explorer Theorem List (p. 337 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 | ismtycnv 33601 | The inverse of an isometry is an isometry. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | ismtyima 33602 | The image of a ball under an isometry is another ball. (Contributed by Jeff Madsen, 31-Jan-2014.) |
Theorem | ismtyhmeolem 33603 | Lemma for ismtyhmeo 33604. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
Theorem | ismtyhmeo 33604 | An isometry is a homeomorphism on the induced topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
Theorem | ismtybndlem 33605 | Lemma for ismtybnd 33606. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 19-Jan-2014.) |
Theorem | ismtybnd 33606 | Isometries preserve boundedness. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 19-Jan-2014.) |
Theorem | ismtyres 33607 | A restriction of an isometry is an isometry. The condition is not necessary but makes the proof easier. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 12-Sep-2015.) |
Theorem | heibor1lem 33608 | Lemma for heibor1 33609. A compact metric space is complete. This proof works by considering the collection for each , which has the finite intersection property because any finite intersection of upper integer sets is another upper integer set, so any finite intersection of the image closures will contain for some . Thus, by compactness, the intersection contains a point , which must then be the convergent point of . (Contributed by Jeff Madsen, 17-Jan-2014.) (Revised by Mario Carneiro, 5-Jun-2014.) |
Theorem | heibor1 33609 | One half of heibor 33620, that does not require any Choice. A compact metric space is complete and totally bounded. We prove completeness in cmpcmet 23116 and total boundedness here, which follows trivially from the fact that the set of all -balls is an open cover of , so finitely many cover . (Contributed by Jeff Madsen, 16-Jan-2014.) |
Theorem | heiborlem1 33610* | Lemma for heibor 33620. We work with a fixed open cover throughout. The set is the set of all subsets of that admit no finite subcover of . (We wish to prove that is empty.) If a set has no finite subcover, then any finite cover of must contain a set that also has no finite subcover. (Contributed by Jeff Madsen, 23-Jan-2014.) |
Theorem | heiborlem2 33611* | Lemma for heibor 33620. Substitutions for the set . (Contributed by Jeff Madsen, 23-Jan-2014.) |
Theorem | heiborlem3 33612* | Lemma for heibor 33620. Using countable choice ax-cc 9257, we have fixed in advance a collection of finite nets for (note that an -net is a set of points in whose -balls cover ). The set is the subset of these points whose corresponding balls have no finite subcover (i.e. in the set ). If the theorem was false, then would be in , and so some ball at each level would also be in . But we can say more than this; given a ball on level , since level covers the space and thus also , using heiborlem1 33610 there is a ball on the next level whose intersection with also has no finite subcover. Now since the set is a countable union of finite sets, it is countable (which needs ax-cc 9257 via iunctb 9396), and so we can apply ax-cc 9257 to directly to get a function from to itself, which points from each ball in to a ball on the next level in , and such that the intersection between these balls is also in . (Contributed by Jeff Madsen, 18-Jan-2014.) |
Theorem | heiborlem4 33613* | Lemma for heibor 33620. Using the function constructed in heiborlem3 33612, construct an infinite path in . (Contributed by Jeff Madsen, 23-Jan-2014.) |
Theorem | heiborlem5 33614* | Lemma for heibor 33620. The function is a set of point-and-radius pairs suitable for application to caubl 23106. (Contributed by Jeff Madsen, 23-Jan-2014.) |
Theorem | heiborlem6 33615* | Lemma for heibor 33620. Since the sequence of balls connected by the function ensures that each ball nontrivially intersects with the next (since the empty set has a finite subcover, the intersection of any two successive balls in the sequence is nonempty), and each ball is half the size of the previous one, the distance between the centers is at most times the size of the larger, and so if we expand each ball by a factor of we get a nested sequence of balls. (Contributed by Jeff Madsen, 23-Jan-2014.) |
Theorem | heiborlem7 33616* | Lemma for heibor 33620. Since the sizes of the balls decrease exponentially, the sequence converges to zero. (Contributed by Jeff Madsen, 23-Jan-2014.) |
Theorem | heiborlem8 33617* | Lemma for heibor 33620. The previous lemmas establish that the sequence is Cauchy, so using completeness we now consider the convergent point . By assumption, is an open cover, so is an element of some , and some ball centered at is contained in . But the sequence contains arbitrarily small balls close to , so some element of the sequence is contained in . And finally we arrive at a contradiction, because is a finite subcover of that covers , yet . For convenience, we write this contradiction as where is all the accumulated hypotheses and is anything at all. (Contributed by Jeff Madsen, 22-Jan-2014.) |
Theorem | heiborlem9 33618* | Lemma for heibor 33620. Discharge the hypotheses of heiborlem8 33617 by applying caubl 23106 to get a convergent point and adding the open cover assumption. (Contributed by Jeff Madsen, 20-Jan-2014.) |
Theorem | heiborlem10 33619* | Lemma for heibor 33620. The last remaining piece of the proof is to find an element such that , i.e. is an element of that has no finite subcover, which is true by heiborlem1 33610, since is a finite cover of , which has no finite subcover. Thus, the rest of the proof follows to a contradiction, and thus there must be a finite subcover of that covers , i.e. is compact. (Contributed by Jeff Madsen, 22-Jan-2014.) |
Theorem | heibor 33620 | Generalized Heine-Borel Theorem. A metric space is compact iff it is complete and totally bounded. See heibor1 33609 and heiborlem1 33610 for a description of the proof. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 28-Jan-2014.) |
Theorem | bfplem1 33621* | Lemma for bfp 33623. The sequence , which simply starts from any point in the space and iterates , satisfies the property that the distance from to decreases by at least after each step. Thus, the total distance from any to is bounded by a geometric series, and the sequence is Cauchy. Therefore, it converges to a point since the space is complete. (Contributed by Jeff Madsen, 17-Jun-2014.) |
Theorem | bfplem2 33622* | Lemma for bfp 33623. Using the point found in bfplem1 33621, we show that this convergent point is a fixed point of . Since for any positive , the sequence is in for all (where ), we have and , so is in every neighborhood of and is a fixed point of . (Contributed by Jeff Madsen, 5-Jun-2014.) |
Theorem | bfp 33623* | Banach fixed point theorem, also known as contraction mapping theorem. A contraction on a complete metric space has a unique fixed point. We show existence in the lemmas, and uniqueness here - if has two fixed points, then the distance between them is less than times itself, a contradiction. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
Syntax | crrn 33624 | Extend class notation with the n-dimensional Euclidean space. |
Definition | df-rrn 33625* | Define n-dimensional Euclidean space as a metric space with the standard Euclidean norm given by the quadratic mean. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | rrnval 33626* | The n-dimensional Euclidean space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
Theorem | rrnmval 33627* | The value of the Euclidean metric. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
Theorem | rrnmet 33628 | Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) |
Theorem | rrndstprj1 33629 | The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
Theorem | rrndstprj2 33630* | Bound on the distance between two points in Euclidean space given bounds on the distances in each coordinate. This theorem and rrndstprj1 33629 can be used to show that the supremum norm and Euclidean norm are equivalent. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
Theorem | rrncmslem 33631* | Lemma for rrncms 33632. (Contributed by Jeff Madsen, 6-Jun-2014.) (Revised by Mario Carneiro, 13-Sep-2015.) |
Theorem | rrncms 33632 | Euclidean space is complete. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) |
Theorem | repwsmet 33633 | The supremum metric on is a metric. (Contributed by Jeff Madsen, 15-Sep-2015.) |
ℂfld ↾s s | ||
Theorem | rrnequiv 33634 | The supremum metric on is equivalent to the metric. (Contributed by Jeff Madsen, 15-Sep-2015.) |
ℂfld ↾s s | ||
Theorem | rrntotbnd 33635 | A set in Euclidean space is totally bounded iff its is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 16-Sep-2015.) |
Theorem | rrnheibor 33636 | Heine-Borel theorem for Euclidean space. A subset of Euclidean space is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.) |
Theorem | ismrer1 33637* | An isometry between and . (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.) |
Theorem | reheibor 33638 | Heine-Borel theorem for real numbers. A subset of is compact iff it is closed and bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Sep-2015.) |
Theorem | iccbnd 33639 | A closed interval in is bounded. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Sep-2015.) |
Theorem | icccmpALT 33640 | A closed interval in is compact. Alternate proof of icccmp 22628 using the Heine-Borel theorem heibor 33620. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 14-Aug-2014.) (New usage is discouraged.) (Proof modification is discouraged.) |
Syntax | cass 33641 | Extend class notation with a device to add associativity to internal operations. |
Definition | df-ass 33642* | A device to add associativity to various sorts of internal operations. The definition is meaningful when is a magma at least. (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.) |
Syntax | cexid 33643 | Extend class notation with the class of all the internal operations with an identity element. |
Definition | df-exid 33644* | A device to add an identity element to various sorts of internal operations. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
Theorem | isass 33645* | The predicate "is an associative operation". (Contributed by FL, 1-Nov-2009.) (New usage is discouraged.) |
Theorem | isexid 33646* | The predicate has a left and right identity element. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
Syntax | cmagm 33647 | Extend class notation with the class of all magmas. |
Definition | df-mgmOLD 33648* | Obsolete version of df-mgm 17242 as of 3-Feb-2020. A magma is a binary internal operation. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
Theorem | ismgmOLD 33649 | Obsolete version of ismgm 17243 as of 3-Feb-2020. The predicate "is a magma". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | clmgmOLD 33650 | Obsolete version of mgmcl 17245 as of 3-Feb-2020. Closure of a magma. (Contributed by FL, 14-Sep-2010.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | opidonOLD 33651 | Obsolete version of mndpfo 17314 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | rngopidOLD 33652 | Obsolete version of mndpfo 17314 as of 23-Jan-2020. Range of an operation with a left and right identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | opidon2OLD 33653 | Obsolete version of mndpfo 17314 as of 23-Jan-2020. An operation with a left and right identity element is onto. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | isexid2 33654* | If , then it has a left and right identity element that belongs to the range of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
Theorem | exidu1 33655* | Unicity of the left and right identity element of a magma when it exists. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
Theorem | idrval 33656* | The value of the identity element. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
GId | ||
Theorem | iorlid 33657 | A magma right and left identity belongs to the underlying set of the operation. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
GId | ||
Theorem | cmpidelt 33658 | A magma right and left identity element keeps the other elements unchanged. (Contributed by FL, 12-Dec-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
GId | ||
Syntax | csem 33659 | Extend class notation with the class of all semi-groups. |
Definition | df-sgrOLD 33660 | Obsolete version of df-sgrp 17284 as of 3-Feb-2020. A semi-group is an associative magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
Theorem | smgrpismgmOLD 33661 | Obsolete version of sgrpmgm 17289 as of 3-Feb-2020. A semi-group is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | issmgrpOLD 33662* | Obsolete version of issgrp 17285 as of 3-Feb-2020. The predicate "is a semi-group". (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | smgrpmgm 33663 | A semi-group is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
Theorem | smgrpassOLD 33664* | Obsolete version of sgrpass 17290 as of 3-Feb-2020. A semi-group is associative. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
Syntax | cmndo 33665 | Extend class notation with the class of all monoids. |
MndOp | ||
Definition | df-mndo 33666 | A monoid is a semi-group with an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
MndOp | ||
Theorem | mndoissmgrpOLD 33667 | Obsolete version of mndsgrp 17299 as of 3-Feb-2020. A monoid is a semi-group. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
MndOp | ||
Theorem | mndoisexid 33668 | A monoid has an identity element. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) |
MndOp | ||
Theorem | mndoismgmOLD 33669 | Obsolete version of mndmgm 17300 as of 3-Feb-2020. A monoid is a magma. (Contributed by FL, 2-Nov-2009.) (New usage is discouraged.) (Proof modification is discouraged.) |
MndOp | ||
Theorem | mndomgmid 33670 | A monoid is a magma with an identity element. (Contributed by FL, 18-Feb-2010.) (New usage is discouraged.) |
MndOp | ||
Theorem | ismndo 33671* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
MndOp | ||
Theorem | ismndo1 33672* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
MndOp | ||
Theorem | ismndo2 33673* | The predicate "is a monoid". (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
MndOp | ||
Theorem | grpomndo 33674 | A group is a monoid. (Contributed by FL, 2-Nov-2009.) (Revised by Mario Carneiro, 22-Dec-2013.) (New usage is discouraged.) |
MndOp | ||
Theorem | exidcl 33675 | Closure of the binary operation of a magma with identity. (Contributed by Jeff Madsen, 16-Jun-2011.) |
Theorem | exidreslem 33676* | Lemma for exidres 33677 and exidresid 33678. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
GId | ||
Theorem | exidres 33677 | The restriction of a binary operation with identity to a subset containing the identity has an identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
GId | ||
Theorem | exidresid 33678 | The restriction of a binary operation with identity to a subset containing the identity has the same identity element. (Contributed by Jeff Madsen, 8-Jun-2010.) (Revised by Mario Carneiro, 23-Dec-2013.) |
GId GId | ||
Theorem | ablo4pnp 33679 | A commutative/associative law for Abelian groups. (Contributed by Jeff Madsen, 11-Jun-2010.) |
Theorem | grpoeqdivid 33680 | Two group elements are equal iff their quotient is the identity. (Contributed by Jeff Madsen, 6-Jan-2011.) |
GId | ||
Theorem | grposnOLD 33681 | The group operation for the singleton group. Obsolete, use grp1 17522. instead (Contributed by NM, 4-Nov-2006.) (New usage is discouraged.) (Proof modification is discouraged.) |
Syntax | cghomOLD 33682 | Obsolete version of cghm 17657 as of 15-Mar-2020. Extend class notation to include the class of group homomorphisms. (New usage is discouraged.) |
GrpOpHom | ||
Definition | df-ghomOLD 33683* | Obsolete version of df-ghm 17658 as of 15-Mar-2020. Define the set of group homomorphisms from to . (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) |
GrpOpHom | ||
Theorem | elghomlem1OLD 33684* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 33686. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
GrpOpHom | ||
Theorem | elghomlem2OLD 33685* | Obsolete as of 15-Mar-2020. Lemma for elghomOLD 33686. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
GrpOpHom | ||
Theorem | elghomOLD 33686* | Obsolete version of isghm 17660 as of 15-Mar-2020. Membership in the set of group homomorphisms from to . (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
GrpOpHom | ||
Theorem | ghomlinOLD 33687 | Obsolete version of ghmlin 17665 as of 15-Mar-2020. Linearity of a group homomorphism. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
GrpOpHom | ||
Theorem | ghomidOLD 33688 | Obsolete version of ghmid 17666 as of 15-Mar-2020. A group homomorphism maps identity element to identity element. (Contributed by Paul Chapman, 3-Mar-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
GId GId GrpOpHom | ||
Theorem | ghomf 33689 | Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) |
GrpOpHom | ||
Theorem | ghomco 33690 | The composition of two group homomorphisms is a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |
GrpOpHom GrpOpHom GrpOpHom | ||
Theorem | ghomdiv 33691 | Group homomorphisms preserve division. (Contributed by Jeff Madsen, 16-Jun-2011.) |
GrpOpHom | ||
Theorem | grpokerinj 33692 | A group homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.) |
GId GId GrpOpHom | ||
Syntax | crngo 33693 | Extend class notation with the class of all unital rings. |
Definition | df-rngo 33694* | Define the class of all unital rings. (Contributed by Jeff Hankins, 21-Nov-2006.) (New usage is discouraged.) |
Theorem | relrngo 33695 | The class of all unital rings is a relation. (Contributed by FL, 31-Aug-2009.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
Theorem | isrngo 33696* | The predicate "is a (unital) ring." Definition of ring with unit in [Schechter] p. 187. (Contributed by Jeff Hankins, 21-Nov-2006.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
Theorem | isrngod 33697* | Conditions that determine a ring. (Changed label from isringd 18585 to isrngod 33697-NM 2-Aug-2013.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
Theorem | rngoi 33698* | The properties of a unital ring. (Contributed by Steve Rodriguez, 8-Sep-2007.) (Proof shortened by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
Theorem | rngosm 33699 | Functionality of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 21-Dec-2013.) (New usage is discouraged.) |
Theorem | rngocl 33700 | Closure of the multiplication operation of a ring. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |