Home | Metamath
Proof ExplorerTheorem List
(p. 310 of 323)
| < 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-21811) |
Hilbert Space Explorer
(21812-23334) |
Users' Mathboxes
(23335-32225) |

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

Statement | ||

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem | cdlemg24 30948* | Combine cdlemg16z 30919 and cdlemg22 30947. TODO: Fix comment. (Contributed by NM, 24-May-2013.) |

Theorem | cdlemg37 30949* | Use cdlemg8 30891 to eliminate the condition of cdlemg24 30948. (Contributed by NM, 31-May-2013.) |

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

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

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

Theorem | cdlemg28a 30953 | 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 30954 | TODO: Fix comment. (Contributed by NM, 30-May-2013.) (New usage is discouraged.) |

Theorem | cdlemg31b0a 30955 | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |

Theorem | cdlemg27b 30956 | TODO: Fix comment. (Contributed by NM, 28-May-2013.) |

Theorem | cdlemg31a 30957 | TODO: fix comment. (Contributed by NM, 29-May-2013.) |

Theorem | cdlemg31b 30958 | TODO: fix comment. (Contributed by NM, 29-May-2013.) |

Theorem | cdlemg31c 30959 | Show that when is an atom, it is not under . TODO: Is there a shorter direct proof? Todo: should we eliminate here? (Contributed by NM, 29-May-2013.) |

Theorem | cdlemg31d 30960 | Eliminate from cdlemg31c 30959. TODO: Prove directly. Todo: do we need to eliminate ? It might be better to do this all at once at the end. See also cdlemg29 30965 vs. cdlemg28 30964. (Contributed by NM, 29-May-2013.) |

Theorem | cdlemg33b0 30961* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |

Theorem | cdlemg33c0 30962* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |

Theorem | cdlemg28b 30963* | Part of proof of Lemma G of [Crawley] p. 116. Second equality of the equation of line 14 on p. 117. Note that is redundant here (but simplifies cdlemg28 30964.) (Contributed by NM, 29-May-2013.) |

Theorem | cdlemg28 30964* | Part of proof of Lemma G of [Crawley] p. 116. Chain the equalities of line 14 on p. 117. TODO: rearrange hypotheses in the order of cdlemg29 30965 (and maybe leading up to this too)? (Contributed by NM, 29-May-2013.) |

Theorem | cdlemg29 30965* | Eliminate and from cdlemg28 30964. TODO: would it be better to do this later? (Contributed by NM, 29-May-2013.) |

Theorem | cdlemg33a 30966* | TODO: Fix comment. (Contributed by NM, 29-May-2013.) |

Theorem | cdlemg33b 30967* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |

Theorem | cdlemg33c 30968* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |

Theorem | cdlemg33d 30969* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |

Theorem | cdlemg33e 30970* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |

Theorem | cdlemg33 30971* | Combine cdlemg33b 30967, cdlemg33c 30968, cdlemg33d 30969, cdlemg33e 30970. TODO: Fix comment. (Contributed by NM, 30-May-2013.) |

Theorem | cdlemg34 30972* | Use cdlemg33 to eliminate from cdlemg29 30965. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |

Theorem | cdlemg35 30973* | TODO: Fix comment. TODO: should we have a more general version of hlsupr 29646 to avoid the conditions? (Contributed by NM, 31-May-2013.) |

Theorem | cdlemg36 30974* | Use cdlemg35 to eliminate from cdlemg34 30972. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |

Theorem | cdlemg38 30975 | Use cdlemg37 30949 to eliminate from cdlemg36 30974. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |

Theorem | cdlemg39 30976 | Eliminate conditions from cdlemg38 30975. TODO: Would this better be done at cdlemg35 30973? TODO: Fix comment. (Contributed by NM, 31-May-2013.) |

Theorem | cdlemg40 30977 | Eliminate conditions from cdlemg39 30976. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |

Theorem | cdlemg41 30978 | Convert cdlemg40 30977 to function composition. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |

Theorem | ltrnco 30979 | The composition of two translations is a translation. Part of proof of Lemma G of [Crawley] p. 116, line 15 on p. 117. (Contributed by NM, 31-May-2013.) |

Theorem | trlcocnv 30980 | Swap the arguments of the trace of a composition with converse. (Contributed by NM, 1-Jul-2013.) |

Theorem | trlcoabs 30981 | Absorption into a composition by joining with trace. (Contributed by NM, 22-Jul-2013.) |

Theorem | trlcoabs2N 30982 | Absorption of the trace of a composition. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |

Theorem | trlcoat 30983 | The trace of a composition of two translations is an atom if their traces are different. (Contributed by NM, 15-Jun-2013.) |

Theorem | trlcocnvat 30984 | Commonly used special case of trlcoat 30983. (Contributed by NM, 1-Jul-2013.) |