HomeTheorem List (p. 330 of 393)
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. 330 of 393) | < 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-26406) |
Hilbert Space Explorer
(26407-27929) |
Users' Mathboxes
(27930-39300) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | dalemrea 32901 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
       ![/\](wedge.gif "/\"){kind=small}    
            
  | ||
| Theorem | dalemsea 32902 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemtea 32903 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemuea 32904 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemyeo 32905 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemzeo 32906 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclpjs 32907 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclqjt 32908 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclrju 32909 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalem-clpjq 32910 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemceb 32911 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
   | ||
| Theorem | dalempeb 32912 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqeb 32913 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemreb 32914 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemseb 32915 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemteb 32916 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemueb 32917 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempjqeb 32918 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 | ||
| Theorem | dalemsjteb 32919 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemtjueb 32920 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqrprot 32921 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemyeb 32922 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 | ||
| Theorem | dalemcnes 32923 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 | ||
| Theorem | dalempnes 32924 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqnet 32925 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempjsen 32926 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 | ||
| Theorem | dalemply 32927 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemsly 32928 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemswapyz 32929 |
Lemma for dath 33009. Swap the role of planes and to allow
reuse of analogous proofs. (Contributed by NM, 14-Aug-2012.)
|
|
| ||
| Theorem | dalemrot 32930 |
Lemma for dath 33009. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
14-Aug-2012.)
|
|
| ||
| Theorem | dalemrotyz 32931 |
Lemma for dath 33009. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
19-Aug-2012.)
|
|
| ||
| Theorem | dalem1 32932 |
Lemma for dath 33009. Show the lines and are different.
(Contributed by NM, 9-Aug-2012.)
|
|
| ||
| Theorem | dalemcea 32933 |
Lemma for dath 33009. 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 32934 |
Lemma for dath 33009. Show the lines and form a plane.
(Contributed by NM, 11-Aug-2012.)
|
|
| ||
| Theorem | dalemdea 32935 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 11-Aug-2012.) |
![./\](_.wedge.gif "./\"){kind=small} 
| ||
| Theorem | dalemeea 32936 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 11-Aug-2012.) |
| ||
| Theorem | dalem3 32937 | Lemma for dalemdnee 32939. (Contributed by NM, 10-Aug-2012.) |
|
| ||
| Theorem | dalem4 32938 | Lemma for dalemdnee 32939. (Contributed by NM, 10-Aug-2012.) |
|
| ||
| Theorem | dalemdnee 32939 |
Lemma for dath 33009. Axis of perspectivity points and are
different. (Contributed by NM, 10-Aug-2012.)
|
|
| ||
| Theorem | dalem5 32940 |
Lemma for dath 33009. Atom (in plane ) belongs to
the 3-dimensional volume formed by and . (Contributed by
NM, 21-Jul-2012.)
|
 | ||
| Theorem | dalem6 32941 |
Lemma for dath 33009. Analog of dalem5 32940 for . (Contributed by
NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem7 32942 |
Lemma for dath 33009. Analog of dalem5 32940 for . (Contributed by
NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem8 32943 |
Lemma for dath 33009. Plane belongs to the 3-dimensional space.
(Contributed by NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem-cly 32944 |
Lemma for dalem9 32945. Center of perspectivity is not in plane
(when and are different planes). (Contributed by
NM, 13-Aug-2012.)
|
|
| ||
| Theorem | dalem9 32945 |
Lemma for dath 33009. Since
, the join forms
a 3-dimensional space. (Contributed by NM, 20-Jul-2012.)
|
 
| ||
| Theorem | dalem10 32946 |
Lemma for dath 33009. Atom belongs to the axis of perspectivity
 .
(Contributed by NM, 19-Jul-2012.)
|
|
| ||
| Theorem | dalem11 32947 |
Lemma for dath 33009. Analog of dalem10 32946 for . (Contributed by
NM, 23-Jul-2012.)
|
|
| ||
| Theorem | dalem12 32948 |
Lemma for dath 33009. Analog of dalem10 32946 for  . (Contributed by
NM, 11-Aug-2012.)
|
|
| ||
| Theorem | dalem13 32949 | Lemma for dalem14 32950. (Contributed by NM, 21-Jul-2012.) |
|
| ||
| Theorem | dalem14 32950 |
Lemma for dath 33009. Planes and form a 3-dimensional space
(when they are different). (Contributed by NM, 22-Jul-2012.)
|
|
| ||
| Theorem | dalem15 32951 |
Lemma for dath 33009. The axis of perspectivity is a line.
(Contributed by NM, 21-Jul-2012.)
|
| ||
| Theorem | dalem16 32952 |
Lemma for dath 33009. 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 32953 |
Lemma for dath 33009. When planes and are equal, the center
of perspectivity is in .
(Contributed by NM,
1-Aug-2012.)
|
|
| ||
| Theorem | dalem18 32954* |
Lemma for dath 33009. 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 32955* |
Lemma for dath 33009. 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 32956 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
| ||
| Theorem | dalemddea 32957 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalem-ccly 32958 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalem-ddly 32959 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemccnedd 32960 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemclccjdd 32961 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemcceb 32962 | Lemma for dath 33009. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemswapyzps 32963 |
Lemma for dath 33009. 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 32964 |
Lemma for dath 33009. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
15-Aug-2012.)
|
|
| ||
| Theorem | dalemcjden 32965 | Lemma for dath 33009. Show that the dummy atoms form a line. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalem20 32966* |
Lemma for dath 33009. 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 32967 |
Lemma for dath 33009. Show that lines and intersect at
an atom. (Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem22 32968 |
Lemma for dath 33009. Show that lines and determine a
plane. (Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem23 32969 |
Lemma for dath 33009. Show that auxiliary atom  is an atom.
(Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem24 32970 |
Lemma for dath 33009. Show that auxiliary atom is outside of plane
.
(Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem25 32971 |
Lemma for dath 33009. Show that the dummy center of
perspectivity
is different from auxiliary atom . (Contributed by NM,
3-Aug-2012.)
|
|
| ||
| Theorem | dalem27 32972 |
Lemma for dath 33009. Show that the line intersects the dummy
center of perspectivity . (Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem28 32973 | Lemma for dath 33009. Lemma dalem27 32972 expressed differently. (Contributed by NM, 4-Aug-2012.) |
|
| ||
| Theorem | dalem29 32974 |
Lemma for dath 33009. Analog of dalem23 32969 for  . (Contributed by
NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem30 32975 |
Lemma for dath 33009. Analog of dalem24 32970 for . (Contributed by
NM, 3-Aug-2012.)
|
|
| ||
| Theorem | dalem31N 32976 |
Lemma for dath 33009. Analog of dalem25 32971 for . (Contributed by
NM, 4-Aug-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | dalem32 32977 |
Lemma for dath 33009. Analog of dalem27 32972 for . (Contributed by
NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem33 32978 |
Lemma for dath 33009. Analog of dalem28 32973 for . (Contributed by
NM, 4-Aug-2012.)
|
|
| ||