Home | Metamath
Proof Explorer Theorem List (p. 314 of 328) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21514) |
Hilbert Space Explorer
(21515-23037) |
Users' Mathboxes
(23038-32776) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdleme43bN 31301 | Lemma for Lemma E in [Crawley] p. 113. g(s) is an atom not under w. (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
Theorem | cdleme43cN 31302 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT p. 115 last line: r v g(s) = r v v_{2} (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
Theorem | cdleme43dN 31303 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT p. 116 2nd line: f(r) v s = f(r) v f(g(s)) (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
Theorem | cdleme46f2g2 31304 | Conversion for to reuse theorems. TODO FIX COMMENT TODO What other conversion theorems would be reused? e.g. cdlemeg46nlpq 31328? Find other hlatjcom 30179 uses giving . (Contributed by NM, 1-Apr-2013.) |
Theorem | cdleme46f2g1 31305 | Conversion for to reuse theorems. TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.) |
Theorem | cdleme17d2 31306* | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. , represent f(s), f_{s}(p) respectively. We show, in their notation, f_{s}(p)=q. TODO FIX COMMENT (Contributed by NM, 5-Apr-2013.) |
Theorem | cdleme17d3 31307* | TODO FIX COMMENT (Contributed by NM, 5-Apr-2013.) |
Theorem | cdleme17d4 31308* | TODO FIX COMMENT (Contributed by NM, 11-Apr-2013.) |
Theorem | cdleme17d 31309* | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. We show, in their notation, f_{s}(p)=q. TODO FIX COMMENT (Contributed by NM, 11-Apr-2013.) |
Theorem | cdleme48fv 31310* | Part of proof of Lemma D in [Crawley] p. 113. TODO: Can this replace uses of cdleme32a 31252? TODO: Can this be used to help prove the or case where is an atom? (Contributed by NM, 8-Apr-2013.) |
Theorem | cdleme48fvg 31311* | Remove condition in cdleme48fv 31310. TODO: Can this replace uses of cdleme32a 31252? TODO: Can this be used to help prove the or case where is an atom? TODO: Can this be proved more directly by eliminating in earlier theorems? Should this replace uses of cdleme48fv 31310? (Contributed by NM, 23-Apr-2013.) |
Theorem | cdleme46fvaw 31312* | Show that is an atom not under when is an atom not under . (Contributed by NM, 18-Apr-2013.) |
Theorem | cdleme48bw 31313* | TODO: fix comment. TODO: Remove unnecessary from cdleme48bw 31313 cdlemeg46c 31324 cdlemeg46fvaw 31327 cdlemeg46rgv 31339 cdlemeg46gfv 31341? cdleme48d 31346? and possibly others they affect. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme48b 31314* | TODO: fix comment. (Contributed by NM, 8-Apr-2013.) |
Theorem | cdleme46frvlpq 31315* | Show that is not under when isn't. (Contributed by NM, 1-Apr-2013.) |
Theorem | cdleme46fsvlpq 31316* | Show that is under when is. (Contributed by NM, 1-Apr-2013.) |
Theorem | cdlemeg46fvcl 31317* | TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme4gfv 31318* | Part of proof of Lemma D in [Crawley] p. 113. TODO: Can this replace uses of cdleme32a 31252? TODO: Can this be used to help prove the or case where is an atom? TODO: Would an antecedent transformer like cdleme46f2g2 31304 help? (Contributed by NM, 8-Apr-2013.) |
Theorem | cdlemeg47b 31319* | TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.) |
Theorem | cdlemeg47rv 31320* | Value of g_{s}(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.) |
Theorem | cdlemeg47rv2 31321* | Value of g_{s}(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, 1-Apr-2013.) |
Theorem | cdlemeg49le 31322* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdlemeg46bOLDN 31323* | TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemeg46c 31324* | TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.) |
Theorem | cdlemeg46rvOLDN 31325* | Value of g_{s}(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.) |
Theorem | cdlemeg46rv2OLDN 31326* | Value of g_{s}(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.) |
Theorem | cdlemeg46fvaw 31327* | Show that is an atom not under when is an atom not under . (Contributed by NM, 1-Apr-2013.) |
Theorem | cdlemeg46nlpq 31328* | Show that is not under when isn't. (Contributed by NM, 3-Apr-2013.) |
Theorem | cdlemeg46ngfr 31329* | TODO FIX COMMENT g(f(s))=s p. 115 4th line from bottom. (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46nfgr 31330* | TODO FIX COMMENT f(g(s))=s p. 115 antepenultimate line. (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46sfg 31331* | TODO FIX COMMENT f(r) s = f(r) g(s) p. 116 2nd line TODO: eliminate eqcomd? (Contributed by NM, 4-Apr-2013.) |
Theorem | cdlemeg46fjgN 31332* | NOT NEEDED? TODO FIX COMMENT TODO eliminate eqcomd 2301? p. 116 2nd line. (Contributed by NM, 2-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemeg46rjgN 31333* | NOT NEEDED? TODO FIX COMMENT r g(s) = r v_{2} p. 115 last line. (Contributed by NM, 2-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemeg46fjv 31334* | TODO FIX COMMENT f(r) f(g(s)) = f(r) v_{2} p. 116 2nd line. (Contributed by NM, 2-Apr-2013.) |
Theorem | cdlemeg46fsfv 31335* | TODO FIX COMMENT f(r) s = f(r) v_{2} p. 116 2nd line. (Contributed by NM, 2-Apr-2013.) |
Theorem | cdlemeg46frv 31336* | TODO FIX COMMENT (f(r) v_{2}) w = v_{2} p. 116 3rd line. (Contributed by NM, 2-Apr-2013.) |
Theorem | cdlemeg46v1v2 31337* | TODO FIX COMMENT v_{1} = v_{2} p. 116 3rd line. (Contributed by NM, 2-Apr-2013.) |
Theorem | cdlemeg46vrg 31338* | TODO FIX COMMENT v_{1} r g(s) p. 116 3rd line. (Contributed by NM, 3-Apr-2013.) |
Theorem | cdlemeg46rgv 31339* | TODO FIX COMMENT r g(s) v_{1} p. 116 3rd line. (Contributed by NM, 3-Apr-2013.) |
Theorem | cdlemeg46req 31340* | TODO FIX COMMENT r = (v_{1} g(s)) p. 116 3rd line. (Contributed by NM, 3-Apr-2013.) |
Theorem | cdlemeg46gfv 31341* | 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 31342* | TODO FIX COMMENT p. 116 penultimate line: g(f(r)) = r. (Contributed by NM, 4-Apr-2013.) |