Home | Metamath
Proof ExplorerTheorem List
(p. 305 of 328)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21514) |
Hilbert Space Explorer
(21515-23037) |
Users' Mathboxes
(23038-32776) |

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | lvolnelpln 30401 | No lattice volume is a lattice plane. (Contributed by NM, 19-Jun-2012.) |

Theorem | lvoln0N 30402 | A lattice volume is non-zero. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |

Theorem | islvol2aN 30403 | The predicate "is a lattice volume". (Contributed by NM, 16-Jul-2012.) (New usage is discouraged.) |

Theorem | 4atlem0a 30404 | Lemma for 4at 30424. (Contributed by NM, 10-Jul-2012.) |

Theorem | 4atlem0ae 30405 | Lemma for 4at 30424. (Contributed by NM, 10-Jul-2012.) |

Theorem | 4atlem0be 30406 | Lemma for 4at 30424. (Contributed by NM, 10-Jul-2012.) |

Theorem | 4atlem3 30407 | Lemma for 4at 30424. Break inequality into 4 cases. (Contributed by NM, 8-Jul-2012.) |

Theorem | 4atlem3a 30408 | Lemma for 4at 30424. Break inequality into 3 cases. (Contributed by NM, 9-Jul-2012.) |

Theorem | 4atlem3b 30409 | Lemma for 4at 30424. Break inequality into 2 cases. (Contributed by NM, 9-Jul-2012.) |

Theorem | 4atlem4a 30410 | Lemma for 4at 30424. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |

Theorem | 4atlem4b 30411 | Lemma for 4at 30424. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |

Theorem | 4atlem4c 30412 | Lemma for 4at 30424. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |

Theorem | 4atlem4d 30413 | Lemma for 4at 30424. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |

Theorem | 4atlem9 30414 | Lemma for 4at 30424. Substitute for . (Contributed by NM, 9-Jul-2012.) |

Theorem | 4atlem10a 30415 | Lemma for 4at 30424. Substitute for . (Contributed by NM, 9-Jul-2012.) |

Theorem | 4atlem10b 30416 | Lemma for 4at 30424. Substitute for (cont.). (Contributed by NM, 10-Jul-2012.) |

Theorem | 4atlem10 30417 | Lemma for 4at 30424. Combine both possible cases. (Contributed by NM, 9-Jul-2012.) |

Theorem | 4atlem11a 30418 | Lemma for 4at 30424. Substitute for . (Contributed by NM, 9-Jul-2012.) |

Theorem | 4atlem11b 30419 | Lemma for 4at 30424. Substitute for (cont.). (Contributed by NM, 10-Jul-2012.) |

Theorem | 4atlem11 30420 | Lemma for 4at 30424. Combine all three possible cases. (Contributed by NM, 10-Jul-2012.) |

Theorem | 4atlem12a 30421 | Lemma for 4at 30424. Substitute for . (Contributed by NM, 9-Jul-2012.) |

Theorem | 4atlem12b 30422 | Lemma for 4at 30424. Substitute for (cont.). (Contributed by NM, 11-Jul-2012.) |

Theorem | 4atlem12 30423 | Lemma for 4at 30424. Combine all four possible cases. (Contributed by NM, 11-Jul-2012.) |

Theorem | 4at 30424 | Four atoms determine a lattice volume uniquely. Three-dimensional analog of ps-1 30288 and 3at 30301. (Contributed by NM, 11-Jul-2012.) |

Theorem | 4at2 30425 | Four atoms determine a lattice volume uniquely. (Contributed by NM, 11-Jul-2012.) |

Theorem | lplncvrlvol2 30426 | A lattice line under a lattice plane is covered by it. (Contributed by NM, 12-Jul-2012.) |

Theorem | lplncvrlvol 30427 | An element covering a lattice plane is a lattice volume and vice-versa. (Contributed by NM, 15-Jul-2012.) |

Theorem | lvolcmp 30428 | If two lattice planes are comparable, they are equal. (Contributed by NM, 12-Jul-2012.) |

Theorem | lvolnltN 30429 | Two lattice volumes cannot satisfy the less than relation. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |

Theorem | 2lplnja 30430 | The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 30431 in terms of atoms). (Contributed by NM, 12-Jul-2012.) |

Theorem | 2lplnj 30431 | The join of two different lattice planes in a (3-dimensional) lattice volume equals the volume. (Contributed by NM, 12-Jul-2012.) |

Theorem | 2lplnm2N 30432 | 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.) |

Theorem | 2lplnmj 30433 | 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 30434 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemkelat 30435 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemkeop 30436 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalempea 30437 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemqea 30438 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemrea 30439 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemsea 30440 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemtea 30441 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemuea 30442 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemyeo 30443 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemzeo 30444 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemclpjs 30445 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemclqjt 30446 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemclrju 30447 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalem-clpjq 30448 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemceb 30449 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalempeb 30450 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemqeb 30451 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemreb 30452 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemseb 30453 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemteb 30454 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemueb 30455 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalempjqeb 30456 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemsjteb 30457 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemtjueb 30458 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemqrprot 30459 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemyeb 30460 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemcnes 30461 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalempnes 30462 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemqnet 30463 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalempjsen 30464 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemply 30465 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |

Theorem | dalemsly 30466 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |

Theorem | dalemswapyz 30467 | Lemma for dath 30547. Swap the role of planes and to allow reuse of analogous proofs. (Contributed by NM, 14-Aug-2012.) |

Theorem | dalemrot 30468 | Lemma for dath 30547. Rotate triangles and to allow reuse of analogous proofs. (Contributed by NM, 14-Aug-2012.) |

Theorem | dalemrotyz 30469 | Lemma for dath 30547. Rotate triangles and to allow reuse of analogous proofs. (Contributed by NM, 19-Aug-2012.) |

Theorem | dalem1 30470 | Lemma for dath 30547. Show the lines and are different. (Contributed by NM, 9-Aug-2012.) |

Theorem | dalemcea 30471 | Lemma for dath 30547. 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 30472 | Lemma for dath 30547. Show the lines and form a plane. (Contributed by NM, 11-Aug-2012.) |

Theorem | dalemdea 30473 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 11-Aug-2012.) |

Theorem | dalemeea 30474 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 11-Aug-2012.) |

Theorem | dalem3 30475 | Lemma for dalemdnee 30477. (Contributed by NM, 10-Aug-2012.) |

Theorem | dalem4 30476 | Lemma for dalemdnee 30477. (Contributed by NM, 10-Aug-2012.) |

Theorem | dalemdnee 30477 | Lemma for dath 30547. Axis of perspectivity points and are different. (Contributed by NM, 10-Aug-2012.) |

Theorem | dalem5 30478 | Lemma for dath 30547. Atom (in plane ) belongs to the 3-dimensional volume formed by and . (Contributed by NM, 21-Jul-2012.) |

Theorem | dalem6 30479 | Lemma for dath 30547. Analog of dalem5 30478 for . (Contributed by NM, 21-Jul-2012.) |

Theorem | dalem7 30480 | Lemma for dath 30547. Analog of dalem5 30478 for . (Contributed by NM, 21-Jul-2012.) |

Theorem | dalem8 30481 | Lemma for dath 30547. Plane belongs to the 3-dimensional space. (Contributed by NM, 21-Jul-2012.) |

Theorem | dalem-cly 30482 | Lemma for dalem9 30483. Center of perspectivity is not in plane (when and are different planes). (Contributed by NM, 13-Aug-2012.) |

Theorem | dalem9 30483 | Lemma for dath 30547. Since , the join forms a 3-dimensional space. (Contributed by NM, 20-Jul-2012.) |

Theorem | dalem10 30484 | Lemma for dath 30547. Atom belongs to the axis of perspectivity . (Contributed by NM, 19-Jul-2012.) |

Theorem | dalem11 30485 | Lemma for dath 30547. Analog of dalem10 30484 for . (Contributed by NM, 23-Jul-2012.) |

Theorem | dalem12 30486 | Lemma for dath 30547. Analog of dalem10 30484 for . (Contributed by NM, 11-Aug-2012.) |

Theorem | dalem13 30487 | Lemma for dalem14 30488. (Contributed by NM, 21-Jul-2012.) |

Theorem | dalem14 30488 | Lemma for dath 30547. Planes and form a 3-dimensional space (when they are different). (Contributed by NM, 22-Jul-2012.) |

Theorem | dalem15 30489 | Lemma for dath 30547. The axis of perspectivity is a line. (Contributed by NM, 21-Jul-2012.) |

Theorem | dalem16 30490 | Lemma for dath 30547. 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 30491 | Lemma for dath 30547. When planes and are equal, the center of perspectivity is in . (Contributed by NM, 1-Aug-2012.) |

Theorem | dalem18 30492* | Lemma for dath 30547. 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 30493* | Lemma for dath 30547. 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 30494 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |

Theorem | dalemddea 30495 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |

Theorem | dalem-ccly 30496 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |

Theorem | dalem-ddly 30497 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |

Theorem | dalemccnedd 30498 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |

Theorem | dalemclccjdd 30499 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |

Theorem | dalemcceb 30500 | Lemma for dath 30547. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |