HomeTheorem List (p. 350 of 426)
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. 350 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 | lplncvrlvol2 34901 | A lattice line under a lattice plane is covered by it. (Contributed by NM, 12-Jul-2012.) |
                  ![/\](wedge.gif "/\"){kind=small}    | ||
| Theorem | lplncvrlvol 34902 | An element covering a lattice plane is a lattice volume and vice-versa. (Contributed by NM, 15-Jul-2012.) |
 
 | ||
| Theorem | lvolcmp 34903 | If two lattice planes are comparable, they are equal. (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | lvolnltN 34904 | Two lattice volumes cannot satisfy the less than relation. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
   | ||
| Theorem | 2lplnja 34905 | The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 34906 in terms of atoms). (Contributed by NM, 12-Jul-2012.) |
   
   
| ||
| Theorem | 2lplnj 34906 | The join of two different lattice planes in a (3-dimensional) lattice volume equals the volume. (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | 2lplnm2N 34907 | 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.) |
![./\](_.wedge.gif "./\"){kind=small}   
| ||
| Theorem | 2lplnmj 34908 | 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 34909 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 
| ||
| Theorem | dalemkelat 34910 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 | ||
| Theorem | dalemkeop 34911 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 | ||
| Theorem | dalempea 34912 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqea 34913 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemrea 34914 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemsea 34915 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemtea 34916 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemuea 34917 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemyeo 34918 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemzeo 34919 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclpjs 34920 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclqjt 34921 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclrju 34922 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalem-clpjq 34923 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemceb 34924 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempeb 34925 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqeb 34926 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemreb 34927 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemseb 34928 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemteb 34929 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemueb 34930 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempjqeb 34931 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemsjteb 34932 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemtjueb 34933 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqrprot 34934 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemyeb 34935 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemcnes 34936 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempnes 34937 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqnet 34938 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempjsen 34939 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemply 34940 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemsly 34941 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemswapyz 34942 |
Lemma for dath 35022. Swap the role of planes and to allow
reuse of analogous proofs. (Contributed by NM, 14-Aug-2012.)
|
|
| ||
| Theorem | dalemrot 34943 |
Lemma for dath 35022. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
14-Aug-2012.)
|
|
| ||
| Theorem | dalemrotyz 34944 |
Lemma for dath 35022. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
19-Aug-2012.)
|
|
| ||
| Theorem | dalem1 34945 |
Lemma for dath 35022. Show the lines and are different.
(Contributed by NM, 9-Aug-2012.)
|
|
| ||
| Theorem | dalemcea 34946 |
Lemma for dath 35022. 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.)
|
|
| ||
| Theorem | dalem2 34947 |
Lemma for dath 35022. Show the lines and form a plane.
(Contributed by NM, 11-Aug-2012.)
|
|
| ||
| Theorem | dalemdea 34948 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 11-Aug-2012.) |
| ||
| Theorem | dalemeea 34949 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 11-Aug-2012.) |
| ||
| Theorem | dalem3 34950 | Lemma for dalemdnee 34952. (Contributed by NM, 10-Aug-2012.) |
|
| ||
| Theorem | dalem4 34951 | Lemma for dalemdnee 34952. (Contributed by NM, 10-Aug-2012.) |
|
| ||
| Theorem | dalemdnee 34952 |
Lemma for dath 35022. Axis of perspectivity points and are
different. (Contributed by NM, 10-Aug-2012.)
|
|
| ||
| Theorem | dalem5 34953 |
Lemma for dath 35022. Atom (in plane ) belongs to
the 3-dimensional volume formed by and . (Contributed by
NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem6 34954 |
Lemma for dath 35022. Analogue of dalem5 34953 for . (Contributed by
NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem7 34955 |
Lemma for dath 35022. Analogue of dalem5 34953 for . (Contributed by
NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem8 34956 |
Lemma for dath 35022. Plane belongs to the 3-dimensional space.
(Contributed by NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem-cly 34957 |
Lemma for dalem9 34958. Center of perspectivity is not in plane
(when and are different planes). (Contributed by
NM, 13-Aug-2012.)
|
|
| ||
| Theorem | dalem9 34958 |
Lemma for dath 35022. Since
, the join forms
a 3-dimensional space. (Contributed by NM, 20-Jul-2012.)
|
|
| ||
| Theorem | dalem10 34959 |
Lemma for dath 35022. Atom belongs to the axis of perspectivity
.
(Contributed by NM, 19-Jul-2012.)
|
|
| ||
| Theorem | dalem11 34960 |
Lemma for dath 35022. Analogue of dalem10 34959 for . (Contributed by
NM, 23-Jul-2012.)
|
|
| ||
| Theorem | dalem12 34961 |
Lemma for dath 35022. Analogue of dalem10 34959 for  . (Contributed by
NM, 11-Aug-2012.)
|
|
| ||
| Theorem | dalem13 34962 | Lemma for dalem14 34963. (Contributed by NM, 21-Jul-2012.) |
|
| ||
| Theorem | dalem14 34963 |
Lemma for dath 35022. Planes and form a 3-dimensional space
(when they are different). (Contributed by NM, 22-Jul-2012.)
|
|
| ||
| Theorem | dalem15 34964 |
Lemma for dath 35022. The axis of perspectivity is a line.
(Contributed by NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem16 34965 |
Lemma for dath 35022. The atoms , , and form
a line of
perspectivity. This is Desargue's Theorem for the special case where
planes and
are different.
(Contributed by NM,
7-Aug-2012.)
|
|
| ||
| Theorem | dalem17 34966 |
Lemma for dath 35022. When planes and are equal, the center
of perspectivity is in .
(Contributed by NM,
1-Aug-2012.)
|
|
| ||
| Theorem | dalem18 34967* |
Lemma for dath 35022. Show that a dummy atom  exists outside of the
and planes (when those planes
are equal). This requires
that the projective space be 3-dimensional. (Desargue's theorem
doesn't always hold in 2 dimensions.) (Contributed by NM,
29-Jul-2012.)
|
| ||
| Theorem | dalem19 34968* |
Lemma for dath 35022. Show that a second dummy atom  exists outside
of the and
planes (when those
planes are equal).
(Contributed by NM, 15-Aug-2012.)
|
|
| ||
| Theorem | dalemccea 34969 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
| ||
| Theorem | dalemddea 34970 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalem-ccly 34971 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalem-ddly 34972 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemccnedd 34973 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemclccjdd 34974 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemcceb 34975 | Lemma for dath 35022. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemswapyzps 34976 |
Lemma for dath 35022. Swap the and planes, along with dummy
concurrency (center of perspectivity) atoms and , to allow
reuse of analogous proofs. (Contributed by NM, 17-Aug-2012.)
|
|
| ||
| Theorem | dalemrotps 34977 |
Lemma for dath 35022. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
15-Aug-2012.)
|
|
| ||
| Theorem | dalemcjden 34978 | Lemma for dath 35022. Show that the dummy atoms form a line. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalem20 34979* |
Lemma for dath 35022. Show that a second dummy atom exists outside
of the and
planes (when those
planes are equal).
(Contributed by NM, 14-Aug-2012.)
|
|
| ||
| Theorem | dalem21 34980 |
Lemma for dath 35022. Show that lines and intersect at
an atom. (Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem22 34981 |
Lemma for dath 35022. Show that lines and determine a
plane. (Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem23 34982 |
Lemma for dath 35022. Show that auxiliary atom  is an atom.
(Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem24 34983 |
Lemma for dath 35022. Show that auxiliary atom is outside of plane
.
(Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem25 34984 |
Lemma for dath 35022. Show that the dummy center of
perspectivity
is different from auxiliary atom . (Contributed by NM,
3-Aug-2012.)
|
|
| ||
| Theorem | dalem27 34985 |
Lemma for dath 35022. Show that the line intersects the dummy
center of perspectivity . (Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem28 34986 | Lemma for dath 35022. Lemma dalem27 34985 expressed differently. (Contributed by NM, 4-Aug-2012.) |
|
| ||
| Theorem | dalem29 34987 |
Lemma for dath 35022. Analogue of dalem23 34982 for  . (Contributed by
NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem30 34988 |
Lemma for dath 35022. Analogue of dalem24 34983 for . (Contributed by
NM, 3-Aug-2012.)
|
|
| ||
| Theorem | dalem31N 34989 |
Lemma for dath 35022. Analogue of dalem25 34984 for . (Contributed by
NM, 4-Aug-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | dalem32 34990 |
Lemma for dath 35022. Analogue of dalem27 34985 for . (Contributed by
NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem33 34991 |
Lemma for dath 35022. Analogue of dalem28 34986 for . (Contributed by
NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem34 34992 |
Lemma for dath 35022. Analogue of dalem23 34982 for  . (Contributed by
NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem35 34993 |
Lemma for dath 35022. Analogue of dalem24 34983 for . (Contributed by
NM, 3-Aug-2012.)
|
|
| ||
| Theorem | dalem36 34994 |
Lemma for dath 35022. Analogue of dalem27 34985 for . (Contributed by
NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem37 34995 |
Lemma for dath 35022. Analogue of dalem28 34986 for . (Contributed by
NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem38 34996 |
Lemma for dath 35022. Plane belongs to the 3-dimensional volume
. (Contributed by NM, 5-Aug-2012.)
|
|
| ||
| Theorem | dalem39 34997 |
Lemma for dath 35022. Auxiliary atoms , , and are not
colinear. (Contributed by NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem40 34998 |
Lemma for dath 35022. Analogue of dalem39 34997 for . (Contributed by
NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem41 34999 | Lemma for dath 35022. (Contributed by NM, 4-Aug-2012.) |
|
| ||
| Theorem | dalem42 35000 |
Lemma for dath 35022. Auxiliary atoms
form a plane.
(Contributed by NM, 4-Aug-2012.)
|
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |