Home | Metamath
Proof ExplorerTheorem List
(p. 315 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-22421) |
Hilbert Space Explorer
(22422-23944) |
Users' Mathboxes
(23945-32762) |

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

Statement | ||

Theorem | cdlemg2m 31401 | TODO: FIX COMMENT T (Contributed by NM, 25-Apr-2013.) |

Theorem | cdlemg5 31402* | TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle 30802? TODO: The hypothesis is unused. FIX COMMENT (Contributed by NM, 26-Apr-2013.) |

Theorem | cdlemb3 31403* | Given two atoms not under the fiducial co-atom , there is a third. Lemma B in [Crawley] p. 112. TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle 30802? Then replace cdlemb2 30838 with it. This is a more general version of cdlemb2 30838 without condition. (Contributed by NM, 27-Apr-2013.) |

Theorem | cdlemg7fvbwN 31404 | Properties of a translation of an element not under . TODO: Fix comment. Can this be simplified? Perhaps derived from cdleme48bw 31299? Done with a *ltrn* theorem? (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | cdlemg4a 31405 | TODO: FIX COMMENT If fg(p) = p, then tr f = tr g. (Contributed by NM, 23-Apr-2013.) |

Theorem | cdlemg4b1 31406 | TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.) |

Theorem | cdlemg4b2 31407 | TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.) |

Theorem | cdlemg4b12 31408 | TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.) |

Theorem | cdlemg4c 31409 | TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.) |

Theorem | cdlemg4d 31410 | TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.) |

Theorem | cdlemg4e 31411 | TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.) |

Theorem | cdlemg4f 31412 | TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.) |

Theorem | cdlemg4g 31413 | TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.) |

Theorem | cdlemg4 31414 | TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.) |

Theorem | cdlemg6a 31415* | TODO: FIX COMMENT TODO: replace with cdlemg4 31414. (Contributed by NM, 27-Apr-2013.) |

Theorem | cdlemg6b 31416* | TODO: FIX COMMENT TODO: replace with cdlemg4 31414. (Contributed by NM, 27-Apr-2013.) |

Theorem | cdlemg6c 31417* | TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.) |

Theorem | cdlemg6d 31418* | TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.) |

Theorem | cdlemg6e 31419 | TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.) |

Theorem | cdlemg6 31420 | TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.) |

Theorem | cdlemg7fvN 31421 | Value of a translation composition in terms of an associated atom. (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | cdlemg7aN 31422 | TODO: FIX COMMENT (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | cdlemg7N 31423 | TODO: FIX COMMENT (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.) |

Theorem | cdlemg8a 31424 | TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.) |

Theorem | cdlemg8b 31425 | TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.) |

Theorem | cdlemg8c 31426 | TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.) |

Theorem | cdlemg8d 31427 | TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.) |

Theorem | cdlemg8 31428 | TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.) |

Theorem | cdlemg9a 31429 | TODO: FIX COMMENT (Contributed by NM, 1-May-2013.) |

Theorem | cdlemg9b 31430 | The triples and are centrally perspective. TODO: FIX COMMENT (Contributed by NM, 1-May-2013.) |

Theorem | cdlemg9 31431 | The triples and are axially perspective by dalaw 30683. Part of Lemma G of [Crawley] p. 116, last 2 lines. TODO: FIX COMMENT (Contributed by NM, 1-May-2013.) |

Theorem | cdlemg10b 31432 | TODO: FIX COMMENT TODO: Can this be moved up as a stand-alone theorem in ltrn* area? (Contributed by NM, 4-May-2013.) |

Theorem | cdlemg10bALTN 31433 | TODO: FIX COMMENT TODO: Can this be moved up as a stand-alone theorem in ltrn* area? TODO: Compare this proof to cdlemg2m 31401 and pick best, if moved to ltrn* area. (Contributed by NM, 4-May-2013.) (New usage is discouraged.) |

Theorem | cdlemg11a 31434 | TODO: FIX COMMENT (Contributed by NM, 4-May-2013.) |

Theorem | cdlemg11aq 31435 | TODO: FIX COMMENT TODO: can proof using this be restructured to use cdlemg11a 31434? (Contributed by NM, 4-May-2013.) |

Theorem | cdlemg10c 31436 | TODO: FIX COMMENT TODO: Can this be moved up as a stand-alone theorem in trl* area? (Contributed by NM, 4-May-2013.) |

Theorem | cdlemg10a 31437 | TODO: FIX COMMENT (Contributed by NM, 3-May-2013.) |

Theorem | cdlemg10 31438 | TODO: FIX COMMENT (Contributed by NM, 4-May-2013.) |

Theorem | cdlemg11b 31439 | TODO: FIX COMMENT (Contributed by NM, 5-May-2013.) |

Theorem | cdlemg12a 31440 | TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.) |

Theorem | cdlemg12b 31441 | The triples and are centrally perspective. TODO: FIX COMMENT (Contributed by NM, 5-May-2013.) |

Theorem | cdlemg12c 31442 | The triples and are axially perspective by dalaw 30683. TODO: FIX COMMENT (Contributed by NM, 5-May-2013.) |

Theorem | cdlemg12d 31443 | TODO: FIX COMMENT (Contributed by NM, 5-May-2013.) |

Theorem | cdlemg12e 31444 | TODO: FIX COMMENT (Contributed by NM, 6-May-2013.) |

Theorem | cdlemg12f 31445 | TODO: FIX COMMENT (Contributed by NM, 6-May-2013.) |

Theorem | cdlemg12g 31446 | TODO: FIX COMMENT TODO: Combine with cdlemg12f 31445. (Contributed by NM, 6-May-2013.) |

Theorem | cdlemg12 31447 | TODO: FIX COMMENT (Contributed by NM, 6-May-2013.) |

Theorem | cdlemg13a 31448 | TODO: FIX COMMENT (Contributed by NM, 6-May-2013.) |

Theorem | cdlemg13 31449 | TODO: FIX COMMENT (Contributed by NM, 6-May-2013.) |

Theorem | cdlemg14f 31450 | TODO: FIX COMMENT (Contributed by NM, 6-May-2013.) |

Theorem | cdlemg14g 31451 | TODO: FIX COMMENT (Contributed by NM, 22-May-2013.) |

Theorem | cdlemg15a 31452 | Eliminate the condition from cdlemg13 31449. TODO: FIX COMMENT (Contributed by NM, 6-May-2013.) |

Theorem | cdlemg15 31453 | Eliminate the condition from cdlemg13 31449. TODO: FIX COMMENT (Contributed by NM, 25-May-2013.) |

Theorem | cdlemg16 31454 | Part of proof of Lemma G of [Crawley] p. 116; 2nd line p. 117, which says that (our) cdlemg10 31438 "implies (2)" (of p. 116). No details are provided by the authors, so there may be a shorter proof; but ours requires the 14 lemmas, one using Desargues' law dalaw 30683, in order to make this inference. This final step eliminates the condition from cdlemg12 31447. TODO: FIX COMMENT TODO: should we also eliminate here (or earlier)? Do it if we don't need to add it in for something else later. (Contributed by NM, 6-May-2013.) |

Theorem | cdlemg16ALTN 31455 | This version of cdlemg16 31454 uses cdlemg15a 31452 instead of cdlemg15 31453, in case cdlemg15 31453 ends up not being needed. TODO: FIX COMMENT (Contributed by NM, 6-May-2013.) (New usage is discouraged.) |

Theorem | cdlemg16z 31456 | Eliminate condition from cdlemg16 31454. TODO: would it help to also eliminate here or later? (Contributed by NM, 25-May-2013.) |

Theorem | cdlemg16zz 31457 | Eliminate from cdlemg16z 31456. TODO: Use this only if needed. (Contributed by NM, 26-May-2013.) |

Theorem | cdlemg17a 31458 | TODO: FIX COMMENT (Contributed by NM, 8-May-2013.) |

Theorem | cdlemg17b 31459* | Part of proof of Lemma G in [Crawley] p. 117, 4th line. Whenever (in their terminology) p q/0 (i.e. the sublattice from 0 to p q) contains precisely three atoms and g is not the identity, g(p) = q. See also comments under cdleme0nex 31087. (Contributed by NM, 8-May-2013.) |

Theorem | cdlemg17dN 31460* | TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.) |

Theorem | cdlemg17dALTN 31461 | Same as cdlemg17dN 31460 with fewer antecedents but longer proof TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.) |

Theorem | cdlemg17e 31462* | TODO: fix comment. (Contributed by NM, 8-May-2013.) |

Theorem | cdlemg17f 31463* | TODO: fix comment. (Contributed by NM, 8-May-2013.) |

Theorem | cdlemg17g 31464* | TODO: fix comment. (Contributed by NM, 9-May-2013.) |

Theorem | cdlemg17h 31465* | TODO: fix comment. (Contributed by NM, 10-May-2013.) |

Theorem | cdlemg17i 31466* | TODO: fix comment. (Contributed by NM, 10-May-2013.) |

Theorem | cdlemg17ir 31467* | TODO: fix comment. (Contributed by NM, 13-May-2013.) |

Theorem | cdlemg17j 31468* | TODO: fix comment. (Contributed by NM, 11-May-2013.) |

Theorem | cdlemg17pq 31469* | Utility theorem for swapping and . TODO: fix comment. (Contributed by NM, 11-May-2013.) |

Theorem | cdlemg17bq 31470* | cdlemg17b 31459 with and swapped. Antecedent is redundant for easier use. TODO: should we have redundant antecedent for cdlemg17b 31459 also? (Contributed by NM, 13-May-2013.) |

Theorem | cdlemg17iqN 31471* | cdlemg17i 31466 with and swapped. (Contributed by NM, 13-May-2013.) (New usage is discouraged.) |

Theorem | cdlemg17irq 31472* | cdlemg17ir 31467 with and swapped. (Contributed by NM, 13-May-2013.) |

Theorem | cdlemg17jq 31473* | cdlemg17j 31468 with and swapped. (Contributed by NM, 13-May-2013.) |

Theorem | cdlemg17 31474* | Part of Lemma G of [Crawley] p. 117, lines 7 and 8. We show an argument whose value at equals itself. TODO: fix comment. (Contributed by NM, 12-May-2013.) |

Theorem | cdlemg18a 31475 | Show two lines are different. TODO: fix comment. (Contributed by NM, 14-May-2013.) |

Theorem | cdlemg18b 31476 | Lemma for cdlemg18c 31477. TODO: fix comment. (Contributed by NM, 15-May-2013.) |

Theorem | cdlemg18c 31477 | Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.) |

Theorem | cdlemg18d 31478* | Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.) |

Theorem | cdlemg18 31479* | Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.) |

Theorem | cdlemg19a 31480* | Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.) |

Theorem | cdlemg19 31481* | Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.) |

Theorem | cdlemg20 31482* | Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 23-May-2013.) |

Theorem | cdlemg21 31483* | Version of cdlemg19 with instead of as a condition. (Contributed by NM, 23-May-2013.) |

Theorem | cdlemg22 31484* | cdlemg21 31483 with condition removed. (Contributed by NM, 23-May-2013.) |

Theorem | cdlemg24 31485* | Combine cdlemg16z 31456 and cdlemg22 31484. TODO: Fix comment. (Contributed by NM, 24-May-2013.) |

Theorem | cdlemg37 31486* | Use cdlemg8 31428 to eliminate the condition of cdlemg24 31485. (Contributed by NM, 31-May-2013.) |

Theorem | cdlemg25zz 31487 | cdlemg16zz 31457 restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-2013.) |

Theorem | cdlemg26zz 31488 | cdlemg16zz 31457 restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-2013.) |

Theorem | cdlemg27a 31489 | For use with case when or is zero, letting us establish via 4atex 30873. TODO: Fix comment. (Contributed by NM, 28-May-2013.) |

Theorem | cdlemg28a 31490 | Part of proof of Lemma G of [Crawley] p. 116. First equality of the equation of line 14 on p. 117. (Contributed by NM, 29-May-2013.) |

Theorem | cdlemg31b0N 31491 | TODO: Fix comment. (Contributed by NM, 30-May-2013.) (New usage is discouraged.) |