P. 361 of Theorem List - Metamath Proof Explorer

Home	Metamath Proof Explorer Theorem List (p. 361 of 377)	< 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-25811)

Hilbert Space Explorer
(25812-27336)

Users' Mathboxes
(27337-37662)

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

Theorem	cdleme48d 36001*	TODO: fix comment. (Contributed by NM, 8-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$

Theorem	cdleme48gfv1 36002*	TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme48gfv 36003*	TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme48fgv 36004*	TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemeg49lebilem 36005*	Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme50lebi 36006*	Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme50eq 36007*	Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme50f 36008*	Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment TODO: can we use just since range is computed in cdleme50rn 36011? (Contributed by NM, 9-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme50f1 36009*	Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme50rnlem 36010*	Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment TODO: can we get rid of stuff if we show earlier? (Contributed by NM, 9-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme50rn 36011*	Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme50f1o 36012*	Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme50laut 36013*	Part of proof of Lemma D in [Crawley] p. 113. is a lattice automorphism. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme50ldil 36014*	Part of proof of Lemma D in [Crawley] p. 113. is a lattice dilation. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme50trn1 36015*	Part of proof that is a tranlation. $.\/$ case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$

Theorem	cdleme50trn2a 36016*	Part of proof that is a translation. $.\/$ case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$

Theorem	cdleme50trn2 36017*	Part of proof that is a translation. Remove hypotheses no longer needed from cdleme50trn2a 36016. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $./\$

Theorem	cdleme50trn12 36018*	Part of proof that is a translation. Combine $.\/$ and $.\/$ cases. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$

Theorem	cdleme50trn3 36019*	Part of proof that is a translation. case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$

Theorem	cdleme50trn123 36020*	Part of proof that is a translation. Combine all cases. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$

Theorem	cdleme51finvfvN 36021*	Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-Apr-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme51finvN 36022*	Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-Apr-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme50ltrn 36023*	Part of proof of Lemma E in [Crawley] p. 113. is a lattice translation. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme51finvtrN 36024*	Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-Apr-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $.\/$ $./\$ $.\/$ $/\$ $.\/$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme50ex 36025*	Part of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 11-Apr-2013.)
$/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdleme 36026*	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 36027*	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 36028*	Part of Lemma F in [Crawley] p. 116. (Contributed by NM, 12-Apr-2013.)
$.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem	cdlemg2k 36067	cdleme42keg 35952 with simpler hypotheses. TODO: FIX COMMENT Todo: derive from cdlemg3a 36063, cdlemg2fv2 36066, cdlemg2jOLDN 36064, ltrnel 35603? (Contributed by NM, 22-Apr-2013.)
$.\/$ $./\$ $.\/$ $./\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$

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

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

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

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

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

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