Home | Metamath
Proof Explorer Theorem List (p. 300 of 315) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21490) |
Hilbert Space Explorer
(21491-23013) |
Users' Mathboxes
(23014-31421) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdleme32e 29901* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
Theorem | cdleme32f 29902* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
Theorem | cdleme32le 29903* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
Theorem | cdleme35a 29904 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35fnpq 29905 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.) |
Theorem | cdleme35b 29906 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35c 29907 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35d 29908 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35e 29909 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35f 29910 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35g 29911 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
Theorem | cdleme35h 29912 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of line. TODO: FIX COMMENT (Contributed by NM, 11-Mar-2013.) |
Theorem | cdleme35h2 29913 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of line. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.) |
Theorem | cdleme35sn2aw 29914* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of line case; compare cdleme32sn2awN 29890. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.) |
Theorem | cdleme35sn3a 29915* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.) |
Theorem | cdleme36a 29916 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 11-Mar-2013.) |
Theorem | cdleme36m 29917 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT (Contributed by NM, 11-Mar-2013.) |
Theorem | cdleme37m 29918 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT (Contributed by NM, 13-Mar-2013.) |
Theorem | cdleme38m 29919 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT (Contributed by NM, 13-Mar-2013.) |
Theorem | cdleme38n 29920 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT TODO shorter if proved directly from cdleme36m 29917 and cdleme37m 29918? (Contributed by NM, 14-Mar-2013.) |
Theorem | cdleme39a 29921 | 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 29920 in convention of cdleme32sn1awN 29888. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.) |
Theorem | cdleme39n 29922 | 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 29920 in convention of cdleme32sn1awN 29888. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.) |
Theorem | cdleme40m 29923* | 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 29888. (Contributed by NM, 18-Mar-2013.) |
Theorem | cdleme40n 29924* | 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 29925* | 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 29926* | Part of proof of Lemma E in [Crawley] p. 113. Apply cdleme40v 29925 bound variable change to . TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.) |
Theorem | cdleme42a 29927 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 3-Mar-2013.) |
Theorem | cdleme42c 29928 | Part of proof of Lemma E in [Crawley] p. 113. Match . (Contributed by NM, 6-Mar-2013.) |
Theorem | cdleme42d 29929 | Part of proof of Lemma E in [Crawley] p. 113. Match . (Contributed by NM, 6-Mar-2013.) |
Theorem | cdleme41sn3aw 29930* | 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 29931* | 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 29932* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for combined cases; compare cdleme32snaw 29891. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.) |
Theorem | cdleme41fva11 29933* | 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 29934* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 6-Mar-2013.) |
Theorem | cdleme42e 29935* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
Theorem | cdleme42f 29936* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
Theorem | cdleme42g 29937* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
Theorem | cdleme42h 29938* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
Theorem | cdleme42i 29939* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
Theorem | cdleme42k 29940* | 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 29939 and ps-1 28933 TODO: FIX COMMENT (Contributed by NM, 20-Mar-2013.) |
Theorem | cdleme42ke 29941* | Part of proof of Lemma E in [Crawley] p. 113. Remove condition. TODO: FIX COMMENT (Contributed by NM, 2-Apr-2013.) |
Theorem | cdleme42keg 29942* | Part of proof of Lemma E in [Crawley] p. 113. Remove condition. TODO: FIX COMMENT TODO: Use instead of cdleme42ke 29941 and even combine with it? (Contributed by NM, 22-Apr-2013.) |
Theorem | cdleme42mN 29943* | 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 29944* | 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 29943? Combine with cdleme42mN 29943? (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
Theorem | cdleme43aN 29945 | 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 29946 | 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 29947 | 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 29948 | 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 29949 | Conversion for to reuse theorems. TODO FIX COMMENT TODO What other conversion theorems would be reused? e.g. cdlemeg46nlpq 29973? Find other hlatjcom 28824 uses giving . (Contributed by NM, 1-Apr-2013.) |
Theorem | cdleme46f2g1 29950 | Conversion for to reuse theorems. TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.) |
Theorem | cdleme17d2 29951* | 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 29952* | TODO FIX COMMENT (Contributed by NM, 5-Apr-2013.) |
Theorem | cdleme17d4 29953* | TODO FIX COMMENT (Contributed by NM, 11-Apr-2013.) |
Theorem | cdleme17d 29954* | 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 29955* | Part of proof of Lemma D in [Crawley] p. 113. TODO: Can this replace uses of cdleme32a 29897? TODO: Can this be used to help prove the or case where is an atom? (Contributed by NM, 8-Apr-2013.) |
Theorem | cdleme48fvg 29956* | Remove condition in cdleme48fv 29955. TODO: Can this replace uses of cdleme32a 29897? 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 29955? (Contributed by NM, 23-Apr-2013.) |
Theorem | cdleme46fvaw 29957* | Show that is an atom not under when is an atom not under . (Contributed by NM, 18-Apr-2013.) |
Theorem | cdleme48bw 29958* | TODO: fix comment. TODO: Remove unnecessary from cdleme48bw 29958 cdlemeg46c 29969 cdlemeg46fvaw 29972 cdlemeg46rgv 29984 cdlemeg46gfv 29986? cdleme48d 29991? and possibly others they affect. (Contributed by NM, 9-Apr-2013.) |
Theorem | cdleme48b 29959* | TODO: fix comment. (Contributed by NM, 8-Apr-2013.) |