Home | Metamath
Proof Explorer Theorem List (p. 295 of 309) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21328) |
Hilbert Space Explorer
(21329-22851) |
Users' Mathboxes
(22852-30843) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemeg46fjv 29401* | TODO FIX COMMENT f(r) f(g(s)) = f(r) v_{2} p. 116 2nd line. (Contributed by NM, 2-Apr-2013.) |
Theorem | cdlemeg46fsfv 29402* | TODO FIX COMMENT f(r) s = f(r) v_{2} p. 116 2nd line. (Contributed by NM, 2-Apr-2013.) |
Theorem | cdlemeg46frv 29403* | TODO FIX COMMENT (f(r) v_{2}) w = v_{2} p. 116 3rd line. (Contributed by NM, 2-Apr-2013.) |
Theorem | cdlemeg46v1v2 29404* | TODO FIX COMMENT v_{1} = v_{2} p. 116 3rd line. (Contributed by NM, 2-Apr-2013.) |
Theorem | cdlemeg46vrg 29405* | TODO FIX COMMENT v_{1} r g(s) p. 116 3rd line. (Contributed by NM, 3-Apr-2013.) |
Theorem | cdlemeg46rgv 29406* | TODO FIX COMMENT r g(s) v_{1} p. 116 3rd line. (Contributed by NM, 3-Apr-2013.) |
Theorem | cdlemeg46req 29407* | TODO FIX COMMENT r = (v_{1} g(s)) p. 116 3rd line. (Contributed by NM, 3-Apr-2013.) |
Theorem | cdlemeg46gfv 29408* | TODO FIX COMMENT p. 115 penultimate line: g(f(r)) = (p v q) ^ (g(s) v v_{1}) (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46gfr 29409* | TODO FIX COMMENT p. 116 penultimate line: g(f(r)) = r. (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46gfre 29410* | TODO FIX COMMENT p. 116 penultimate line: g(f(r)) = r. (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46gf 29411* | TODO FIX COMMENT Eliminate antecedent . (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46fgN 29412* | TODO FIX COMMENT p. 116 penultimate line: f(g(r)) = r. (Contributed by NM, 4-Apr-2013.) (New usage is discouraged.) |
Theorem | cdleme48d 29413* | TODO: fix comment. (Contributed by NM, 8-Apr-2013.) |
Theorem | cdleme48gfv1 29414* | TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme48gfv 29415* | TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme48fgv 29416* | TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdlemeg49lebilem 29417* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50lebi 29418* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50eq 29419* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50f 29420* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment TODO: can we use just since range is computed in cdleme50rn 29423? (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50f1 29421* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50rnlem 29422* | 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 29423* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50f1o 29424* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme50laut 29425* | 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 29426* | 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 29427* | Part of proof that is a tranlation. case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
Theorem | cdleme50trn2a 29428* | Part of proof that is a translation. case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
Theorem | cdleme50trn2 29429* | Part of proof that is a translation. Remove hypotheses no longer needed from cdleme50trn2a 29428. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
Theorem | cdleme50trn12 29430* | Part of proof that is a translation. Combine and cases. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
Theorem | cdleme50trn3 29431* | Part of proof that is a translation. case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
Theorem | cdleme50trn123 29432* | Part of proof that is a translation. Combine all cases. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
Theorem | cdleme51finvfvN 29433* | 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 29434* | 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 29435* | 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 29436* | 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 29437* | Part of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 11-Apr-2013.) |
Theorem | cdleme 29438* | 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 29439* | 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 29440* | Part of Lemma F in [Crawley] p. 116. (Contributed by NM, 12-Apr-2013.) |
Theorem | cdlemf 29441* | 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 29442* | cdlemf 29441 with additional constraint of non-identity. (Contributed by NM, 20-Jun-2013.) |
Theorem | cdlemftr3 29443* | Special case of cdlemf 29441 showing existence of non-identity translation with trace different from any 3 given lattice elements. (Contributed by NM, 24-Jul-2013.) |
Theorem | cdlemftr2 29444* | Special case of cdlemf 29441 showing existence of non-identity translation with trace different from any 2 given lattice elements. (Contributed by NM, 25-Jul-2013.) |
Theorem | cdlemftr1 29445* | 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 29446* | Special case of cdlemf 29441 showing existence of a non-identity translation. (Contributed by NM, 1-Aug-2013.) |
Theorem | trlord 29447* | 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 29448* | Shorter expression for . TODO: fix comment. TODO: shorten using cdleme 29438 or vice-versa? Also, if not shortened with cdleme 29438, then it can be moved up to save repeating hypotheses. (Contributed by NM, 15-Apr-2013.) |
Theorem | cdlemg1b2 29449* | This theorem can be used to shorten hypothesis. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) |
Theorem | cdlemg1idlemN 29450* | Lemma for cdlemg1idN 29455. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |