HomeTheorem List (p. 358 of 386)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 358 of 386) | < 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-26036) |
Hilbert Space Explorer
(26037-27561) |
Users' Mathboxes
(27562-38534) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | 2atmat 35701 | The meet of two intersecting lines (expressed as joins of atoms) is an atom. (Contributed by NM, 21-Nov-2012.) |
         
 ![./\](_.wedge.gif "./\"){kind=small}
      ![/\](wedge.gif "/\"){kind=small}      
| ||
| Theorem | lplncmp 35702 | If two lattice planes are comparable, they are equal. (Contributed by NM, 24-Jun-2012.) |
   
| ||
| Theorem | lplnexatN 35703* | 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 35704* | 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 35705 | Two lattice planes cannot satisfy the less than relation. (Contributed by NM, 7-Jul-2012.) |
  | ||
| Theorem | 2llnjaN 35706 | The join of two different lattice lines in a lattice plane equals the plane (version of 2llnjN 35707 in terms of atoms). (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
| ||
| Theorem | 2llnjN 35707 | 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 35708 | 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 35709 | Two lattice lines in a lattice plane always meet. (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
| ||
| Theorem | 2llnm4 35710 | Two lattice lines that majorize the same atom always meet. (Contributed by NM, 20-Jul-2012.) |
|
| ||
| Theorem | 2llnmeqat 35711 | An atom equals the intersection of two majorizing lines. (Contributed by NM, 3-Apr-2013.) |
|
| ||
| Theorem | lvolset 35712* | The set of 3-dim lattice volumes in a Hilbert lattice. (Contributed by NM, 1-Jul-2012.) |
  
    
 | ||
| Theorem | islvol 35713* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
|
| ||
| Theorem | islvol4 35714* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
|
| ||
| Theorem | lvoli 35715 | Condition implying a 3-dim lattice volume. (Contributed by NM, 1-Jul-2012.) |
| ||
| Theorem | islvol3 35716* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
| ||
| Theorem | lvoli3 35717 | Condition implying a 3-dim lattice volume. (Contributed by NM, 2-Aug-2012.) |
|
| ||
| Theorem | lvolbase 35718 | A 3-dim lattice volume is a lattice element. (Contributed by NM, 1-Jul-2012.) |
|
| ||
| Theorem | islvol5 35719* | The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012.) |
 
| ||
| Theorem | islvol2 35720* | The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012.) |
|
| ||
| Theorem | lvoli2 35721 | The join of 4 different atoms is a lattice volume. (Contributed by NM, 8-Jul-2012.) |
|
| ||
| Theorem | lvolnle3at 35722 | A lattice plane (or lattice line or atom) cannot majorize a lattice volume. (Contributed by NM, 8-Jul-2012.) |
|
| ||
| Theorem | lvolnleat 35723 | An atom cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
|
| ||
| Theorem | lvolnlelln 35724 | A lattice line cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
|
| ||
| Theorem | lvolnlelpln 35725 | A lattice plane cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
|
| ||
| Theorem | 3atnelvolN 35726 | The join of 3 atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2atnelvolN 35727 | The join of two atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | lvolneatN 35728 | No lattice volume is an atom. (Contributed by NM, 15-Jul-2012.) (New usage is discouraged.) |
| | ||
| Theorem | lvolnelln 35729 | No lattice volume is a lattice line. (Contributed by NM, 15-Jul-2012.) |
| | ||
| Theorem | lvolnelpln 35730 | No lattice volume is a lattice plane. (Contributed by NM, 19-Jun-2012.) |
| | ||
| Theorem | lvoln0N 35731 | A lattice volume is non-zero. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
| | ||
| Theorem | islvol2aN 35732 | The predicate "is a lattice volume". (Contributed by NM, 16-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 4atlem0a 35733 | Lemma for 4at 35753. (Contributed by NM, 10-Jul-2012.) |
|
| ||
| Theorem | 4atlem0ae 35734 | Lemma for 4at 35753. (Contributed by NM, 10-Jul-2012.) |
|
| ||
| Theorem | 4atlem0be 35735 | Lemma for 4at 35753. (Contributed by NM, 10-Jul-2012.) |
|
| ||
| Theorem | 4atlem3 35736 | Lemma for 4at 35753. Break inequality into 4 cases. (Contributed by NM, 8-Jul-2012.) |
| ||
| Theorem | 4atlem3a 35737 | Lemma for 4at 35753. Break inequality into 3 cases. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem3b 35738 | Lemma for 4at 35753. Break inequality into 2 cases. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem4a 35739 | Lemma for 4at 35753. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem4b 35740 | Lemma for 4at 35753. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem4c 35741 | Lemma for 4at 35753. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem4d 35742 | Lemma for 4at 35753. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem9 35743 |
Lemma for 4at 35753. Substitute for . (Contributed by NM,
9-Jul-2012.)
|
|
| ||
| Theorem | 4atlem10a 35744 |
Lemma for 4at 35753. Substitute for . (Contributed by NM,
9-Jul-2012.)
|
|
| ||
| Theorem | 4atlem10b 35745 |
Lemma for 4at 35753. Substitute for (cont.). (Contributed by
NM, 10-Jul-2012.)
|
|
| ||
| Theorem | 4atlem10 35746 | Lemma for 4at 35753. Combine both possible cases. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem11a 35747 |
Lemma for 4at 35753. Substitute for . (Contributed by NM,
9-Jul-2012.)
|
|
| ||
| Theorem | 4atlem11b 35748 |
Lemma for 4at 35753. Substitute for (cont.). (Contributed by
NM, 10-Jul-2012.)
|
|
| ||
| Theorem | 4atlem11 35749 | Lemma for 4at 35753. Combine all three possible cases. (Contributed by NM, 10-Jul-2012.) |
|
| ||
| Theorem | 4atlem12a 35750 |
Lemma for 4at 35753. Substitute for . (Contributed by NM,
9-Jul-2012.)
|
|
| ||
| Theorem | 4atlem12b 35751 |
Lemma for 4at 35753. Substitute for (cont.). (Contributed by
NM, 11-Jul-2012.)
|
|
| ||
| Theorem | 4atlem12 35752 | Lemma for 4at 35753. Combine all four possible cases. (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | 4at 35753 | Four atoms determine a lattice volume uniquely. Three-dimensional analog of ps-1 35617 and 3at 35630. (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | 4at2 35754 | Four atoms determine a lattice volume uniquely. (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | lplncvrlvol2 35755 | A lattice line under a lattice plane is covered by it. (Contributed by NM, 12-Jul-2012.) |
| | ||
| Theorem | lplncvrlvol 35756 | An element covering a lattice plane is a lattice volume and vice-versa. (Contributed by NM, 15-Jul-2012.) |
|
| ||
| Theorem | lvolcmp 35757 | If two lattice planes are comparable, they are equal. (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | lvolnltN 35758 | Two lattice volumes cannot satisfy the less than relation. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
| | ||
| Theorem | 2lplnja 35759 | The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 35760 in terms of atoms). (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | 2lplnj 35760 | The join of two different lattice planes in a (3-dimensional) lattice volume equals the volume. (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | 2lplnm2N 35761 | The meet of two different lattice planes in a lattice volume is a lattice line. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2lplnmj 35762 | The meet of two lattice planes is a lattice line iff their join is a lattice volume. (Contributed by NM, 13-Jul-2012.) |
|
| ||
| Theorem | dalemkehl 35763 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 
| ||
| Theorem | dalemkelat 35764 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 | ||
| Theorem | dalemkeop 35765 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 | ||
| Theorem | dalempea 35766 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqea 35767 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemrea 35768 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemsea 35769 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemtea 35770 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemuea 35771 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemyeo 35772 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemzeo 35773 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclpjs 35774 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclqjt 35775 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclrju 35776 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalem-clpjq 35777 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemceb 35778 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempeb 35779 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqeb 35780 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemreb 35781 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemseb 35782 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemteb 35783 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemueb 35784 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempjqeb 35785 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemsjteb 35786 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemtjueb 35787 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqrprot 35788 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemyeb 35789 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemcnes 35790 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempnes 35791 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqnet 35792 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempjsen 35793 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemply 35794 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemsly 35795 | Lemma for dath 35876. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemswapyz 35796 |
Lemma for dath 35876. Swap the role of planes and to allow
reuse of analogous proofs. (Contributed by NM, 14-Aug-2012.)
|
|
| ||
| Theorem | dalemrot 35797 |
Lemma for dath 35876. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
14-Aug-2012.)
|
|
| ||
| Theorem | dalemrotyz 35798 |
Lemma for dath 35876. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
19-Aug-2012.)
|
|
| ||
| Theorem | dalem1 35799 |
Lemma for dath 35876. Show the lines and are different.
(Contributed by NM, 9-Aug-2012.)
|
|
| ||
| Theorem | dalemcea 35800 |
Lemma for dath 35876. Frequently-used utility lemma. Here we
show that
must be an
atom. This is an assumption in most presentations of
Desargue's theorem; instead, we assume only the is a lattice
element, in order to make later substitutions for easier.
(Contributed by NM, 23-Sep-2012.)
|
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |