HomeTheorem List (p. 351 of 426)
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. 351 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | dalem43 35001 |
Lemma for dath 35022. Planes    and  are different.
(Contributed by NM, 8-Aug-2012.)
|
       ![/\](wedge.gif "/\"){kind=small}    
           
  
     
![./\](_.wedge.gif "./\"){kind=small}  
 
| ||
| Theorem | dalem44 35002 |
Lemma for dath 35022. Dummy center of perspectivity lies outside
of plane . (Contributed by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem45 35003 |
Lemma for dath 35022. Dummy center of perspectivity is not on the
line . (Contributed by NM,
16-Aug-2012.)
|
|
| ||
| Theorem | dalem46 35004 |
Lemma for dath 35022. Analogue of dalem45 35003 for .
(Contributed
by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem47 35005 |
Lemma for dath 35022. Analogue of dalem45 35003 for .
(Contributed
by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem48 35006 |
Lemma for dath 35022. Analogue of dalem45 35003 for .
(Contributed
by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem49 35007 |
Lemma for dath 35022. Analogue of dalem45 35003 for .
(Contributed
by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem50 35008 |
Lemma for dath 35022. Analogue of dalem45 35003 for .
(Contributed
by NM, 16-Aug-2012.)
|
|
| ||
| Theorem | dalem51 35009 |
Lemma for dath 35022. 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 35010 |
Lemma for dath 35022. Lines and intersect at an atom.
(Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem53 35011 |
Lemma for dath 35022. The auxliary axis of perspectivity  is a line
(analogous to the actual axis of perspectivity  in dalem15 34964.
(Contributed by NM, 8-Aug-2012.)
|
 
| ||
| Theorem | dalem54 35012 |
Lemma for dath 35022. Line
intersects the auxiliary axis of
perspectivity . (Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem55 35013 |
Lemma for dath 35022. Lines and intersect at the
auxiliary line (later shown to be an axis of perspectivity; see
dalem60 35018). (Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem56 35014 |
Lemma for dath 35022. Analogue of dalem55 35013 for line .
(Contributed by NM, 8-Aug-2012.)
|
|
| ||
| Theorem | dalem57 35015 |
Lemma for dath 35022. Axis of perspectivity point  is on the
auxiliary line . (Contributed by NM, 9-Aug-2012.)
|
|
| ||
| Theorem | dalem58 35016 |
Lemma for dath 35022. Analogue of dalem57 35015 for  . (Contributed by
NM, 10-Aug-2012.)
|
|
| ||
| Theorem | dalem59 35017 |
Lemma for dath 35022. Analogue of dalem57 35015 for  . (Contributed by
NM, 10-Aug-2012.)
|
|
| ||
| Theorem | dalem60 35018 |
Lemma for dath 35022. is an axis of perspectivity (almost).
(Contributed by NM, 11-Aug-2012.)
|
|
| ||
| Theorem | dalem61 35019 |
Lemma for dath 35022. 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 35020 |
Lemma for dath 35022. Eliminate the condition containing dummy
variables and
. (Contributed by NM,
11-Aug-2012.)
|
|
| ||
| Theorem | dalem63 35021 |
Lemma for dath 35022. 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 35022 |
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 35172 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 35023 | Version of Desargues' Theorem dath 35022 with a different variable ordering. (Contributed by NM, 7-Oct-2012.) |
|
| ||
| Theorem | lineset 35024* | The set of lines in a Hilbert lattice. (Contributed by NM, 19-Sep-2011.) |
     
 | ||
| Theorem | isline 35025* | The predicate "is a line". (Contributed by NM, 19-Sep-2011.) |
|
| ||
| Theorem | islinei 35026* | Condition implying "is a line". (Contributed by NM, 3-Feb-2012.) |
|
| ||
| Theorem | pointsetN 35027* | The set of points in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.) |
| ||
| Theorem | ispointN 35028* | The predicate "is a point". (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | atpointN 35029 | The singleton of an atom is a point. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
| | ||
| Theorem | psubspset 35030* | The set of projective subspaces in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) |
 
| ||
| Theorem | ispsubsp 35031* | The predicate "is a projective subspace". (Contributed by NM, 2-Oct-2011.) |
|
| ||
| Theorem | ispsubsp2 35032* | The predicate "is a projective subspace". (Contributed by NM, 13-Jan-2012.) |
|
| ||
| Theorem | psubspi 35033* | Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) |
|
| ||
| Theorem | psubspi2N 35034 | Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 0psubN 35035 | 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 35036 | The singleton of an atom is a projective subspace. (Contributed by NM, 9-Sep-2013.) (New usage is discouraged.) |
 | ||
| Theorem | pointpsubN 35037 | 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 35038 | A line is a projective subspace. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.) |
 | ||
| Theorem | atpsubN 35039 | 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 35040 | A projective subspace consists of atoms. (Contributed by NM, 4-Nov-2011.) |
|
| ||
| Theorem | psubatN 35041 | A member of a projective subspace is an atom. (Contributed by NM, 4-Nov-2011.) (New usage is discouraged.) |
|
| ||
| Theorem | pmapfval 35042* | The projective map of a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) |
    | ||
| Theorem | pmapval 35043* | 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 35044 | Member of a projective map. (Contributed by NM, 27-Jan-2012.) |
|
| ||
| Theorem | pmapssat 35045 | The projective map of a Hilbert lattice is a set of atoms. (Contributed by NM, 14-Jan-2012.) |
| | ||
| Theorem | pmapssbaN 35046 | A weakening of pmapssat 35045 to shorten some proofs. (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.) |
| | ||
| Theorem | pmaple 35047 | 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 35048 | 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 35049 | The projective map of an atom. (Contributed by NM, 25-Jan-2012.) |
|
| ||
| Theorem | elpmapat 35050 | Member of the projective map of an atom. (Contributed by NM, 27-Jan-2012.) |
|
| ||
| Theorem | pmap0 35051 | 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 35052 | A projective map value is zero iff its argument is lattice zero. (Contributed by NM, 27-Jan-2012.) |
| | ||
| Theorem | pmap1N 35053 | 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 35054 | 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 35055* |
The projective map of the GLB of a set of lattice elements. Index-set
version of pmapglb 35056, where we read as  . Theorem
15.5.2 of [MaedaMaeda] p. 62.
(Contributed by NM, 5-Dec-2011.)
|
 | ||
| Theorem | pmapglb 35056* |
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 35057* |
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 35058* |
The projective map of the GLB of a set of lattice elements. Index-set
version of pmapglb2N 35057, 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 35059 | The projective map of a meet. (Contributed by NM, 25-Jan-2012.) |
|
| ||
| Theorem | isline2 35060* | Definition of line in terms of projective map. (Contributed by NM, 25-Jan-2012.) |
|
| ||
| Theorem | linepmap 35061 | A line described with a projective map. (Contributed by NM, 3-Feb-2012.) |
|
| ||
| Theorem | isline3 35062* | Definition of line in terms of original lattice elements. (Contributed by NM, 29-Apr-2012.) |
|
| ||
| Theorem | isline4N 35063* | Definition of line in terms of original lattice elements. (Contributed by NM, 16-Jun-2012.) (New usage is discouraged.) |
| ||
| Theorem | lneq2at 35064 | A line equals the join of any two of its distinct points (atoms). (Contributed by NM, 29-Apr-2012.) |
|
| ||
| Theorem | lnatexN 35065* | There is an atom in a line different from any other. (Contributed by NM, 30-Apr-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | lnjatN 35066* | 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 35067 | A lattice element covered by a line is an atom. (Contributed by NM, 28-Apr-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | lncvrat 35068 | A line covers the atoms it contains. (Contributed by NM, 30-Apr-2012.) |
| | ||
| Theorem | lncmp 35069 | If two lines are comparable, they are equal. (Contributed by NM, 30-Apr-2012.) |
|
| ||
| Theorem | 2lnat 35070 | Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012.) |
|
| ||
| Theorem | 2atm2atN 35071 | Two joins with a common atom have a nonzero meet. (Contributed by NM, 4-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | 2llnma1b 35072 | Generalization of 2llnma1 35073. (Contributed by NM, 26-Apr-2013.) |
|
| ||
| Theorem | 2llnma1 35073 | Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 11-Oct-2012.) |
|
| ||
| Theorem | 2llnma3r 35074 | Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 30-Apr-2013.) |
|
| ||
| Theorem | 2llnma2 35075 | Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 28-May-2012.) |
|
| ||
| Theorem | 2llnma2rN 35076 | 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 35077 | 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 35078 | 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 35079 | Lemma for cdlemb 35080. (Contributed by NM, 8-May-2012.) |
 
| ||
| Theorem | cdlemb 35080* | 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 35081 | Extend class notation with projective subspace sum. |
   | ||
| Definition | df-padd 35082* | 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 35083* | Projective subspace sum operation. (Contributed by NM, 29-Dec-2011.) |
| ||
| Theorem | paddval 35084* | Projective subspace sum operation value. (Contributed by NM, 29-Dec-2011.) |
|
| ||
| Theorem | elpadd 35085* | Member of a projective subspace sum. (Contributed by NM, 29-Dec-2011.) |
| ||
| Theorem | elpaddn0 35086* | Member of projective subspace sum of nonempty sets. (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | paddvaln0N 35087* | Projective subspace sum operation value for nonempty sets. (Contributed by NM, 27-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | elpaddri 35088 | Condition implying membership in a projective subspace sum. (Contributed by NM, 8-Jan-2012.) |
|
| ||
| Theorem | elpaddatriN 35089 | Condition implying membership in a projective subspace sum with a point. (Contributed by NM, 1-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | elpaddat 35090* | Membership in a projective subspace sum with a point. (Contributed by NM, 29-Jan-2012.) |
|
| ||
| Theorem | elpaddatiN 35091* | Consequence of membership in a projective subspace sum with a point. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | elpadd2at 35092 | Membership in a projective subspace sum of two points. (Contributed by NM, 29-Jan-2012.) |
|
| ||
| Theorem | elpadd2at2 35093 | Membership in a projective subspace sum of two points. (Contributed by NM, 8-Mar-2012.) |
|
| ||
| Theorem | paddunssN 35094 | Projective subspace sum includes the set union of its arguments. (Contributed by NM, 12-Jan-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | elpadd0 35095 | Member of projective subspace sum with at least one empty set. (Contributed by NM, 29-Dec-2011.) |
|
| ||
| Theorem | paddval0 35096 | Projective subspace sum with at least one empty set. (Contributed by NM, 11-Jan-2012.) |
|
| ||
| Theorem | padd01 35097 | Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012.) |
| | ||
| Theorem | padd02 35098 | Projective subspace sum with an empty set. (Contributed by NM, 11-Jan-2012.) |
|
| ||
| Theorem | paddcom 35099 | Projective subspace sum commutes. (Contributed by NM, 3-Jan-2012.) |
|
| ||
| Theorem | paddssat 35100 | A projective subspace sum is a set of atoms. (Contributed by NM, 3-Jan-2012.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |