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

 Color key: Metamath Proof Explorer (1-22374) Hilbert Space Explorer (22375-23897) Users' Mathboxes (23898-32447)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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