P. 343 of Theorem List - Metamath Proof Explorer

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

Hilbert Space Explorer
(26565-28087)

Users' Mathboxes
(28088-40527)

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

Theorem	cdlemg10a 34201	TODO: FIX COMMENT. (Contributed by NM, 3-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $.\/$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem	cdlemg16z 34220	Eliminate $.\/$ $.\/$ condition from cdlemg16 34218. TODO: would it help to also eliminate here or later? (Contributed by NM, 25-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg16zz 34221	Eliminate from cdlemg16z 34220. TODO: Use this only if needed. (Contributed by NM, 26-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg17a 34222	TODO: FIX COMMENT. (Contributed by NM, 8-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17b 34223*	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 33850. (Contributed by NM, 8-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17dN 34224*	TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $./\$

Theorem	cdlemg17dALTN 34225	Same as cdlemg17dN 34224 with fewer antecedents but longer proof TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $./\$

Theorem	cdlemg17e 34226*	TODO: fix comment. (Contributed by NM, 8-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$

Theorem	cdlemg17f 34227*	TODO: fix comment. (Contributed by NM, 8-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$

Theorem	cdlemg17g 34228*	TODO: fix comment. (Contributed by NM, 9-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$

Theorem	cdlemg17h 34229*	TODO: fix comment. (Contributed by NM, 10-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $\/$

Theorem	cdlemg17i 34230*	TODO: fix comment. (Contributed by NM, 10-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17ir 34231*	TODO: fix comment. (Contributed by NM, 13-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17j 34232*	TODO: fix comment. (Contributed by NM, 11-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17pq 34233*	Utility theorem for swapping and . TODO: fix comment. (Contributed by NM, 11-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

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

Theorem	cdlemg17iqN 34235*	cdlemg17i 34230 with and swapped. (Contributed by NM, 13-May-2013.) (New usage is discouraged.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$

Theorem	cdlemg17irq 34236*	cdlemg17ir 34231 with and swapped. (Contributed by NM, 13-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

Theorem	cdlemg17jq 34237*	cdlemg17j 34232 with and swapped. (Contributed by NM, 13-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$

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

Theorem	cdlemg18b 34240	Lemma for cdlemg18c 34241. TODO: fix comment. (Contributed by NM, 15-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$

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

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

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

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

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

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

Theorem	cdlemg21 34247*	Version of cdlemg19 with $.\/$ instead of $.\/$ as a condition. (Contributed by NM, 23-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg22 34248*	cdlemg21 34247 with condition removed. (Contributed by NM, 23-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg24 34249*	Combine cdlemg16z 34220 and cdlemg22 34248. TODO: Fix comment. (Contributed by NM, 24-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg37 34250*	Use cdlemg8 34192 to eliminate the $.\/$ condition of cdlemg24 34249. (Contributed by NM, 31-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg25zz 34251	cdlemg16zz 34221 restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg26zz 34252	cdlemg16zz 34221 restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg27a 34253	For use with case when $.\/$ $./\$ $.\/$ or $.\/$ $./\$ $.\/$ is zero, letting us establish $/\$ $.\/$ via 4atex 33635. TODO: Fix comment. (Contributed by NM, 28-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$

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

Theorem	cdlemg31b0a 34256	TODO: Fix comment. (Contributed by NM, 30-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $\/$

Theorem	cdlemg27b 34257	TODO: Fix comment. (Contributed by NM, 28-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$

Theorem	cdlemg31a 34258	TODO: fix comment. (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemg31b 34259	TODO: fix comment. (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemg31c 34260	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 34261	Eliminate from cdlemg31c 34260. 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 34266 vs. cdlemg28 34265. (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemg33b0 34262*	TODO: Fix comment. (Contributed by NM, 30-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$

Theorem	cdlemg33c0 34263*	TODO: Fix comment. (Contributed by NM, 30-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$

Theorem	cdlemg28b 34264*	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 34265.) (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg28 34265*	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 34266 (and maybe leading up to this too)? (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg29 34266*	Eliminate and from cdlemg28 34265. TODO: would it be better to do this later? (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg33a 34267*	TODO: Fix comment. (Contributed by NM, 29-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemg33b 34268*	TODO: Fix comment. (Contributed by NM, 30-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemg33c 34269*	TODO: Fix comment. (Contributed by NM, 30-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemg33d 34270*	TODO: Fix comment. (Contributed by NM, 30-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemg33e 34271*	TODO: Fix comment. (Contributed by NM, 30-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemg33 34272*	Combine cdlemg33b 34268, cdlemg33c 34269, cdlemg33d 34270, cdlemg33e 34271. TODO: Fix comment. (Contributed by NM, 30-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$

Theorem	cdlemg34 34273*	Use cdlemg33 to eliminate from cdlemg29 34266. TODO: Fix comment. (Contributed by NM, 31-May-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

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

Theorem	cdlemg36 34275*	Use cdlemg35 to eliminate from cdlemg34 34273. TODO: Fix comment. (Contributed by NM, 31-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg38 34276	Use cdlemg37 34250 to eliminate from cdlemg36 34275. TODO: Fix comment. (Contributed by NM, 31-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg39 34277	Eliminate conditions from cdlemg38 34276. TODO: Would this better be done at cdlemg35 34274? TODO: Fix comment. (Contributed by NM, 31-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg40 34278	Eliminate conditions from cdlemg39 34277. TODO: Fix comment. (Contributed by NM, 31-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	cdlemg41 34279	Convert cdlemg40 34278 to function composition. TODO: Fix comment. (Contributed by NM, 31-May-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $./\$

Theorem	ltrnco 34280	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 34281	Swap the arguments of the trace of a composition with converse. (Contributed by NM, 1-Jul-2013.)
$/\$ $/\$ $/\$

Theorem	trlcoabs 34282	Absorption into a composition by joining with trace. (Contributed by NM, 22-Jul-2013.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

Theorem	trlcoabs2N 34283	Absorption of the trace of a composition. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)
$.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$