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