HomeTheorem List (p. 334 of 409)
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. 334 of 409) | < 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-26620) |
Hilbert Space Explorer
(26621-28143) |
Users' Mathboxes
(28144-40813) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | dalemrotps 33301 |
Lemma for dath 33346. Rotate triangles      and    
to allow reuse of analogous proofs. (Contributed by NM,
15-Aug-2012.)
|
       ![/\](wedge.gif "/\"){kind=small}    
    
 
     
 
| ||
| Theorem | dalemcjden 33302 | Lemma for dath 33346. Show that the dummy atoms form a line. (Contributed by NM, 15-Aug-2012.) |
 | ||
| Theorem | dalem20 33303* |
Lemma for dath 33346. 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 33304 |
Lemma for dath 33346. Show that lines and intersect at
an atom. (Contributed by NM, 2-Aug-2012.)
|
![./\](_.wedge.gif "./\"){kind=small} 
| ||
| Theorem | dalem22 33305 |
Lemma for dath 33346. Show that lines and determine a
plane. (Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem23 33306 |
Lemma for dath 33346. Show that auxiliary atom  is an atom.
(Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem24 33307 |
Lemma for dath 33346. Show that auxiliary atom is outside of plane
.
(Contributed by NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem25 33308 |
Lemma for dath 33346. Show that the dummy center of
perspectivity
is different from auxiliary atom . (Contributed by NM,
3-Aug-2012.)
|
|
| ||
| Theorem | dalem27 33309 |
Lemma for dath 33346. Show that the line intersects the dummy
center of perspectivity . (Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem28 33310 | Lemma for dath 33346. Lemma dalem27 33309 expressed differently. (Contributed by NM, 4-Aug-2012.) |
|
| ||
| Theorem | dalem29 33311 |
Lemma for dath 33346. Analogue of dalem23 33306 for  . (Contributed by
NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem30 33312 |
Lemma for dath 33346. Analogue of dalem24 33307 for . (Contributed by
NM, 3-Aug-2012.)
|
|
| ||
| Theorem | dalem31N 33313 |
Lemma for dath 33346. Analogue of dalem25 33308 for . (Contributed by
NM, 4-Aug-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | dalem32 33314 |
Lemma for dath 33346. Analogue of dalem27 33309 for . (Contributed by
NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem33 33315 |
Lemma for dath 33346. Analogue of dalem28 33310 for . (Contributed by
NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem34 33316 |
Lemma for dath 33346. Analogue of dalem23 33306 for  . (Contributed by
NM, 2-Aug-2012.)
|
|
| ||
| Theorem | dalem35 33317 |
Lemma for dath 33346. Analogue of dalem24 33307 for . (Contributed by
NM, 3-Aug-2012.)
|
|
| ||
| Theorem | dalem36 33318 |
Lemma for dath 33346. Analogue of dalem27 33309 for . (Contributed by
NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem37 33319 |
Lemma for dath 33346. Analogue of dalem28 33310 for . (Contributed by
NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem38 33320 |
Lemma for dath 33346. Plane belongs to the 3-dimensional volume
. (Contributed by NM, 5-Aug-2012.)
|
|
| ||
| Theorem | dalem39 33321 |
Lemma for dath 33346. Auxiliary atoms , , and are not
colinear. (Contributed by NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem40 33322 |
Lemma for dath 33346. Analogue of dalem39 33321 for . (Contributed by
NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem41 33323 | Lemma for dath 33346. (Contributed by NM, 4-Aug-2012.) |
|
| ||
| Theorem | dalem42 33324 |
Lemma for dath 33346. Auxiliary atoms
form a plane.
(Contributed by NM, 4-Aug-2012.)
|
|
| ||
| Theorem | dalem43 33325 |
Lemma for dath 33346. Planes and are different.
(Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem44 33326 |
Lemma for dath 33346. Dummy center of perspectivity lies outside
of plane . (Contributed by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem45 33327 |
Lemma for dath 33346. Dummy center of perspectivity is not on the
line . (Contributed by NM,
16-Aug-2012.)
|
|
| ||
| Theorem | dalem46 33328 |
Lemma for dath 33346. Analogue of dalem45 33327 for .
(Contributed
by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem47 33329 |
Lemma for dath 33346. Analogue of dalem45 33327 for .
(Contributed
by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem48 33330 |
Lemma for dath 33346. Analogue of dalem45 33327 for .
(Contributed
by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem49 33331 |
Lemma for dath 33346. Analogue of dalem45 33327 for .
(Contributed
by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem50 33332 |
Lemma for dath 33346. Analogue of dalem45 33327 for .
(Contributed
by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem51 33333 |
Lemma for dath 33346. 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 33334 |
Lemma for dath 33346. Lines and intersect at an atom.
(Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem53 33335 |
Lemma for dath 33346. The auxliary axis of perspectivity  is a line
(analogous to the actual axis of perspectivity  in dalem15 33288.
(Contributed by NM, 8-Aug-2012.)
|
| ||
| Theorem | dalem54 33336 |
Lemma for dath 33346. Line
intersects the auxiliary axis of
perspectivity . (Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem55 33337 |
Lemma for dath 33346. Lines and intersect at the
auxiliary line (later shown to be an axis of perspectivity; see
dalem60 33342). (Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem56 33338 |
Lemma for dath 33346. Analogue of dalem55 33337 for line .
(Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem57 33339 |
Lemma for dath 33346. Axis of perspectivity point  is on the
auxiliary line . (Contributed by NM, 9-Aug-2012.)
|
|
| ||
| Theorem | dalem58 33340 |
Lemma for dath 33346. Analogue of dalem57 33339 for  . (Contributed by
NM, 10-Aug-2012.)
|
|
| ||
| Theorem | dalem59 33341 |
Lemma for dath 33346. Analogue of dalem57 33339 for  . (Contributed by
NM, 10-Aug-2012.)
|
|
| ||
| Theorem | dalem60 33342 |
Lemma for dath 33346. is an axis of perspectivity (almost).
(Contributed by NM, 11-Aug-2012.)
|
|
| ||
| Theorem | dalem61 33343 |
Lemma for dath 33346. 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 33344 |
Lemma for dath 33346. Eliminate the condition containing dummy
variables and
. (Contributed by NM,
11-Aug-2012.)
|
|
| ||
| Theorem | dalem63 33345 |
Lemma for dath 33346. Combine the cases where and are
different planes with the case where and are the same
plane. (Contributed by NM, 11-Aug-2012.)
|
|
| ||
| Theorem | dath 33346 |
Desargues' Theorem of projective geometry (proved for a Hilbert
lattice). Assume each triple of atoms (points)
and
forms a triangle (i.e. determines a plane). Assume that lines ,
, and meet at a "center of perspectivity" . (We
also assume that is not on any of the 6 lines forming the two
triangles.) Then the atoms
,
,
are colinear, forming an "axis of
perspectivity".
Our proof roughly follows Theorem 2.7.1, p. 78 in Beutelspacher and
Rosenbaum, Projective Geometry: From Foundations to
Applications,
Cambridge University Press (1988). Unlike them, we don't assume For a visual demonstration, see the "Desargue's Theorem" applet at http://www.dynamicgeometry.com/JavaSketchpad/Gallery.html. The points I, J, and K there define the axis of perspectivity. See theorem dalaw 33496 for Desargues Law, which eliminates all of the preconditions on the atoms except for central perspectivity. This is Metamath 100 proof #87. (Contributed by NM, 20-Aug-2012.) |
|
| ||
| Theorem | dath2 33347 | Version of Desargues' Theorem dath 33346 with a different variable ordering. (Contributed by NM, 7-Oct-2012.) |
|
| ||
| Theorem | lineset 33348* | The set of lines in a Hilbert lattice. (Contributed by NM, 19-Sep-2011.) |
    
 | ||
| Theorem | isline 33349* | The predicate "is a line". (Contributed by NM, 19-Sep-2011.) |
|
| ||
| Theorem | islinei 33350* | Condition implying "is a line". (Contributed by NM, 3-Feb-2012.) |
|
| ||
| Theorem | pointsetN 33351* | The set of points in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.) |
| ||
| Theorem | ispointN 33352* | The predicate "is a point". (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | atpointN 33353 | The singleton of an atom is a point. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
| | ||
| Theorem | psubspset 33354* | The set of projective subspaces in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) |
 
| ||
| Theorem | ispsubsp 33355* | The predicate "is a projective subspace". (Contributed by NM, 2-Oct-2011.) |
|
| ||
| Theorem | ispsubsp2 33356* | The predicate "is a projective subspace". (Contributed by NM, 13-Jan-2012.) |
|
| ||
| Theorem | psubspi 33357* | Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) |
|
| ||
| Theorem | psubspi2N 33358 | Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 0psubN 33359 | The empty set is a projective subspace. Remark below Definition 15.1 of [MaedaMaeda] p. 61. (Contributed by NM, 13-Oct-2011.) (New usage is discouraged.) |
  | ||
| Theorem | snatpsubN 33360 | The singleton of an atom is a projective subspace. (Contributed by NM, 9-Sep-2013.) (New usage is discouraged.) |
 | ||
| Theorem | pointpsubN 33361 | A point (singleton of an atom) is a projective subspace. Remark below Definition 15.1 of [MaedaMaeda] p. 61. (Contributed by NM, 13-Oct-2011.) (New usage is discouraged.) |
| | ||
| Theorem | linepsubN 33362 | A line is a projective subspace. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.) |
 | ||
| Theorem | atpsubN 33363 | The set of all atoms is a projective subspace. Remark below Definition 15.1 of [MaedaMaeda] p. 61. (Contributed by NM, 13-Oct-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | psubssat 33364 | A projective subspace consists of atoms. (Contributed by NM, 4-Nov-2011.) |
|
| ||
| Theorem | psubatN 33365 | A member of a projective subspace is an atom. (Contributed by NM, 4-Nov-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | pmapfval 33366* | The projective map of a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) |
    | ||
| Theorem | pmapval 33367* | Value of the projective map of a Hilbert lattice. Definition in Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 2-Oct-2011.) |
|
| ||
| Theorem | elpmap 33368 | Member of a projective map. (Contributed by NM, 27-Jan-2012.) |
|
| ||
| Theorem | pmapssat 33369 | The projective map of a Hilbert lattice is a set of atoms. (Contributed by NM, 14-Jan-2012.) |
| | ||
| Theorem | pmapssbaN 33370 | A weakening of pmapssat 33369 to shorten some proofs. (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.) |
| | ||
| Theorem | pmaple 33371 | The projective map of a Hilbert lattice preserves ordering. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 22-Oct-2011.) |
|
| ||
| Theorem | pmap11 33372 | The projective map of a Hilbert lattice is one-to-one. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 22-Oct-2011.) |
| | ||