Home | Metamath
Proof Explorer Theorem List (p. 298 of 309) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21328) |
Hilbert Space Explorer
(21329-22851) |
Users' Mathboxes
(22852-30843) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemj3 29701 | Part of proof of Lemma J of [Crawley] p. 118. Eliminate . (Contributed by NM, 20-Jun-2013.) |
Theorem | tendocan 29702 | 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 29703* | 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 29704* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013.) |
Theorem | tendo0mulr 29705* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014.) |
Theorem | tendo1ne0 29706* | The identity (unity) is not equal to the zero trace-preserving endomorphism. (Contributed by NM, 8-Aug-2013.) |
Theorem | tendoconid 29707* | The composition (product) of trace-preserving endormorphisms is nonzero when each argument is nonzero. (Contributed by NM, 8-Aug-2013.) |
Theorem | tendotr 29708* | 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 29709 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
Theorem | cdlemk2 29710 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
Theorem | cdlemk3 29711 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk4 29712 | 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 29713 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk5 29714 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 25-Jun-2013.) |
Theorem | cdlemk6 29715 | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 28764. (Contributed by NM, 25-Jun-2013.) |
Theorem | cdlemk8 29716 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 26-Jun-2013.) |
Theorem | cdlemk9 29717 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.) |
Theorem | cdlemk9bN 29718 | Part of proof of Lemma K of [Crawley] p. 118. TODO: is this needed? If so, shorten with cdlemk9 29717 if that one is also needed. (Contributed by NM, 28-Jun-2013.) (New usage is discouraged.) |
Theorem | cdlemki 29719* | Part of proof of Lemma K of [Crawley] p. 118. TODO: Eliminate and put into cdlemksel 29723. (Contributed by NM, 25-Jun-2013.) |
Theorem | cdlemkvcl 29720 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.) |
Theorem | cdlemk10 29721 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.) |
Theorem | cdlemksv 29722* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma(p) function. (Contributed by NM, 26-Jun-2013.) |
Theorem | cdlemksel 29723* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma(p) function to be a translation. TODO: combine cdlemki 29719? (Contributed by NM, 26-Jun-2013.) |
Theorem | cdlemksat 29724* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.) |
Theorem | cdlemksv2 29725* | 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 29726* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119. (Contributed by NM, 27-Jun-2013.) |
Theorem | cdlemk11 29727* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 3, line 8, p. 119. (Contributed by NM, 29-Jun-2013.) |
Theorem | cdlemk12 29728* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 4, line 10, p. 119. (Contributed by NM, 30-Jun-2013.) |
Theorem | cdlemkoatnle 29729* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemk13 29730* | 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 29731* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemk14 29732* | 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 29733* | 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 29734* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk16 29735* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) |
Theorem | cdlemk17 29736* | 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 29737* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk5auN 29738* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk5u 29739* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemk6u 29740* | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 28764. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemkj 29741* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemkuvN 29742* | 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 29743* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma_{1} (p) function to be a translation. TODO: combine cdlemkj 29741? (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemkuat 29744* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemkuv2 29745* | 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 29746* | 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 29747* | 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 29748* | 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 29749* | 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 29750* | 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 29751* | 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 29752* | 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 29753* | Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk13-2N 29754* | 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 29755* | Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk14-2N 29756* | 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 29757* | 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 29758* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk17-2N 29759* | 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 29760* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkuv-2N 29761* | 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 29762* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma_{2} (p) function to be a translation. TODO: combine cdlemkj 29741? (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemkuv2-2 29763* | 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 29764* | 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 29765* | 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 29766* | 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 29767* | 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.) |