P. 343 of Theorem List - Metamath Proof Explorer

Home	Metamath Proof Explorer Theorem List (p. 343 of 357)	< 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-24318)

Hilbert Space Explorer
(24319-25843)

Users' Mathboxes
(25844-35614)

**Theorem List for Metamath Proof Explorer -** 34201-34300 *Has distinct variable group(s)
Type	Label	Description
Statement

Theorem	cdleme 34201*	Lemma E in [Crawley] p. 113. If p,q are atoms not under hyperplane w, then there is a unique translation f such that f(p) = q. (Contributed by NM, 11-Apr-2013.)
$/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemf1 34202*	Part of Lemma F in [Crawley] p. 116. TODO: should this or part of it become a stand-alone theorem? (Contributed by NM, 12-Apr-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemf2 34203*	Part of Lemma F in [Crawley] p. 116. (Contributed by NM, 12-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$

Theorem	cdlemf 34204*	Lemma F in [Crawley] p. 116. If u is an atom under w, there exists a translation whose trace is u. (Contributed by NM, 12-Apr-2013.)
$/\$ $/\$ $/\$

Theorem	cdlemfnid 34205*	cdlemf 34204 with additional constraint of non-identity. (Contributed by NM, 20-Jun-2013.)
$/\$ $/\$ $/\$ $/\$

Theorem	cdlemftr3 34206*	Special case of cdlemf 34204 showing existence of non-identity translation with trace different from any 3 given lattice elements. (Contributed by NM, 24-Jul-2013.)
$/\$ $/\$ $/\$ $/\$

Theorem	cdlemftr2 34207*	Special case of cdlemf 34204 showing existence of non-identity translation with trace different from any 2 given lattice elements. (Contributed by NM, 25-Jul-2013.)
$/\$ $/\$ $/\$

Theorem	cdlemftr1 34208*	Part of proof of Lemma G of [Crawley] p. 116, sixth line of third paragraph on p. 117: there is "a translation h, different from the identity, such that tr h tr f." (Contributed by NM, 25-Jul-2013.)
$/\$ $/\$

Theorem	cdlemftr0 34209*	Special case of cdlemf 34204 showing existence of a non-identity translation. (Contributed by NM, 1-Aug-2013.)
$/\$

Theorem	trlord 34210*	The ordering of two Hilbert lattice elements (under the fiducial hyperplane ) is determined by the translations whose traces are under them. (Contributed by NM, 3-Mar-2014.)
$/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg1a 34211*	Shorter expression for . TODO: fix comment. TODO: shorten using cdleme 34201 or vice-versa? Also, if not shortened with cdleme 34201, then it can be moved up to save repeating hypotheses. (Contributed by NM, 15-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg1b2 34212*	This theorem can be used to shorten hypothesis. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg1idlemN 34213*	Lemma for cdlemg1idN 34218. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg1fvawlemN 34214*	Lemma for ltrniotafvawN 34219. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg1ltrnlem 34215*	Lemma for ltrniotacl 34220. (Contributed by NM, 18-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg1finvtrlemN 34216*	Lemma for ltrniotacnvN 34221. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg1bOLDN 34217*	This theorem can be used to shorten hypothesis that have the form of the conclusion. TODO: fix comment. (Contributed by NM, 16-Apr-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$

Theorem	cdlemg1idN 34218*	Version of cdleme31id 34035 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	ltrniotafvawN 34219*	Version of cdleme46fvaw 34142 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	ltrniotacl 34220*	Version of cdleme50ltrn 34198 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 17-Apr-2013.)
$/\$ $/\$ $/\$ $/\$ $/\$

Theorem	ltrniotacnvN 34221*	Version of cdleme51finvtrN 34199 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$ $/\$

Theorem	ltrniotaval 34222*	Value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014.)
$/\$ $/\$ $/\$ $/\$ $/\$

Theorem	ltrniotacnvval 34223*	Converse value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014.)
$/\$ $/\$ $/\$ $/\$ $/\$

Theorem	ltrniotaidvalN 34224*	Value of the unique translation specified by identity value. (Contributed by NM, 25-Aug-2014.) (New usage is discouraged.)
$/\$ $/\$ $/\$

Theorem	ltrniotavalbN 34225*	Value of the unique translation specified by a value. (Contributed by NM, 10-Mar-2014.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemeiota 34226*	A translation is uniquely determined by one of its values. (Contributed by NM, 18-Apr-2013.)
$/\$ $/\$ $/\$ $/\$

Theorem	cdlemg1ci2 34227*	Any function of the form of the function constructed for cdleme 34201 is a translation. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg1cN 34228*	Any translation belongs to the set of functions constructed for cdleme 34201. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg1cex 34229*	Any translation is one of our s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf 34204? (Contributed by NM, 17-Apr-2013.)
$/\$ $/\$ $/\$

Theorem	cdlemg2cN 34230*	Any translation belongs to the set of functions constructed for cdleme 34201. TODO: Fix comment. (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

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

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

Theorem	cdlemg2jlemOLDN 34234*	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 34239? (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg2fvlem 34235*	Lemma for cdlemg2fv 34240. (Contributed by NM, 23-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg2klem 34236*	cdleme42keg 34127 with simpler hypotheses. TODO: FIX COMMENT (Contributed by NM, 22-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg2idN 34237	Version of cdleme31id 34035 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 21-Apr-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

Theorem	cdlemg2jOLDN 34239	TODO: Replace this with ltrnj 33773. (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg2fv 34240	Value of a translation in terms of an associated atom. cdleme48fvg 34141 with simpler hypotheses. TODO: Use ltrnj 33773 to vastly simplify. (Contributed by NM, 23-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

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

Theorem	cdlemg2k 34242	cdleme42keg 34127 with simpler hypotheses. TODO: FIX COMMENT Todo: derive from cdlemg3a 34238, cdlemg2fv2 34241, cdlemg2jOLDN 34239, ltrnel 33780? (Contributed by NM, 22-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg2kq 34243	cdlemg2k 34242 with and swapped. TODO: FIX COMMENT (Contributed by NM, 15-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg2l 34244	TODO: FIX COMMENT (Contributed by NM, 23-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg2m 34245	TODO: FIX COMMENT T (Contributed by NM, 25-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$

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

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

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

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

Theorem	cdlemg4b1 34250	TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg4b2 34251	TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg4b12 34252	TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg4c 34253	TODO: FIX COMMENT (Contributed by NM, 24-Apr-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg4d 34254	TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$

Theorem	cdlemg4e 34255	TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Theorem	cdlemg4f 34256	TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Theorem	cdlemg4g 34257	TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemg4 34258	TODO: FIX COMMENT (Contributed by NM, 25-Apr-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$

Theorem	cdlemg6a 34259*	TODO: FIX COMMENT TODO: replace with cdlemg4 34258. (Contributed by NM, 27-Apr-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$

Theorem	cdlemg6b 34260*	TODO: FIX COMMENT TODO: replace with cdlemg4 34258. (Contributed by NM, 27-Apr-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$

Theorem	cdlemg6c 34261*	TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemg6d 34262*	TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemg6e 34263	TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$

Theorem	cdlemg6 34264	TODO: FIX COMMENT (Contributed by NM, 27-Apr-2013.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

Theorem	cdlemg7aN 34266	TODO: FIX COMMENT (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg7N 34267	TODO: FIX COMMENT (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg8a 34268	TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg8b 34269	TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$

Theorem	cdlemg8c 34270	TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$

Theorem	cdlemg8d 34271	TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg8 34272	TODO: FIX COMMENT (Contributed by NM, 29-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg9a 34273	TODO: FIX COMMENT (Contributed by NM, 1-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdlemg9b 34274	The triples and are centrally perspective. TODO: FIX COMMENT (Contributed by NM, 1-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$

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

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

Theorem	cdlemg11a 34278	TODO: FIX COMMENT (Contributed by NM, 4-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg11aq 34279	TODO: FIX COMMENT TODO: can proof using this be restructured to use cdlemg11a 34278? (Contributed by NM, 4-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg10c 34280	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 34281	TODO: FIX COMMENT (Contributed by NM, 3-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdlemg10 34282	TODO: FIX COMMENT (Contributed by NM, 4-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemg11b 34283	TODO: FIX COMMENT (Contributed by NM, 5-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$

Theorem	cdlemg12a 34284	TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdlemg12b 34285	The triples and are centrally perspective. TODO: FIX COMMENT (Contributed by NM, 5-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$

Theorem	cdlemg12c 34286	The triples and are axially perspective by dalaw 33527. TODO: FIX COMMENT (Contributed by NM, 5-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemg12d 34287	TODO: FIX COMMENT (Contributed by NM, 5-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$

Theorem	cdlemg12e 34288	TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $./\$ $.\/$

Theorem	cdlemg12f 34289	TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Theorem	cdlemg12g 34290	TODO: FIX COMMENT TODO: Combine with cdlemg12f 34289. (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$ $./\$

Theorem	cdlemg12 34291	TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg13a 34292	TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$

Theorem	cdlemg13 34293	TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg14f 34294	TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg14g 34295	TODO: FIX COMMENT (Contributed by NM, 22-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg15a 34296	Eliminate the condition from cdlemg13 34293. TODO: FIX COMMENT (Contributed by NM, 6-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg15 34297	Eliminate the $.\/$ $.\/$ condition from cdlemg13 34293. TODO: FIX COMMENT (Contributed by NM, 25-May-2013.)
$.\/$ $./\$