Home | Metamath
Proof Explorer Theorem List (p. 362 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | erngfmul-rN 36101* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
Theorem | erngmul-rN 36102 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
Theorem | cdlemh1 36103 | Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.) |
Theorem | cdlemh2 36104 | Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 16-Jun-2013.) |
Theorem | cdlemh 36105 | Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.) |
Theorem | cdlemi1 36106 | Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.) |
Theorem | cdlemi2 36107 | Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.) |
Theorem | cdlemi 36108 | Lemma I of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.) |
Theorem | cdlemj1 36109 | Part of proof of Lemma J of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.) |
Theorem | cdlemj2 36110 | Part of proof of Lemma J of [Crawley] p. 118. Eliminate . (Contributed by NM, 20-Jun-2013.) |
Theorem | cdlemj3 36111 | Part of proof of Lemma J of [Crawley] p. 118. Eliminate . (Contributed by NM, 20-Jun-2013.) |
Theorem | tendocan 36112 | Cancellation law: if the values of two trace-preserving endormorphisms are equal, so are the endormorphisms. Lemma J of [Crawley] p. 118. (Contributed by NM, 21-Jun-2013.) |
Theorem | tendoid0 36113* | A trace-preserving endomorphism is the additive identity iff at least one of its values (at a non-identity translation) is the identity translation. (Contributed by NM, 1-Aug-2013.) |
Theorem | tendo0mul 36114* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013.) |
Theorem | tendo0mulr 36115* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014.) |
Theorem | tendo1ne0 36116* | The identity (unity) is not equal to the zero trace-preserving endomorphism. (Contributed by NM, 8-Aug-2013.) |
Theorem | tendoconid 36117* | The composition (product) of trace-preserving endormorphisms is nonzero when each argument is nonzero. (Contributed by NM, 8-Aug-2013.) |
Theorem | tendotr 36118* | The trace of the value of a nonzero trace-preserving endomorphism equals the trace of the argument. (Contributed by NM, 11-Aug-2013.) |
Theorem | cdlemk1 36119 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
Theorem | cdlemk2 36120 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
Theorem | cdlemk3 36121 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk4 36122 | Part of proof of Lemma K of [Crawley] p. 118, last line. We use for their h, since is already used. (Contributed by NM, 24-Jun-2013.) |
Theorem | cdlemk5a 36123 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk5 36124 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 25-Jun-2013.) |
Theorem | cdlemk6 36125 | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 35172. (Contributed by NM, 25-Jun-2013.) |
Theorem | cdlemk8 36126 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 26-Jun-2013.) |
Theorem | cdlemk9 36127 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.) |
Theorem | cdlemk9bN 36128 | Part of proof of Lemma K of [Crawley] p. 118. TODO: is this needed? If so, shorten with cdlemk9 36127 if that one is also needed. (Contributed by NM, 28-Jun-2013.) (New usage is discouraged.) |
Theorem | cdlemki 36129* | Part of proof of Lemma K of [Crawley] p. 118. TODO: Eliminate and put into cdlemksel 36133. (Contributed by NM, 25-Jun-2013.) |
Theorem | cdlemkvcl 36130 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.) |
Theorem | cdlemk10 36131 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.) |
Theorem | cdlemksv 36132* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma(p) function. (Contributed by NM, 26-Jun-2013.) |
Theorem | cdlemksel 36133* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma(p) function to be a translation. TODO: combine cdlemki 36129? (Contributed by NM, 26-Jun-2013.) |
Theorem | cdlemksat 36134* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.) |
Theorem | cdlemksv2 36135* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma(p) function at the fixed parameter. (Contributed by NM, 26-Jun-2013.) |
Theorem | cdlemk7 36136* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119. (Contributed by NM, 27-Jun-2013.) |
Theorem | cdlemk11 36137* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 3, line 8, p. 119. (Contributed by NM, 29-Jun-2013.) |
Theorem | cdlemk12 36138* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 4, line 10, p. 119. (Contributed by NM, 30-Jun-2013.) |
Theorem | cdlemkoatnle 36139* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemk13 36140* | Part of proof of Lemma K of [Crawley] p. 118. Line 13 on p. 119. , are k1, f1. (Contributed by NM, 1-Jul-2013.) |
Theorem | cdlemkole 36141* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemk14 36142* | Part of proof of Lemma K of [Crawley] p. 118. Line 19 on p. 119. , are k1, f1. (Contributed by NM, 1-Jul-2013.) |
Theorem | cdlemk15 36143* | Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k1, f1. (Contributed by NM, 1-Jul-2013.) |
Theorem | cdlemk16a 36144* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk16 36145* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) |
Theorem | cdlemk17 36146* | Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k1, f1. (Contributed by NM, 1-Jul-2013.) |
Theorem | cdlemk1u 36147* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk5auN 36148* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk5u 36149* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemk6u 36150* | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 35172. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemkj 36151* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemkuvN 36152* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma1 (p) function . (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkuel 36153* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma1 (p) function to be a translation. TODO: combine cdlemkj 36151? (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemkuat 36154* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemkuv2 36155* | 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.) |
Theorem | cdlemk18 36156* | 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.) |
Theorem | cdlemk19 36157* | 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.) |
Theorem | cdlemk7u 36158* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119 for the sigma1 case. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk11u 36159* | 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.) |
Theorem | cdlemk12u 36160* | 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.) |
Theorem | cdlemk21N 36161* | 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 36162* | 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.) |
Theorem | cdlemkoatnle-2N 36163* | Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk13-2N 36164* | 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.) |
Theorem | cdlemkole-2N 36165* | Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk14-2N 36166* | 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.) |
Theorem | cdlemk15-2N 36167* | 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.) |
Theorem | cdlemk16-2N 36168* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk17-2N 36169* | 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.) |
Theorem | cdlemkj-2N 36170* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkuv-2N 36171* | 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.) |
Theorem | cdlemkuel-2N 36172* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma2 (p) function to be a translation. TODO: combine cdlemkj 36151? (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkuv2-2 36173* | 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.) |
Theorem | cdlemk18-2N 36174* | 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.) |
Theorem | cdlemk19-2N 36175* | 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.) |
Theorem | cdlemk7u-2N 36176* | 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.) |
Theorem | cdlemk11u-2N 36177* | 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.) |
Theorem | cdlemk12u-2N 36178* | 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.) |
Theorem | cdlemk21-2N 36179* | 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 36180* | 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.) |
Theorem | cdlemk22 36181* | 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 36182* | 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 36183* | Convert between function and operation forms of . TODO: Use operation form everywhere. (Contributed by NM, 6-Jul-2013.) |
Theorem | cdlemk31 36184* | 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 36185* | 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 36186* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma2 (p) function to be a translation. TODO: combine cdlemkj 36151? (Contributed by NM, 11-Jul-2013.) |
Theorem | cdlemkuv2-3N 36187* | 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.) |
Theorem | cdlemk18-3N 36188* | 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.) |
Theorem | cdlemk22-3 36189* | 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 36190* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the requirement from cdlemk22-3 36189. (Contributed by NM, 7-Jul-2013.) |
Theorem | cdlemk24-3 36191* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the requirement from cdlemk23-3 36190 using . (Contributed by NM, 7-Jul-2013.) |
Theorem | cdlemk25-3 36192* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the requirement from cdlemk24-3 36191. (Contributed by NM, 7-Jul-2013.) |
Theorem | cdlemk26b-3 36193* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 14-Jul-2013.) |
Theorem | cdlemk26-3 36194* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the requirements from cdlemk25-3 36192. (Contributed by NM, 10-Jul-2013.) |
Theorem | cdlemk27-3 36195* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the from the conclusion of cdlemk25-3 36192. (Contributed by NM, 10-Jul-2013.) |
Theorem | cdlemk28-3 36196* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 14-Jul-2013.) |
Theorem | cdlemk33N 36197* | 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 36198. (Contributed by NM, 18-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk34 36198* | 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 36199* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 14-Jul-2013.) |
Theorem | cdlemk35 36200* | Part of proof of Lemma K of [Crawley] p. 118. cdlemk29-3 36199 with shorter hypotheses. (Contributed by NM, 18-Jul-2013.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |