Home | Metamath
Proof Explorer Theorem List (p. 359 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemeg46c 35801* | TODO FIX COMMENT. (Contributed by NM, 1-Apr-2013.) |
Theorem | cdlemeg46rvOLDN 35802* | Value of gs(r) when r is an atom under pq and s is any atom not under pq, using very compact hypotheses. TODO FIX COMMENT. (Contributed by NM, 3-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemeg46rv2OLDN 35803* | Value of gs(r) when r is an atom under pq and s is any atom not under pq, using very compact hypotheses. TODO FIX COMMENT. (Contributed by NM, 3-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemeg46fvaw 35804* | Show that is an atom not under when is an atom not under . (Contributed by NM, 1-Apr-2013.) |
Theorem | cdlemeg46nlpq 35805* | Show that is not under when isn't. (Contributed by NM, 3-Apr-2013.) |
Theorem | cdlemeg46ngfr 35806* | TODO FIX COMMENT g(f(s))=s p. 115 4th line from bottom. (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46nfgr 35807* | TODO FIX COMMENT f(g(s))=s p. 115 antepenultimate line. (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46sfg 35808* | TODO FIX COMMENT f(r) s = f(r) g(s) p. 116 2nd line TODO: eliminate eqcomd? (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46fjgN 35809* | NOT NEEDED? TODO FIX COMMENT. TODO eliminate eqcomd 2628? p. 116 2nd line. (Contributed by NM, 2-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemeg46rjgN 35810* | NOT NEEDED? TODO FIX COMMENT. r g(s) = r v2 p. 115 last line. (Contributed by NM, 2-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemeg46fjv 35811* | TODO FIX COMMENT f(r) f(g(s)) = f(r) v2 p. 116 2nd line. (Contributed by NM, 2-Apr-2013.) |
Theorem | cdlemeg46fsfv 35812* | TODO FIX COMMENT f(r) s = f(r) v2 p. 116 2nd line. (Contributed by NM, 2-Apr-2013.) |
Theorem | cdlemeg46frv 35813* | TODO FIX COMMENT. (f(r) v2) w = v2 p. 116 3rd line. (Contributed by NM, 2-Apr-2013.) |
Theorem | cdlemeg46v1v2 35814* | TODO FIX COMMENT v1 = v2 p. 116 3rd line. (Contributed by NM, 2-Apr-2013.) |
Theorem | cdlemeg46vrg 35815* | TODO FIX COMMENT v1 r g(s) p. 116 3rd line. (Contributed by NM, 3-Apr-2013.) |
Theorem | cdlemeg46rgv 35816* | TODO FIX COMMENT r g(s) v1 p. 116 3rd line. (Contributed by NM, 3-Apr-2013.) |
Theorem | cdlemeg46req 35817* | TODO FIX COMMENT r = (v1 g(s)) p. 116 3rd line. (Contributed by NM, 3-Apr-2013.) |
Theorem | cdlemeg46gfv 35818* | TODO FIX COMMENT p. 115 penultimate line: g(f(r)) = (p v q) ^ (g(s) v v1). (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46gfr 35819* | TODO FIX COMMENT p. 116 penultimate line: g(f(r)) = r. (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46gfre 35820* | TODO FIX COMMENT p. 116 penultimate line: g(f(r)) = r. (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46gf 35821* | TODO FIX COMMENT Eliminate antecedent . (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46fgN 35822* | TODO FIX COMMENT p. 116 penultimate line: f(g(r)) = r. (Contributed by NM, 4-Apr-2013.) (New usage is discouraged.) |
Theorem | cdleme48d 35823* | TODO: fix comment. (Contributed by NM, 8-Apr-2013.) |
Theorem | cdleme48gfv1 35824* | TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme48gfv 35825* | TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme48fgv 35826* | TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdlemeg49lebilem 35827* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50lebi 35828* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50eq 35829* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50f 35830* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. TODO: can we use just since range is computed in cdleme50rn 35833? (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50f1 35831* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50rnlem 35832* | 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 35833* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50f1o 35834* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50laut 35835* | 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 35836* | 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 35837* | Part of proof that is a translation. case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
Theorem | cdleme50trn2a 35838* | Part of proof that is a translation. case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
Theorem | cdleme50trn2 35839* | Part of proof that is a translation. Remove hypotheses no longer needed from cdleme50trn2a 35838. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
Theorem | cdleme50trn12 35840* | Part of proof that is a translation. Combine and cases. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
Theorem | cdleme50trn3 35841* | Part of proof that is a translation. case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
Theorem | cdleme50trn123 35842* | Part of proof that is a translation. Combine all cases. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
Theorem | cdleme51finvfvN 35843* | 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 35844* | 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 35845* | 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 35846* | 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 35847* | Part of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 11-Apr-2013.) |
Theorem | cdleme 35848* | 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 35849* | 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 35850* | Part of Lemma F in [Crawley] p. 116. (Contributed by NM, 12-Apr-2013.) |
Theorem | cdlemf 35851* | 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 35852* | cdlemf 35851 with additional constraint of non-identity. (Contributed by NM, 20-Jun-2013.) |
Theorem | cdlemftr3 35853* | Special case of cdlemf 35851 showing existence of non-identity translation with trace different from any 3 given lattice elements. (Contributed by NM, 24-Jul-2013.) |
Theorem | cdlemftr2 35854* | Special case of cdlemf 35851 showing existence of non-identity translation with trace different from any 2 given lattice elements. (Contributed by NM, 25-Jul-2013.) |
Theorem | cdlemftr1 35855* | 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 35856* | Special case of cdlemf 35851 showing existence of a non-identity translation. (Contributed by NM, 1-Aug-2013.) |
Theorem | trlord 35857* | 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 35858* | Shorter expression for . TODO: fix comment. TODO: shorten using cdleme 35848 or vice-versa? Also, if not shortened with cdleme 35848, then it can be moved up to save repeating hypotheses. (Contributed by NM, 15-Apr-2013.) |
Theorem | cdlemg1b2 35859* | This theorem can be used to shorten hypothesis. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) |
Theorem | cdlemg1idlemN 35860* | Lemma for cdlemg1idN 35865. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemg1fvawlemN 35861* | Lemma for ltrniotafvawN 35866. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemg1ltrnlem 35862* | Lemma for ltrniotacl 35867. (Contributed by NM, 18-Apr-2013.) |
Theorem | cdlemg1finvtrlemN 35863* | Lemma for ltrniotacnvN 35868. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemg1bOLDN 35864* | 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 35865* | Version of cdleme31id 35682 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
Theorem | ltrniotafvawN 35866* | Version of cdleme46fvaw 35789 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
Theorem | ltrniotacl 35867* | Version of cdleme50ltrn 35845 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 17-Apr-2013.) |
Theorem | ltrniotacnvN 35868* | Version of cdleme51finvtrN 35846 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
Theorem | ltrniotaval 35869* | Value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014.) |
Theorem | ltrniotacnvval 35870* | Converse value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014.) |
Theorem | ltrniotaidvalN 35871* | Value of the unique translation specified by identity value. (Contributed by NM, 25-Aug-2014.) (New usage is discouraged.) |
Theorem | ltrniotavalbN 35872* | Value of the unique translation specified by a value. (Contributed by NM, 10-Mar-2014.) (New usage is discouraged.) |
Theorem | cdlemeiota 35873* | A translation is uniquely determined by one of its values. (Contributed by NM, 18-Apr-2013.) |
Theorem | cdlemg1ci2 35874* | Any function of the form of the function constructed for cdleme 35848 is a translation. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) |
Theorem | cdlemg1cN 35875* | Any translation belongs to the set of functions constructed for cdleme 35848. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemg1cex 35876* | Any translation is one of our s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf 35851? (Contributed by NM, 17-Apr-2013.) |
Theorem | cdlemg2cN 35877* | Any translation belongs to the set of functions constructed for cdleme 35848. TODO: Fix comment. (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemg2dN 35878* | This theorem can be used to shorten hypothesis. TODO: Fix comment. (Contributed by NM, 21-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemg2cex 35879* | Any translation is one of our s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf 35851? (Contributed by NM, 22-Apr-2013.) |
Theorem | cdlemg2ce 35880* | Utility theorem to eliminate p,q when converting theorems with explicit f. TODO: fix comment. (Contributed by NM, 22-Apr-2013.) |
Theorem | cdlemg2jlemOLDN 35881* | 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 35886? (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemg2fvlem 35882* | Lemma for cdlemg2fv 35887. (Contributed by NM, 23-Apr-2013.) |
Theorem | cdlemg2klem 35883* | cdleme42keg 35774 with simpler hypotheses. TODO: FIX COMMENT. (Contributed by NM, 22-Apr-2013.) |
Theorem | cdlemg2idN 35884 | Version of cdleme31id 35682 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 21-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemg3a 35885 | Part of proof of Lemma G in [Crawley] p. 116, line 19. Show p q = p u. TODO: reformat cdleme0cp 35501 to match this, then replace with cdleme0cp 35501. (Contributed by NM, 19-Apr-2013.) |
Theorem | cdlemg2jOLDN 35886 | TODO: Replace this with ltrnj 35418. (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemg2fv 35887 | Value of a translation in terms of an associated atom. cdleme48fvg 35788 with simpler hypotheses. TODO: Use ltrnj 35418 to vastly simplify. (Contributed by NM, 23-Apr-2013.) |
Theorem | cdlemg2fv2 35888 | Value of a translation in terms of an associated atom. TODO: FIX COMMENT. TODO: Is this useful elsewhere e.g. around cdlemeg46fjv 35811 that use more complex proofs? TODO: Use ltrnj 35418 to vastly simplify. (Contributed by NM, 23-Apr-2013.) |
Theorem | cdlemg2k 35889 | cdleme42keg 35774 with simpler hypotheses. TODO: FIX COMMENT. TODO: derive from cdlemg3a 35885, cdlemg2fv2 35888, cdlemg2jOLDN 35886, ltrnel 35425? (Contributed by NM, 22-Apr-2013.) |
Theorem | cdlemg2kq 35890 | cdlemg2k 35889 with and swapped. TODO: FIX COMMENT. (Contributed by NM, 15-May-2013.) |
Theorem | cdlemg2l 35891 | TODO: FIX COMMENT. (Contributed by NM, 23-Apr-2013.) |
Theorem | cdlemg2m 35892 | TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.) |
Theorem | cdlemg5 35893* | TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle 35291? TODO: The hypothesis is unused. FIX COMMENT. (Contributed by NM, 26-Apr-2013.) |
Theorem | cdlemb3 35894* | 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 35291? Then replace cdlemb2 35327 with it. This is a more general version of cdlemb2 35327 without condition. (Contributed by NM, 27-Apr-2013.) |
Theorem | cdlemg7fvbwN 35895 | Properties of a translation of an element not under . TODO: Fix comment. Can this be simplified? Perhaps derived from cdleme48bw 35790? Done with a *ltrn* theorem? (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemg4a 35896 | TODO: FIX COMMENT If fg(p) = p, then tr f = tr g. (Contributed by NM, 23-Apr-2013.) |
Theorem | cdlemg4b1 35897 | TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.) |
Theorem | cdlemg4b2 35898 | TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.) |
Theorem | cdlemg4b12 35899 | TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.) |
Theorem | cdlemg4c 35900 | TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |