HomeTheorem List (p. 331 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. 331 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 | dalem56 33001 |
Lemma for dath 33009. Analog of dalem55 33000 for line   .
(Contributed by NM, 8-Aug-2012.)
|
       ![/\](wedge.gif "/\"){kind=small}    
          
  
     
![./\](_.wedge.gif "./\"){kind=small}  
  
| ||
| Theorem | dalem57 33002 |
Lemma for dath 33009. Axis of perspectivity point  is on the
auxiliary line . (Contributed by NM, 9-Aug-2012.)
|
|
| ||
| Theorem | dalem58 33003 |
Lemma for dath 33009. Analog of dalem57 33002 for  . (Contributed by
NM, 10-Aug-2012.)
|
|
| ||
| Theorem | dalem59 33004 |
Lemma for dath 33009. Analog of dalem57 33002 for  . (Contributed by
NM, 10-Aug-2012.)
|
|
| ||
| Theorem | dalem60 33005 |
Lemma for dath 33009. is an axis of perspectivity (almost).
(Contributed by NM, 11-Aug-2012.)
|
|
| ||
| Theorem | dalem61 33006 |
Lemma for dath 33009. 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 33007 |
Lemma for dath 33009. Eliminate the condition containing dummy
variables and
. (Contributed by NM,
11-Aug-2012.)
|
|
| ||
| Theorem | dalem63 33008 |
Lemma for dath 33009. 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 33009 |
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 33159 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 33010 | Version of Desargues' Theorem dath 33009 with a different variable ordering. (Contributed by NM, 7-Oct-2012.) |
|
| ||
| Theorem | lineset 33011* | The set of lines in a Hilbert lattice. (Contributed by NM, 19-Sep-2011.) |
 
     
 | ||
| Theorem | isline 33012* | The predicate "is a line". (Contributed by NM, 19-Sep-2011.) |
| ||
| Theorem | islinei 33013* | Condition implying "is a line". (Contributed by NM, 3-Feb-2012.) |
|
| ||
| Theorem | pointsetN 33014* | The set of points in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.) |
| ||
| Theorem | ispointN 33015* | The predicate "is a point". (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | atpointN 33016 | The singleton of an atom is a point. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
| | ||
| Theorem | psubspset 33017* | The set of projective subspaces in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) |
 
| ||
| Theorem | ispsubsp 33018* | The predicate "is a projective subspace". (Contributed by NM, 2-Oct-2011.) |
|
| ||
| Theorem | ispsubsp2 33019* | The predicate "is a projective subspace". (Contributed by NM, 13-Jan-2012.) |
|
| ||
| Theorem | psubspi 33020* | Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) |
|
| ||
| Theorem | psubspi2N 33021 | Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 0psubN 33022 | 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 33023 | The singleton of an atom is a projective subspace. (Contributed by NM, 9-Sep-2013.) (New usage is discouraged.) |
 | ||
| Theorem | pointpsubN 33024 | 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 33025 | A line is a projective subspace. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.) |
 | ||
| Theorem | atpsubN 33026 | 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 33027 | A projective subspace consists of atoms. (Contributed by NM, 4-Nov-2011.) |
|
| ||
| Theorem | psubatN 33028 | A member of a projective subspace is an atom. (Contributed by NM, 4-Nov-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | pmapfval 33029* | The projective map of a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) |
    | ||
| Theorem | pmapval 33030* | 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 33031 | Member of a projective map. (Contributed by NM, 27-Jan-2012.) |
|
| ||
| Theorem | pmapssat 33032 | The projective map of a Hilbert lattice is a set of atoms. (Contributed by NM, 14-Jan-2012.) |
| | ||
| Theorem | pmapssbaN 33033 | A weakening of pmapssat 33032 to shorten some proofs. (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.) |
| | ||
| Theorem | pmaple 33034 | 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 33035 | 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.) |
|
| ||
| Theorem | pmapat 33036 | The projective map of an atom. (Contributed by NM, 25-Jan-2012.) |
|
| ||
| Theorem | elpmapat 33037 | Member of the projective map of an atom. (Contributed by NM, 27-Jan-2012.) |
|
| ||
| Theorem | pmap0 33038 | Value of the projective map of a Hilbert lattice at lattice zero. Part of Theorem 15.5.1 of [MaedaMaeda] p. 62. (Contributed by NM, 17-Oct-2011.) |
  | ||
| Theorem | pmapeq0 33039 | A projective map value is zero iff its argument is lattice zero. (Contributed by NM, 27-Jan-2012.) |
| | ||
| Theorem | pmap1N 33040 | Value of the projective map of a Hilbert lattice at lattice unit. Part of Theorem 15.5.1 of [MaedaMaeda] p. 62. (Contributed by NM, 22-Oct-2011.) (New usage is discouraged.) |
   | ||
| Theorem | pmapsub 33041 | The projective map of a Hilbert lattice maps to projective subspaces. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 17-Oct-2011.) |
|
| ||
| Theorem | pmapglbx 33042* |
The projective map of the GLB of a set of lattice elements. Index-set
version of pmapglb 33043, where we read as  . Theorem
15.5.2 of [MaedaMaeda] p. 62.
(Contributed by NM, 5-Dec-2011.)
|
 | ||
| Theorem | pmapglb 33043* |
The projective map of the GLB of a set of lattice elements .
Variant of Theorem 15.5.2 of [MaedaMaeda] p. 62. (Contributed by NM,
5-Dec-2011.)
|
| | ||
| Theorem | pmapglb2N 33044* |
The projective map of the GLB of a set of lattice elements .
Variant of Theorem 15.5.2 of [MaedaMaeda] p. 62. Allows .
(Contributed by NM, 21-Jan-2012.) (New usage is discouraged.)
|
 | ||
| Theorem | pmapglb2xN 33045* |
The projective map of the GLB of a set of lattice elements. Index-set
version of pmapglb2N 33044, where we read as . Extension
of Theorem 15.5.2 of [MaedaMaeda] p.
62 that allows .
(Contributed by NM, 21-Jan-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | pmapmeet 33046 | The projective map of a meet. (Contributed by NM, 25-Jan-2012.) |
|
| ||
| Theorem | isline2 33047* | Definition of line in terms of projective map. (Contributed by NM, 25-Jan-2012.) |
|
| ||
| Theorem | linepmap 33048 | A line described with a projective map. (Contributed by NM, 3-Feb-2012.) |
|
| ||
| Theorem | isline3 33049* | Definition of line in terms of original lattice elements. (Contributed by NM, 29-Apr-2012.) |
|
| ||
| Theorem | isline4N 33050* | Definition of line in terms of original lattice elements. (Contributed by NM, 16-Jun-2012.) (New usage is discouraged.) |
| ||
| Theorem | lneq2at 33051 | A line equals the join of any two of its distinct points (atoms). (Contributed by NM, 29-Apr-2012.) |
|
| ||
| Theorem | lnatexN 33052* | There is an atom in a line different from any other. (Contributed by NM, 30-Apr-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | lnjatN 33053* | Given an atom in a line, there is another atom which when joined equals the line. (Contributed by NM, 30-Apr-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | lncvrelatN 33054 | A lattice element covered by a line is an atom. (Contributed by NM, 28-Apr-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | lncvrat 33055 | A line covers the atoms it contains. (Contributed by NM, 30-Apr-2012.) |
| | ||
| Theorem | lncmp 33056 | If two lines are comparable, they are equal. (Contributed by NM, 30-Apr-2012.) |
|
| ||
| Theorem | 2lnat 33057 | Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012.) |
|
| ||
| Theorem | 2atm2atN 33058 | Two joins with a common atom have a nonzero meet. (Contributed by NM, 4-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2llnma1b 33059 | Generalization of 2llnma1 33060. (Contributed by NM, 26-Apr-2013.) |
|
| ||
| Theorem | 2llnma1 33060 | Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 11-Oct-2012.) |
|
| ||
| Theorem | 2llnma3r 33061 | Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 30-Apr-2013.) |
|
| ||
| Theorem | 2llnma2 33062 | Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 28-May-2012.) |
|
| ||
| Theorem | 2llnma2rN 33063 | Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 2-May-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdlema1N 33064 | A condition for required for proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 29-Apr-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdlema2N 33065 | A condition for required for proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 9-May-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdlemblem 33066 | Lemma for cdlemb 33067. (Contributed by NM, 8-May-2012.) |
 
| ||
| Theorem | cdlemb 33067* | Given two atoms not less than or equal to an element covered by 1, there is a third. Lemma B in [Crawley] p. 112. (Contributed by NM, 8-May-2012.) |
|
| ||
| Syntax | cpadd 33068 | Extend class notation with projective subspace sum. |
   | ||
| Definition | df-padd 33069* | Define projective sum of two subspaces (or more generally two sets of atoms), which is the union of all lines generated by pairs of atoms from each subspace. Lemma 16.2 of [MaedaMaeda] p. 68. For convenience, our definition is generalized to apply to empty sets. (Contributed by NM, 29-Dec-2011.) |
      
| ||
| Theorem | paddfval 33070* | Projective subspace sum operation. (Contributed by NM, 29-Dec-2011.) |
| ||
| Theorem | paddval 33071* | Projective subspace sum operation value. (Contributed by NM, 29-Dec-2011.) |
|
| ||
| Theorem | elpadd 33072* | Member of a projective subspace sum. (Contributed by NM, 29-Dec-2011.) |
| ||
| Theorem | elpaddn0 33073* | Member of projective subspace sum of nonempty sets. (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | paddvaln0N 33074* | Projective subspace sum operation value for nonempty sets. (Contributed by NM, 27-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | elpaddri 33075 | Condition implying membership in a projective subspace sum. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | elpaddatriN 33076 | Condition implying membership in a projective subspace sum with a point. (Contributed by NM, 1-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | elpaddat 33077* | Membership in a projective subspace sum with a point. (Contributed by NM, 29-Jan-2012.) |
|
| ||
| Theorem | elpaddatiN 33078* | Consequence of membership in a projective subspace sum with a point. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | elpadd2at 33079 | Membership in a projective subspace sum of two points. (Contributed by NM, 29-Jan-2012.) |
|
| ||
| Theorem | elpadd2at2 33080 | Membership in a projective subspace sum of two points. (Contributed by NM, 8-Mar-2012.) |
|
| ||
| Theorem | paddunssN 33081 | Projective subspace sum includes the set union of its arguments. (Contributed by NM, 12-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | elpadd0 33082 | Member of projective subspace sum with at least one empty set. (Contributed by NM, 29-Dec-2011.) |
|
| ||
| Theorem | paddval0 33083 | Projective subspace sum with at least one empty set. (Contributed by NM, 11-Jan-2012.) |
|
| ||
| Theorem | padd01 33084 | Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012.) |
| | ||
| Theorem | padd02 33085 | Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012.) |
|
| ||
| Theorem | paddcom 33086 | Projective subspace sum commutes. (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | paddssat 33087 | A projective subspace sum is a set of atoms. (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | sspadd1 33088 | A projective subspace sum is a superset of its first summand. (ssun1 3635 analog.) (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | sspadd2 33089 | A projective subspace sum is a superset of its second summand. (ssun2 3636 analog.) (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | paddss1 33090 | Subset law for projective subspace sum. (unss1 3641 analog.) (Contributed by NM, 7-Mar-2012.) |
|
| ||
| Theorem | paddss2 33091 | Subset law for projective subspace sum. (unss2 3643 analog.) (Contributed by NM, 7-Mar-2012.) |
|
| ||
| Theorem | paddss12 33092 | Subset law for projective subspace sum. (unss12 3644 analog.) (Contributed by NM, 7-Mar-2012.) |
| ||
| Theorem | paddasslem1 33093 | Lemma for paddass 33111. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | paddasslem2 33094 | Lemma for paddass 33111. (Contributed by NM, 8-Jan-2012.) |
| ||
| Theorem | paddasslem3 33095* | Lemma for paddass 33111. Restate projective space axiom ps-2 32751. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | paddasslem4 33096* | Lemma for paddass 33111. Combine paddasslem1 33093, paddasslem2 33094, and paddasslem3 33095. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | paddasslem5 33097 |
Lemma for paddass 33111. Show by
contradiction. (Contributed
by NM, 8-Jan-2012.)
|
|
| ||
| Theorem | paddasslem6 33098 | Lemma for paddass 33111. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | paddasslem7 33099 | Lemma for paddass 33111. Combine paddasslem5 33097 and paddasslem6 33098. (Contributed by NM, 9-Jan-2012.) |
|
| ||
| Theorem | paddasslem8 33100 | Lemma for paddass 33111. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |