![]() |
Metamath
Proof Explorer Theorem List (p. 404 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tendopl 40301* | Value of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = ((LTrnβπΎ)βπ) β β’ ((π β πΈ β§ π β πΈ) β (πππ) = (π β π β¦ ((πβπ) β (πβπ)))) | ||
Theorem | tendopl2 40302* | Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = ((LTrnβπΎ)βπ) β β’ ((π β πΈ β§ π β πΈ β§ πΉ β π) β ((πππ)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
Theorem | tendoplcl2 40303* | Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ πΉ β π) β ((πππ)βπΉ) β π) | ||
Theorem | tendoplco2 40304* | Value of result of endomorphism sum operation on a translation composition. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (πΉ β π β§ πΊ β π)) β ((πππ)β(πΉ β πΊ)) = (((πππ)βπΉ) β ((πππ)βπΊ))) | ||
Theorem | tendopltp 40305* | Trace-preserving property of endomorphism sum operation π, based on Theorems trlco 40252. Part of remark in [Crawley] p. 118, 2nd line, "it is clear from the second part of G (our trlco 40252) 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 40306* | Endomorphism sum is a trace-preserving endomorphism. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) β πΈ) | ||
Theorem | tendoplcom 40307* | The endomorphism sum operation is commutative. (Contributed by NM, 11-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β πΈ) β (πππ) = (πππ)) | ||
Theorem | tendoplass 40308* | The endomorphism sum operation is associative. (Contributed by NM, 11-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β ((πππ)ππ) = (ππ(πππ))) | ||
Theorem | tendodi1 40309* | Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β (π β (πππ)) = ((π β π)π(π β π))) | ||
Theorem | tendodi2 40310* | Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β πΈ)) β ((πππ) β π) = ((π β π)π(π β π))) | ||
Theorem | tendo0cbv 40311* | Define additive identity for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 11-Jun-2013.) |
β’ π = (π β π β¦ ( I βΎ π΅)) β β’ π = (π β π β¦ ( I βΎ π΅)) | ||
Theorem | tendo02 40312* | Value of additive identity endomorphism. (Contributed by NM, 11-Jun-2013.) |
β’ π = (π β π β¦ ( I βΎ π΅)) & β’ π΅ = (BaseβπΎ) β β’ (πΉ β π β (πβπΉ) = ( I βΎ π΅)) | ||
Theorem | tendo0co2 40313* | The additive identity trace-preserving endormorphism preserves composition of translations. TODO: why isn't this a special case of tendospdi1 40545? (Contributed by NM, 11-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) | ||
Theorem | tendo0tp 40314* | Trace-preserving property of endomorphism additive identity. (Contributed by NM, 11-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ β€ = (leβπΎ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π β(πβπΉ)) β€ (π βπΉ)) | ||
Theorem | tendo0cl 40315* | The additive identity is a trace-preserving endormorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ ((πΎ β HL β§ π β π») β π β πΈ) | ||
Theorem | tendo0pl 40316* | Property of the additive identity endormorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πππ) = π) | ||
Theorem | tendo0plr 40317* | Property of the additive identity endormorphism. (Contributed by NM, 21-Feb-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πππ) = π) | ||
Theorem | tendoicbv 40318* | Define inverse function for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 12-Jun-2013.) |
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) β β’ πΌ = (π’ β πΈ β¦ (π β π β¦ β‘(π’βπ))) | ||
Theorem | tendoi 40319* | Value of inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π = ((LTrnβπΎ)βπ) β β’ (π β πΈ β (πΌβπ) = (π β π β¦ β‘(πβπ))) | ||
Theorem | tendoi2 40320* | Value of additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π = ((LTrnβπΎ)βπ) β β’ ((π β πΈ β§ πΉ β π) β ((πΌβπ)βπΉ) = β‘(πβπΉ)) | ||
Theorem | tendoicl 40321* | Closure of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πΌβπ) β πΈ) | ||
Theorem | tendoipl 40322* | Property of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π΅ = (BaseβπΎ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β ((πΌβπ)ππ) = π) | ||
Theorem | tendoipl2 40323* | Property of the additive inverse endomorphism. (Contributed by NM, 29-Sep-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π΅ = (BaseβπΎ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (ππ(πΌβπ)) = π) | ||
Theorem | erngfset 40324* | 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 40325* | 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 40326 | 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 40327* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ + = (+gβπ·) β β’ ((πΎ β π β§ π β π») β + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) | ||
Theorem | erngplus 40328* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π + π) = (π β π β¦ ((πβπ) β (πβπ)))) | ||
Theorem | erngplus2 40329 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΉ β π)) β ((π + π)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
Theorem | erngfmul 40330* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π‘ β πΈ β¦ (π β π‘))) | ||
Theorem | erngmul 40331 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π Β· π) = (π β π)) | ||
Theorem | erngfset-rN 40332* | 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 40333* | 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 40334 | 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 40335* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ + = (+gβπ·) β β’ ((πΎ β π β§ π β π») β + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) | ||
Theorem | erngplus-rN 40336* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π + π) = (π β π β¦ ((πβπ) β (πβπ)))) | ||
Theorem | erngplus2-rN 40337 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΉ β π)) β ((π + π)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
Theorem | erngfmul-rN 40338* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π‘ β πΈ β¦ (π‘ β π ))) | ||
Theorem | erngmul-rN 40339 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π Β· π) = (π β π)) | ||
Theorem | cdlemh1 40340 | 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 40341 | 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 40342 | 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 40343 | 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 40344 | 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 40345 | 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 40346 | 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 40347 | 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 40348 | 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 40349 | 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 40350* | 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 40351* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π β π) = π) | ||
Theorem | tendo0mulr 40352* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π β π) = π) | ||
Theorem | tendo1ne0 40353* | 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 40354* | 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 40355* | 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 40356 | 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 40357 | 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 40358 | 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 40359 | 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 40360 | 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 40361 | 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 40362 | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 39411. (Contributed by NM, 25-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ ((π βπΊ) β (π βπΉ) β§ (π βπ) β (π βπΉ)))) β ((π β¨ (πΊβπ)) β§ ((πβπ) β¨ (π β(πΊ β β‘πΉ)))) β€ ((((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘πΉ)) β¨ (π β(π β β‘πΉ)))) β¨ (((πβπ) β¨ π) β§ ((π β(π β β‘πΉ)) β¨ (πβπ))))) | ||
Theorem | cdlemk8 40363 | 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 40364 | 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 40365 | Part of proof of Lemma K of [Crawley] p. 118. TODO: is this needed? If so, shorten with cdlemk9 40364 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 40366* | Part of proof of Lemma K of [Crawley] p. 118. TODO: Eliminate and put into cdlemksel 40370. (Contributed by NM, 25-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ πΌ = (β©π β π (πβπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘πΉ))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΉ))) β πΌ β π) | ||
Theorem | cdlemkvcl 40367 | 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 40368 | 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 40369* | 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 40370* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma(p) function to be a translation. TODO: combine cdlemki 40366? (Contributed by NM, 26-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΉ))) β (πβπΊ) β π) | ||
Theorem | cdlemksat 40371* | 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 40372* | 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 40373* | 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 40374* | 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 40375* | 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 40376* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β ((πβπ) β π΄ β§ Β¬ (πβπ) β€ π)) | ||
Theorem | cdlemk13 40377* | Part of proof of Lemma K of [Crawley] p. 118. Line 13 on p. 119. π, π· are k1, f1. (Contributed by NM, 1-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπ) = ((π β¨ (π βπ·)) β§ ((πβπ) β¨ (π β(π· β β‘πΉ))))) | ||
Theorem | cdlemkole 40378* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπ) β€ (π β¨ (π βπ·))) | ||
Theorem | cdlemk14 40379* | Part of proof of Lemma K of [Crawley] p. 118. Line 19 on p. 119. π, π· are k1, f1. (Contributed by NM, 1-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπ) β€ ((πβπ) β¨ (π β(πΉ β β‘π·)))) | ||
Theorem | cdlemk15 40380* | Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. π, π· are k1, f1. (Contributed by NM, 1-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπ) β€ ((π β¨ (π βπΉ)) β§ ((πβπ) β¨ (π β(πΉ β β‘π·))))) | ||
Theorem | cdlemk16a 40381* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘π·)))) β π΄ β§ Β¬ ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘π·)))) β€ π)) | ||
Theorem | cdlemk16 40382* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (((π β¨ (π βπΉ)) β§ ((πβπ) β¨ (π β(πΉ β β‘π·)))) β π΄ β§ Β¬ ((π β¨ (π βπΉ)) β§ ((πβπ) β¨ (π β(πΉ β β‘π·)))) β€ π)) | ||
Theorem | cdlemk17 40383* | Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. π, π· are k1, f1. (Contributed by NM, 1-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπ) = ((π β¨ (π βπΉ)) β§ ((πβπ) β¨ (π β(πΉ β β‘π·))))) | ||
Theorem | cdlemk1u 40384* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (π β¨ (πβπ)) β€ ((π·βπ) β¨ (π βπ·))) | ||
Theorem | cdlemk5auN 40385* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π· β π β§ πΊ β π β§ π β π) β§ ((π βπΊ) β (π βπ·) β§ (π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (((π·βπ) β¨ (π βπ·)) β§ ((π·βπ) β¨ (π β(πΊ β β‘π·)))) β€ ((πβπ) β¨ (π β(π β β‘π·)))) | ||
Theorem | cdlemk5u 40386* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπ) β (π βπ·)))) β ((π β¨ (πβπ)) β§ ((πΊβπ) β¨ (π β(πΊ β β‘π·)))) β€ ((πβπ) β¨ (π β(π β β‘π·)))) | ||
Theorem | cdlemk6u 40387* | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 39411. (Contributed by NM, 4-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπ) β (π βπ·)))) β ((π β¨ (πΊβπ)) β§ ((πβπ) β¨ (π β(πΊ β β‘π·)))) β€ ((((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘π·)) β¨ (π β(π β β‘π·)))) β¨ (((πβπ) β¨ π) β§ ((π β(π β β‘π·)) β¨ (πβπ))))) | ||
Theorem | cdlemkj 40388* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (β©π β π (πβπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘π·))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β π β π) | ||
Theorem | cdlemkuvN 40389* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma1 (p) function π. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ (πΊ β π β (πβπΊ) = (β©π β π (πβπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘π·)))))) | ||
Theorem | cdlemkuel 40390* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma1 (p) function to be a translation. TODO: combine cdlemkj 40388? (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπΊ) β π) | ||
Theorem | cdlemkuat 40391* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) β π΄) | ||
Theorem | cdlemkuv2 40392* | Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 1, where sigma1 (p) is π, f1 is π·, and k1 is π. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘π·))))) | ||
Theorem | cdlemk18 40393* | Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. π, π, π, π· are k, sigma1 (p), k1, f1. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπ) = ((πβπΉ)βπ)) | ||
Theorem | cdlemk19 40394* | Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. π, π, π, π· are k, sigma1 (p), k1, f1. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπΉ) = π) | ||
Theorem | cdlemk7u 40395* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119 for the sigma1 case. (Contributed by NM, 3-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) & β’ π = (((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘π·)) β¨ (π β(π β β‘π·)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπ) β (π βπ·)))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ π)) | ||
Theorem | cdlemk11u 40396* | Part of proof of Lemma K of [Crawley] p. 118. Line 17, p. 119, showing Eq. 3 (line 8, p. 119) for the sigma1 (π) case. (Contributed by NM, 4-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) & β’ π = (((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘π·)) β¨ (π β(π β β‘π·)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπ) β (π βπ·)))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ (π β(π β β‘πΊ)))) | ||
Theorem | cdlemk12u 40397* | Part of proof of Lemma K of [Crawley] p. 118. Line 18, p. 119, showing Eq. 4 (line 10, p. 119) for the sigma1 (π) case. (Contributed by NM, 4-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π βπΊ) β (π βπ)) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπ) β (π βπ·)))) β ((πβπΊ)βπ) = ((π β¨ (πΊβπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘πΊ))))) | ||
Theorem | cdlemk21N 40398* | Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=0 and j=1. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπΊ) β (π βπΉ)))) β ((πβπΊ)βπ) = ((πβπΊ)βπ)) | ||
Theorem | cdlemk20 40399* | Part of proof of Lemma K of [Crawley] p. 118. Line 22, p. 119 for the i=2, j=1 case. Note typo on line 22: f should be fi. Our π·, πΆ, π, π, π, π represent their f1, f2, k1, k2, sigma1, sigma2. (Contributed by NM, 5-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) & β’ π = (πβπΆ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΆ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ ((π βπ·) β (π βπΉ) β§ (π βπΆ) β (π βπΉ) β§ (π βπΆ) β (π βπ·)))) β ((πβπΆ)βπ) = (πβπ)) | ||
Theorem | cdlemkoatnle-2N 40400* | Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ ((π βπΆ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπ) β π΄ β§ Β¬ (πβπ) β€ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |