Home | Metamath
Proof Explorer Theorem List (p. 349 of 357) | < 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-24325) |
Hilbert Space Explorer
(24326-25850) |
Users' Mathboxes
(25851-35622) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dibelval1st2N 34801 | Membership in value of the partial isomorphism B for a lattice . (Contributed by NM, 13-Feb-2014.) (New usage is discouraged.) |
Theorem | dibelval2nd 34802* | Membership in value of the partial isomorphism B for a lattice . (Contributed by NM, 13-Feb-2014.) |
Theorem | dibn0 34803 | The value of the partial isomorphism B is not empty. (Contributed by NM, 18-Jan-2014.) |
Theorem | dibfna 34804 | Functionality and domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) |
Theorem | dibdiadm 34805 | Domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) |
Theorem | dibfnN 34806* | Functionality and domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
Theorem | dibdmN 34807* | Domain of the partial isomorphism A. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
Theorem | dibeldmN 34808 | Member of domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
Theorem | dibord 34809 | The isomorphism B for a lattice is order-preserving in the region under co-atom . (Contributed by NM, 24-Feb-2014.) |
Theorem | dib11N 34810 | The isomorphism B for a lattice is one-to-one in the region under co-atom . (Contributed by NM, 24-Feb-2014.) (New usage is discouraged.) |
Theorem | dibf11N 34811 | The partial isomorphism A for a lattice is a one-to-one function. Part of Lemma M of [Crawley] p. 120 line 27. (Contributed by NM, 4-Dec-2013.) (New usage is discouraged.) |
Theorem | dibclN 34812 | Closure of partial isomorphism B for a lattice . (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
Theorem | dibvalrel 34813 | The value of partial isomorphism B is a relation. (Contributed by NM, 8-Mar-2014.) |
Theorem | dib0 34814 | The value of partial isomorphism B at the lattice zero is the singleton of the zero vector i.e. the zero subspace. (Contributed by NM, 27-Mar-2014.) |
Theorem | dib1dim 34815* | Two expressions for the 1-dimensional subspaces of vector space H. (Contributed by NM, 24-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
Theorem | dibglbN 34816* | Partial isomorphism B of a lattice glb. (Contributed by NM, 9-Mar-2014.) (New usage is discouraged.) |
Theorem | dibintclN 34817 | The intersection of partial isomorphism B closed subspaces is a closed subspace. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
Theorem | dib1dim2 34818* | Two expressions for a 1-dimensional subspace of vector space H (when is a nonzero vector i.e. non-identity translation). (Contributed by NM, 24-Feb-2014.) |
Theorem | dibss 34819 | The partial isomorphism B maps to a set of vectors in full vector space H. (Contributed by NM, 1-Jan-2014.) |
Theorem | diblss 34820 | The value of partial isomorphism B is a subspace of partial vector space H. TODO: use dib* specific theorems instead of dia* ones to shorten proof? (Contributed by NM, 11-Feb-2014.) |
Theorem | diblsmopel 34821* | Membership in subspace sum for partial isomorphism B. (Contributed by NM, 21-Sep-2014.) (Revised by Mario Carneiro, 6-May-2015.) |
Syntax | cdic 34822 | Extend class notation with isomorphism C. |
Definition | df-dic 34823* | Isomorphism C has domain of lattice atoms that are not less than or equal to the fiducial co-atom . The value is a one-dimensional subspace generated by the pair consisting of the vector below and the endomorphism ring unit. Definition of phi(q) in [Crawley] p. 121. Note that we use the fixed atom k ) to represent the p in their "Choose an atom p..." on line 21. (Contributed by NM, 15-Dec-2013.) |
Theorem | dicffval 34824* | The partial isomorphism C for a lattice . (Contributed by NM, 15-Dec-2013.) |
Theorem | dicfval 34825* | The partial isomorphism C for a lattice . (Contributed by NM, 15-Dec-2013.) |
Theorem | dicval 34826* | The partial isomorphism C for a lattice . (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 22-Sep-2015.) |
Theorem | dicopelval 34827* | Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 15-Feb-2014.) |
Theorem | dicelvalN 34828* | Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 25-Feb-2014.) (New usage is discouraged.) |
Theorem | dicval2 34829* | The partial isomorphism C for a lattice . (Contributed by NM, 20-Feb-2014.) |
Theorem | dicelval3 34830* | Member of the partial isomorphism C. (Contributed by NM, 26-Feb-2014.) |
Theorem | dicopelval2 34831* | Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 20-Feb-2014.) |
Theorem | dicelval2N 34832* | Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 25-Feb-2014.) (New usage is discouraged.) |
Theorem | dicfnN 34833* | Functionality and domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
Theorem | dicdmN 34834* | Domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
Theorem | dicvalrelN 34835 | The value of partial isomorphism C is a relation. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
Theorem | dicssdvh 34836 | The partial isomorphism C maps to a set of vectors in full vector space H. (Contributed by NM, 19-Jan-2014.) |
Theorem | dicelval1sta 34837* | Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 16-Feb-2014.) |
Theorem | dicelval1stN 34838 | Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 16-Feb-2014.) (New usage is discouraged.) |
Theorem | dicelval2nd 34839 | Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 16-Feb-2014.) |
Theorem | dicvaddcl 34840 | Membership in value of the partial isomorphism C is closed under vector sum. (Contributed by NM, 16-Feb-2014.) |
Theorem | dicvscacl 34841 | Membership in value of the partial isomorphism C is closed under scalar product. (Contributed by NM, 16-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
Theorem | dicn0 34842 | The value of the partial isomorphism C is not empty. (Contributed by NM, 15-Feb-2014.) |
Theorem | diclss 34843 | The value of partial isomorphism C is a subspace of partial vector space H. (Contributed by NM, 16-Feb-2014.) |
Theorem | diclspsn 34844* | The value of isomorphism C is spanned by vector . Part of proof of Lemma N of [Crawley] p. 121 line 29. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
Theorem | cdlemn2 34845* | Part of proof of Lemma N of [Crawley] p. 121 line 30. (Contributed by NM, 21-Feb-2014.) |
Theorem | cdlemn2a 34846* | Part of proof of Lemma N of [Crawley] p. 121. (Contributed by NM, 24-Feb-2014.) |
Theorem | cdlemn3 34847* | Part of proof of Lemma N of [Crawley] p. 121 line 31. (Contributed by NM, 21-Feb-2014.) |
Theorem | cdlemn4 34848* | Part of proof of Lemma N of [Crawley] p. 121 line 31. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
Theorem | cdlemn4a 34849* | Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 24-Feb-2014.) |
Theorem | cdlemn5pre 34850* | Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.) |
Theorem | cdlemn5 34851 | Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.) |
Theorem | cdlemn6 34852* | Part of proof of Lemma N of [Crawley] p. 121 line 35. (Contributed by NM, 26-Feb-2014.) |
Theorem | cdlemn7 34853* | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.) |
Theorem | cdlemn8 34854* | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.) |
Theorem | cdlemn9 34855* | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.) |
Theorem | cdlemn10 34856 | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.) |
Theorem | cdlemn11a 34857* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
Theorem | cdlemn11b 34858* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
Theorem | cdlemn11c 34859* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
Theorem | cdlemn11pre 34860* | Part of proof of Lemma N of [Crawley] p. 121 line 37. TODO: combine cdlemn11a 34857, cdlemn11b 34858, cdlemn11c 34859, cdlemn11pre into one? (Contributed by NM, 27-Feb-2014.) |
Theorem | cdlemn11 34861 | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
Theorem | cdlemn 34862 | Lemma N of [Crawley] p. 121 line 27. (Contributed by NM, 27-Feb-2014.) |
Theorem | dihordlem6 34863* | Part of proof of Lemma N of [Crawley] p. 122 line 35. (Contributed by NM, 3-Mar-2014.) |
Theorem | dihordlem7 34864* | Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
Theorem | dihordlem7b 34865* | Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
Theorem | dihjustlem 34866 | Part of proof after Lemma N of [Crawley] p. 122 line 4, "the definition of phi(x) is independent of the atom q." (Contributed by NM, 2-Mar-2014.) |
Theorem | dihjust 34867 | Part of proof after Lemma N of [Crawley] p. 122 line 4, "the definition of phi(x) is independent of the atom q." (Contributed by NM, 2-Mar-2014.) |
Theorem | dihord1 34868 | Part of proof after Lemma N of [Crawley] p. 122. Forward ordering property. TODO: change to using lhpmcvr3 33674, here and all theorems below. (Contributed by NM, 2-Mar-2014.) |
Theorem | dihord2a 34869 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
Theorem | dihord2b 34870 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
Theorem | dihord2cN 34871* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. TODO: needed? shorten other proof with it? (Contributed by NM, 3-Mar-2014.) (New usage is discouraged.) |
Theorem | dihord11b 34872* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
Theorem | dihord10 34873* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
Theorem | dihord11c 34874* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
Theorem | dihord2pre 34875* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
Theorem | dihord2pre2 34876* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 4-Mar-2014.) |
Theorem | dihord2 34877 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. Todo: do we need and ? (Contributed by NM, 4-Mar-2014.) |
Syntax | cdih 34878 | Extend class notation with isomorphism H. |
Definition | df-dih 34879* | Define isomorphism H. (Contributed by NM, 28-Jan-2014.) |
Theorem | dihffval 34880* | The isomorphism H for a lattice . Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 28-Jan-2014.) |
Theorem | dihfval 34881* | Isomorphism H for a lattice . Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 28-Jan-2014.) |
Theorem | dihval 34882* | Value of isomorphism H for a lattice . Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 3-Feb-2014.) |
Theorem | dihvalc 34883* | Value of isomorphism H for a lattice when . (Contributed by NM, 4-Mar-2014.) |
Theorem | dihlsscpre 34884 | Closure of isomorphism H for a lattice when . (Contributed by NM, 6-Mar-2014.) |
Theorem | dihvalcqpre 34885 | Value of isomorphism H for a lattice when , given auxiliary atom . (Contributed by NM, 6-Mar-2014.) |
Theorem | dihvalcq 34886 | Value of isomorphism H for a lattice when , given auxiliary atom . TODO: Use dihvalcq2 34897 (with lhpmcvr3 33674 for simplification) that changes and to and make this obsolete. Do to other theorems as well. (Contributed by NM, 6-Mar-2014.) |
Theorem | dihvalb 34887 | Value of isomorphism H for a lattice when . (Contributed by NM, 4-Mar-2014.) |
Theorem | dihopelvalbN 34888* | Ordered pair member of the partial isomorphism H for argument under . (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
Theorem | dihvalcqat 34889 | Value of isomorphism H for a lattice at an atom not under . (Contributed by NM, 27-Mar-2014.) |
Theorem | dih1dimb 34890* | Two expressions for a 1-dimensional subspace of vector space H (when is a nonzero vector i.e. non-identity translation). (Contributed by NM, 27-Apr-2014.) |
Theorem | dih1dimb2 34891* | Isomorphism H at an atom under . (Contributed by NM, 27-Apr-2014.) |
Theorem | dih1dimc 34892* | Isomorphism H at an atom not under . (Contributed by NM, 27-Apr-2014.) |
Theorem | dib2dim 34893 | Extend dia2dim 34727 to partial isomorphism B. (Contributed by NM, 22-Sep-2014.) |
Theorem | dih2dimb 34894 | Extend dib2dim 34893 to isomorphism H. (Contributed by NM, 22-Sep-2014.) |
Theorem | dih2dimbALTN 34895 | Extend dia2dim 34727 to isomorphism H. (This version combines dib2dim 34893 and dih2dimb 34894 for shorter overall proof, but may be less easy to understand. TODO: decide which to use.) (Contributed by NM, 22-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | dihopelvalcqat 34896* | Ordered pair member of the partial isomorphism H for atom argument not under . TODO: remove .t hypothesis. (Contributed by NM, 30-Mar-2014.) |
Theorem | dihvalcq2 34897 | Value of isomorphism H for a lattice when , given auxiliary atom . (Contributed by NM, 26-Sep-2014.) |
Theorem | dihopelvalcpre 34898* | Member of value of isomorphism H for a lattice when , given auxiliary atom . TODO: refactor to be shorter and more understandable; add lemmas? (Contributed by NM, 13-Mar-2014.) |
Theorem | dihopelvalc 34899* | Member of value of isomorphism H for a lattice when , given auxiliary atom . (Contributed by NM, 13-Mar-2014.) |
Theorem | dihlss 34900 | The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014.) |
< Previous Next > |