HomeTheorem List (p. 327 of 389)
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. 327 of 389) | < 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-26249) |
Hilbert Space Explorer
(26250-27773) |
Users' Mathboxes
(27774-38860) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | lvolnlelln 32601 | A lattice line cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
                ![/\](wedge.gif "/\"){kind=small}  
  | ||
| Theorem | lvolnlelpln 32602 | A lattice plane cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
 
| ||
| Theorem | 3atnelvolN 32603 | The join of 3 atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
     
| ||
| Theorem | 2atnelvolN 32604 | The join of two atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | lvolneatN 32605 | No lattice volume is an atom. (Contributed by NM, 15-Jul-2012.) (New usage is discouraged.) |
| | ||
| Theorem | lvolnelln 32606 | No lattice volume is a lattice line. (Contributed by NM, 15-Jul-2012.) |
| | ||
| Theorem | lvolnelpln 32607 | No lattice volume is a lattice plane. (Contributed by NM, 19-Jun-2012.) |
| | ||
| Theorem | lvoln0N 32608 | A lattice volume is non-zero. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
   | ||
| Theorem | islvol2aN 32609 | The predicate "is a lattice volume". (Contributed by NM, 16-Jul-2012.) (New usage is discouraged.) |
| ||
| Theorem | 4atlem0a 32610 | Lemma for 4at 32630. (Contributed by NM, 10-Jul-2012.) |
|
| ||
| Theorem | 4atlem0ae 32611 | Lemma for 4at 32630. (Contributed by NM, 10-Jul-2012.) |
|
| ||
| Theorem | 4atlem0be 32612 | Lemma for 4at 32630. (Contributed by NM, 10-Jul-2012.) |
|
| ||
| Theorem | 4atlem3 32613 | Lemma for 4at 32630. Break inequality into 4 cases. (Contributed by NM, 8-Jul-2012.) |
| ||
| Theorem | 4atlem3a 32614 | Lemma for 4at 32630. Break inequality into 3 cases. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem3b 32615 | Lemma for 4at 32630. Break inequality into 2 cases. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem4a 32616 | Lemma for 4at 32630. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem4b 32617 | Lemma for 4at 32630. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem4c 32618 | Lemma for 4at 32630. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem4d 32619 | Lemma for 4at 32630. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem9 32620 |
Lemma for 4at 32630. Substitute  for . (Contributed by NM,
9-Jul-2012.)
|
|
| ||
| Theorem | 4atlem10a 32621 |
Lemma for 4at 32630. Substitute for . (Contributed by NM,
9-Jul-2012.)
|
|
| ||
| Theorem | 4atlem10b 32622 |
Lemma for 4at 32630. Substitute for (cont.). (Contributed by
NM, 10-Jul-2012.)
|
|
| ||
| Theorem | 4atlem10 32623 | Lemma for 4at 32630. Combine both possible cases. (Contributed by NM, 9-Jul-2012.) |
|
| ||
| Theorem | 4atlem11a 32624 |
Lemma for 4at 32630. Substitute for . (Contributed by NM,
9-Jul-2012.)
|
|
| ||
| Theorem | 4atlem11b 32625 |
Lemma for 4at 32630. Substitute for (cont.). (Contributed by
NM, 10-Jul-2012.)
|
|
| ||
| Theorem | 4atlem11 32626 | Lemma for 4at 32630. Combine all three possible cases. (Contributed by NM, 10-Jul-2012.) |
|
| ||
| Theorem | 4atlem12a 32627 |
Lemma for 4at 32630. Substitute for . (Contributed by NM,
9-Jul-2012.)
|
|
| ||
| Theorem | 4atlem12b 32628 |
Lemma for 4at 32630. Substitute for (cont.). (Contributed by
NM, 11-Jul-2012.)
|
|
| ||
| Theorem | 4atlem12 32629 | Lemma for 4at 32630. Combine all four possible cases. (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | 4at 32630 | Four atoms determine a lattice volume uniquely. Three-dimensional analog of ps-1 32494 and 3at 32507. (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | 4at2 32631 | Four atoms determine a lattice volume uniquely. (Contributed by NM, 11-Jul-2012.) |
|
| ||
| Theorem | lplncvrlvol2 32632 | A lattice line under a lattice plane is covered by it. (Contributed by NM, 12-Jul-2012.) |
  | ||
| Theorem | lplncvrlvol 32633 | An element covering a lattice plane is a lattice volume and vice-versa. (Contributed by NM, 15-Jul-2012.) |
 
| ||
| Theorem | lvolcmp 32634 | If two lattice planes are comparable, they are equal. (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | lvolnltN 32635 | Two lattice volumes cannot satisfy the less than relation. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
  | ||
| Theorem | 2lplnja 32636 | The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 32637 in terms of atoms). (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | 2lplnj 32637 | The join of two different lattice planes in a (3-dimensional) lattice volume equals the volume. (Contributed by NM, 12-Jul-2012.) |
|
| ||
| Theorem | 2lplnm2N 32638 | The meet of two different lattice planes in a lattice volume is a lattice line. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
![./\](_.wedge.gif "./\"){kind=small} 
| ||
| Theorem | 2lplnmj 32639 | The meet of two lattice planes is a lattice line iff their join is a lattice volume. (Contributed by NM, 13-Jul-2012.) |
|
| ||
| Theorem | dalemkehl 32640 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 
| ||
| Theorem | dalemkelat 32641 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 | ||
| Theorem | dalemkeop 32642 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
 | ||
| Theorem | dalempea 32643 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqea 32644 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemrea 32645 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemsea 32646 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemtea 32647 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemuea 32648 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemyeo 32649 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemzeo 32650 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclpjs 32651 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclqjt 32652 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemclrju 32653 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalem-clpjq 32654 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemceb 32655 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempeb 32656 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqeb 32657 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemreb 32658 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemseb 32659 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemteb 32660 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemueb 32661 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempjqeb 32662 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemsjteb 32663 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemtjueb 32664 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqrprot 32665 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemyeb 32666 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemcnes 32667 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempnes 32668 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemqnet 32669 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalempjsen 32670 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemply 32671 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
|
| ||
| Theorem | dalemsly 32672 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
|
| ||
| Theorem | dalemswapyz 32673 |
Lemma for dath 32753. Swap the role of planes and to allow
reuse of analogous proofs. (Contributed by NM, 14-Aug-2012.)
|
|
| ||
| Theorem | dalemrot 32674 |
Lemma for dath 32753. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
14-Aug-2012.)
|
|
| ||
| Theorem | dalemrotyz 32675 |
Lemma for dath 32753. Rotate triangles and
to allow reuse of analogous proofs. (Contributed by NM,
19-Aug-2012.)
|
|
| ||
| Theorem | dalem1 32676 |
Lemma for dath 32753. Show the lines and are different.
(Contributed by NM, 9-Aug-2012.)
|
|
| ||
| Theorem | dalemcea 32677 |
Lemma for dath 32753. Frequently-used utility lemma. Here we
show that
must be an
atom. This is an assumption in most presentations of
Desargue's theorem; instead, we assume only the is a lattice
element, in order to make later substitutions for easier.
(Contributed by NM, 23-Sep-2012.)
|
|
| ||
| Theorem | dalem2 32678 |
Lemma for dath 32753. Show the lines and form a plane.
(Contributed by NM, 11-Aug-2012.)
|
|
| ||
| Theorem | dalemdea 32679 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 11-Aug-2012.) |
| ||
| Theorem | dalemeea 32680 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 11-Aug-2012.) |
| ||
| Theorem | dalem3 32681 | Lemma for dalemdnee 32683. (Contributed by NM, 10-Aug-2012.) |
|
| ||
| Theorem | dalem4 32682 | Lemma for dalemdnee 32683. (Contributed by NM, 10-Aug-2012.) |
|
| ||
| Theorem | dalemdnee 32683 |
Lemma for dath 32753. Axis of perspectivity points and are
different. (Contributed by NM, 10-Aug-2012.)
|
|
| ||
| Theorem | dalem5 32684 |
Lemma for dath 32753. Atom (in plane ) belongs to
the 3-dimensional volume formed by and . (Contributed by
NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem6 32685 |
Lemma for dath 32753. Analog of dalem5 32684 for . (Contributed by
NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem7 32686 |
Lemma for dath 32753. Analog of dalem5 32684 for . (Contributed by
NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem8 32687 |
Lemma for dath 32753. Plane belongs to the 3-dimensional space.
(Contributed by NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem-cly 32688 |
Lemma for dalem9 32689. Center of perspectivity is not in plane
(when and are different planes). (Contributed by
NM, 13-Aug-2012.)
|
|
| ||
| Theorem | dalem9 32689 |
Lemma for dath 32753. Since
, the join forms
a 3-dimensional space. (Contributed by NM, 20-Jul-2012.)
|
|
| ||
| Theorem | dalem10 32690 |
Lemma for dath 32753. Atom belongs to the axis of perspectivity
.
(Contributed by NM, 19-Jul-2012.)
|
|
| ||
| Theorem | dalem11 32691 |
Lemma for dath 32753. Analog of dalem10 32690 for . (Contributed by
NM, 23-Jul-2012.)
|
|
| ||
| Theorem | dalem12 32692 |
Lemma for dath 32753. Analog of dalem10 32690 for  . (Contributed by
NM, 11-Aug-2012.)
|
|
| ||
| Theorem | dalem13 32693 | Lemma for dalem14 32694. (Contributed by NM, 21-Jul-2012.) |
|
| ||
| Theorem | dalem14 32694 |
Lemma for dath 32753. Planes and form a 3-dimensional space
(when they are different). (Contributed by NM, 22-Jul-2012.)
|
|
| ||
| Theorem | dalem15 32695 |
Lemma for dath 32753. The axis of perspectivity is a line.
(Contributed by NM, 21-Jul-2012.)
|
|
| ||
| Theorem | dalem16 32696 |
Lemma for dath 32753. 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 32697 |
Lemma for dath 32753. When planes and are equal, the center
of perspectivity is in .
(Contributed by NM,
1-Aug-2012.)
|
|
| ||
| Theorem | dalem18 32698* |
Lemma for dath 32753. 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 32699* |
Lemma for dath 32753. 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 32700 | Lemma for dath 32753. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
| ||
| < Previous Next > |