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