HomeTheorem List (p. 402 of 480)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 402 of 480) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-30439) |
Hilbert Space Explorer
(30440-31962) |
Users' Mathboxes
(31963-47940) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdlemky 40101* | Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up (πππΊ) stuff. π represents π in cdlemk31 40071. (Contributed by NM, 21-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β β¦πΊ / πβ¦π = ((πππΊ)βπ)) | ||
| Theorem | cdlemkyu 40102* | Convert between function and explicit forms. πΆ represents π in cdlemkuu 40070. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) & β’ π = (πβπ) & β’ πΆ = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β β¦πΊ / πβ¦π = ((πΆβπΊ)βπ)) | ||
| Theorem | cdlemkyuu 40103* | cdlemkyu 40102 with some hypotheses eliminated. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ πΆ = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β β¦πΊ / πβ¦π = ((πΆβπΊ)βπ)) | ||
| Theorem | cdlemk11ta 40104* | Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. πΊ, πΌ stand for g, h. TODO: fix comment. (Contributed by NM, 21-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ πΆ = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπ) β (π βπΌ)))) β β¦πΊ / πβ¦π β€ (β¦πΌ / πβ¦π β¨ (π β(πΌ β β‘πΊ)))) | ||
| Theorem | cdlemk19ylem 40105* | Lemma for cdlemk19y 40107. (Contributed by NM, 30-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ πΆ = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ)))) β β¦πΉ / πβ¦π = (πβπ)) | ||
| Theorem | cdlemk11tb 40106* | Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. πΊ, πΌ stand for g, h. cdlemk11ta 40104 with hypotheses removed. TODO: Can this be proved directly with no quantification? (Contributed by NM, 21-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπ) β (π βπΌ)))) β β¦πΊ / πβ¦π β€ (β¦πΌ / πβ¦π β¨ (π β(πΌ β β‘πΊ)))) | ||
| Theorem | cdlemk19y 40107* | cdlemk19 40044 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ)))) β β¦πΉ / πβ¦π = (πβπ)) | ||
| Theorem | cdlemkid3N 40108* | Lemma for cdlemkid 40111. (Contributed by NM, 25-Jul-2013.) (New usage is discouraged.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅))) β β¦πΊ / πβ¦π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β (π§βπ) = π))) | ||
| Theorem | cdlemkid4 40109* | Lemma for cdlemkid 40111. (Contributed by NM, 25-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅))) β β¦πΊ / πβ¦π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β π§ = ( I βΎ π΅)))) | ||
| Theorem | cdlemkid5 40110* | Lemma for cdlemkid 40111. (Contributed by NM, 25-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅))) β β¦πΊ / πβ¦π β π) | ||
| Theorem | cdlemkid 40111* | The value of the tau function (in Lemma K of [Crawley] p. 118) on the identity relation. (Contributed by NM, 25-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅))) β β¦πΊ / πβ¦π = ( I βΎ π΅)) | ||
| Theorem | cdlemk35s 40112* | Substitution version of cdlemk35 40087. (Contributed by NM, 22-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β β¦πΊ / πβ¦π β π) | ||
| Theorem | cdlemk35s-id 40113* | Substitution version of cdlemk35 40087. (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ πΊ β π β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β β¦πΊ / πβ¦π β π) | ||
| Theorem | cdlemk39s 40114* | Substitution version of cdlemk39 40091. TODO: Can any commonality with cdlemk35s 40112 be exploited? (Contributed by NM, 23-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β (π ββ¦πΊ / πβ¦π) β€ (π βπΊ)) | ||
| Theorem | cdlemk39s-id 40115* | Substitution version of cdlemk39 40091 with non-identity requirement on πΊ removed. TODO: Can any commonality with cdlemk35s 40112 be exploited? (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ πΊ β π β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β (π ββ¦πΊ / πβ¦π) β€ (π βπΊ)) | ||
| Theorem | cdlemk42 40116* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 20-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β (β¦πΊ / πβ¦πβπ) = β¦πΊ / πβ¦π) | ||
| Theorem | cdlemk19xlem 40117* | Lemma for cdlemk19x 40118. (Contributed by NM, 30-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ)))) β (β¦πΉ / πβ¦πβπ) = (πβπ)) | ||
| Theorem | cdlemk19x 40118* | cdlemk19 40044 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (β¦πΉ / πβ¦πβπ) = (πβπ)) | ||
| Theorem | cdlemk42yN 40119* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 20-Jul-2013.) (New usage is discouraged.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β (β¦πΊ / πβ¦πβπ) = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘π))))) | ||
| Theorem | cdlemk11tc 40120* | Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. πΊ, πΌ stand for g, h. TODO: fix comment. (Contributed by NM, 21-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπ) β (π βπΌ)))) β (β¦πΊ / πβ¦πβπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π β(πΌ β β‘πΊ)))) | ||
| Theorem | cdlemk11t 40121* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 5, line 36, p. 119. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 21-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β (β¦πΊ / πβ¦πβπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π β(πΌ β β‘πΊ)))) | ||
| Theorem | cdlemk45 40122* | Part of proof of Lemma K of [Crawley] p. 118. Line 37, p. 119. πΊ, πΌ stand for g, h. π represents tau. They do not explicitly mention the requirement (πΊ β πΌ) β ( I βΎ π΅). (Contributed by NM, 22-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (β¦(πΊ β πΌ) / πβ¦πβπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π βπΊ))) | ||
| Theorem | cdlemk46 40123* | Part of proof of Lemma K of [Crawley] p. 118. Line 38 (last line), p. 119. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 22-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (β¦(πΊ β πΌ) / πβ¦πβπ) β€ ((β¦πΊ / πβ¦πβπ) β¨ (π βπΌ))) | ||
| Theorem | cdlemk47 40124* | Part of proof of Lemma K of [Crawley] p. 118. Line 2, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 22-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β (β¦(πΊ β πΌ) / πβ¦πβπ) = (((β¦πΊ / πβ¦πβπ) β¨ (π βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π βπΊ)))) | ||
| Theorem | cdlemk48 40125* | Part of proof of Lemma K of [Crawley] p. 118. Line 4, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 22-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π ββ¦πΊ / πβ¦π))) | ||
| Theorem | cdlemk49 40126* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 23-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ ((β¦πΊ / πβ¦πβπ) β¨ (π ββ¦πΌ / πβ¦π))) | ||
| Theorem | cdlemk50 40127* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. πΊ, πΌ stand for g, h. π represents tau. TODO: Combine into cdlemk52 40129? (Contributed by NM, 23-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π ββ¦πΊ / πβ¦π)))) | ||
| Theorem | cdlemk51 40128* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. πΊ, πΌ stand for g, h. π represents tau. TODO: Combine into cdlemk52 40129? (Contributed by NM, 23-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β (((β¦πΊ / πβ¦πβπ) β¨ (π ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π ββ¦πΊ / πβ¦π))) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π βπΊ)))) | ||
| Theorem | cdlemk52 40129* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 23-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) = (β¦(πΊ β πΌ) / πβ¦πβπ)) | ||
| Theorem | cdlemk53a 40130* | Lemma for cdlemk53 40132. (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
| Theorem | cdlemk53b 40131* | Lemma for cdlemk53 40132. (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
| Theorem | cdlemk53 40132* | Part of proof of Lemma K of [Crawley] p. 118. Line 7, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΌ β π β§ (π βπΊ) β (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
| Theorem | cdlemk54 40133* | Part of proof of Lemma K of [Crawley] p. 118. Line 10, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π βπΊ) = (π βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΊ) β§ (π βπ) β (π β(πΊ β πΌ))))) β (β¦(πΊ β πΌ) / πβ¦π β β¦π / πβ¦π) = ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π) β β¦π / πβ¦π)) | ||
| Theorem | cdlemk55a 40134* | Lemma for cdlemk55 40136. (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π βπΊ) = (π βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΊ) β§ (π βπ) β (π β(πΊ β πΌ))))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
| Theorem | cdlemk55b 40135* | Lemma for cdlemk55 40136. (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΌ β π β§ (π βπΊ) = (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
| Theorem | cdlemk55 40136* | Part of proof of Lemma K of [Crawley] p. 118. Line 11, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ πΌ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
| Theorem | cdlemkyyN 40137* | Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up (πππΊ) stuff. (Contributed by NM, 21-Jul-2013.) (New usage is discouraged.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β (β¦πΊ / πβ¦πβπ) = ((πππΊ)βπ)) | ||
| Theorem | cdlemk43N 40138* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 31-Jul-2013.) (New usage is discouraged.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ π β π β§ πΉ β π) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β ((πβπΊ)βπ) = β¦πΊ / πβ¦π) | ||
| Theorem | cdlemk35u 40139* | Substitution version of cdlemk35 40087. (Contributed by NM, 31-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ π β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβπΊ) β π) | ||
| Theorem | cdlemk55u1 40140* | Lemma for cdlemk55u 40141. (Contributed by NM, 31-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ (((π βπΉ) = (π βπ) β§ πΉ β π) β§ πΊ β π β§ πΌ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβ(πΊ β πΌ)) = ((πβπΊ) β (πβπΌ))) | ||
| Theorem | cdlemk55u 40141* | Part of proof of Lemma K of [Crawley] p. 118. Line 11, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 31-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ ((π βπΉ) = (π βπ) β§ πΊ β π β§ πΌ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβ(πΊ β πΌ)) = ((πβπΊ) β (πβπΌ))) | ||
| Theorem | cdlemk39u1 40142* | Lemma for cdlemk39u 40143. (Contributed by NM, 31-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ ((π βπΉ) = (π βπ) β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β(πβπΊ)) β€ (π βπΊ)) | ||
| Theorem | cdlemk39u 40143* | Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. Trace-preserving property of the value of tau, represented by (πβπΊ). (Contributed by NM, 31-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ ((π βπΉ) = (π βπ) β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β(πβπΊ)) β€ (π βπΊ)) | ||
| Theorem | cdlemk19u1 40144* | cdlemk19 40044 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 31-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΉ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπΉ)βπ) = (πβπ)) | ||
| Theorem | cdlemk19u 40145* | Part of Lemma K of [Crawley] p. 118. Line 12, p. 120, "f (exponent) tau = k". We represent f, k, tau with πΉ, π, π. (Contributed by NM, 31-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβπΉ) = π) | ||
| Theorem | cdlemk56 40146* | Part of Lemma K of [Crawley] p. 118. Line 11, p. 120, "tau is in Delta" i.e. π is a trace-preserving endormorphism. (Contributed by NM, 31-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ) β§ (π β π΄ β§ Β¬ π β€ π)) β π β πΈ) | ||
| Theorem | cdlemk19w 40147* | Use a fixed element to eliminate π in cdlemk19u 40145. (Contributed by NM, 1-Aug-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ( β₯ βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ)) β (πβπΉ) = π) | ||
| Theorem | cdlemk56w 40148* | Use a fixed element to eliminate π in cdlemk56 40146. (Contributed by NM, 1-Aug-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ( β₯ βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ)) β (π β πΈ β§ (πβπΉ) = π)) | ||
| Theorem | cdlemk 40149* | Lemma K of [Crawley] p. 118. Final result, lines 11 and 12 on p. 120: given two translations f and k with the same trace, there exists a trace-preserving endomorphism tau whose value at f is k. We use πΉ, π, and π’ to represent f, k, and tau. (Contributed by NM, 1-Aug-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ)) β βπ’ β πΈ (π’βπΉ) = π) | ||
| Theorem | tendoex 40150* | Generalization of Lemma K of [Crawley] p. 118, cdlemk 40149. TODO: can this be used to shorten uses of cdlemk 40149? (Contributed by NM, 15-Oct-2013.) |
| β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπ) β€ (π βπΉ)) β βπ’ β πΈ (π’βπΉ) = π) | ||
| Theorem | cdleml1N 40151 | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.) |
| β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (π β(πβπ)) = (π β(πβπ))) | ||
| Theorem | cdleml2N 40152* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.) |
| β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β βπ β πΈ (π β(πβπ)) = (πβπ)) | ||
| Theorem | cdleml3N 40153* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.) |
| β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ π β 0 β§ π β 0 )) β βπ β πΈ (π β π) = π) | ||
| Theorem | cdleml4N 40154* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.) |
| β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (π β 0 β§ π β 0 )) β βπ β πΈ (π β π) = π) | ||
| Theorem | cdleml5N 40155* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.) |
| β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β βπ β πΈ (π β π) = π) | ||
| Theorem | cdleml6 40156* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ β β π β§ (π β πΈ β§ π β 0 )) β (π β πΈ β§ (πβ(π ββ)) = β)) | ||
| Theorem | cdleml7 40157* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ β β π β§ (π β πΈ β§ π β 0 )) β ((π β π )ββ) = (( I βΎ π)ββ)) | ||
| Theorem | cdleml8 40158* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β (π β π ) = ( I βΎ π)) | ||
| Theorem | cdleml9 40159* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β π β 0 ) | ||
| Theorem | dva1dim 40160* | Two expressions for the 1-dimensional subspaces of partial vector space A. Remark in [Crawley] p. 120 line 21, but using a non-identity translation (nonzero vector) πΉ whose trace is π rather than π itself; πΉ exists by cdlemf 39738. πΈ is the division ring base by erngdv 40168, and π βπΉ is the scalar product by dvavsca 40192. πΉ must be a non-identity translation for the expression to be a 1-dimensional subspace, although the theorem doesn't require it. (Contributed by NM, 14-Oct-2013.) |
| β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β {π β£ βπ β πΈ π = (π βπΉ)} = {π β π β£ (π βπ) β€ (π βπΉ)}) | ||
| Theorem | dvhb1dimN 40161* | Two expressions for the 1-dimensional subspaces of vector space π», in the isomorphism B case where the second vector component is zero. (Contributed by NM, 23-Feb-2014.) (New usage is discouraged.) |
| β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (β β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β {π β (π Γ πΈ) β£ βπ β πΈ π = β¨(π βπΉ), 0 β©} = {π β (π Γ πΈ) β£ ((π β(1st βπ)) β€ (π βπΉ) β§ (2nd βπ) = 0 )}) | ||
| Theorem | erng1lem 40162 | Value of the endomorphism division ring unity. (Contributed by NM, 12-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ ((πΎ β HL β§ π β π») β π· β Ring) β β’ ((πΎ β HL β§ π β π») β (1rβπ·) = ( I βΎ π)) | ||
| Theorem | erngdvlem1 40163* | Lemma for eringring 40167. (Contributed by NM, 4-Aug-2013.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Grp) | ||
| Theorem | erngdvlem2N 40164* | Lemma for eringring 40167. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Abel) | ||
| Theorem | erngdvlem3 40165* | Lemma for eringring 40167. (Contributed by NM, 6-Aug-2013.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ + = (π β πΈ, π β πΈ β¦ (π β π)) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
| Theorem | erngdvlem4 40166* | Lemma for erngdv 40168. (Contributed by NM, 11-Aug-2013.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ + = (π β πΈ, π β πΈ β¦ (π β π)) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) β β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β π· β DivRing) | ||
| Theorem | eringring 40167 | An endomorphism ring is a ring. TODO: fix comment. (Contributed by NM, 4-Aug-2013.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
| Theorem | erngdv 40168 | An endomorphism ring is a division ring. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π· β DivRing) | ||
| Theorem | erng0g 40169* | The division ring zero of an endomorphism ring. (Contributed by NM, 5-Nov-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |
| β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ 0 = (0gβπ·) β β’ ((πΎ β HL β§ π β π») β 0 = π) | ||
| Theorem | erng1r 40170 | The division ring unity of an endomorphism ring. (Contributed by NM, 5-Nov-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ 1 = (1rβπ·) β β’ ((πΎ β HL β§ π β π») β 1 = ( I βΎ π)) | ||
| Theorem | erngdvlem1-rN 40171* | Lemma for eringring 40167. (Contributed by NM, 4-Aug-2013.) (New usage is discouraged.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Grp) | ||
| Theorem | erngdvlem2-rN 40172* | Lemma for eringring 40167. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Abel) | ||
| Theorem | erngdvlem3-rN 40173* | Lemma for eringring 40167. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ π = (π β πΈ, π β πΈ β¦ (π β π)) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
| Theorem | erngdvlem4-rN 40174* | Lemma for erngdv 40168. (Contributed by NM, 11-Aug-2013.) (New usage is discouraged.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ π = (π β πΈ, π β πΈ β¦ (π β π)) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) β β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β π· β DivRing) | ||
| Theorem | erngring-rN 40175 | An endomorphism ring is a ring. TODO: fix comment. (Contributed by NM, 4-Aug-2013.) (New usage is discouraged.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
| Theorem | erngdv-rN 40176 | An endomorphism ring is a division ring. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) (New usage is discouraged.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π· β DivRing) | ||
| Syntax | cdveca 40177 | Extend class notation with constructed vector space A. |
| class DVecA | ||
| Definition | df-dveca 40178* | Define constructed partial vector space A. (Contributed by NM, 8-Oct-2013.) |
| β’ DVecA = (π β V β¦ (π€ β (LHypβπ) β¦ ({β¨(Baseβndx), ((LTrnβπ)βπ€)β©, β¨(+gβndx), (π β ((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx), ((EDRingβπ)βπ€)β©} βͺ {β¨( Β·π βndx), (π β ((TEndoβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π βπ))β©}))) | ||
| Theorem | dvafset 40179* | The constructed partial vector space A for a lattice πΎ. (Contributed by NM, 8-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
| β’ π» = (LHypβπΎ) β β’ (πΎ β π β (DVecAβπΎ) = (π€ β π» β¦ ({β¨(Baseβndx), ((LTrnβπΎ)βπ€)β©, β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx), ((EDRingβπΎ)βπ€)β©} βͺ {β¨( Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π βπ))β©}))) | ||
| Theorem | dvaset 40180* | The constructed partial vector space A for a lattice πΎ. (Contributed by NM, 8-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β π = ({β¨(Baseβndx), πβ©, β¨(+gβndx), (π β π, π β π β¦ (π β π))β©, β¨(Scalarβndx), π·β©} βͺ {β¨( Β·π βndx), (π β πΈ, π β π β¦ (π βπ))β©})) | ||
| Theorem | dvasca 40181 | The ring base set of the constructed partial vector space A are all translation group endomorphisms (for a fiducial co-atom π). (Contributed by NM, 22-Jun-2014.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) β β’ ((πΎ β π β§ π β π») β πΉ = π·) | ||
| Theorem | dvabase 40182 | The ring base set of the constructed partial vector space A are all translation group endomorphisms (for a fiducial co-atom π). (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
| β’ π» = (LHypβπΎ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ πΆ = (BaseβπΉ) β β’ ((πΎ β π β§ π β π») β πΆ = πΈ) | ||
| Theorem | dvafplusg 40183* | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ + = (+gβπΉ) β β’ ((πΎ β π β§ π β π») β + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) | ||
| Theorem | dvaplusg 40184* | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ + = (+gβπΉ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π + π) = (π β π β¦ ((π βπ) β (πβπ)))) | ||
| Theorem | dvaplusgv 40185 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ + = (+gβπΉ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΊ β π)) β ((π + π)βπΊ) = ((π βπΊ) β (πβπΊ))) | ||
| Theorem | dvafmulr 40186* | Ring multiplication operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ Β· = (.rβπΉ) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π‘ β πΈ β¦ (π β π‘))) | ||
| Theorem | dvamulr 40187 | Ring multiplication operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ Β· = (.rβπΉ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π Β· π) = (π β π)) | ||
| Theorem | dvavbase 40188 | The vectors (vector base set) of the constructed partial vector space A are all translations (for a fiducial co-atom π). (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (Baseβπ) β β’ ((πΎ β π β§ π β π») β π = π) | ||
| Theorem | dvafvadd 40189* | The vector sum operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ + = (+gβπ) β β’ ((πΎ β π β§ π β π») β + = (π β π, π β π β¦ (π β π))) | ||
| Theorem | dvavadd 40190 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ + = (+gβπ) β β’ (((πΎ β π β§ π β π») β§ (πΉ β π β§ πΊ β π)) β (πΉ + πΊ) = (πΉ β πΊ)) | ||
| Theorem | dvafvsca 40191* | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π β π β¦ (π βπ))) | ||
| Theorem | dvavsca 40192 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β π)) β (π Β· πΉ) = (π βπΉ)) | ||
| Theorem | tendospcl 40193 | Closure of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ) β π) | ||
| Theorem | tendospass 40194 | Associative law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΉ β π)) β ((π β π)βπΉ) = (πβ(πβπΉ))) | ||
| Theorem | tendospdi1 40195 | Forward distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β π β§ πΊ β π)) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) | ||
| Theorem | tendocnv 40196 | Converse of a trace-preserving endomorphism value. (Contributed by NM, 7-Apr-2014.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β β‘(πβπΉ) = (πββ‘πΉ)) | ||
| Theorem | tendospdi2 40197* | Reverse distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
| β’ π = ((LTrnβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ ((π β πΈ β§ π β πΈ β§ πΉ β π) β ((πππ)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
| Theorem | tendospcanN 40198* | Cancellation law for trace-preserving endomorphism values (used as scalar product). (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
| β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (πΉ β π β§ πΊ β π)) β ((πβπΉ) = (πβπΊ) β πΉ = πΊ)) | ||
| Theorem | dvaabl 40199 | The constructed partial vector space A for a lattice πΎ is an abelian group. (Contributed by NM, 11-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
| β’ π» = (LHypβπΎ) & β’ π = ((DVecAβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π β Abel) | ||
| Theorem | dvalveclem 40200 | Lemma for dvalvec 40201. (Contributed by NM, 11-Oct-2013.) (Proof shortened by Mario Carneiro, 22-Jun-2014.) |
| β’ π» = (LHypβπΎ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ + = (+gβπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = (Scalarβπ) & β’ π΅ = (BaseβπΎ) & ⒠⨣ = (+gβπ·) & β’ Γ = (.rβπ·) & β’ Β· = ( Β·π βπ) β β’ ((πΎ β HL β§ π β π») β π β LVec) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |