Home Metamath Proof ExplorerTheorem List (p. 316 of 329) < 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-22452) Hilbert Space Explorer (22453-23975) Users' Mathboxes (23976-32860)

Theorem List for Metamath Proof Explorer - 31501-31600   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcdlemb3 31501* 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 30900? Then replace cdlemb2 30936 with it. This is a more general version of cdlemb2 30936 without condition. (Contributed by NM, 27-Apr-2013.)

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

Theoremcdlemg4a 31503 TODO: FIX COMMENT If fg(p) = p, then tr f = tr g. (Contributed by NM, 23-Apr-2013.)

Theoremcdlemg4b1 31504 TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.)

Theoremcdlemg4b2 31505 TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.)

Theoremcdlemg4b12 31506 TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.)

Theoremcdlemg4c 31507 TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.)

Theoremcdlemg4d 31508 TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)

Theoremcdlemg4e 31509 TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)

Theoremcdlemg4f 31510 TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)

Theoremcdlemg4g 31511 TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)

Theoremcdlemg4 31512 TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)

Theoremcdlemg6a 31513* TODO: FIX COMMENT TODO: replace with cdlemg4 31512. (Contributed by NM, 27-Apr-2013.)

Theoremcdlemg6b 31514* TODO: FIX COMMENT TODO: replace with cdlemg4 31512. (Contributed by NM, 27-Apr-2013.)

Theoremcdlemg6c 31515* TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.)

Theoremcdlemg6d 31516* TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.)

Theoremcdlemg6e 31517 TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.)

Theoremcdlemg6 31518 TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.)

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

Theoremcdlemg7aN 31520 TODO: FIX COMMENT (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)

Theoremcdlemg7N 31521 TODO: FIX COMMENT (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)

Theoremcdlemg8a 31522 TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.)

Theoremcdlemg8b 31523 TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.)

Theoremcdlemg8c 31524 TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.)

Theoremcdlemg8d 31525 TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.)

Theoremcdlemg8 31526 TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.)

Theoremcdlemg9a 31527 TODO: FIX COMMENT (Contributed by NM, 1-May-2013.)

Theoremcdlemg9b 31528 The triples and are centrally perspective. TODO: FIX COMMENT (Contributed by NM, 1-May-2013.)

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

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

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

Theoremcdlemg11a 31532 TODO: FIX COMMENT (Contributed by NM, 4-May-2013.)

Theoremcdlemg11aq 31533 TODO: FIX COMMENT TODO: can proof using this be restructured to use cdlemg11a 31532? (Contributed by NM, 4-May-2013.)

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

Theoremcdlemg10a 31535 TODO: FIX COMMENT (Contributed by NM, 3-May-2013.)

Theoremcdlemg10 31536 TODO: FIX COMMENT (Contributed by NM, 4-May-2013.)

Theoremcdlemg11b 31537 TODO: FIX COMMENT (Contributed by NM, 5-May-2013.)

Theoremcdlemg12a 31538 TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.)

Theoremcdlemg12b 31539 The triples and are centrally perspective. TODO: FIX COMMENT (Contributed by NM, 5-May-2013.)

Theoremcdlemg12c 31540 The triples and are axially perspective by dalaw 30781. TODO: FIX COMMENT (Contributed by NM, 5-May-2013.)

Theoremcdlemg12d 31541 TODO: FIX COMMENT (Contributed by NM, 5-May-2013.)

Theoremcdlemg12e 31542 TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)

Theoremcdlemg12f 31543 TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)

Theoremcdlemg12g 31544 TODO: FIX COMMENT TODO: Combine with cdlemg12f 31543. (Contributed by NM, 6-May-2013.)

Theoremcdlemg12 31545 TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)

Theoremcdlemg13a 31546 TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)

Theoremcdlemg13 31547 TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)

Theoremcdlemg14f 31548 TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)

Theoremcdlemg14g 31549 TODO: FIX COMMENT (Contributed by NM, 22-May-2013.)

Theoremcdlemg15a 31550 Eliminate the condition from cdlemg13 31547. TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)

Theoremcdlemg15 31551 Eliminate the condition from cdlemg13 31547. TODO: FIX COMMENT (Contributed by NM, 25-May-2013.)

Theoremcdlemg16 31552 Part of proof of Lemma G of [Crawley] p. 116; 2nd line p. 117, which says that (our) cdlemg10 31536 "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 30781, in order to make this inference. This final step eliminates the condition from cdlemg12 31545. 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.)

Theoremcdlemg16ALTN 31553 This version of cdlemg16 31552 uses cdlemg15a 31550 instead of cdlemg15 31551, in case cdlemg15 31551 ends up not being needed. TODO: FIX COMMENT (Contributed by NM, 6-May-2013.) (New usage is discouraged.)

Theoremcdlemg16z 31554 Eliminate condition from cdlemg16 31552. TODO: would it help to also eliminate here or later? (Contributed by NM, 25-May-2013.)

Theoremcdlemg16zz 31555 Eliminate from cdlemg16z 31554. TODO: Use this only if needed. (Contributed by NM, 26-May-2013.)

Theoremcdlemg17a 31556 TODO: FIX COMMENT (Contributed by NM, 8-May-2013.)

Theoremcdlemg17b 31557* 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 31185. (Contributed by NM, 8-May-2013.)

Theoremcdlemg17dN 31558* TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.)

Theoremcdlemg17dALTN 31559 Same as cdlemg17dN 31558 with fewer antecedents but longer proof TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.)

Theoremcdlemg17e 31560* TODO: fix comment. (Contributed by NM, 8-May-2013.)

Theoremcdlemg17f 31561* TODO: fix comment. (Contributed by NM, 8-May-2013.)

Theoremcdlemg17g 31562* TODO: fix comment. (Contributed by NM, 9-May-2013.)

Theoremcdlemg17h 31563* TODO: fix comment. (Contributed by NM, 10-May-2013.)

Theoremcdlemg17i 31564* TODO: fix comment. (Contributed by NM, 10-May-2013.)

Theoremcdlemg17ir 31565* TODO: fix comment. (Contributed by NM, 13-May-2013.)

Theoremcdlemg17j 31566* TODO: fix comment. (Contributed by NM, 11-May-2013.)

Theoremcdlemg17pq 31567* Utility theorem for swapping and . TODO: fix comment. (Contributed by NM, 11-May-2013.)

Theoremcdlemg17bq 31568* cdlemg17b 31557 with and swapped. Antecedent is redundant for easier use. TODO: should we have redundant antecedent for cdlemg17b 31557 also? (Contributed by NM, 13-May-2013.)

Theoremcdlemg17iqN 31569* cdlemg17i 31564 with and swapped. (Contributed by NM, 13-May-2013.) (New usage is discouraged.)

Theoremcdlemg17irq 31570* cdlemg17ir 31565 with and swapped. (Contributed by NM, 13-May-2013.)

Theoremcdlemg17jq 31571* cdlemg17j 31566 with and swapped. (Contributed by NM, 13-May-2013.)

Theoremcdlemg17 31572* 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.)

Theoremcdlemg18a 31573 Show two lines are different. TODO: fix comment. (Contributed by NM, 14-May-2013.)

Theoremcdlemg18b 31574 Lemma for cdlemg18c 31575. TODO: fix comment. (Contributed by NM, 15-May-2013.)

Theoremcdlemg18c 31575 Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.)

Theoremcdlemg18d 31576* Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.)

Theoremcdlemg18 31577* Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.)

Theoremcdlemg19a 31578* Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.)

Theoremcdlemg19 31579* Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.)

Theoremcdlemg20 31580* Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 23-May-2013.)

Theoremcdlemg21 31581* Version of cdlemg19 with instead of as a condition. (Contributed by NM, 23-May-2013.)

Theoremcdlemg22 31582* cdlemg21 31581 with condition removed. (Contributed by NM, 23-May-2013.)

Theoremcdlemg24 31583* Combine cdlemg16z 31554 and cdlemg22 31582. TODO: Fix comment. (Contributed by NM, 24-May-2013.)

Theoremcdlemg37 31584* Use cdlemg8 31526 to eliminate the condition of cdlemg24 31583. (Contributed by NM, 31-May-2013.)

Theoremcdlemg25zz 31585 cdlemg16zz 31555 restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-2013.)

Theoremcdlemg26zz 31586 cdlemg16zz 31555 restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-2013.)

Theoremcdlemg27a 31587 For use with case when or is zero, letting us establish via 4atex 30971. TODO: Fix comment. (Contributed by NM, 28-May-2013.)

Theoremcdlemg28a 31588 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.)

Theoremcdlemg31b0N 31589 TODO: Fix comment. (Contributed by NM, 30-May-2013.) (New usage is discouraged.)

Theoremcdlemg31b0a 31590 TODO: Fix comment. (Contributed by NM, 30-May-2013.)