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

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

Theoremcdlemkuv2 31601* Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 1, where sigma1 (p) is , f1 is , and k1 is . (Contributed by NM, 2-Jul-2013.)

Theoremcdlemk18 31602* Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. , , , are k, sigma1 (p), k1, f1. (Contributed by NM, 2-Jul-2013.)

Theoremcdlemk19 31603* Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. , , , are k, sigma1 (p), k1, f1. (Contributed by NM, 2-Jul-2013.)

Theoremcdlemk7u 31604* Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119 for the sigma1 case. (Contributed by NM, 3-Jul-2013.)

Theoremcdlemk11u 31605* Part of proof of Lemma K of [Crawley] p. 118. Line 17, p. 119, showing Eq. 3 (line 8, p. 119) for the sigma1 () case. (Contributed by NM, 4-Jul-2013.)

Theoremcdlemk12u 31606* Part of proof of Lemma K of [Crawley] p. 118. Line 18, p. 119, showing Eq. 4 (line 10, p. 119) for the sigma1 () case. (Contributed by NM, 4-Jul-2013.)

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

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

Theoremcdlemkoatnle-2N 31609* Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk13-2N 31610* Part of proof of Lemma K of [Crawley] p. 118. Line 13 on p. 119. , are k2, f2. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.)

Theoremcdlemkole-2N 31611* Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk14-2N 31612* Part of proof of Lemma K of [Crawley] p. 118. Line 19 on p. 119. , are k2, f2. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk15-2N 31613* Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k2, f2. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk16-2N 31614* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk17-2N 31615* Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k2, f2. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.)

Theoremcdlemkj-2N 31616* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)

Theoremcdlemkuv-2N 31617* Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma2 (p) function, given . (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)

Theoremcdlemkuel-2N 31618* Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma2 (p) function to be a translation. TODO: combine cdlemkj 31597? (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)

Theoremcdlemkuv2-2 31619* Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 2, where sigma2 (p) is , f2 is , and k2 is . (Contributed by NM, 2-Jul-2013.)

Theoremcdlemk18-2N 31620* 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.)

Theoremcdlemk19-2N 31621* 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 31622* 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 31623* 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 31624* 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 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.)

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

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

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

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

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

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

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

Theoremcdlemkuv2-3N 31633* 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 31634* 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 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.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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