![]() |
Metamath
Proof Explorer Theorem List (p. 400 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | trlcolem 39901 | Lemma for trlco 39902. (Contributed by NM, 1-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β(πΉ β πΊ)) β€ ((π βπΉ) β¨ (π βπΊ))) | ||
Theorem | trlco 39902 | 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.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (π β(πΉ β πΊ)) β€ ((π βπΉ) β¨ (π βπΊ))) | ||
Theorem | trlcone 39903 | If two translations have different traces, the trace of their composition is also different. (Contributed by NM, 14-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ ((π βπΉ) β (π βπΊ) β§ πΊ β ( I βΎ π΅))) β (π βπΉ) β (π β(πΉ β πΊ))) | ||
Theorem | cdlemg42 39904 | Part of proof of Lemma G of [Crawley] p. 116, first line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (πΊβπ) β π β§ (π βπΉ) β (π βπΊ))) β Β¬ (πΊβπ) β€ (π β¨ (πΉβπ))) | ||
Theorem | cdlemg43 39905 | Part of proof of Lemma G of [Crawley] p. 116, third line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (πΊβπ) β π β§ (π βπΉ) β (π βπΊ))) β (πΉβ(πΊβπ)) = (((πΊβπ) β¨ (π βπΉ)) β§ ((πΉβπ) β¨ (π βπΊ)))) | ||
Theorem | cdlemg44a 39906 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) β π β§ (πΊβπ) β π β§ (π βπΉ) β (π βπΊ))) β (πΉβ(πΊβπ)) = (πΊβ(πΉβπ))) | ||
Theorem | cdlemg44b 39907 | Eliminate (πΉβπ) β π, (πΊβπ) β π from cdlemg44a 39906. (Contributed by NM, 3-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π βπΉ) β (π βπΊ)) β (πΉβ(πΊβπ)) = (πΊβ(πΉβπ))) | ||
Theorem | cdlemg44 39908 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π βπΉ) β (π βπΊ)) β (πΉ β πΊ) = (πΊ β πΉ)) | ||
Theorem | cdlemg47a 39909 | TODO: fix comment. TODO: Use this above in place of (πΉβπ) = π antecedents? (Contributed by NM, 5-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ πΉ = ( I βΎ π΅)) β (πΉ β πΊ) = (πΊ β πΉ)) | ||
Theorem | cdlemg46 39910* | 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.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π ββ) β (π βπΉ))) β (π β(β β πΉ)) β (π βπΉ)) | ||
Theorem | cdlemg47 39911* | 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.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (β β π β§ (π βπΉ) = (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π ββ) β (π βπΉ))) β (πΉ β πΊ) = (πΊ β πΉ)) | ||
Theorem | cdlemg48 39912 | Eliminate β from cdlemg47 39911. (Contributed by NM, 5-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (πΉ β ( I βΎ π΅) β§ (π βπΉ) = (π βπΊ))) β (πΉ β πΊ) = (πΊ β πΉ)) | ||
Theorem | ltrncom 39913 | Composition is commutative for translations. Part of proof of Lemma G of [Crawley] p. 116. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (πΉ β πΊ) = (πΊ β πΉ)) | ||
Theorem | ltrnco4 39914 | Rearrange a composition of 4 translations, analogous to an4 653. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΈ β π β§ πΉ β π) β ((π· β πΈ) β (πΉ β πΊ)) = ((π· β πΉ) β (πΈ β πΊ))) | ||
Theorem | trljco 39915 | Trace joined with trace of composition. (Contributed by NM, 15-Jun-2013.) |
β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β ((π βπΉ) β¨ (π β(πΉ β πΊ))) = ((π βπΉ) β¨ (π βπΊ))) | ||
Theorem | trljco2 39916 | Trace joined with trace of composition. (Contributed by NM, 16-Jun-2013.) |
β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β ((π βπΉ) β¨ (π β(πΉ β πΊ))) = ((π βπΊ) β¨ (π β(πΉ β πΊ)))) | ||
Syntax | ctgrp 39917 | Extend class notation with translation group. |
class TGrp | ||
Definition | df-tgrp 39918* | Define the class of all translation groups. π is normally a member of HL. 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.) |
β’ TGrp = (π β V β¦ (π€ β (LHypβπ) β¦ {β¨(Baseβndx), ((LTrnβπ)βπ€)β©, β¨(+gβndx), (π β ((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©})) | ||
Theorem | tgrpfset 39919* | The translation group maps for a lattice πΎ. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (TGrpβπΎ) = (π€ β π» β¦ {β¨(Baseβndx), ((LTrnβπΎ)βπ€)β©, β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©})) | ||
Theorem | tgrpset 39920* | The translation group for a fiducial co-atom π. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΊ = ((TGrpβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΊ = {β¨(Baseβndx), πβ©, β¨(+gβndx), (π β π, π β π β¦ (π β π))β©}) | ||
Theorem | tgrpbase 39921 | The base set of the translation group is the set of all translations (for a fiducial co-atom π). (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΊ = ((TGrpβπΎ)βπ) & β’ πΆ = (BaseβπΊ) β β’ ((πΎ β π β§ π β π») β πΆ = π) | ||
Theorem | tgrpopr 39922* | The group operation of the translation group is function composition. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΊ = ((TGrpβπΎ)βπ) & β’ + = (+gβπΊ) β β’ ((πΎ β π β§ π β π») β + = (π β π, π β π β¦ (π β π))) | ||
Theorem | tgrpov 39923 | The group operation value of the translation group is the composition of translations. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΊ = ((TGrpβπΎ)βπ) & β’ + = (+gβπΊ) β β’ ((πΎ β π β§ π β π» β§ (π β π β§ π β π)) β (π + π) = (π β π)) | ||
Theorem | tgrpgrplem 39924 | Lemma for tgrpgrp 39925. (Contributed by NM, 6-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΊ = ((TGrpβπΎ)βπ) & β’ + = (+gβπΊ) & β’ π΅ = (BaseβπΎ) β β’ ((πΎ β HL β§ π β π») β πΊ β Grp) | ||
Theorem | tgrpgrp 39925 | The translation group is a group. (Contributed by NM, 6-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ πΊ = ((TGrpβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β πΊ β Grp) | ||
Theorem | tgrpabl 39926 | The translation group is an Abelian group. Lemma G of [Crawley] p. 116. (Contributed by NM, 6-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ πΊ = ((TGrpβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β πΊ β Abel) | ||
Syntax | ctendo 39927 | Extend class notation with translation group endomorphisms. |
class TEndo | ||
Syntax | cedring 39928 | Extend class notation with division ring on trace-preserving endomorphisms. |
class EDRing | ||
Syntax | cedring-rN 39929 | Extend class notation with division ring on trace-preserving endomorphisms, with multiplication reversed. TODO: remove EDRingR theorems if not used. |
class EDRingR | ||
Definition | df-tendo 39930* | Define trace-preserving endomorphisms on the set of translations. (Contributed by NM, 8-Jun-2013.) |
β’ TEndo = (π β V β¦ (π€ β (LHypβπ) β¦ {π β£ (π:((LTrnβπ)βπ€)βΆ((LTrnβπ)βπ€) β§ βπ₯ β ((LTrnβπ)βπ€)βπ¦ β ((LTrnβπ)βπ€)(πβ(π₯ β π¦)) = ((πβπ₯) β (πβπ¦)) β§ βπ₯ β ((LTrnβπ)βπ€)(((trLβπ)βπ€)β(πβπ₯))(leβπ)(((trLβπ)βπ€)βπ₯))})) | ||
Definition | df-edring-rN 39931* | Define division ring on trace-preserving endomorphisms. Definition of E of [Crawley] p. 117, 4th line from bottom. (Contributed by NM, 8-Jun-2013.) |
β’ EDRingR = (π β V β¦ (π€ β (LHypβπ) β¦ {β¨(Baseβndx), ((TEndoβπ)βπ€)β©, β¨(+gβndx), (π β ((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx), (π β ((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π‘ β π ))β©})) | ||
Definition | df-edring 39932* | 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.) |
β’ EDRing = (π β V β¦ (π€ β (LHypβπ) β¦ {β¨(Baseβndx), ((TEndoβπ)βπ€)β©, β¨(+gβndx), (π β ((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β ((LTrnβπ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx), (π β ((TEndoβπ)βπ€), π‘ β ((TEndoβπ)βπ€) β¦ (π β π‘))β©})) | ||
Theorem | tendofset 39933* | The set of all trace-preserving endomorphisms on the set of translations for a lattice πΎ. (Contributed by NM, 8-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β π β (TEndoβπΎ) = (π€ β π» β¦ {π β£ (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))})) | ||
Theorem | tendoset 39934* | The set of trace-preserving endomorphisms on the set of translations for a fiducial co-atom π. (Contributed by NM, 8-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΈ = {π β£ (π :πβΆπ β§ βπ β π βπ β π (π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β π (π β(π βπ)) β€ (π βπ))}) | ||
Theorem | istendo 39935* | 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.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β (π β πΈ β (π:πβΆπ β§ βπ β π βπ β π (πβ(π β π)) = ((πβπ) β (πβπ)) β§ βπ β π (π β(πβπ)) β€ (π βπ)))) | ||
Theorem | tendotp 39936 | Trace-preserving property of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β πΈ β§ πΉ β π) β (π β(πβπΉ)) β€ (π βπΉ)) | ||
Theorem | istendod 39937* | Deduce the predicate "is a trace-preserving endomorphism". (Contributed by NM, 9-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ (π β (πΎ β π β§ π β π»)) & β’ (π β π:πβΆπ) & β’ ((π β§ π β π β§ π β π) β (πβ(π β π)) = ((πβπ) β (πβπ))) & β’ ((π β§ π β π) β (π β(πβπ)) β€ (π βπ)) β β’ (π β π β πΈ) | ||
Theorem | tendof 39938 | Functionality of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β πΈ) β π:πβΆπ) | ||
Theorem | tendoeq1 39939* | Condition determining equality of two trace-preserving endomorphisms. (Contributed by NM, 11-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ βπ β π (πβπ) = (πβπ)) β π = π) | ||
Theorem | tendovalco 39940 | Value of composition of translations in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π» β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) | ||
Theorem | tendocoval 39941 | Value of composition of endomorphisms in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β ((π β π)βπΉ) = (πβ(πβπΉ))) | ||
Theorem | tendocl 39942 | Closure of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ) β π) | ||
Theorem | tendoco2 39943 | Distribution of compositions in preparation for endomorphism sum definition. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β ((πβ(πΉ β πΊ)) β (πβ(πΉ β πΊ))) = (((πβπΉ) β (πβπΉ)) β ((πβπΊ) β (πβπΊ)))) | ||
Theorem | tendoidcl 39944 | The identity is a trace-preserving endomorphism. (Contributed by NM, 30-Jul-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β πΈ) | ||
Theorem | tendo1mul 39945 | Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (( I βΎ π) β π) = π) | ||
Theorem | tendo1mulr 39946 | Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π β ( I βΎ π)) = π) | ||
Theorem | tendococl 39947 | The composition of two trace-preserving endomorphisms (multiplication in the endormorphism ring) is a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (π β π) β πΈ) | ||
Theorem | tendoid 39948 | The identity value of a trace-preserving endomorphism. (Contributed by NM, 21-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πβ( I βΎ π΅)) = ( I βΎ π΅)) | ||
Theorem | tendoeq2 39949* | Condition determining equality of two trace-preserving endomorphisms, showing it is unnecessary to consider the identity translation. In tendocan 39999, we show that we only need to consider a single non-identity translation. (Contributed by NM, 21-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ βπ β π (π β ( I βΎ π΅) β (πβπ) = (πβπ))) β π = π) | ||
Theorem | tendoplcbv 39950* | Define sum operation for trace-preserving endomorphisms. Change bound variables to isolate them later. (Contributed by NM, 11-Jun-2013.) |
β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ π = (π’ β πΈ, π£ β πΈ β¦ (π β π β¦ ((π’βπ) β (π£βπ)))) | ||
Theorem | tendopl 39951* | Value of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = ((LTrnβπΎ)βπ) β β’ ((π β πΈ β§ π β πΈ) β (πππ) = (π β π β¦ ((πβπ) β (πβπ)))) | ||
Theorem | tendopl2 39952* | Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = ((LTrnβπΎ)βπ) β β’ ((π β πΈ β§ π β πΈ β§ πΉ β π) β ((πππ)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
Theorem | tendoplcl2 39953* | Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β ((πππ)βπΉ) β π) | ||
Theorem | tendoplco2 39954* | Value of result of endomorphism sum operation on a translation composition. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β ((πππ)β(πΉ β πΊ)) = (((πππ)βπΉ) β ((πππ)βπΊ))) | ||
Theorem | tendopltp 39955* | Trace-preserving property of endomorphism sum operation π, based on Theorems trlco 39902. Part of remark in [Crawley] p. 118, 2nd line, "it is clear from the second part of G (our trlco 39902) 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 (TEndoβπΎ)βπ.) (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ β€ = (leβπΎ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β (π β((πππ)βπΉ)) β€ (π βπΉ)) | ||
Theorem | tendoplcl 39956* | Endomorphism sum is a trace-preserving endomorphism. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) β πΈ) | ||
Theorem | tendoplcom 39957* | The endomorphism sum operation is commutative. (Contributed by NM, 11-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) = (πππ)) | ||
Theorem | tendoplass 39958* | The endomorphism sum operation is associative. (Contributed by NM, 11-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β ((πππ)ππ) = (ππ(πππ))) | ||
Theorem | tendodi1 39959* | Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (π β (πππ)) = ((π β π)π(π β π))) | ||
Theorem | tendodi2 39960* | Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β ((πππ) β π) = ((π β π)π(π β π))) | ||
Theorem | tendo0cbv 39961* | Define additive identity for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 11-Jun-2013.) |
β’ π = (π β π β¦ ( I βΎ π΅)) β β’ π = (π β π β¦ ( I βΎ π΅)) | ||
Theorem | tendo02 39962* | Value of additive identity endomorphism. (Contributed by NM, 11-Jun-2013.) |
β’ π = (π β π β¦ ( I βΎ π΅)) & β’ π΅ = (BaseβπΎ) β β’ (πΉ β π β (πβπΉ) = ( I βΎ π΅)) | ||
Theorem | tendo0co2 39963* | The additive identity trace-preserving endormorphism preserves composition of translations. TODO: why isn't this a special case of tendospdi1 40195? (Contributed by NM, 11-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) | ||
Theorem | tendo0tp 39964* | Trace-preserving property of endomorphism additive identity. (Contributed by NM, 11-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ β€ = (leβπΎ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π β(πβπΉ)) β€ (π βπΉ)) | ||
Theorem | tendo0cl 39965* | The additive identity is a trace-preserving endormorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ ((πΎ β HL β§ π β π») β π β πΈ) | ||
Theorem | tendo0pl 39966* | Property of the additive identity endormorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πππ) = π) | ||
Theorem | tendo0plr 39967* | Property of the additive identity endormorphism. (Contributed by NM, 21-Feb-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πππ) = π) | ||
Theorem | tendoicbv 39968* | Define inverse function for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 12-Jun-2013.) |
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) β β’ πΌ = (π’ β πΈ β¦ (π β π β¦ β‘(π’βπ))) | ||
Theorem | tendoi 39969* | Value of inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π = ((LTrnβπΎ)βπ) β β’ (π β πΈ β (πΌβπ) = (π β π β¦ β‘(πβπ))) | ||
Theorem | tendoi2 39970* | Value of additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π = ((LTrnβπΎ)βπ) β β’ ((π β πΈ β§ πΉ β π) β ((πΌβπ)βπΉ) = β‘(πβπΉ)) | ||
Theorem | tendoicl 39971* | Closure of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πΌβπ) β πΈ) | ||
Theorem | tendoipl 39972* | Property of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π΅ = (BaseβπΎ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β ((πΌβπ)ππ) = π) | ||
Theorem | tendoipl2 39973* | Property of the additive inverse endomorphism. (Contributed by NM, 29-Sep-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π΅ = (BaseβπΎ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (ππ(πΌβπ)) = π) | ||
Theorem | erngfset 39974* | The division rings on trace-preserving endomorphisms for a lattice πΎ. (Contributed by NM, 8-Jun-2013.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (EDRingβπΎ) = (π€ β π» β¦ {β¨(Baseβndx), ((TEndoβπΎ)βπ€)β©, β¨(+gβndx), (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx), (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©})) | ||
Theorem | erngset 39975* | The division ring on trace-preserving endomorphisms for a fiducial co-atom π. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β π· = {β¨(Baseβndx), πΈβ©, β¨(+gβndx), (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx), (π β πΈ, π‘ β πΈ β¦ (π β π‘))β©}) | ||
Theorem | erngbase 39976 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ πΆ = (Baseβπ·) β β’ ((πΎ β π β§ π β π») β πΆ = πΈ) | ||
Theorem | erngfplus 39977* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ + = (+gβπ·) β β’ ((πΎ β π β§ π β π») β + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) | ||
Theorem | erngplus 39978* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π + π) = (π β π β¦ ((πβπ) β (πβπ)))) | ||
Theorem | erngplus2 39979 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΉ β π)) β ((π + π)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
Theorem | erngfmul 39980* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π‘ β πΈ β¦ (π β π‘))) | ||
Theorem | erngmul 39981 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π Β· π) = (π β π)) | ||
Theorem | erngfset-rN 39982* | The division rings on trace-preserving endomorphisms for a lattice πΎ. (Contributed by NM, 8-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (EDRingRβπΎ) = (π€ β π» β¦ {β¨(Baseβndx), ((TEndoβπΎ)βπ€)β©, β¨(+gβndx), (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx), (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π‘ β π ))β©})) | ||
Theorem | erngset-rN 39983* | The division ring on trace-preserving endomorphisms for a fiducial co-atom π. (Contributed by NM, 5-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β π· = {β¨(Baseβndx), πΈβ©, β¨(+gβndx), (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx), (π β πΈ, π‘ β πΈ β¦ (π‘ β π ))β©}) | ||
Theorem | erngbase-rN 39984 | 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.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ πΆ = (Baseβπ·) β β’ ((πΎ β π β§ π β π») β πΆ = πΈ) | ||
Theorem | erngfplus-rN 39985* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ + = (+gβπ·) β β’ ((πΎ β π β§ π β π») β + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) | ||
Theorem | erngplus-rN 39986* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π + π) = (π β π β¦ ((πβπ) β (πβπ)))) | ||
Theorem | erngplus2-rN 39987 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΉ β π)) β ((π + π)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
Theorem | erngfmul-rN 39988* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π‘ β πΈ β¦ (π‘ β π ))) | ||
Theorem | erngmul-rN 39989 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π Β· π) = (π β π)) | ||
Theorem | cdlemh1 39990 | Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘πΉ)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ π β π΄) β§ (π β€ (π β¨ (π βπΉ)) β§ (π βπΉ) β (π βπΊ))) β (π β¨ (π β(πΊ β β‘πΉ))) = (π β¨ (π β(πΊ β β‘πΉ)))) | ||
Theorem | cdlemh2 39991 | Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 16-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘πΉ)))) & β’ 0 = (0.βπΎ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΉ) β (π βπΊ))) β (π β§ π) = 0 ) | ||
Theorem | cdlemh 39992 | Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘πΉ)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ (π βπΉ))) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΉ) β (π βπΊ))) β (π β π΄ β§ Β¬ π β€ π)) | ||
Theorem | cdlemi1 39993 | Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπΊ)βπ) β€ (π β¨ (π βπΊ))) | ||
Theorem | cdlemi2 39994 | Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπΊ)βπ) β€ (((πβπΉ)βπ) β¨ (π β(πΊ β β‘πΉ)))) | ||
Theorem | cdlemi 39995 | Lemma I of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((π β¨ (π βπΊ)) β§ (((πβπΉ)βπ) β¨ (π β(πΊ β β‘πΉ)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΉ) β (π βπΊ))) β ((πβπΊ)βπ) = π) | ||
Theorem | cdlemj1 39996 | Part of proof of Lemma J of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ (β β ( I βΎ π΅) β§ π β π β§ π β ( I βΎ π΅)) β§ ((π βπΉ) β (π βπ) β§ (π βπ) β (π ββ) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πββ)βπ) = ((πββ)βπ)) | ||
Theorem | cdlemj2 39997 | Part of proof of Lemma J of [Crawley] p. 118. Eliminate π. (Contributed by NM, 20-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ (β β ( I βΎ π΅) β§ π β π β§ π β ( I βΎ π΅)) β§ ((π βπΉ) β (π βπ) β§ (π βπ) β (π ββ))) β (πββ) = (πββ)) | ||
Theorem | cdlemj3 39998 | Part of proof of Lemma J of [Crawley] p. 118. Eliminate π. (Contributed by NM, 20-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β (πββ) = (πββ)) | ||
Theorem | tendocan 39999 | 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.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅))) β π = π) | ||
Theorem | tendoid0 40000* | 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.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΉ β ( I βΎ π΅))) β ((πβπΉ) = ( I βΎ π΅) β π = π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |