Home | Metamath
Proof Explorer Theorem List (p. 361 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 | cdlemg35 36001* | TODO: Fix comment. TODO: should we have a more general version of hlsupr 34672 to avoid the conditions? (Contributed by NM, 31-May-2013.) |
Theorem | cdlemg36 36002* | Use cdlemg35 to eliminate from cdlemg34 36000. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
Theorem | cdlemg38 36003 | Use cdlemg37 35977 to eliminate from cdlemg36 36002. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
Theorem | cdlemg39 36004 | Eliminate conditions from cdlemg38 36003. TODO: Would this better be done at cdlemg35 36001? TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
Theorem | cdlemg40 36005 | Eliminate conditions from cdlemg39 36004. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
Theorem | cdlemg41 36006 | Convert cdlemg40 36005 to function composition. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
Theorem | ltrnco 36007 | The composition of two translations is a translation. Part of proof of Lemma G of [Crawley] p. 116, line 15 on p. 117. (Contributed by NM, 31-May-2013.) |
Theorem | trlcocnv 36008 | Swap the arguments of the trace of a composition with converse. (Contributed by NM, 1-Jul-2013.) |
Theorem | trlcoabs 36009 | Absorption into a composition by joining with trace. (Contributed by NM, 22-Jul-2013.) |
Theorem | trlcoabs2N 36010 | Absorption of the trace of a composition. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
Theorem | trlcoat 36011 | The trace of a composition of two translations is an atom if their traces are different. (Contributed by NM, 15-Jun-2013.) |
Theorem | trlcocnvat 36012 | Commonly used special case of trlcoat 36011. (Contributed by NM, 1-Jul-2013.) |
Theorem | trlconid 36013 | The composition of two different translations is not the identity translation. (Contributed by NM, 22-Jul-2013.) |
Theorem | trlcolem 36014 | Lemma for trlco 36015. (Contributed by NM, 1-Jun-2013.) |
Theorem | trlco 36015 | The trace of a composition of translations is less than or equal to the join of their traces. Part of proof of Lemma G of [Crawley] p. 116, second paragraph on p. 117. (Contributed by NM, 2-Jun-2013.) |
Theorem | trlcone 36016 | If two translations have different traces, the trace of their composition is also different. (Contributed by NM, 14-Jun-2013.) |
Theorem | cdlemg42 36017 | Part of proof of Lemma G of [Crawley] p. 116, first line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013.) |
Theorem | cdlemg43 36018 | Part of proof of Lemma G of [Crawley] p. 116, third line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013.) |
Theorem | cdlemg44a 36019 | Part of proof of Lemma G of [Crawley] p. 116, fourth line of third paragraph on p. 117: "so fg(p) = gf(p)." (Contributed by NM, 3-Jun-2013.) |
Theorem | cdlemg44b 36020 | Eliminate , from cdlemg44a 36019. (Contributed by NM, 3-Jun-2013.) |
Theorem | cdlemg44 36021 | Part of proof of Lemma G of [Crawley] p. 116, fifth line of third paragraph on p. 117: "and hence fg = gf." (Contributed by NM, 3-Jun-2013.) |
Theorem | cdlemg47a 36022 | TODO: fix comment. TODO: Use this above in place of antecedents? (Contributed by NM, 5-Jun-2013.) |
Theorem | cdlemg46 36023* | Part of proof of Lemma G of [Crawley] p. 116, seventh line of third paragraph on p. 117: "hf and f have different traces." (Contributed by NM, 5-Jun-2013.) |
Theorem | cdlemg47 36024* | Part of proof of Lemma G of [Crawley] p. 116, ninth line of third paragraph on p. 117: "we conclude that gf = fg." (Contributed by NM, 5-Jun-2013.) |
Theorem | cdlemg48 36025 | Elmininate from cdlemg47 36024. (Contributed by NM, 5-Jun-2013.) |
Theorem | ltrncom 36026 | Composition is commutative for translations. Part of proof of Lemma G of [Crawley] p. 116. (Contributed by NM, 5-Jun-2013.) |
Theorem | ltrnco4 36027 | Rearrange a composition of 4 translations, analogous to an4 865. (Contributed by NM, 10-Jun-2013.) |
Theorem | trljco 36028 | Trace joined with trace of composition. (Contributed by NM, 15-Jun-2013.) |
Theorem | trljco2 36029 | Trace joined with trace of composition. (Contributed by NM, 16-Jun-2013.) |
Syntax | ctgrp 36030 | Extend class notation with translation group. |
Definition | df-tgrp 36031* | Define the class of all translation groups. is normally a member of . Each base set is the set of all lattice translations with respect to a hyperplane , and the operation is function composition. Similar to definition of G in [Crawley] p. 116, third paragraph (which defines this for geomodular lattices). (Contributed by NM, 5-Jun-2013.) |
Theorem | tgrpfset 36032* | The translation group maps for a lattice . (Contributed by NM, 5-Jun-2013.) |
Theorem | tgrpset 36033* | The translation group for a fiducial co-atom . (Contributed by NM, 5-Jun-2013.) |
Theorem | tgrpbase 36034 | The base set of the translation group is the set of all translations (for a fiducial co-atom ). (Contributed by NM, 5-Jun-2013.) |
Theorem | tgrpopr 36035* | The group operation of the translation group is function composition. (Contributed by NM, 5-Jun-2013.) |
Theorem | tgrpov 36036 | The group operation value of the translation group is the composition of translations. (Contributed by NM, 5-Jun-2013.) |
Theorem | tgrpgrplem 36037 | Lemma for tgrpgrp 36038. (Contributed by NM, 6-Jun-2013.) |
Theorem | tgrpgrp 36038 | The translation group is a group. (Contributed by NM, 6-Jun-2013.) |
Theorem | tgrpabl 36039 | The translation group is an Abelian group. Lemma G of [Crawley] p. 116. (Contributed by NM, 6-Jun-2013.) |
Syntax | ctendo 36040 | Extend class notation with translation group endomorphisms. |
Syntax | cedring 36041 | Extend class notation with division ring on trace-preserving endomorphisms. |
Syntax | cedring-rN 36042 | Extend class notation with division ring on trace-preserving endomorphisms, with multiplication reversed. TODO: remove theorems if not used. |
Definition | df-tendo 36043* | Define trace-preserving endomorphisms on the set of translations. (Contributed by NM, 8-Jun-2013.) |
Definition | df-edring-rN 36044* | Define division ring on trace-preserving endomorphisms. Definition of E of [Crawley] p. 117, 4th line from bottom. (Contributed by NM, 8-Jun-2013.) |
Definition | df-edring 36045* | Define division ring on trace-preserving endomorphisms. The multiplication operation is reversed composition, per the definition of E of [Crawley] p. 117, 4th line from bottom. (Contributed by NM, 8-Jun-2013.) |
Theorem | tendofset 36046* | The set of all trace-preserving endomorphisms on the set of translations for a lattice . (Contributed by NM, 8-Jun-2013.) |
Theorem | tendoset 36047* | The set of trace-preserving endomorphisms on the set of translations for a fiducial co-atom . (Contributed by NM, 8-Jun-2013.) |
Theorem | istendo 36048* | The predicate "is a trace-preserving endomorphism". Similar to definition of trace-preserving endomorphism in [Crawley] p. 117, penultimate line. (Contributed by NM, 8-Jun-2013.) |
Theorem | tendotp 36049 | Trace-preserving property of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
Theorem | istendod 36050* | Deduce the predicate "is a trace-preserving endomorphism". (Contributed by NM, 9-Jun-2013.) |
Theorem | tendof 36051 | Functionality of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
Theorem | tendoeq1 36052* | Condition determining equality of two trace-preserving endomorphisms. (Contributed by NM, 11-Jun-2013.) |
Theorem | tendovalco 36053 | Value of composition of translations in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
Theorem | tendocoval 36054 | Value of composition of endomorphisms in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
Theorem | tendocl 36055 | Closure of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
Theorem | tendoco2 36056 | Distribution of compositions in preparation for endomorphism sum definition. (Contributed by NM, 10-Jun-2013.) |
Theorem | tendoidcl 36057 | The identity is a trace-preserving endomorphism. (Contributed by NM, 30-Jul-2013.) |
Theorem | tendo1mul 36058 | Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013.) |
Theorem | tendo1mulr 36059 | Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013.) |
Theorem | tendococl 36060 | 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 36061 | The identity value of a trace-preserving endomorphism. (Contributed by NM, 21-Jun-2013.) |
Theorem | tendoeq2 36062* | Condition determining equality of two trace-preserving endomorphisms, showing it is unnecessary to consider the identity translation. In tendocan 36112, we show that we only need to consider a single non-identity translation. (Contributed by NM, 21-Jun-2013.) |
Theorem | tendoplcbv 36063* | Define sum operation for trace-perserving endomorphisms. Change bound variables to isolate them later. (Contributed by NM, 11-Jun-2013.) |
Theorem | tendopl 36064* | Value of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
Theorem | tendopl2 36065* | Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
Theorem | tendoplcl2 36066* | Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
Theorem | tendoplco2 36067* | Value of result of endomorphism sum operation on a translation composition. (Contributed by NM, 10-Jun-2013.) |
Theorem | tendopltp 36068* | Trace-preserving property of endomorphism sum operation , based on theorem trlco 36015. Part of remark in [Crawley] p. 118, 2nd line, "it is clear from the second part of G (our trlco 36015) 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 36069* | Endomorphism sum is a trace-preserving endomorphism. (Contributed by NM, 10-Jun-2013.) |
Theorem | tendoplcom 36070* | The endomorphism sum operation is commutative. (Contributed by NM, 11-Jun-2013.) |
Theorem | tendoplass 36071* | The endomorphism sum operation is associative. (Contributed by NM, 11-Jun-2013.) |
Theorem | tendodi1 36072* | Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.) |
Theorem | tendodi2 36073* | Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.) |
Theorem | tendo0cbv 36074* | Define additive identity for trace-perserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 11-Jun-2013.) |
Theorem | tendo02 36075* | Value of additive identity endomorphism. (Contributed by NM, 11-Jun-2013.) |
Theorem | tendo0co2 36076* | The additive identity trace-perserving endormorphism preserves composition of translations. TODO: why isn't this a special case of tendospdi1 36309? (Contributed by NM, 11-Jun-2013.) |
Theorem | tendo0tp 36077* | Trace-preserving property of endomorphism additive identity. (Contributed by NM, 11-Jun-2013.) |
Theorem | tendo0cl 36078* | The additive identity is a trace-perserving endormorphism. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendo0pl 36079* | Property of the additive identity endormorphism. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendo0plr 36080* | Property of the additive identity endormorphism. (Contributed by NM, 21-Feb-2014.) |
Theorem | tendoicbv 36081* | Define inverse function for trace-perserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendoi 36082* | Value of inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendoi2 36083* | Value of additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendoicl 36084* | Closure of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendoipl 36085* | Property of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
Theorem | tendoipl2 36086* | Property of the additive inverse endomorphism. (Contributed by NM, 29-Sep-2014.) |
Theorem | erngfset 36087* | The division rings on trace-preserving endomorphisms for a lattice . (Contributed by NM, 8-Jun-2013.) |
Theorem | erngset 36088* | The division ring on trace-preserving endomorphisms for a fiducial co-atom . (Contributed by NM, 5-Jun-2013.) |
Theorem | erngbase 36089 | 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 36090* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) |
Theorem | erngplus 36091* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
Theorem | erngplus2 36092 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
Theorem | erngfmul 36093* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) |
Theorem | erngmul 36094 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
Theorem | erngfset-rN 36095* | The division rings on trace-preserving endomorphisms for a lattice . (Contributed by NM, 8-Jun-2013.) (New usage is discouraged.) |
Theorem | erngset-rN 36096* | 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 36097 | 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 36098* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
Theorem | erngplus-rN 36099* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
Theorem | erngplus2-rN 36100 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |