Home | Metamath
Proof Explorer Theorem List (p. 349 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 | 2atneat 34801 | The join of two distinct atoms is not an atom. (Contributed by NM, 12-Oct-2012.) |
Theorem | llnn0 34802 | A lattice line is nonzero. (Contributed by NM, 15-Jul-2012.) |
Theorem | islln2a 34803 | The predicate "is a lattice line" in terms of atoms. (Contributed by NM, 15-Jul-2012.) |
Theorem | llnle 34804* | Any element greater than 0 and not an atom majorizes a lattice line. (Contributed by NM, 28-Jun-2012.) |
Theorem | atcvrlln2 34805 | An atom under a line is covered by it. (Contributed by NM, 2-Jul-2012.) |
Theorem | atcvrlln 34806 | An element covering an atom is a lattice line and vice-versa. (Contributed by NM, 18-Jun-2012.) |
Theorem | llnexatN 34807* | Given an atom on a line, there is another atom whose join equals the line. (Contributed by NM, 26-Jun-2012.) (New usage is discouraged.) |
Theorem | llncmp 34808 | If two lattice lines are comparable, they are equal. (Contributed by NM, 19-Jun-2012.) |
Theorem | llnnlt 34809 | Two lattice lines cannot satisfy the less than relation. (Contributed by NM, 26-Jun-2012.) |
Theorem | 2llnmat 34810 | Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012.) |
Theorem | 2at0mat0 34811 | Special case of 2atmat0 34812 where one atom could be zero. (Contributed by NM, 30-May-2013.) |
Theorem | 2atmat0 34812 | The meet of two unequal lines (expressed as joins of atoms) is an atom or zero. (Contributed by NM, 2-Dec-2012.) |
Theorem | 2atm 34813 | An atom majorized by two different atom joins (which could be atoms or lines) is equal to their intersection. (Contributed by NM, 30-Jun-2013.) |
Theorem | ps-2c 34814 | Variation of projective geometry axiom ps-2 34764. (Contributed by NM, 3-Jul-2012.) |
Theorem | lplnset 34815* | The set of lattice planes in a Hilbert lattice. (Contributed by NM, 16-Jun-2012.) |
Theorem | islpln 34816* | The predicate "is a lattice plane". (Contributed by NM, 16-Jun-2012.) |
Theorem | islpln4 34817* | The predicate "is a lattice plane". (Contributed by NM, 17-Jun-2012.) |
Theorem | lplni 34818 | Condition implying a lattice plane. (Contributed by NM, 20-Jun-2012.) |
Theorem | islpln3 34819* | The predicate "is a lattice plane". (Contributed by NM, 17-Jun-2012.) |
Theorem | lplnbase 34820 | A lattice plane is a lattice element. (Contributed by NM, 17-Jun-2012.) |
Theorem | islpln5 34821* | The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 24-Jun-2012.) |
Theorem | islpln2 34822* | The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 25-Jun-2012.) |
Theorem | lplni2 34823 | The join of 3 different atoms is a lattice plane. (Contributed by NM, 4-Jul-2012.) |
Theorem | lvolex3N 34824* | There is an atom outside of a lattice plane i.e. a 3-dimensional lattice volume exists. (Contributed by NM, 28-Jul-2012.) (New usage is discouraged.) |
Theorem | llnmlplnN 34825 | The intersection of a line with a plane not containing it is an atom. (Contributed by NM, 29-Jun-2012.) (New usage is discouraged.) |
Theorem | lplnle 34826* | Any element greater than 0 and not an atom and not a lattice line majorizes a lattice plane. (Contributed by NM, 28-Jun-2012.) |
Theorem | lplnnle2at 34827 | A lattice line (or atom) cannot majorize a lattice plane. (Contributed by NM, 8-Jul-2012.) |
Theorem | lplnnleat 34828 | A lattice plane cannot majorize an atom. (Contributed by NM, 14-Jul-2012.) |
Theorem | lplnnlelln 34829 | A lattice plane is not less than or equal to a lattice line. (Contributed by NM, 14-Jul-2012.) |
Theorem | 2atnelpln 34830 | The join of two atoms is not a lattice plane. (Contributed by NM, 16-Jul-2012.) |
Theorem | lplnneat 34831 | No lattice plane is an atom. (Contributed by NM, 15-Jul-2012.) |
Theorem | lplnnelln 34832 | No lattice plane is a lattice line. (Contributed by NM, 19-Jun-2012.) |
Theorem | lplnn0N 34833 | A lattice plane is nonzero. (Contributed by NM, 15-Jul-2012.) (New usage is discouraged.) |
Theorem | islpln2a 34834 | The predicate "is a lattice plane" for join of atoms. (Contributed by NM, 16-Jul-2012.) |
Theorem | islpln2ah 34835 | The predicate "is a lattice plane" for join of atoms. Version of islpln2a 34834 expressed with an abbreviation hypothesis. (Contributed by NM, 30-Jul-2012.) |
Theorem | lplnriaN 34836 | Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012.) (New usage is discouraged.) |
Theorem | lplnribN 34837 | Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012.) (New usage is discouraged.) |
Theorem | lplnric 34838 | Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012.) |
Theorem | lplnri1 34839 | Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012.) |
Theorem | lplnri2N 34840 | Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012.) (New usage is discouraged.) |
Theorem | lplnri3N 34841 | Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012.) (New usage is discouraged.) |
Theorem | lplnllnneN 34842 | Two lattice lines defined by atoms defining a lattice plane are not equal. (Contributed by NM, 9-Oct-2012.) (New usage is discouraged.) |
Theorem | llncvrlpln2 34843 | A lattice line under a lattice plane is covered by it. (Contributed by NM, 24-Jun-2012.) |
Theorem | llncvrlpln 34844 | An element covering a lattice line is a lattice plane and vice-versa. (Contributed by NM, 26-Jun-2012.) |
Theorem | 2lplnmN 34845 | If the join of two lattice planes covers one of them, their meet is a lattice line. (Contributed by NM, 30-Jun-2012.) (New usage is discouraged.) |
Theorem | 2llnmj 34846 | The meet of two lattice lines is an atom iff their join is a lattice plane. (Contributed by NM, 27-Jun-2012.) |
Theorem | 2atmat 34847 | The meet of two intersecting lines (expressed as joins of atoms) is an atom. (Contributed by NM, 21-Nov-2012.) |
Theorem | lplncmp 34848 | If two lattice planes are comparable, they are equal. (Contributed by NM, 24-Jun-2012.) |
Theorem | lplnexatN 34849* | Given a lattice line on a lattice plane, there is an atom whose join with the line equals the plane. (Contributed by NM, 29-Jun-2012.) (New usage is discouraged.) |
Theorem | lplnexllnN 34850* | Given an atom on a lattice plane, there is a lattice line whose join with the atom equals the plane. (Contributed by NM, 26-Jun-2012.) (New usage is discouraged.) |
Theorem | lplnnlt 34851 | Two lattice planes cannot satisfy the less than relation. (Contributed by NM, 7-Jul-2012.) |
Theorem | 2llnjaN 34852 | The join of two different lattice lines in a lattice plane equals the plane (version of 2llnjN 34853 in terms of atoms). (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
Theorem | 2llnjN 34853 | The join of two different lattice lines in a lattice plane equals the plane. (Contributed by NM, 4-Jul-2012.) (New usage is discouraged.) |
Theorem | 2llnm2N 34854 | The meet of two different lattice lines in a lattice plane is an atom. (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
Theorem | 2llnm3N 34855 | Two lattice lines in a lattice plane always meet. (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
Theorem | 2llnm4 34856 | Two lattice lines that majorize the same atom always meet. (Contributed by NM, 20-Jul-2012.) |
Theorem | 2llnmeqat 34857 | An atom equals the intersection of two majorizing lines. (Contributed by NM, 3-Apr-2013.) |
Theorem | lvolset 34858* | The set of 3-dim lattice volumes in a Hilbert lattice. (Contributed by NM, 1-Jul-2012.) |
Theorem | islvol 34859* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
Theorem | islvol4 34860* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
Theorem | lvoli 34861 | Condition implying a 3-dim lattice volume. (Contributed by NM, 1-Jul-2012.) |
Theorem | islvol3 34862* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
Theorem | lvoli3 34863 | Condition implying a 3-dim lattice volume. (Contributed by NM, 2-Aug-2012.) |
Theorem | lvolbase 34864 | A 3-dim lattice volume is a lattice element. (Contributed by NM, 1-Jul-2012.) |
Theorem | islvol5 34865* | The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012.) |
Theorem | islvol2 34866* | The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012.) |
Theorem | lvoli2 34867 | The join of 4 different atoms is a lattice volume. (Contributed by NM, 8-Jul-2012.) |
Theorem | lvolnle3at 34868 | A lattice plane (or lattice line or atom) cannot majorize a lattice volume. (Contributed by NM, 8-Jul-2012.) |
Theorem | lvolnleat 34869 | An atom cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
Theorem | lvolnlelln 34870 | A lattice line cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
Theorem | lvolnlelpln 34871 | A lattice plane cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
Theorem | 3atnelvolN 34872 | The join of 3 atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
Theorem | 2atnelvolN 34873 | The join of two atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
Theorem | lvolneatN 34874 | No lattice volume is an atom. (Contributed by NM, 15-Jul-2012.) (New usage is discouraged.) |
Theorem | lvolnelln 34875 | No lattice volume is a lattice line. (Contributed by NM, 15-Jul-2012.) |
Theorem | lvolnelpln 34876 | No lattice volume is a lattice plane. (Contributed by NM, 19-Jun-2012.) |
Theorem | lvoln0N 34877 | A lattice volume is nonzero. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
Theorem | islvol2aN 34878 | The predicate "is a lattice volume". (Contributed by NM, 16-Jul-2012.) (New usage is discouraged.) |
Theorem | 4atlem0a 34879 | Lemma for 4at 34899. (Contributed by NM, 10-Jul-2012.) |
Theorem | 4atlem0ae 34880 | Lemma for 4at 34899. (Contributed by NM, 10-Jul-2012.) |
Theorem | 4atlem0be 34881 | Lemma for 4at 34899. (Contributed by NM, 10-Jul-2012.) |
Theorem | 4atlem3 34882 | Lemma for 4at 34899. Break inequality into 4 cases. (Contributed by NM, 8-Jul-2012.) |
Theorem | 4atlem3a 34883 | Lemma for 4at 34899. Break inequality into 3 cases. (Contributed by NM, 9-Jul-2012.) |
Theorem | 4atlem3b 34884 | Lemma for 4at 34899. Break inequality into 2 cases. (Contributed by NM, 9-Jul-2012.) |
Theorem | 4atlem4a 34885 | Lemma for 4at 34899. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
Theorem | 4atlem4b 34886 | Lemma for 4at 34899. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
Theorem | 4atlem4c 34887 | Lemma for 4at 34899. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
Theorem | 4atlem4d 34888 | Lemma for 4at 34899. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
Theorem | 4atlem9 34889 | Lemma for 4at 34899. Substitute for . (Contributed by NM, 9-Jul-2012.) |
Theorem | 4atlem10a 34890 | Lemma for 4at 34899. Substitute for . (Contributed by NM, 9-Jul-2012.) |
Theorem | 4atlem10b 34891 | Lemma for 4at 34899. Substitute for (cont.). (Contributed by NM, 10-Jul-2012.) |
Theorem | 4atlem10 34892 | Lemma for 4at 34899. Combine both possible cases. (Contributed by NM, 9-Jul-2012.) |
Theorem | 4atlem11a 34893 | Lemma for 4at 34899. Substitute for . (Contributed by NM, 9-Jul-2012.) |
Theorem | 4atlem11b 34894 | Lemma for 4at 34899. Substitute for (cont.). (Contributed by NM, 10-Jul-2012.) |
Theorem | 4atlem11 34895 | Lemma for 4at 34899. Combine all three possible cases. (Contributed by NM, 10-Jul-2012.) |
Theorem | 4atlem12a 34896 | Lemma for 4at 34899. Substitute for . (Contributed by NM, 9-Jul-2012.) |
Theorem | 4atlem12b 34897 | Lemma for 4at 34899. Substitute for (cont.). (Contributed by NM, 11-Jul-2012.) |
Theorem | 4atlem12 34898 | Lemma for 4at 34899. Combine all four possible cases. (Contributed by NM, 11-Jul-2012.) |
Theorem | 4at 34899 | Four atoms determine a lattice volume uniquely. Three-dimensional analogue of ps-1 34763 and 3at 34776. (Contributed by NM, 11-Jul-2012.) |
Theorem | 4at2 34900 | Four atoms determine a lattice volume uniquely. (Contributed by NM, 11-Jul-2012.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |