Home Metamath Proof ExplorerTheorem 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)
TypeLabelDescription
Statement

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

Theoremcdlemfnid 34202* cdlemf 34201 with additional constraint of non-identity. (Contributed by NM, 20-Jun-2013.)

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

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

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

Theoremcdlemftr0 34206* Special case of cdlemf 34201 showing existence of a non-identity translation. (Contributed by NM, 1-Aug-2013.)

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

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

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

Theoremcdlemg1idlemN 34210* Lemma for cdlemg1idN 34215. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)

Theoremcdlemg1fvawlemN 34211* Lemma for ltrniotafvawN 34216. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)

Theoremcdlemg1ltrnlem 34212* Lemma for ltrniotacl 34217. (Contributed by NM, 18-Apr-2013.)

Theoremcdlemg1finvtrlemN 34213* Lemma for ltrniotacnvN 34218. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)

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

Theoremcdlemg1idN 34215* Version of cdleme31id 34032 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.)

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

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

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

Theoremltrniotaval 34219* Value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014.)

Theoremltrniotacnvval 34220* Converse value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014.)

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

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

Theoremcdlemeiota 34223* A translation is uniquely determined by one of its values. (Contributed by NM, 18-Apr-2013.)

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

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

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

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

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

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

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

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

Theoremcdlemg2fvlem 34232* Lemma for cdlemg2fv 34237. (Contributed by NM, 23-Apr-2013.)

Theoremcdlemg2klem 34233* cdleme42keg 34124 with simpler hypotheses. TODO: FIX COMMENT. (Contributed by NM, 22-Apr-2013.)

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

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

Theoremcdlemg2jOLDN 34236 TODO: Replace this with ltrnj 33768. (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.)

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

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

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

Theoremcdlemg2kq 34240 cdlemg2k 34239 with and swapped. TODO: FIX COMMENT. (Contributed by NM, 15-May-2013.)

Theoremcdlemg2l 34241 TODO: FIX COMMENT. (Contributed by NM, 23-Apr-2013.)

Theoremcdlemg2m 34242 TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.)

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

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

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

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

Theoremcdlemg4b1 34247 TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.)

Theoremcdlemg4b2 34248 TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.)

Theoremcdlemg4b12 34249 TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.)

Theoremcdlemg4c 34250 TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.)

Theoremcdlemg4d 34251 TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.)

Theoremcdlemg4e 34252 TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.)

Theoremcdlemg4f 34253 TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.)

Theoremcdlemg4g 34254 TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.)

Theoremcdlemg4 34255 TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.)

Theoremcdlemg6a 34256* TODO: FIX COMMENT. TODO: replace with cdlemg4 34255. (Contributed by NM, 27-Apr-2013.)

Theoremcdlemg6b 34257* TODO: FIX COMMENT. TODO: replace with cdlemg4 34255. (Contributed by NM, 27-Apr-2013.)

Theoremcdlemg6c 34258* TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.)

Theoremcdlemg6d 34259* TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.)

Theoremcdlemg6e 34260 TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.)

Theoremcdlemg6 34261 TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.)

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

Theoremcdlemg7aN 34263 TODO: FIX COMMENT. (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)

Theoremcdlemg7N 34264 TODO: FIX COMMENT. (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.)

Theoremcdlemg8a 34265 TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)

Theoremcdlemg8b 34266 TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)

Theoremcdlemg8c 34267 TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)

Theoremcdlemg8d 34268 TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)

Theoremcdlemg8 34269 TODO: FIX COMMENT. (Contributed by NM, 29-Apr-2013.)

Theoremcdlemg9a 34270 TODO: FIX COMMENT. (Contributed by NM, 1-May-2013.)

Theoremcdlemg9b 34271 The triples and are centrally perspective. TODO: FIX COMMENT. (Contributed by NM, 1-May-2013.)

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

Theoremcdlemg10b 34273 TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in ltrn* area? (Contributed by NM, 4-May-2013.)

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

Theoremcdlemg11a 34275 TODO: FIX COMMENT. (Contributed by NM, 4-May-2013.)

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

Theoremcdlemg10c 34277 TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in trl* area? (Contributed by NM, 4-May-2013.)

Theoremcdlemg10a 34278 TODO: FIX COMMENT. (Contributed by NM, 3-May-2013.)

Theoremcdlemg10 34279 TODO: FIX COMMENT. (Contributed by NM, 4-May-2013.)

Theoremcdlemg11b 34280 TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.)

Theoremcdlemg12a 34281 TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.)

Theoremcdlemg12b 34282 The triples and are centrally perspective. TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.)

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

Theoremcdlemg12d 34284 TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.)

Theoremcdlemg12e 34285 TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)

Theoremcdlemg12f 34286 TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)

Theoremcdlemg12g 34287 TODO: FIX COMMENT. TODO: Combine with cdlemg12f 34286. (Contributed by NM, 6-May-2013.)

Theoremcdlemg12 34288 TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)

Theoremcdlemg13a 34289 TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)

Theoremcdlemg13 34290 TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)

Theoremcdlemg14f 34291 TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)

Theoremcdlemg14g 34292 TODO: FIX COMMENT. (Contributed by NM, 22-May-2013.)

Theoremcdlemg15a 34293 Eliminate the condition from cdlemg13 34290. TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.)

Theoremcdlemg15 34294 Eliminate the condition from cdlemg13 34290. TODO: FIX COMMENT. (Contributed by NM, 25-May-2013.)

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