Home | Metamath
Proof Explorer Theorem List (p. 341 of 402) | < 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-26569) |
Hilbert Space Explorer
(26570-28092) |
Users' Mathboxes
(28093-40162) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdleme39a 34001 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT. , , , serve as f(t), f(u), f_{t}(), f_{t}(). Put hypotheses of cdleme38n 34000 in convention of cdleme32sn1awN 33968. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.) |
Theorem | cdleme39n 34002 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT. , , , serve as f(t), f(u), f_{t}(), f_{t}(). Put hypotheses of cdleme38n 34000 in convention of cdleme32sn1awN 33968. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.) |
Theorem | cdleme40m 34003* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT Use proof idea from cdleme32sn1awN 33968. (Contributed by NM, 18-Mar-2013.) |
Theorem | cdleme40n 34004* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT TODO get rid of '.<' class? (Contributed by NM, 18-Mar-2013.) |
Theorem | cdleme40v 34005* | Part of proof of Lemma E in [Crawley] p. 113. Change bound variables in (but we use for convenience since we have its hypotheses available) . (Contributed by NM, 18-Mar-2013.) |
Theorem | cdleme40w 34006* | Part of proof of Lemma E in [Crawley] p. 113. Apply cdleme40v 34005 bound variable change to . TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.) |
Theorem | cdleme42a 34007 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 3-Mar-2013.) |
Theorem | cdleme42c 34008 | Part of proof of Lemma E in [Crawley] p. 113. Match . (Contributed by NM, 6-Mar-2013.) |
Theorem | cdleme42d 34009 | Part of proof of Lemma E in [Crawley] p. 113. Match . (Contributed by NM, 6-Mar-2013.) |
Theorem | cdleme41sn3aw 34010* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is different on and off the line. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.) |
Theorem | cdleme41sn4aw 34011* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for on and off line. TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.) |
Theorem | cdleme41snaw 34012* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for combined cases; compare cdleme32snaw 33971. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.) |
Theorem | cdleme41fva11 34013* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is one-to-one for r in W (r an atom not under w). TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.) |
Theorem | cdleme42b 34014* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 6-Mar-2013.) |
Theorem | cdleme42e 34015* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
Theorem | cdleme42f 34016* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
Theorem | cdleme42g 34017* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
Theorem | cdleme42h 34018* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
Theorem | cdleme42i 34019* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
Theorem | cdleme42k 34020* | Part of proof of Lemma E in [Crawley] p. 113. Since F ' S =/= F'R when S =/= R (i.e. 1-1); then ( ( F ' R ) .\/ ( F ' S ) ) is 2-dim therefore = ( ( F ' R ) .\/ V ) by cdleme42i 34019 and ps-1 33011 TODO: FIX COMMENT (Contributed by NM, 20-Mar-2013.) |
Theorem | cdleme42ke 34021* | Part of proof of Lemma E in [Crawley] p. 113. Remove condition. TODO: FIX COMMENT (Contributed by NM, 2-Apr-2013.) |
Theorem | cdleme42keg 34022* | Part of proof of Lemma E in [Crawley] p. 113. Remove condition. TODO: FIX COMMENT TODO: Use instead of cdleme42ke 34021 and even combine with it? (Contributed by NM, 22-Apr-2013.) |
Theorem | cdleme42mN 34023* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT . f preserves join: f(r s) = f(r) s, p. 115 10th line from bottom. (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
Theorem | cdleme42mgN 34024* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT . f preserves join: f(r s) = f(r) s, p. 115 10th line from bottom. TODO: Use instead of cdleme42mN 34023? Combine with cdleme42mN 34023? (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
Theorem | cdleme43aN 34025 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT p. 115 penultimate line: g(f(r)) = (p v q) ^ (g(s) v v_{1}) (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
Theorem | cdleme43bN 34026 | 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 34027 | 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 34028 | 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 34029 | Conversion for to reuse theorems. TODO FIX COMMENT TODO What other conversion theorems would be reused? e.g. cdlemeg46nlpq 34053? Find other hlatjcom 32902 uses giving . (Contributed by NM, 1-Apr-2013.) |
Theorem | cdleme46f2g1 34030 | Conversion for to reuse theorems. TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.) |
Theorem | cdleme17d2 34031* | 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 34032* | TODO FIX COMMENT (Contributed by NM, 5-Apr-2013.) |
Theorem | cdleme17d4 34033* | TODO FIX COMMENT (Contributed by NM, 11-Apr-2013.) |
Theorem | cdleme17d 34034* | 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 34035* | Part of proof of Lemma D in [Crawley] p. 113. TODO: Can this replace uses of cdleme32a 33977? TODO: Can this be used to help prove the or case where is an atom? (Contributed by NM, 8-Apr-2013.) |
Theorem | cdleme48fvg 34036* | Remove condition in cdleme48fv 34035. TODO: Can this replace uses of cdleme32a 33977? 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 34035? (Contributed by NM, 23-Apr-2013.) |
Theorem | cdleme46fvaw 34037* | Show that is an atom not under when is an atom not under . (Contributed by NM, 18-Apr-2013.) |
Theorem | cdleme48bw 34038* | TODO: fix comment. TODO: Remove unnecessary from cdleme48bw 34038 cdlemeg46c 34049 cdlemeg46fvaw 34052 cdlemeg46rgv 34064 cdlemeg46gfv 34066? cdleme48d 34071? and possibly others they affect. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme48b 34039* | TODO: fix comment. (Contributed by NM, 8-Apr-2013.) |
Theorem | cdleme46frvlpq 34040* | Show that is not under when isn't. (Contributed by NM, 1-Apr-2013.) |
Theorem | cdleme46fsvlpq 34041* | Show that is under when is. (Contributed by NM, 1-Apr-2013.) |
Theorem | cdlemeg46fvcl 34042* | TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme4gfv 34043* | Part of proof of Lemma D in [Crawley] p. 113. TODO: Can this replace uses of cdleme32a 33977? TODO: Can this be used to help prove the or case where is an atom? TODO: Would an antecedent transformer like cdleme46f2g2 34029 help? (Contributed by NM, 8-Apr-2013.) |
Theorem | cdlemeg47b 34044* | TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.) |
Theorem | cdlemeg47rv 34045* | 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 34046* | 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 34047* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdlemeg46bOLDN 34048* | TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.) (New usage is discouraged.) |
Theorem | cdlemeg46c 34049* | TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.) |
Theorem | cdlemeg46rvOLDN 34050* | 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 34051* | 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 34052* | Show that is an atom not under when |