P. 343 of Theorem List - Metamath Proof Explorer

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

Hilbert Space Explorer
(26653-28175)

Users' Mathboxes
(28176-41046)

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

Theorem	cdlemf 34201*	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 34202*	cdlemf 34201 with additional constraint of non-identity. (Contributed by NM, 20-Jun-2013.)
$/\$ $/\$ $/\$ $/\$

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

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

Theorem	cdlemftr1 34205*	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 34206*	Special case of cdlemf 34201 showing existence of a non-identity translation. (Contributed by NM, 1-Aug-2013.)
$/\$

Theorem	trlord 34207*	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 34208*	Shorter expression for . TODO: fix comment. TODO: shorten using cdleme 34198 or vice-versa? Also, if not shortened with cdleme 34198, then it can be moved up to save repeating hypotheses. (Contributed by NM, 15-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

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

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

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

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

Theorem	cdlemg1bOLDN 34214*	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 34215*	Version of cdleme31id 34032 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem	cdlemg2k 34239	cdleme42keg 34124 with simpler hypotheses. TODO: FIX COMMENT. TODO: derive from cdlemg3a 34235, cdlemg2fv2 34238, cdlemg2jOLDN 34236, ltrnel 33775? (Contributed by NM, 22-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem	cdlemg16 34295	Part of proof of Lemma G of [Crawley] p. 116; 2nd line p. 117, which says that (our) cdlemg10 34279 "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 33522, in order to make this inference. This final step eliminates the condition from cdlemg12 34288. 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.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$