Home Metamath Proof ExplorerTheorem List (p. 339 of 394) < 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-26406) Hilbert Space Explorer (26407-27929) Users' Mathboxes (27930-39313)

Theorem List for Metamath Proof Explorer - 33801-33900   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcdlemeg46rjgN 33801* NOT NEEDED? TODO FIX COMMENT r g(s) = r v2 p. 115 last line. (Contributed by NM, 2-Apr-2013.) (New usage is discouraged.)

Theoremcdlemeg46fjv 33802* TODO FIX COMMENT f(r) f(g(s)) = f(r) v2 p. 116 2nd line. (Contributed by NM, 2-Apr-2013.)

Theoremcdlemeg46fsfv 33803* TODO FIX COMMENT f(r) s = f(r) v2 p. 116 2nd line. (Contributed by NM, 2-Apr-2013.)

Theoremcdlemeg46frv 33804* TODO FIX COMMENT (f(r) v2) w = v2 p. 116 3rd line. (Contributed by NM, 2-Apr-2013.)

Theoremcdlemeg46v1v2 33805* TODO FIX COMMENT v1 = v2 p. 116 3rd line. (Contributed by NM, 2-Apr-2013.)

Theoremcdlemeg46vrg 33806* TODO FIX COMMENT v1 r g(s) p. 116 3rd line. (Contributed by NM, 3-Apr-2013.)

Theoremcdlemeg46rgv 33807* TODO FIX COMMENT r g(s) v1 p. 116 3rd line. (Contributed by NM, 3-Apr-2013.)

Theoremcdlemeg46req 33808* TODO FIX COMMENT r = (v1 g(s)) p. 116 3rd line. (Contributed by NM, 3-Apr-2013.)

Theoremcdlemeg46gfv 33809* TODO FIX COMMENT p. 115 penultimate line: g(f(r)) = (p v q) ^ (g(s) v v1) (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46gfr 33810* TODO FIX COMMENT p. 116 penultimate line: g(f(r)) = r. (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46gfre 33811* TODO FIX COMMENT p. 116 penultimate line: g(f(r)) = r. (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46gf 33812* TODO FIX COMMENT Eliminate antecedent . (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46fgN 33813* TODO FIX COMMENT p. 116 penultimate line: f(g(r)) = r. (Contributed by NM, 4-Apr-2013.) (New usage is discouraged.)

Theoremcdleme48d 33814* TODO: fix comment. (Contributed by NM, 8-Apr-2013.)

Theoremcdleme48gfv1 33815* TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme48gfv 33816* TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme48fgv 33817* TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdlemeg49lebilem 33818* Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme50lebi 33819* Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme50eq 33820* Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme50f 33821* Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment TODO: can we use just since range is computed in cdleme50rn 33824? (Contributed by NM, 9-Apr-2013.)

Theoremcdleme50f1 33822* Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme50rnlem 33823* 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.)

Theoremcdleme50rn 33824* Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme50f1o 33825* Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme50laut 33826* Part of proof of Lemma D in [Crawley] p. 113. is a lattice automorphism. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme50ldil 33827* Part of proof of Lemma D in [Crawley] p. 113. is a lattice dilation. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

Theoremcdleme50trn1 33828* Part of proof that is a tranlation. case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)

Theoremcdleme50trn2a 33829* Part of proof that is a translation. case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)

Theoremcdleme50trn2 33830* Part of proof that is a translation. Remove hypotheses no longer needed from cdleme50trn2a 33829. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)

Theoremcdleme50trn12 33831* Part of proof that is a translation. Combine and cases. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)

Theoremcdleme50trn3 33832* Part of proof that is a translation. case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)

Theoremcdleme50trn123 33833* Part of proof that is a translation. Combine all cases. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)

Theoremcdleme51finvfvN 33834* Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-Apr-2013.) (New usage is discouraged.)

Theoremcdleme51finvN 33835* Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-Apr-2013.) (New usage is discouraged.)

Theoremcdleme50ltrn 33836* Part of proof of Lemma E in [Crawley] p. 113. is a lattice translation. TODO: fix comment. (Contributed by NM, 10-Apr-2013.)

Theoremcdleme51finvtrN 33837* Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-Apr-2013.) (New usage is discouraged.)

Theoremcdleme50ex 33838* Part of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 11-Apr-2013.)

Theoremcdleme 33839* 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.)

Theoremcdlemf1 33840* 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.)

Theoremcdlemf2 33841* Part of Lemma F in [Crawley] p. 116. (Contributed by NM, 12-Apr-2013.)

Theoremcdlemf 33842* 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 33843* cdlemf 33842 with additional constraint of non-identity. (Contributed by NM, 20-Jun-2013.)

Theoremcdlemftr3 33844* Special case of cdlemf 33842 showing existence of non-identity translation with trace different from any 3 given lattice elements. (Contributed by NM, 24-Jul-2013.)

Theoremcdlemftr2 33845* Special case of cdlemf 33842 showing existence of non-identity translation with trace different from any 2 given lattice elements. (Contributed by NM, 25-Jul-2013.)

Theoremcdlemftr1 33846* 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 33847* Special case of cdlemf 33842 showing existence of a non-identity translation. (Contributed by NM, 1-Aug-2013.)

Theoremtrlord 33848* 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 33849* Shorter expression for . TODO: fix comment. TODO: shorten using cdleme 33839 or vice-versa? Also, if not shortened with cdleme 33839, then it can be moved up to save repeating hypotheses. (Contributed by NM, 15-Apr-2013.)

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