Home | Metamath
Proof Explorer Theorem List (p. 392 of 470) | < 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: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-tgrp 39101* | 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 39102* | The translation group maps for a lattice πΎ. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (TGrpβπΎ) = (π€ β π» β¦ {β¨(Baseβndx), ((LTrnβπΎ)βπ€)β©, β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©})) | ||
Theorem | tgrpset 39103* | The translation group for a fiducial co-atom π. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΊ = ((TGrpβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΊ = {β¨(Baseβndx), πβ©, β¨(+gβndx), (π β π, π β π β¦ (π β π))β©}) | ||
Theorem | tgrpbase 39104 | 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 39105* | The group operation of the translation group is function composition. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΊ = ((TGrpβπΎ)βπ) & β’ + = (+gβπΊ) β β’ ((πΎ β π β§ π β π») β + = (π β π, π β π β¦ (π β π))) | ||
Theorem | tgrpov 39106 | 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 39107 | Lemma for tgrpgrp 39108. (Contributed by NM, 6-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΊ = ((TGrpβπΎ)βπ) & β’ + = (+gβπΊ) & β’ π΅ = (BaseβπΎ) β β’ ((πΎ β HL β§ π β π») β πΊ β Grp) | ||
Theorem | tgrpgrp 39108 | The translation group is a group. (Contributed by NM, 6-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ πΊ = ((TGrpβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β πΊ β Grp) | ||
Theorem | tgrpabl 39109 | 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 39110 | Extend class notation with translation group endomorphisms. |
class TEndo | ||
Syntax | cedring 39111 | Extend class notation with division ring on trace-preserving endomorphisms. |
class EDRing | ||
Syntax | cedring-rN 39112 | 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 39113* | 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 39114* | 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 39115* | 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 39116* | 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 39117* | 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 39118* | 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 39119 | Trace-preserving property of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β πΈ β§ πΉ β π) β (π β(πβπΉ)) β€ (π βπΉ)) | ||
Theorem | istendod 39120* | Deduce the predicate "is a trace-preserving endomorphism". (Contributed by NM, 9-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ (π β (πΎ β π β§ π β π»)) & β’ (π β π:πβΆπ) & β’ ((π β§ π β π β§ π β π) β (πβ(π β π)) = ((πβπ) β (πβπ))) & β’ ((π β§ π β π) β (π β(πβπ)) β€ (π βπ)) β β’ (π β π β πΈ) | ||
Theorem | tendof 39121 | Functionality of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β πΈ) β π:πβΆπ) | ||
Theorem | tendoeq1 39122* | Condition determining equality of two trace-preserving endomorphisms. (Contributed by NM, 11-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ βπ β π (πβπ) = (πβπ)) β π = π) | ||
Theorem | tendovalco 39123 | Value of composition of translations in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π» β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) | ||
Theorem | tendocoval 39124 | Value of composition of endomorphisms in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β ((π β π)βπΉ) = (πβ(πβπΉ))) | ||
Theorem | tendocl 39125 | Closure of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ) β π) | ||
Theorem | tendoco2 39126 | Distribution of compositions in preparation for endomorphism sum definition. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β ((πβ(πΉ β πΊ)) β (πβ(πΉ β πΊ))) = (((πβπΉ) β (πβπΉ)) β ((πβπΊ) β (πβπΊ)))) | ||
Theorem | tendoidcl 39127 | The identity is a trace-preserving endomorphism. (Contributed by NM, 30-Jul-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β πΈ) | ||
Theorem | tendo1mul 39128 | Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (( I βΎ π) β π) = π) | ||
Theorem | tendo1mulr 39129 | Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π β ( I βΎ π)) = π) | ||
Theorem | tendococl 39130 | 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 39131 | The identity value of a trace-preserving endomorphism. (Contributed by NM, 21-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πβ( I βΎ π΅)) = ( I βΎ π΅)) | ||
Theorem | tendoeq2 39132* | Condition determining equality of two trace-preserving endomorphisms, showing it is unnecessary to consider the identity translation. In tendocan 39182, 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 39133* | Define sum operation for trace-preserving endomorphisms. Change bound variables to isolate them later. (Contributed by NM, 11-Jun-2013.) |
β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ π = (π’ β πΈ, π£ β πΈ β¦ (π β π β¦ ((π’βπ) β (π£βπ)))) | ||
Theorem | tendopl 39134* | Value of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = ((LTrnβπΎ)βπ) β β’ ((π β πΈ β§ π β πΈ) β (πππ) = (π β π β¦ ((πβπ) β (πβπ)))) | ||
Theorem | tendopl2 39135* | Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = ((LTrnβπΎ)βπ) β β’ ((π β πΈ β§ π β πΈ β§ πΉ β π) β ((πππ)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
Theorem | tendoplcl2 39136* | Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β ((πππ)βπΉ) β π) | ||
Theorem | tendoplco2 39137* | Value of result of endomorphism sum operation on a translation composition. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β ((πππ)β(πΉ β πΊ)) = (((πππ)βπΉ) β ((πππ)βπΊ))) | ||
Theorem | tendopltp 39138* | Trace-preserving property of endomorphism sum operation π, based on Theorems trlco 39085. Part of remark in [Crawley] p. 118, 2nd line, "it is clear from the second part of G (our trlco 39085) 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 39139* | Endomorphism sum is a trace-preserving endomorphism. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) β πΈ) | ||
Theorem | tendoplcom 39140* | The endomorphism sum operation is commutative. (Contributed by NM, 11-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) = (πππ)) | ||
Theorem | tendoplass 39141* | The endomorphism sum operation is associative. (Contributed by NM, 11-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β ((πππ)ππ) = (ππ(πππ))) | ||
Theorem | tendodi1 39142* | Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (π β (πππ)) = ((π β π)π(π β π))) | ||
Theorem | tendodi2 39143* | Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β ((πππ) β π) = ((π β π)π(π β π))) | ||
Theorem | tendo0cbv 39144* | Define additive identity for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 11-Jun-2013.) |
β’ π = (π β π β¦ ( I βΎ π΅)) β β’ π = (π β π β¦ ( I βΎ π΅)) | ||
Theorem | tendo02 39145* | Value of additive identity endomorphism. (Contributed by NM, 11-Jun-2013.) |
β’ π = (π β π β¦ ( I βΎ π΅)) & β’ π΅ = (BaseβπΎ) β β’ (πΉ β π β (πβπΉ) = ( I βΎ π΅)) | ||
Theorem | tendo0co2 39146* | The additive identity trace-preserving endormorphism preserves composition of translations. TODO: why isn't this a special case of tendospdi1 39378? (Contributed by NM, 11-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) | ||
Theorem | tendo0tp 39147* | Trace-preserving property of endomorphism additive identity. (Contributed by NM, 11-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ β€ = (leβπΎ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π β(πβπΉ)) β€ (π βπΉ)) | ||
Theorem | tendo0cl 39148* | The additive identity is a trace-preserving endormorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ ((πΎ β HL β§ π β π») β π β πΈ) | ||
Theorem | tendo0pl 39149* | Property of the additive identity endormorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πππ) = π) | ||
Theorem | tendo0plr 39150* | Property of the additive identity endormorphism. (Contributed by NM, 21-Feb-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πππ) = π) | ||
Theorem | tendoicbv 39151* | Define inverse function for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 12-Jun-2013.) |
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) β β’ πΌ = (π’ β πΈ β¦ (π β π β¦ β‘(π’βπ))) | ||
Theorem | tendoi 39152* | Value of inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π = ((LTrnβπΎ)βπ) β β’ (π β πΈ β (πΌβπ) = (π β π β¦ β‘(πβπ))) | ||
Theorem | tendoi2 39153* | Value of additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π = ((LTrnβπΎ)βπ) β β’ ((π β πΈ β§ πΉ β π) β ((πΌβπ)βπΉ) = β‘(πβπΉ)) | ||
Theorem | tendoicl 39154* | Closure of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πΌβπ) β πΈ) | ||
Theorem | tendoipl 39155* | Property of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π΅ = (BaseβπΎ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β ((πΌβπ)ππ) = π) | ||
Theorem | tendoipl2 39156* | Property of the additive inverse endomorphism. (Contributed by NM, 29-Sep-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π΅ = (BaseβπΎ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (ππ(πΌβπ)) = π) | ||
Theorem | erngfset 39157* | 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 39158* | 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 39159 | 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 39160* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ + = (+gβπ·) β β’ ((πΎ β π β§ π β π») β + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) | ||
Theorem | erngplus 39161* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π + π) = (π β π β¦ ((πβπ) β (πβπ)))) | ||
Theorem | erngplus2 39162 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΉ β π)) β ((π + π)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
Theorem | erngfmul 39163* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π‘ β πΈ β¦ (π β π‘))) | ||
Theorem | erngmul 39164 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π Β· π) = (π β π)) | ||
Theorem | erngfset-rN 39165* | 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 39166* | 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 39167 | 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 39168* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ + = (+gβπ·) β β’ ((πΎ β π β§ π β π») β + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) | ||
Theorem | erngplus-rN 39169* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π + π) = (π β π β¦ ((πβπ) β (πβπ)))) | ||
Theorem | erngplus2-rN 39170 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΉ β π)) β ((π + π)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
Theorem | erngfmul-rN 39171* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π‘ β πΈ β¦ (π‘ β π ))) | ||
Theorem | erngmul-rN 39172 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π Β· π) = (π β π)) | ||
Theorem | cdlemh1 39173 | 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 39174 | 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 39175 | 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 39176 | 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 39177 | 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 39178 | 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 39179 | 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 39180 | 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 39181 | 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 39182 | 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 39183* | 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 βΎ π΅) β π = π)) | ||
Theorem | tendo0mul 39184* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π β π) = π) | ||
Theorem | tendo0mulr 39185* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π β π) = π) | ||
Theorem | tendo1ne0 39186* | The identity (unity) is not equal to the zero trace-preserving endomorphism. (Contributed by NM, 8-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β π) | ||
Theorem | tendoconid 39187* | The composition (product) of trace-preserving endormorphisms is nonzero when each argument is nonzero. (Contributed by NM, 8-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β (π β π) β π) | ||
Theorem | tendotr 39188* | The trace of the value of a nonzero trace-preserving endomorphism equals the trace of the argument. (Contributed by NM, 11-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β (π β(πβπΉ)) = (π βπΉ)) | ||
Theorem | cdlemk1 39189 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ ((π βπΉ) = (π βπ) β§ (π β π΄ β§ Β¬ π β€ π))) β (π β¨ (πβπ)) = ((πΉβπ) β¨ (π βπΉ))) | ||
Theorem | cdlemk2 39190 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊβπ) β¨ (π β(πΊ β β‘πΉ))) = ((πΉβπ) β¨ (π β(πΊ β β‘πΉ)))) | ||
Theorem | cdlemk3 39191 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ ((π βπΊ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (((πΉβπ) β¨ (π βπΉ)) β§ ((πΉβπ) β¨ (π β(πΊ β β‘πΉ)))) = (πΉβπ)) | ||
Theorem | cdlemk4 39192 | 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.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) β€ ((πβπ) β¨ (π β(π β β‘πΉ)))) | ||
Theorem | cdlemk5a 39193 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((π βπΊ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (((πΉβπ) β¨ (π βπΉ)) β§ ((πΉβπ) β¨ (π β(πΊ β β‘πΉ)))) β€ ((πβπ) β¨ (π β(π β β‘πΉ)))) | ||
Theorem | cdlemk5 39194 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 25-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΉ))) β ((π β¨ (πβπ)) β§ ((πΊβπ) β¨ (π β(πΊ β β‘πΉ)))) β€ ((πβπ) β¨ (π β(π β β‘πΉ)))) | ||
Theorem | cdlemk6 39195 | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 38244. (Contributed by NM, 25-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ ((π βπΊ) β (π βπΉ) β§ (π βπ) β (π βπΉ)))) β ((π β¨ (πΊβπ)) β§ ((πβπ) β¨ (π β(πΊ β β‘πΉ)))) β€ ((((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘πΉ)) β¨ (π β(π β β‘πΉ)))) β¨ (((πβπ) β¨ π) β§ ((π β(π β β‘πΉ)) β¨ (πβπ))))) | ||
Theorem | cdlemk8 39196 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 26-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊβπ) β¨ (πβπ)) = ((πΊβπ) β¨ (π β(π β β‘πΊ)))) | ||
Theorem | cdlemk9 39197 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΊβπ) β¨ (πβπ)) β§ π) = (π β(π β β‘πΊ))) | ||
Theorem | cdlemk9bN 39198 | Part of proof of Lemma K of [Crawley] p. 118. TODO: is this needed? If so, shorten with cdlemk9 39197 if that one is also needed. (Contributed by NM, 28-Jun-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΊβπ) β¨ (πβπ)) β§ π) = (π β(πΊ β β‘π))) | ||
Theorem | cdlemki 39199* | Part of proof of Lemma K of [Crawley] p. 118. TODO: Eliminate and put into cdlemksel 39203. (Contributed by NM, 25-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ πΌ = (β©π β π (πβπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘πΉ))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΉ))) β πΌ β π) | ||
Theorem | cdlemkvcl 39200 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π = (((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘πΉ)) β¨ (π β(π β β‘πΉ)))) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π β§ π β π) β§ π β π΄) β π β π΅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |