Home Metamath Proof ExplorerTheorem 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)

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

Theoremcdlemk19-2N 31001* Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. , , , are k, sigma2 (p), k2, f2. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk7u-2N 31002* Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119 for the sigma2 case. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk11u-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 sigma2 () case. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk12u-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 sigma2 () case. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk21-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.)

Theoremcdlemk20-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 fi. Our , , , , , represent their f1, f2, k1, k2, sigma1, sigma2. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk22 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.)

Theoremcdlemk30 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.)

Theoremcdlemkuu 31009* Convert between function and operation forms of . TODO: Use operation form everywhere. (Contributed by NM, 6-Jul-2013.)

Theoremcdlemk31 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.)

Theoremcdlemk32 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.)

Theoremcdlemkuel-3 31012* Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma2 (p) function to be a translation. TODO: combine cdlemkj 30977? (Contributed by NM, 11-Jul-2013.)

Theoremcdlemkuv2-3N 31013* Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 1, where sigma2 (p) is , f1 is , and k1 is . (Contributed by NM, 6-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk18-3N 31014* Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. , , , are k, sigma2 (p), k1, f1. (Contributed by NM, 7-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk22-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.)

Theoremcdlemk23-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.)

Theoremcdlemk24-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.)

Theoremcdlemk25-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.)

Theoremcdlemk26b-3 31019* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 14-Jul-2013.)

Theoremcdlemk26-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.)

Theoremcdlemk27-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.)

Theoremcdlemk28-3 31022* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 14-Jul-2013.)

Theoremcdlemk33N 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.)

Theoremcdlemk34 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.)

Theoremcdlemk29-3 31025* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 14-Jul-2013.)

Theoremcdlemk35 31026* Part of proof of Lemma K of [Crawley] p. 118. cdlemk29-3 31025 with shorter hypotheses. (Contributed by NM, 18-Jul-2013.)

Theoremcdlemk36 31027* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 18-Jul-2013.)

Theoremcdlemk37 31028* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 18-Jul-2013.)

Theoremcdlemk38 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.)

Theoremcdlemk39 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.)

Theoremcdlemk40 31031* TODO: fix comment. (Contributed by NM, 31-Jul-2013.)

Theoremcdlemk40t 31032* TODO: fix comment. (Contributed by NM, 31-Jul-2013.)

Theoremcdlemk40f 31033* TODO: fix comment. (Contributed by NM, 31-Jul-2013.)

Theoremcdlemk41 31034* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 19-Jul-2013.)

Theoremcdlemkfid1N 31035 Lemma for cdlemkfid3N 31039. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)

Theoremcdlemkid1 31036 Lemma for cdlemkid 31050. (Contributed by NM, 24-Jul-2013.)

Theoremcdlemkfid2N 31037 Lemma for cdlemkfid3N 31039. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)

Theoremcdlemkid2 31038* Lemma for cdlemkid 31050. (Contributed by NM, 24-Jul-2013.)

Theoremcdlemkfid3N 31039* TODO: is this useful or should it be deleted? (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)

Theoremcdlemky 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.)

Theoremcdlemkyu 31041* Convert between function and explicit forms. represents in cdlemkuu 31009. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.)

Theoremcdlemkyuu 31042* cdlemkyu 31041 with some hypotheses eliminated. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.)

Theoremcdlemk11ta 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.)

Theoremcdlemk19ylem 31044* Lemma for cdlemk19y 31046. (Contributed by NM, 30-Jul-2013.)

Theoremcdlemk11tb 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.)

Theoremcdlemk19y 31046* cdlemk19 30983 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013.)

Theoremcdlemkid3N 31047* Lemma for cdlemkid 31050. (Contributed by NM, 25-Jul-2013.) (New usage is discouraged.)

Theoremcdlemkid4 31048* Lemma for cdlemkid 31050. (Contributed by NM, 25-Jul-2013.)

Theoremcdlemkid5 31049* Lemma for cdlemkid 31050. (Contributed by NM, 25-Jul-2013.)

Theoremcdlemkid 31050* The value of the tau function (in Lemma K of [Crawley] p. 118) on the identity relation. (Contributed by NM, 25-Jul-2013.)

Theoremcdlemk35s 31051* Substitution version of cdlemk35 31026. (Contributed by NM, 22-Jul-2013.)

Theoremcdlemk35s-id 31052* Substitution version of cdlemk35 31026. (Contributed by NM, 26-Jul-2013.)

Theoremcdlemk39s 31053* Substitution version of cdlemk39 31030. TODO: Can any commonality with cdlemk35s 31051 be exploited? (Contributed by NM, 23-Jul-2013.)

Theoremcdlemk39s-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.)

Theoremcdlemk42 31055* Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 20-Jul-2013.)