Home Metamath Proof ExplorerTheorem List (p. 340 of 394) < 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-26406) Hilbert Space Explorer (26407-27929) Users' Mathboxes (27930-39313)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theoremcdlemg24 33967* Combine cdlemg16z 33938 and cdlemg22 33966. TODO: Fix comment. (Contributed by NM, 24-May-2013.)

Theoremcdlemg37 33968* Use cdlemg8 33910 to eliminate the condition of cdlemg24 33967. (Contributed by NM, 31-May-2013.)

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

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

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

Theoremcdlemg28a 33972 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 33973 TODO: Fix comment. (Contributed by NM, 30-May-2013.) (New usage is discouraged.)

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

Theoremcdlemg27b 33975 TODO: Fix comment. (Contributed by NM, 28-May-2013.)

Theoremcdlemg31a 33976 TODO: fix comment. (Contributed by NM, 29-May-2013.)

Theoremcdlemg31b 33977 TODO: fix comment. (Contributed by NM, 29-May-2013.)

Theoremcdlemg31c 33978 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.)

Theoremcdlemg31d 33979 Eliminate from cdlemg31c 33978. 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 33984 vs. cdlemg28 33983. (Contributed by NM, 29-May-2013.)

Theoremcdlemg33b0 33980* TODO: Fix comment. (Contributed by NM, 30-May-2013.)

Theoremcdlemg33c0 33981* TODO: Fix comment. (Contributed by NM, 30-May-2013.)

Theoremcdlemg28b 33982* 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 33983.) (Contributed by NM, 29-May-2013.)

Theoremcdlemg28 33983* 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 33984 (and maybe leading up to this too)? (Contributed by NM, 29-May-2013.)

Theoremcdlemg29 33984* Eliminate and from cdlemg28 33983. TODO: would it be better to do this later? (Contributed by NM, 29-May-2013.)

Theoremcdlemg33a 33985* TODO: Fix comment. (Contributed by NM, 29-May-2013.)

Theoremcdlemg33b 33986* TODO: Fix comment. (Contributed by NM, 30-May-2013.)