Home Metamath Proof ExplorerTheorem List (p. 308 of 322) < Previous  Next > Browser slow? Try the Unicode version.

 Color key: Metamath Proof Explorer (1-21498) Hilbert Space Explorer (21499-23021) Users' Mathboxes (23022-32154)

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

Theoremcdlemeg46bOLDN 30701* TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.) (New usage is discouraged.)

Theoremcdlemeg46c 30702* TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.)

Theoremcdlemeg46rvOLDN 30703* 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.)

Theoremcdlemeg46rv2OLDN 30704* 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.)

Theoremcdlemeg46fvaw 30705* Show that is an atom not under when is an atom not under . (Contributed by NM, 1-Apr-2013.)

Theoremcdlemeg46nlpq 30706* Show that is not under when isn't. (Contributed by NM, 3-Apr-2013.)

Theoremcdlemeg46ngfr 30707* TODO FIX COMMENT g(f(s))=s p. 115 4th line from bottom. (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46nfgr 30708* TODO FIX COMMENT f(g(s))=s p. 115 antepenultimate line. (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46sfg 30709* TODO FIX COMMENT f(r) s = f(r) g(s) p. 116 2nd line TODO: eliminate eqcomd? (Contributed by NM, 4-Apr-2013.)

Theoremcdlemeg46fjgN 30710* NOT NEEDED? TODO FIX COMMENT TODO eliminate eqcomd 2288? p. 116 2nd line. (Contributed by NM, 2-Apr-2013.) (New usage is discouraged.)

Theoremcdlemeg46rjgN 30711* 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 30712* TODO FIX COMMENT f(r) f(g(s)) = f(r) v2 p. 116 2nd line. (Contributed by NM, 2-Apr-2013.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theoremcdleme50rnlem 30733* 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 30734* Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.)

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

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

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