Home | Metamath
Proof Explorer Theorem List (p. 314 of 325) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-22374) |
Hilbert Space Explorer
(22375-23897) |
Users' Mathboxes
(23898-32447) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemi2 31301 | Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.) |
Theorem | cdlemi 31302 | Lemma I of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.) |
Theorem | cdlemj1 31303 | Part of proof of Lemma J of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.) |
Theorem | cdlemj2 31304 | Part of proof of Lemma J of [Crawley] p. 118. Eliminate . (Contributed by NM, 20-Jun-2013.) |
Theorem | cdlemj3 31305 | Part of proof of Lemma J of [Crawley] p. 118. Eliminate . (Contributed by NM, 20-Jun-2013.) |
Theorem | tendocan 31306 | 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 31307* | 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 31308* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013.) |
Theorem | tendo0mulr 31309* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014.) |
Theorem | tendo1ne0 31310* | The identity (unity) is not equal to the zero trace-preserving endomorphism. (Contributed by NM, 8-Aug-2013.) |
Theorem | tendoconid 31311* | The composition (product) of trace-preserving endormorphisms is nonzero when each argument is nonzero. (Contributed by NM, 8-Aug-2013.) |
Theorem | tendotr 31312* | The trace of the value of a non-zero trace-preserving endomorphism equals the trace of the argument. (Contributed by NM, 11-Aug-2013.) |
Theorem | cdlemk1 31313 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
Theorem | cdlemk2 31314 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
Theorem | cdlemk3 31315 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk4 31316 | 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 31317 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk5 31318 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 25-Jun-2013.) |
Theorem | cdlemk6 31319 | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 30368. (Contributed by NM, 25-Jun-2013.) |
Theorem | cdlemk8 31320 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 26-Jun-2013.) |
Theorem | cdlemk9 31321 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.) |
Theorem | cdlemk9bN 31322 | Part of proof of Lemma K of [Crawley] p. 118. TODO: is this needed? If so, shorten with cdlemk9 31321 if that one is also needed. (Contributed by NM, 28-Jun-2013.) (New usage is discouraged.) |
Theorem | cdlemki 31323* | Part of proof of Lemma K of [Crawley] p. 118. TODO: Eliminate and put into cdlemksel 31327. (Contributed by NM, 25-Jun-2013.) |
Theorem | cdlemkvcl 31324 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.) |
Theorem | cdlemk10 31325 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.) |
Theorem | cdlemksv 31326* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma(p) function. (Contributed by NM, 26-Jun-2013.) |
Theorem | cdlemksel 31327* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma(p) function to be a translation. TODO: combine cdlemki 31323? (Contributed by NM, 26-Jun-2013.) |
Theorem | cdlemksat 31328* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.) |
Theorem | cdlemksv2 31329* | 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 31330* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119. (Contributed by NM, 27-Jun-2013.) |
Theorem | cdlemk11 31331* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 3, line 8, p. 119. (Contributed by NM, 29-Jun-2013.) |
Theorem | cdlemk12 31332* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 4, line 10, p. 119. (Contributed by NM, 30-Jun-2013.) |
Theorem | cdlemkoatnle 31333* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemk13 31334* | Part of proof of Lemma K of [Crawley] p. 118. Line 13 on p. 119. , are k_{1}, f_{1}. (Contributed by NM, 1-Jul-2013.) |
Theorem | cdlemkole 31335* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemk14 31336* | Part of proof of Lemma K of [Crawley] p. 118. Line 19 on p. 119. , are k_{1}, f_{1}. (Contributed by NM, 1-Jul-2013.) |
Theorem | cdlemk15 31337* | Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k_{1}, f_{1}. (Contributed by NM, 1-Jul-2013.) |
Theorem | cdlemk16a 31338* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk16 31339* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) |
Theorem | cdlemk17 31340* | Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k_{1}, f_{1}. (Contributed by NM, 1-Jul-2013.) |
Theorem | cdlemk1u 31341* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk5auN 31342* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk5u 31343* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemk6u 31344* | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 30368. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemkj 31345* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemkuvN 31346* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma_{1} (p) function . (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkuel 31347* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma_{1} (p) function to be a translation. TODO: combine cdlemkj 31345? (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemkuat 31348* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemkuv2 31349* | 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 31350* | 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 31351* | 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 31352* | 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 31353* | 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 31354* | 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 31355* | 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 31356* | 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 31357* | Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk13-2N 31358* | 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 31359* | Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk14-2N 31360* | 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 31361* | 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 31362* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk17-2N 31363* | 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 31364* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkuv-2N 31365* | 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 31366* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma_{2} (p) function to be a translation. TODO: combine cdlemkj 31345? (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkuv2-2 31367* | 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 31368* | 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 31369* | 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.) |