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

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

Theoremcdlemi2 31301 Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.)

Theoremcdlemi 31302 Lemma I of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.)

Theoremcdlemj1 31303 Part of proof of Lemma J of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.)

Theoremcdlemj2 31304 Part of proof of Lemma J of [Crawley] p. 118. Eliminate . (Contributed by NM, 20-Jun-2013.)

Theoremcdlemj3 31305 Part of proof of Lemma J of [Crawley] p. 118. Eliminate . (Contributed by NM, 20-Jun-2013.)

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

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

Theoremtendo0mul 31308* Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013.)

Theoremtendo0mulr 31309* Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014.)

Theoremtendo1ne0 31310* The identity (unity) is not equal to the zero trace-preserving endomorphism. (Contributed by NM, 8-Aug-2013.)

Theoremtendoconid 31311* The composition (product) of trace-preserving endormorphisms is nonzero when each argument is nonzero. (Contributed by NM, 8-Aug-2013.)

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

Theoremcdlemk1 31313 Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.)

Theoremcdlemk2 31314 Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.)

Theoremcdlemk3 31315 Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.)

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

Theoremcdlemk5a 31317 Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.)

Theoremcdlemk5 31318 Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 25-Jun-2013.)

Theoremcdlemk6 31319 Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 30368. (Contributed by NM, 25-Jun-2013.)

Theoremcdlemk8 31320 Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 26-Jun-2013.)

Theoremcdlemk9 31321 Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.)

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

Theoremcdlemki 31323* Part of proof of Lemma K of [Crawley] p. 118. TODO: Eliminate and put into cdlemksel 31327. (Contributed by NM, 25-Jun-2013.)

Theoremcdlemkvcl 31324 Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.)

Theoremcdlemk10 31325 Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.)

Theoremcdlemksv 31326* Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma(p) function. (Contributed by NM, 26-Jun-2013.)

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

Theoremcdlemksat 31328* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.)

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

Theoremcdlemk7 31330* Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119. (Contributed by NM, 27-Jun-2013.)

Theoremcdlemk11 31331* Part of proof of Lemma K of [Crawley] p. 118. Eq. 3, line 8, p. 119. (Contributed by NM, 29-Jun-2013.)

Theoremcdlemk12 31332* Part of proof of Lemma K of [Crawley] p. 118. Eq. 4, line 10, p. 119. (Contributed by NM, 30-Jun-2013.)

Theoremcdlemkoatnle 31333* Utility lemma. (Contributed by NM, 2-Jul-2013.)

Theoremcdlemk13 31334* Part of proof of Lemma K of [Crawley] p. 118. Line 13 on p. 119. , are k1, f1. (Contributed by NM, 1-Jul-2013.)

Theoremcdlemkole 31335* Utility lemma. (Contributed by NM, 2-Jul-2013.)

Theoremcdlemk14 31336* Part of proof of Lemma K of [Crawley] p. 118. Line 19 on p. 119. , are k1, f1. (Contributed by NM, 1-Jul-2013.)

Theoremcdlemk15 31337* Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k1, f1. (Contributed by NM, 1-Jul-2013.)

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

Theoremcdlemk16 31339* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.)

Theoremcdlemk17 31340* Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. , are k1, f1. (Contributed by NM, 1-Jul-2013.)

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

Theoremcdlemk5auN 31342* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk5u 31343* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.)

Theoremcdlemk6u 31344* Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 30368. (Contributed by NM, 4-Jul-2013.)

Theoremcdlemkj 31345* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.)

TheoremcdlemkuvN 31346* 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.)

Theoremcdlemkuel 31347* Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma1 (p) function to be a translation. TODO: combine cdlemkj 31345? (Contributed by NM, 2-Jul-2013.)

Theoremcdlemkuat 31348* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.)

Theoremcdlemkuv2 31349* 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 31350* 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 31351* 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 31352* 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 31353* 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 31354* 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 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.)

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

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

Theoremcdlemk13-2N 31358* 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 31359* Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk14-2N 31360* 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 31361* 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 31362* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.)

Theoremcdlemk17-2N 31363* 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 31364* Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)

Theoremcdlemkuv-2N 31365* 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 31366* Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma2 (p) function to be a translation. TODO: combine cdlemkj 31345? (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.)

Theoremcdlemkuv2-2 31367* 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 31368* 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 31369* 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.)