HomeTheorem List (p. 356 of 382)
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. 356 of 382) | < 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-25961) |
Hilbert Space Explorer
(25962-27486) |
Users' Mathboxes
(27487-38122) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | dalem13 35501 | Lemma for dalem14 35502. (Contributed by NM, 21-Jul-2012.) |
       ![/\](wedge.gif "/\"){kind=small}    
            
  
  
    | ||
| Theorem | dalem14 35502 |
Lemma for dath 35561. Planes and form a 3-dimensional space
(when they are different). (Contributed by NM, 22-Jul-2012.)
|
 
| ||
| Theorem | dalem15 35503 |
Lemma for dath 35561. The axis of perspectivity  is a line.
(Contributed by NM, 21-Jul-2012.)
|
![./\](_.wedge.gif "./\"){kind=small}   
| ||
| Theorem | dalem16 35504 |
Lemma for dath 35561. 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 35505 |
Lemma for dath 35561. When planes and are equal, the center
of perspectivity is in .
(Contributed by NM,
1-Aug-2012.)
|
|
| ||
| Theorem | dalem18 35506* |
Lemma for dath 35561. 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 35507* |
Lemma for dath 35561. 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 35508 | Lemma for dath 35561. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
| ||
| Theorem | dalemddea 35509 | Lemma for dath 35561. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalem-ccly 35510 | Lemma for dath 35561. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalem-ddly 35511 | Lemma for dath 35561. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemccnedd 35512 | Lemma for dath 35561. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemclccjdd 35513 | Lemma for dath 35561. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemcceb 35514 | Lemma for dath 35561. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemswapyzps 35515 |
Lemma for dath 35561. 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 35516 |
Lemma for dath 35561. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
15-Aug-2012.)
|
|
| ||
| Theorem | dalemcjden 35517 | Lemma for dath 35561. Show that the dummy atoms form a line. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalem20 35518* |
Lemma for dath 35561. 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 35519 |
Lemma for dath 35561. Show that lines and intersect at
an atom. (Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem22 35520 |
Lemma for dath 35561. Show that lines and determine a
plane. (Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem23 35521 |
Lemma for dath 35561. Show that auxiliary atom  is an atom.
(Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem24 35522 |
Lemma for dath 35561. Show that auxiliary atom is outside of plane
.
(Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem25 35523 |
Lemma for dath 35561. Show that the dummy center of
perspectivity
is different from auxiliary atom . (Contributed by NM,
3-Aug-2012.)
|
|
| ||
| Theorem | dalem27 35524 |
Lemma for dath 35561. Show that the line intersects the dummy
center of perspectivity . (Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem28 35525 | Lemma for dath 35561. Lemma dalem27 35524 expressed differently. (Contributed by NM, 4-Aug-2012.) |
|
| ||
| Theorem | dalem29 35526 |
Lemma for dath 35561. Analog of dalem23 35521 for  . (Contributed by
NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem30 35527 |
Lemma for dath 35561. Analog of dalem24 35522 for . (Contributed by
NM, 3-Aug-2012.)
|
|
| ||
| Theorem | dalem31N 35528 |
Lemma for dath 35561. Analog of dalem25 35523 for . (Contributed by
NM, 4-Aug-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | dalem32 35529 |
Lemma for dath 35561. Analog of dalem27 35524 for . (Contributed by
NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem33 35530 |
Lemma for dath 35561. Analog of dalem28 35525 for . (Contributed by
NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem34 35531 |
Lemma for dath 35561. Analog of dalem23 35521 for  . (Contributed by
NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem35 35532 |
Lemma for dath 35561. Analog of dalem24 35522 for . (Contributed by
NM, 3-Aug-2012.)
|
|
| ||
| Theorem | dalem36 35533 |
Lemma for dath 35561. Analog of dalem27 35524 for . (Contributed by
NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem37 35534 |
Lemma for dath 35561. Analog of dalem28 35525 for . (Contributed by
NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem38 35535 |
Lemma for dath 35561. Plane belongs to the 3-dimensional volume
. (Contributed by NM, 5-Aug-2012.)
|
|
| ||
| Theorem | dalem39 35536 |
Lemma for dath 35561. Auxiliary atoms , , and are not
colinear. (Contributed by NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem40 35537 |
Lemma for dath 35561. Analog of dalem39 35536 for . (Contributed by
NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem41 35538 | Lemma for dath 35561. (Contributed by NM, 4-Aug-2012.) |
|
| ||
| Theorem | dalem42 35539 |
Lemma for dath 35561. Auxiliary atoms
form a plane.
(Contributed by NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem43 35540 |
Lemma for dath 35561. Planes and are different.
(Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem44 35541 |
Lemma for dath 35561. Dummy center of perspectivity lies outside
of plane . (Contributed by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem45 35542 |
Lemma for dath 35561. Dummy center of perspectivity is not on the
line . (Contributed by NM,
16-Aug-2012.)
|
|
| ||
| Theorem | dalem46 35543 |
Lemma for dath 35561. Analog of dalem45 35542 for .
(Contributed by
NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem47 35544 |
Lemma for dath 35561. Analog of dalem45 35542 for .
(Contributed by
NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem48 35545 |
Lemma for dath 35561. Analog of dalem45 35542 for .
(Contributed by
NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem49 35546 |
Lemma for dath 35561. Analog of dalem45 35542 for .
(Contributed by
NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem50 35547 |
Lemma for dath 35561. Analog of dalem45 35542 for .
(Contributed by
NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem51 35548 |
Lemma for dath 35561. 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 35549 |
Lemma for dath 35561. Lines and intersect at an atom.
(Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem53 35550 |
Lemma for dath 35561. The auxliary axis of perspectivity  is a line
(analogous to the actual axis of perspectivity in dalem15 35503.
(Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem54 35551 |
Lemma for dath 35561. Line
intersects the auxiliary axis of
perspectivity . (Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem55 35552 |
Lemma for dath 35561. Lines and intersect at the
auxiliary line (later shown to be an axis of perspectivity; see
dalem60 35557). (Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem56 35553 |
Lemma for dath 35561. Analog of dalem55 35552 for line .
(Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem57 35554 |
Lemma for dath 35561. Axis of perspectivity point is on the
auxiliary line . (Contributed by NM, 9-Aug-2012.)
|
|
| ||
| Theorem | dalem58 35555 |
Lemma for dath 35561. Analog of dalem57 35554 for . (Contributed by
NM, 10-Aug-2012.)
|
|
| ||
| Theorem | dalem59 35556 |
Lemma for dath 35561. Analog of dalem57 35554 for . (Contributed by
NM, 10-Aug-2012.)
|
|
| ||
| Theorem | dalem60 35557 |
Lemma for dath 35561. is an axis of perspectivity (almost).
(Contributed by NM, 11-Aug-2012.)
|
|
| ||
| Theorem | dalem61 35558 |
Lemma for dath 35561. Show that atoms , , and lie on
the same line (axis of perspectivity). Eliminate hypotheses
containing dummy atoms and .
(Contributed by NM,
11-Aug-2012.)
|
|
| ||
| Theorem | dalem62 35559 |
Lemma for dath 35561. Eliminate the condition containing dummy
variables and
. (Contributed by NM,
11-Aug-2012.)
|
|
| ||