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

 Color key: Metamath Proof Explorer (1-21423) Hilbert Space Explorer (21424-22946) Users' Mathboxes (22947-31284)

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

Theoremcdleme42h 29801* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)

Theoremcdleme42i 29802* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)

Theoremcdleme42k 29803* 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 29802 and ps-1 28796 TODO: FIX COMMENT (Contributed by NM, 20-Mar-2013.)

Theoremcdleme42ke 29804* Part of proof of Lemma E in [Crawley] p. 113. Remove condition. TODO: FIX COMMENT (Contributed by NM, 2-Apr-2013.)

Theoremcdleme42keg 29805* Part of proof of Lemma E in [Crawley] p. 113. Remove condition. TODO: FIX COMMENT TODO: Use instead of cdleme42ke 29804 and even combine with it? (Contributed by NM, 22-Apr-2013.)

Theoremcdleme42mN 29806* 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.)

Theoremcdleme42mgN 29807* 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 29806? Combine with cdleme42mN 29806? (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.)

Theoremcdleme43aN 29808 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 v1) (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.)

Theoremcdleme43bN 29809 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.)

Theoremcdleme43cN 29810 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT p. 115 last line: r v g(s) = r v v2 (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.)

Theoremcdleme43dN 29811 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.)

Theoremcdleme46f2g2 29812 Conversion for to reuse theorems. TODO FIX COMMENT TODO What other conversion theorems would be reused? e.g. cdlemeg46nlpq 29836? Find other hlatjcom 28687 uses giving . (Contributed by NM, 1-Apr-2013.)

Theoremcdleme46f2g1 29813 Conversion for to reuse theorems. TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.)

Theoremcdleme17d2 29814* Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. , represent f(s), fs(p) respectively. We show, in their notation, fs(p)=q. TODO FIX COMMENT (Contributed by NM, 5-Apr-2013.)

Theoremcdleme17d3 29815* TODO FIX COMMENT (Contributed by NM, 5-Apr-2013.)

Theoremcdleme17d4 29816* TODO FIX COMMENT (Contributed by NM, 11-Apr-2013.)

Theoremcdleme17d 29817* Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. We show, in their notation, fs(p)=q. TODO FIX COMMENT (Contributed by NM, 11-Apr-2013.)

Theoremcdleme48fv 29818* Part of proof of Lemma D in [Crawley] p. 113. TODO: Can this replace uses of cdleme32a 29760? TODO: Can this be used to help prove the or case where is an atom? (Contributed by NM, 8-Apr-2013.)

Theoremcdleme48fvg 29819* Remove condition in cdleme48fv 29818. TODO: Can this replace uses of cdleme32a 29760? 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 29818? (Contributed by NM, 23-Apr-2013.)

Theoremcdleme46fvaw 29820* Show that is an atom not under when is an atom not under . (Contributed by NM, 18-Apr-2013.)

Theoremcdleme48bw 29821* TODO: fix comment. TODO: Remove unnecessary from cdleme48bw 29821 cdlemeg46c 29832 cdlemeg46fvaw 29835 cdlemeg46rgv 29847 cdlemeg46gfv 29849? cdleme48d 29854? and possibly others they affect. (Contributed by NM, 9-Apr-2013.)

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

Theoremcdleme46frvlpq 29823* Show that is not under when isn't. (Contributed by NM, 1-Apr-2013.)

Theoremcdleme46fsvlpq 29824* Show that is under when is. (Contributed by NM, 1-Apr-2013.)

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

Theoremcdleme4gfv 29826* Part of proof of Lemma D in [Crawley] p. 113. TODO: Can this replace uses of cdleme32a 29760? TODO: Can this be used to help prove the or case where is an atom? TODO: Would an antecedent transformer like cdleme46f2g2 29812 help? (Contributed by NM, 8-Apr-2013.)

Theoremcdlemeg47b 29827* TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.)

Theoremcdlemeg47rv 29828* 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.)

Theoremcdlemeg47rv2 29829* 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, 1-Apr-2013.)

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

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

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

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

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

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

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

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

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

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

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

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

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