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