Home | Metamath
Proof Explorer Theorem List (p. 317 of 327) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-22413) |
Hilbert Space Explorer
(22414-23936) |
Users' Mathboxes
(23937-32699) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemkuv2 31601* | Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 1, where sigma_{1} (p) is , f_{1} is , and k_{1} is . (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemk18 31602* | Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. , , , are k, sigma_{1} (p), k_{1}, f_{1}. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemk19 31603* | Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. , , , are k, sigma_{1} (p), k_{1}, f_{1}. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemk7u 31604* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119 for the sigma_{1} case. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk11u 31605* | Part of proof of Lemma K of [Crawley] p. 118. Line 17, p. 119, showing Eq. 3 (line 8, p. 119) for the sigma_{1} () case. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemk12u 31606* | Part of proof of Lemma K of [Crawley] p. 118. Line 18, p. 119, showing Eq. 4 (line 10, p. 119) for the sigma_{1} () case. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemk21N 31607* | Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=0 and j=1. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk20 31608* | 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.) |
Theorem | cdlemkoatnle-2N 31609* | Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk13-2N 31610* | Part of proof of Lemma K of [Crawley] p. 118. Line 13 on p. 119. , are k_{2}, f_{2}. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkole-2N 31611* | Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk14-2N 31612* | Part of proof of Lemma K of [Crawley] p. 118. Line 19 on p. 119. , are k_{2}, f_{2}. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk15-2N 31613* | Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k_{2}, f_{2}. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk16-2N 31614* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk17-2N 31615* | Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k_{2}, f_{2}. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkj-2N 31616* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkuv-2N 31617* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma_{2} (p) function, given . (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkuel-2N 31618* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma_{2} (p) function to be a translation. TODO: combine cdlemkj 31597? (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkuv2-2 31619* | Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 2, where sigma_{2} (p) is , f_{2} is , and k_{2} is . (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemk18-2N 31620* | 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 | cdlemk19-2N 31621* | 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 31622* | 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 31623* | 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 31624* | 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 31625* | 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 31626* | 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 31627* | 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 31628* | 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 31629* | Convert between function and operation forms of . TODO: Use operation form everywhere. (Contributed by NM, 6-Jul-2013.) |
Theorem | cdlemk31 31630* | 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 31631* | 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 31632* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma_{2} (p) function to be a translation. TODO: combine cdlemkj 31597? (Contributed by NM, 11-Jul-2013.) |
Theorem | cdlemkuv2-3N 31633* | 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 31634* | 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 31635* | 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 31636* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the requirement from cdlemk22-3 31635. (Contributed by NM, 7-Jul-2013.) |
Theorem | cdlemk24-3 31637* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the requirement from cdlemk23-3 31636 using . (Contributed by NM, 7-Jul-2013.) |
Theorem | cdlemk25-3 31638* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the requirement from cdlemk24-3 31637. (Contributed by NM, 7-Jul-2013.) |
Theorem | cdlemk26b-3 31639* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 14-Jul-2013.) |
Theorem | cdlemk26-3 31640* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the requirements from cdlemk25-3 31638. (Contributed by NM, 10-Jul-2013.) |
Theorem | cdlemk27-3 31641* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the from the conclusion of cdlemk25-3 31638. (Contributed by NM, 10-Jul-2013.) |
Theorem | cdlemk28-3 31642* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 14-Jul-2013.) |
Theorem | cdlemk33N 31643* | 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 31644. (Contributed by NM, 18-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk34 31644* | 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 31645* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 14-Jul-2013.) |
Theorem | cdlemk35 31646* | Part of proof of Lemma K of [Crawley] p. 118. cdlemk29-3 31645 with shorter hypotheses. (Contributed by NM, 18-Jul-2013.) |
Theorem | cdlemk36 31647* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 18-Jul-2013.) |
Theorem | cdlemk37 31648* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 18-Jul-2013.) |
Theorem | cdlemk38 31649* | Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. TODO: derive more directly with r19.23 2813? (Contributed by NM, 19-Jul-2013.) |
Theorem | cdlemk39 31650* | 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 31651* | TODO: fix comment. (Contributed by NM, 31-Jul-2013.) |
Theorem | cdlemk40t 31652* | TODO: fix comment. (Contributed by NM, 31-Jul-2013.) |
Theorem | cdlemk40f 31653* | TODO: fix comment. (Contributed by NM, 31-Jul-2013.) |