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-21514) |
Hilbert Space Explorer
(21515-23037) |
Users' Mathboxes
(23038-32776) |

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

Statement | ||

Theorem | cdlemg2dN 31401* | This theorem can be used to shorten hypothesis. TODO: Fix comment. (Contributed by NM, 21-Apr-2013.) (New usage is discouraged.) |

Theorem | cdlemg2cex 31402* | Any translation is one of our s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf 31374? (Contributed by NM, 22-Apr-2013.) |

Theorem | cdlemg2ce 31403* | Utility theorem to eliminate p,q when converting theorems with explicit f. TODO: fix comment. (Contributed by NM, 22-Apr-2013.) |

Theorem | cdlemg2jlemOLDN 31404* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT . f preserves join: f(r s) = f(r) s, p. 115 10th line from bottom. TODO: Combine with cdlemg2jOLDN 31409? (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.) |

Theorem | cdlemg2fvlem 31405* | Lemma for cdlemg2fv 31410. (Contributed by NM, 23-Apr-2013.) |

Theorem | cdlemg2klem 31406* | cdleme42keg 31297 with simpler hypotheses. TODO: FIX COMMENT (Contributed by NM, 22-Apr-2013.) |

Theorem | cdlemg2idN 31407 | Version of cdleme31id 31205 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 21-Apr-2013.) (New usage is discouraged.) |

Theorem | cdlemg3a 31408 | Part of proof of Lemma G in [Crawley] p. 116, line 19. Show p q = p u. TODO: reformat cdleme0cp 31025 to match this, then replace with cdleme0cp 31025. (Contributed by NM, 19-Apr-2013.) |

Theorem | cdlemg2jOLDN 31409 | TODO: Replace this with ltrnj 30943. (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.) |

Theorem | cdlemg2fv 31410 | Value of a translation in terms of an associated atom. cdleme48fvg 31311 with simpler hypotheses. TODO: Use ltrnj 30943 to vastly simplify. (Contributed by NM, 23-Apr-2013.) |

Theorem | cdlemg2fv2 31411 | Value of a translation in terms of an associated atom. TODO: FIX COMMENT TODO: Is this useful elsewhere e.g. around cdlemeg46fjv 31334 that use more complex proofs? TODO: Use ltrnj 30943 to vastly simplify. (Contributed by NM, 23-Apr-2013.) |

Theorem | cdlemg2k 31412 | cdleme42keg 31297 with simpler hypotheses. TODO: FIX COMMENT Todo: derive from cdlemg3a 31408, cdlemg2fv2 31411, cdlemg2jOLDN 31409, ltrnel 30950? (Contributed by NM, 22-Apr-2013.) |

Theorem | cdlemg2kq 31413 | cdlemg2k 31412 with and swapped. TODO: FIX COMMENT (Contributed by NM, 15-May-2013.) |

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

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

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

Theorem | cdlemb3 31417* | 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 30816? Then replace cdlemb2 30852 with it. This is a more general version of cdlemb2 30852 without condition. (Contributed by NM, 27-Apr-2013.) |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem | cdlemg10b 31446 | 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 31447 | TODO: FIX COMMENT TODO: Can this be moved up as a stand-alone theorem in ltrn* area? TODO: Compare this proof to cdlemg2m 31415 and pick best, if moved to ltrn* area. (Contributed by NM, 4-May-2013.) (New usage is discouraged.) |

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

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

Theorem | cdlemg10c 31450 | 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 31451 | TODO: FIX COMMENT (Contributed by NM, 3-May-2013.) |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem | cdlemg16 31468 | Part of proof of Lemma G of [Crawley] p. 116; 2nd line p. 117, which says that (our) cdlemg10 31452 "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 30697, in order to make this inference. This final step eliminates the condition from cdlemg12 31461. 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 31469 | This version of cdlemg16 31468 uses cdlemg15a 31466 instead of cdlemg15 31467, in case cdlemg15 31467 ends up not being needed. TODO: FIX COMMENT (Contributed by NM, 6-May-2013.) (New usage is discouraged.) |

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

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

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

Theorem | cdlemg17b 31473* | 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 31101. (Contributed by NM, 8-May-2013.) |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem | cdlemg17 31488* | 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 31489 | Show two lines are different. TODO: fix comment. (Contributed by NM, 14-May-2013.) |

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

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