HomeTheorem List (p. 359 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. 359 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-25952) |
Hilbert Space Explorer
(25953-27476) |
Users' Mathboxes
(27477-38550) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | dalem3 35801 | Lemma for dalemdnee 35803. (Contributed by NM, 10-Aug-2012.) |
       ![/\](wedge.gif "/\"){kind=small}    
            
  
  ![./\](_.wedge.gif "./\"){kind=small}  
   | ||
| Theorem | dalem4 35802 | Lemma for dalemdnee 35803. (Contributed by NM, 10-Aug-2012.) |
|
| ||
| Theorem | dalemdnee 35803 |
Lemma for dath 35873. Axis of perspectivity points and are
different. (Contributed by NM, 10-Aug-2012.)
|
|
| ||
| Theorem | dalem5 35804 |
Lemma for dath 35873. Atom (in plane ) belongs to
the 3-dimensional volume formed by and . (Contributed by
NM, 21-Jul-2012.)
|
 | ||
| Theorem | dalem6 35805 |
Lemma for dath 35873. Analog of dalem5 35804 for . (Contributed by
NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem7 35806 |
Lemma for dath 35873. Analog of dalem5 35804 for . (Contributed by
NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem8 35807 |
Lemma for dath 35873. Plane belongs to the 3-dimensional space.
(Contributed by NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem-cly 35808 |
Lemma for dalem9 35809. Center of perspectivity is not in plane
(when and are different planes). (Contributed by
NM, 13-Aug-2012.)
|
|
| ||
| Theorem | dalem9 35809 |
Lemma for dath 35873. Since
, the join forms
a 3-dimensional space. (Contributed by NM, 20-Jul-2012.)
|
 
| ||
| Theorem | dalem10 35810 |
Lemma for dath 35873. Atom belongs to the axis of perspectivity
 .
(Contributed by NM, 19-Jul-2012.)
|
|
| ||
| Theorem | dalem11 35811 |
Lemma for dath 35873. Analog of dalem10 35810 for . (Contributed by
NM, 23-Jul-2012.)
|
|
| ||
| Theorem | dalem12 35812 |
Lemma for dath 35873. Analog of dalem10 35810 for  . (Contributed by
NM, 11-Aug-2012.)
|
|
| ||
| Theorem | dalem13 35813 | Lemma for dalem14 35814. (Contributed by NM, 21-Jul-2012.) |
|
| ||
| Theorem | dalem14 35814 |
Lemma for dath 35873. Planes and form a 3-dimensional space
(when they are different). (Contributed by NM, 22-Jul-2012.)
|
|
| ||
| Theorem | dalem15 35815 |
Lemma for dath 35873. The axis of perspectivity is a line.
(Contributed by NM, 21-Jul-2012.)
|
 
| ||
| Theorem | dalem16 35816 |
Lemma for dath 35873. 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 35817 |
Lemma for dath 35873. When planes and are equal, the center
of perspectivity is in .
(Contributed by NM,
1-Aug-2012.)
|
|
| ||
| Theorem | dalem18 35818* |
Lemma for dath 35873. 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 35819* |
Lemma for dath 35873. 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 35820 | Lemma for dath 35873. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
| ||
| Theorem | dalemddea 35821 | Lemma for dath 35873. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalem-ccly 35822 | Lemma for dath 35873. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalem-ddly 35823 | Lemma for dath 35873. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemccnedd 35824 | Lemma for dath 35873. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemclccjdd 35825 | Lemma for dath 35873. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemcceb 35826 | Lemma for dath 35873. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemswapyzps 35827 |
Lemma for dath 35873. 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 35828 |
Lemma for dath 35873. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
15-Aug-2012.)
|
|
| ||
| Theorem | dalemcjden 35829 | Lemma for dath 35873. Show that the dummy atoms form a line. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalem20 35830* |
Lemma for dath 35873. 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 35831 |
Lemma for dath 35873. Show that lines and intersect at
an atom. (Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem22 35832 |
Lemma for dath 35873. Show that lines and determine a
plane. (Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem23 35833 |
Lemma for dath 35873. Show that auxiliary atom  is an atom.
(Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem24 35834 |
Lemma for dath 35873. Show that auxiliary atom is outside of plane
.
(Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem25 35835 |
Lemma for dath 35873. Show that the dummy center of
perspectivity
is different from auxiliary atom . (Contributed by NM,
3-Aug-2012.)
|
|
| ||
| Theorem | dalem27 35836 |
Lemma for dath 35873. Show that the line intersects the dummy
center of perspectivity . (Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem28 35837 | Lemma for dath 35873. Lemma dalem27 35836 expressed differently. (Contributed by NM, 4-Aug-2012.) |
|
| ||
| Theorem | dalem29 35838 |
Lemma for dath 35873. Analog of dalem23 35833 for  . (Contributed by
NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem30 35839 |
Lemma for dath 35873. Analog of dalem24 35834 for . (Contributed by
NM, 3-Aug-2012.)
|
|
| ||
| Theorem | dalem31N 35840 |
Lemma for dath 35873. Analog of dalem25 35835 for . (Contributed by
NM, 4-Aug-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | dalem32 35841 |
Lemma for dath 35873. Analog of dalem27 35836 for . (Contributed by
NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem33 35842 |
Lemma for dath 35873. Analog of dalem28 35837 for . (Contributed by
NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem34 35843 |
Lemma for dath 35873. Analog of dalem23 35833 for  . (Contributed by
NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem35 35844 |
Lemma for dath 35873. Analog of dalem24 35834 for . (Contributed by
NM, 3-Aug-2012.)
|
|
| ||
| Theorem | dalem36 35845 |
Lemma for dath 35873. Analog of dalem27 35836 for . (Contributed by
NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem37 35846 |
Lemma for dath 35873. Analog of dalem28 35837 for . (Contributed by
NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem38 35847 |
Lemma for dath 35873. Plane belongs to the 3-dimensional volume
. (Contributed by NM, 5-Aug-2012.)
|
|
| ||
| Theorem | dalem39 35848 |
Lemma for dath 35873. Auxiliary atoms , , and are not
colinear. (Contributed by NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem40 35849 |
Lemma for dath 35873. Analog of dalem39 35848 for . (Contributed by
NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem41 35850 | Lemma for dath 35873. (Contributed by NM, 4-Aug-2012.) |
|
| ||
| Theorem | dalem42 35851 |
Lemma for dath 35873. Auxiliary atoms
form a plane.
(Contributed by NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem43 35852 |
Lemma for dath 35873. Planes and are different.
(Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem44 35853 |
Lemma for dath 35873. Dummy center of perspectivity lies outside
of plane . (Contributed by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem45 35854 |
Lemma for dath 35873. Dummy center of perspectivity is not on the
line . (Contributed by NM,
16-Aug-2012.)
|
|
| ||
| Theorem | dalem46 35855 |
Lemma for dath 35873. Analog of dalem45 35854 for .
(Contributed by
NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem47 35856 |
Lemma for dath 35873. Analog of dalem45 35854 for .
(Contributed by
NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem48 35857 |
Lemma for dath 35873. Analog of dalem45 35854 for .
(Contributed by
NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem49 35858 |
Lemma for dath 35873. Analog of dalem45 35854 for .
(Contributed by
NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem50 35859 |
Lemma for dath 35873. Analog of dalem45 35854 for .
(Contributed by
NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem51 35860 |
Lemma for dath 35873. Construct the condition with ,
, and in place of , , and
respectively. This lets us reuse the special case of Desargues'
Theorem where , to eventually prove the
case where
. (Contributed by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem52 35861 |
Lemma for dath 35873. Lines and intersect at an atom.
(Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem53 35862 |
Lemma for dath 35873. The auxliary axis of perspectivity  is a line
(analogous to the actual axis of perspectivity in dalem15 35815.
(Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem54 35863 |
Lemma for dath 35873. Line
intersects the auxiliary axis of
perspectivity . (Contributed by NM, 8-Aug-2012.)
|
|
| ||