Home | Metamath
Proof Explorer Theorem List (p. 311 of 321) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-22269) |
Hilbert Space Explorer
(22270-23792) |
Users' Mathboxes
(23793-32079) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemk19-2N 31001* | Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. , , , are k, sigma_{2} (p), k_{2}, f_{2}. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk7u-2N 31002* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119 for the sigma_{2} case. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk11u-2N 31003* | Part of proof of Lemma K of [Crawley] p. 118. Line 17, p. 119, showing Eq. 3 (line 8, p. 119) for the sigma_{2} () case. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk12u-2N 31004* | Part of proof of Lemma K of [Crawley] p. 118. Line 18, p. 119, showing Eq. 4 (line 10, p. 119) for the sigma_{2} () case. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk21-2N 31005* | Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=0 and j=2. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk20-2N 31006* | Part of proof of Lemma K of [Crawley] p. 118. Line 22, p. 119 for the i=2, j=1 case. Note typo on line 22: f should be f_{i}. Our , , , , , represent their f_{1}, f_{2}, k_{1}, k_{2}, sigma_{1}, sigma_{2}. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk22 31007* | Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=1 and j=2. (Contributed by NM, 5-Jul-2013.) |
Theorem | cdlemk30 31008* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. (Contributed by NM, 17-Jul-2013.) |
Theorem | cdlemkuu 31009* | Convert between function and operation forms of . TODO: Use operation form everywhere. (Contributed by NM, 6-Jul-2013.) |
Theorem | cdlemk31 31010* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. (Contributed by NM, 17-Jul-2013.) |
Theorem | cdlemk32 31011* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. (Contributed by NM, 17-Jul-2013.) |
Theorem | cdlemkuel-3 31012* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma_{2} (p) function to be a translation. TODO: combine cdlemkj 30977? (Contributed by NM, 11-Jul-2013.) |
Theorem | cdlemkuv2-3N 31013* | Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 1, where sigma_{2} (p) is , f_{1} is , and k_{1} is . (Contributed by NM, 6-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk18-3N 31014* | Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. , , , are k, sigma_{2} (p), k_{1}, f_{1}. (Contributed by NM, 7-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk22-3 31015* | Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=1 and j=2. (Contributed by NM, 7-Jul-2013.) |
Theorem | cdlemk23-3 31016* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the requirement from cdlemk22-3 31015. (Contributed by NM, 7-Jul-2013.) |
Theorem | cdlemk24-3 31017* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the requirement from cdlemk23-3 31016 using . (Contributed by NM, 7-Jul-2013.) |
Theorem | cdlemk25-3 31018* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the requirement from cdlemk24-3 31017. (Contributed by NM, 7-Jul-2013.) |
Theorem | cdlemk26b-3 31019* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 14-Jul-2013.) |
Theorem | cdlemk26-3 31020* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the requirements from cdlemk25-3 31018. (Contributed by NM, 10-Jul-2013.) |
Theorem | cdlemk27-3 31021* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the from the conclusion of cdlemk25-3 31018. (Contributed by NM, 10-Jul-2013.) |
Theorem | cdlemk28-3 31022* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 14-Jul-2013.) |
Theorem | cdlemk33N 31023* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. TODO: not needed, is embodied in cdlemk34 31024. (Contributed by NM, 18-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk34 31024* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. (Contributed by NM, 18-Jul-2013.) |
Theorem | cdlemk29-3 31025* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 14-Jul-2013.) |
Theorem | cdlemk35 31026* | Part of proof of Lemma K of [Crawley] p. 118. cdlemk29-3 31025 with shorter hypotheses. (Contributed by NM, 18-Jul-2013.) |
Theorem | cdlemk36 31027* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 18-Jul-2013.) |
Theorem | cdlemk37 31028* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 18-Jul-2013.) |
Theorem | cdlemk38 31029* | Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. TODO: derive more directly with r19.23 2764? (Contributed by NM, 19-Jul-2013.) |
Theorem | cdlemk39 31030* | Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. Trace-preserving property of tau, represented by . (Contributed by NM, 19-Jul-2013.) |
Theorem | cdlemk40 31031* | TODO: fix comment. (Contributed by NM, 31-Jul-2013.) |
Theorem | cdlemk40t 31032* | TODO: fix comment. (Contributed by NM, 31-Jul-2013.) |
Theorem | cdlemk40f 31033* | TODO: fix comment. (Contributed by NM, 31-Jul-2013.) |
Theorem | cdlemk41 31034* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 19-Jul-2013.) |
Theorem | cdlemkfid1N 31035 | Lemma for cdlemkfid3N 31039. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkid1 31036 | Lemma for cdlemkid 31050. (Contributed by NM, 24-Jul-2013.) |
Theorem | cdlemkfid2N 31037 | Lemma for cdlemkfid3N 31039. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkid2 31038* | Lemma for cdlemkid 31050. (Contributed by NM, 24-Jul-2013.) |
Theorem | cdlemkfid3N 31039* | TODO: is this useful or should it be deleted? (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemky 31040* | Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up stuff. represents in cdlemk31 31010. (Contributed by NM, 21-Jul-2013.) |
Theorem | cdlemkyu 31041* | Convert between function and explicit forms. represents in cdlemkuu 31009. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.) |
Theorem | cdlemkyuu 31042* | cdlemkyu 31041 with some hypotheses eliminated. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.) |
Theorem | cdlemk11ta 31043* | Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. , stand for g, h. TODO: fix comment. (Contributed by NM, 21-Jul-2013.) |
Theorem | cdlemk19ylem 31044* | Lemma for cdlemk19y 31046. (Contributed by NM, 30-Jul-2013.) |
Theorem | cdlemk11tb 31045* | Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. , stand for g, h. cdlemk11ta 31043 with hypotheses removed. TODO: Can this be proved directly with no quantification? (Contributed by NM, 21-Jul-2013.) |
Theorem | cdlemk19y 31046* | cdlemk19 30983 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013.) |
Theorem | cdlemkid3N 31047* | Lemma for cdlemkid 31050. (Contributed by NM, 25-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkid4 31048* | Lemma for cdlemkid 31050. (Contributed by NM, 25-Jul-2013.) |
Theorem | cdlemkid5 31049* | Lemma for cdlemkid 31050. (Contributed by NM, 25-Jul-2013.) |
Theorem | cdlemkid 31050* | The value of the tau function (in Lemma K of [Crawley] p. 118) on the identity relation. (Contributed by NM, 25-Jul-2013.) |
Theorem | cdlemk35s 31051* | Substitution version of cdlemk35 31026. (Contributed by NM, 22-Jul-2013.) |
Theorem | cdlemk35s-id 31052* | Substitution version of cdlemk35 31026. (Contributed by NM, 26-Jul-2013.) |
Theorem | cdlemk39s 31053* | Substitution version of cdlemk39 31030. TODO: Can any commonality with cdlemk35s 31051 be exploited? (Contributed by NM, 23-Jul-2013.) |
Theorem | cdlemk39s-id 31054* | Substitution version of cdlemk39 31030 with non-identity requirement on removed. TODO: Can any commonality with cdlemk35s 31051 be exploited? (Contributed by NM, 26-Jul-2013.) |
Theorem | cdlemk42 31055* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 20-Jul-2013.) |