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

 Color key: Metamath Proof Explorer (1-21328) Hilbert Space Explorer (21329-22851) Users' Mathboxes (22852-30955)

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

Theoremcdlemeg49le 29501* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 9-Apr-2013.)

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

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

Theoremcdlemeg46rvOLDN 29504* 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 29505* 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 29506* Show that is an atom not under when is an atom not under . (Contributed by NM, 1-Apr-2013.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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