Home | Metamath
Proof Explorer Theorem List (p. 310 of 321) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-22283) |
Hilbert Space Explorer
(22284-23806) |
Users' Mathboxes
(23807-32095) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tendo1mulr 30901 | Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013.) |
Theorem | tendococl 30902 | The composition of two trace-preserving endomorphisms (multiplication in the endormorphism ring) is a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
Theorem | tendoid 30903 | The identity value of a trace-preserving endomorphism. (Contributed by NM, 21-Jun-2013.) |
Theorem | tendoeq2 30904* | Condition determining equality of two trace-preserving endomorphisms, showing it is unnecessary to consider the identity translation. In tendocan 30954, we show that we only need to consider a single non-identity translation. (Contributed by NM, 21-Jun-2013.) |
Theorem | tendoplcbv 30905* | Define sum operation for trace-perserving endomorphisms. Change bound variables to isolate them later. (Contributed by NM, 11-Jun-2013.) |
Theorem | tendopl 30906* | Value of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
Theorem | tendopl2 30907* | Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
Theorem | tendoplcl2 30908* | Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
Theorem | tendoplco2 30909* | Value of result of endomorphism sum operation on a translation composition. (Contributed by NM, 10-Jun-2013.) |
Theorem | tendopltp 30910* | Trace-preserving property of endomorphism sum operation , based on theorem trlco 30857. Part of remark in [Crawley] p. 118, 2nd line, "it is clear from the second part of G (our trlco 30857) that Delta is a subring of E." (In our development, we will bypass their E and go directly to their Delta, whose base set is our .) (Contributed by NM, 9-Jun-2013.) |
Theorem | tendoplcl 30911* | Endomorphism sum is a trace-preserving endomorphism. (Contributed by NM, 10-Jun-2013.) |
Theorem | tendoplcom 30912* | The endomorphism sum operation is commutative. (Contributed by NM, 11-Jun-2013.) |
Theorem | tendoplass 30913* | The endomorphism sum operation is associative. (Contributed by NM, 11-Jun-2013.) |
Theorem | tendodi1 30914* | Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.) |
Theorem | tendodi2 30915* | Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.) |
Theorem | tendo0cbv 30916* | Define additive identity for trace-perserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 11-Jun-2013.) |
Theorem | tendo02 30917* | Value of additive identity endomorphism. (Contributed by NM, 11-Jun-2013.) |
Theorem | tendo0co2 30918* | The additive identity trace-perserving endormorphism preserves composition of translations. TODO: why isn't this a special case of tendospdi1 31151? (Contributed by NM, 11-Jun-2013.) |
Theorem | tendo0tp 30919* | Trace-preserving property of endomorphism additive identity. (Contributed by NM, 11-Jun-2013.) |
Theorem | tendo0cl 30920* | The additive identity is a trace-perserving endormorphism. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendo0pl 30921* | Property of the additive identity endormorphism. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendo0plr 30922* | Property of the additive identity endormorphism. (Contributed by NM, 21-Feb-2014.) |
Theorem | tendoicbv 30923* | Define inverse function for trace-perserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendoi 30924* | Value of inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendoi2 30925* | Value of additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendoicl 30926* | Closure of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendoipl 30927* | Property of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendoipl2 30928* | Property of the additive inverse endomorphism. (Contributed by NM, 29-Sep-2014.) |
Theorem | erngfset 30929* | The division rings on trace-preserving endomorphisms for a lattice . (Contributed by NM, 8-Jun-2013.) |
Theorem | erngset 30930* | The division ring on trace-preserving endomorphisms for a fiducial co-atom . (Contributed by NM, 5-Jun-2013.) |
Theorem | erngbase 30931 | The base set of the division ring on trace-preserving endomorphisms is the set of all trace-preserving endomorphisms (for a fiducial co-atom ). TODO: the .t hypothesis isn't used. (Also look at others.) (Contributed by NM, 9-Jun-2013.) |
Theorem | erngfplus 30932* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) |
Theorem | erngplus 30933* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
Theorem | erngplus2 30934 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
Theorem | erngfmul 30935* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) |
Theorem | erngmul 30936 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
Theorem | erngfset-rN 30937* | The division rings on trace-preserving endomorphisms for a lattice . (Contributed by NM, 8-Jun-2013.) (New usage is discouraged.) |
Theorem | erngset-rN 30938* | The division ring on trace-preserving endomorphisms for a fiducial co-atom . (Contributed by NM, 5-Jun-2013.) (New usage is discouraged.) |
Theorem | erngbase-rN 30939 | The base set of the division ring on trace-preserving endomorphisms is the set of all trace-preserving endomorphisms (for a fiducial co-atom ). (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
Theorem | erngfplus-rN 30940* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
Theorem | erngplus-rN 30941* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
Theorem | erngplus2-rN 30942 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
Theorem | erngfmul-rN 30943* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
Theorem | erngmul-rN 30944 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
Theorem | cdlemh1 30945 | Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.) |
Theorem | cdlemh2 30946 | Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 16-Jun-2013.) |
Theorem | cdlemh 30947 | Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.) |
Theorem | cdlemi1 30948 | Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.) |
Theorem | cdlemi2 30949 | Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.) |
Theorem | cdlemi 30950 | Lemma I of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.) |
Theorem | cdlemj1 30951 | Part of proof of Lemma J of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.) |
Theorem | cdlemj2 30952 | Part of proof of Lemma J of [Crawley] p. 118. Eliminate . (Contributed by NM, 20-Jun-2013.) |
Theorem | cdlemj3 30953 | Part of proof of Lemma J of [Crawley] p. 118. Eliminate . (Contributed by NM, 20-Jun-2013.) |
Theorem | tendocan 30954 | 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 30955* | 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 30956* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013.) |
Theorem | tendo0mulr 30957* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014.) |
Theorem | tendo1ne0 30958* | The identity (unity) is not equal to the zero trace-preserving endomorphism. (Contributed by NM, 8-Aug-2013.) |
Theorem | tendoconid 30959* | The composition (product) of trace-preserving endormorphisms is nonzero when each argument is nonzero. (Contributed by NM, 8-Aug-2013.) |
Theorem | tendotr 30960* | 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 30961 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
Theorem | cdlemk2 30962 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
Theorem | cdlemk3 30963 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk4 30964 | 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 30965 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk5 30966 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 25-Jun-2013.) |
Theorem | cdlemk6 30967 | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 30016. (Contributed by NM, 25-Jun-2013.) |
Theorem | cdlemk8 30968 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 26-Jun-2013.) |
Theorem | cdlemk9 30969 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.) |
Theorem | cdlemk9bN 30970 | Part of proof of Lemma K of [Crawley] p. 118. TODO: is this needed? If so, shorten with cdlemk9 30969 if that one is also needed. (Contributed by NM, 28-Jun-2013.) (New usage is discouraged.) |
Theorem | cdlemki 30971* | Part of proof of Lemma K of [Crawley] p. 118. TODO: Eliminate and put into cdlemksel 30975. (Contributed by NM, 25-Jun-2013.) |
Theorem | cdlemkvcl 30972 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.) |
Theorem | cdlemk10 30973 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.) |
Theorem | cdlemksv 30974* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma(p) function. (Contributed by NM, 26-Jun-2013.) |
Theorem | cdlemksel 30975* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma(p) function to be a translation. TODO: combine cdlemki 30971? (Contributed by NM, 26-Jun-2013.) |
Theorem | cdlemksat 30976* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.) |
Theorem | cdlemksv2 30977* | 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 30978* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119. (Contributed by NM, 27-Jun-2013.) |
Theorem | cdlemk11 30979* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 3, line 8, p. 119. (Contributed by NM, 29-Jun-2013.) |
Theorem | cdlemk12 30980* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 4, line 10, p. 119. (Contributed by NM, 30-Jun-2013.) |
Theorem | cdlemkoatnle 30981* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemk13 30982* | 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 30983* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemk14 30984* | 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 30985* | 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 30986* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk16 30987* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) |
Theorem | cdlemk17 30988* | 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 30989* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
Theorem | cdlemk5auN 30990* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) (New usage is discouraged.) |
Theorem | cdlemk5u 30991* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemk6u 30992* | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 30016. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemkj 30993* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemkuvN 30994* | 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 30995* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma_{1} (p) function to be a translation. TODO: combine cdlemkj 30993? (Contributed by NM, 2-Jul-2013.) |
Theorem | cdlemkuat 30996* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
Theorem | cdlemkuv2 30997* | 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 30998* | 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 30999* | 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 31000* | 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.) |