HomeTheorem List (p. 399 of 479)
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. 399 of 479) | < 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-30166) |
Hilbert Space Explorer
(30167-31689) |
Users' Mathboxes
(31690-47842) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdlemkid5 39801* | Lemma for cdlemkid 39802. (Contributed by NM, 25-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅))) β β¦πΊ / πβ¦π β π) | ||
| Theorem | cdlemkid 39802* | 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 39803* | Substitution version of cdlemk35 39778. (Contributed by NM, 22-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β β¦πΊ / πβ¦π β π) | ||
| Theorem | cdlemk35s-id 39804* | Substitution version of cdlemk35 39778. (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ πΊ β π β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β β¦πΊ / πβ¦π β π) | ||
| Theorem | cdlemk39s 39805* | Substitution version of cdlemk39 39782. TODO: Can any commonality with cdlemk35s 39803 be exploited? (Contributed by NM, 23-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β (π ββ¦πΊ / πβ¦π) β€ (π βπΊ)) | ||
| Theorem | cdlemk39s-id 39806* | Substitution version of cdlemk39 39782 with non-identity requirement on πΊ removed. TODO: Can any commonality with cdlemk35s 39803 be exploited? (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ πΊ β π β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β (π ββ¦πΊ / πβ¦π) β€ (π βπΊ)) | ||
| Theorem | cdlemk42 39807* | 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 39808* | Lemma for cdlemk19x 39809. (Contributed by NM, 30-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ)))) β (β¦πΉ / πβ¦πβπ) = (πβπ)) | ||
| Theorem | cdlemk19x 39809* | cdlemk19 39735 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 39810* | 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 39811* | 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 39812* | 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 39813* | 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 39814* | 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 39815* | 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 39816* | 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 39817* | 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 39818* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. πΊ, πΌ stand for g, h. π represents tau. TODO: Combine into cdlemk52 39820? (Contributed by NM, 23-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π ββ¦πΊ / πβ¦π)))) | ||
| Theorem | cdlemk51 39819* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. πΊ, πΌ stand for g, h. π represents tau. TODO: Combine into cdlemk52 39820? (Contributed by NM, 23-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β (((β¦πΊ / πβ¦πβπ) β¨ (π ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π ββ¦πΊ / πβ¦π))) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π βπΊ)))) | ||
| Theorem | cdlemk52 39820* | 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 39821* | Lemma for cdlemk53 39823. (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
| Theorem | cdlemk53b 39822* | Lemma for cdlemk53 39823. (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
| Theorem | cdlemk53 39823* | 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 39824* | 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 39825* | Lemma for cdlemk55 39827. (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π βπΊ) = (π βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΊ) β§ (π βπ) β (π β(πΊ β πΌ))))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
| Theorem | cdlemk55b 39826* | Lemma for cdlemk55 39827. (Contributed by NM, 26-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΌ β π β§ (π βπΊ) = (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
| Theorem | cdlemk55 39827* | 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 39828* | 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 39829* | 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 39830* | Substitution version of cdlemk35 39778. (Contributed by NM, 31-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ π β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβπΊ) β π) | ||
| Theorem | cdlemk55u1 39831* | Lemma for cdlemk55u 39832. (Contributed by NM, 31-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ (((π βπΉ) = (π βπ) β§ πΉ β π) β§ πΊ β π β§ πΌ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβ(πΊ β πΌ)) = ((πβπΊ) β (πβπΌ))) | ||
| Theorem | cdlemk55u 39832* | 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 39833* | Lemma for cdlemk39u 39834. (Contributed by NM, 31-Jul-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ ((π βπΉ) = (π βπ) β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β(πβπΊ)) β€ (π βπΊ)) | ||
| Theorem | cdlemk39u 39834* | 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 39835* | cdlemk19 39735 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 39836* | 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 39837* | 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 39838* | Use a fixed element to eliminate π in cdlemk19u 39836. (Contributed by NM, 1-Aug-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ( β₯ βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ)) β (πβπΉ) = π) | ||
| Theorem | cdlemk56w 39839* | Use a fixed element to eliminate π in cdlemk56 39837. (Contributed by NM, 1-Aug-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ( β₯ βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ)) β (π β πΈ β§ (πβπΉ) = π)) | ||
| Theorem | cdlemk 39840* | 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 39841* | Generalization of Lemma K of [Crawley] p. 118, cdlemk 39840. TODO: can this be used to shorten uses of cdlemk 39840? (Contributed by NM, 15-Oct-2013.) |
| β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπ) β€ (π βπΉ)) β βπ’ β πΈ (π’βπΉ) = π) | ||
| Theorem | cdleml1N 39842 | 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 39843* | 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 39844* | 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 39845* | 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 39846* | 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 39847* | 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 39848* | 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 39849* | 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 39850* | 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 39851* | 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 39429. πΈ is the division ring base by erngdv 39859, and π βπΉ is the scalar product by dvavsca 39883. πΉ 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 39852* | 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 39853 | Value of the endomorphism division ring unity. (Contributed by NM, 12-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ ((πΎ β HL β§ π β π») β π· β Ring) β β’ ((πΎ β HL β§ π β π») β (1rβπ·) = ( I βΎ π)) | ||
| Theorem | erngdvlem1 39854* | Lemma for eringring 39858. (Contributed by NM, 4-Aug-2013.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Grp) | ||
| Theorem | erngdvlem2N 39855* | Lemma for eringring 39858. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Abel) | ||
| Theorem | erngdvlem3 39856* | Lemma for eringring 39858. (Contributed by NM, 6-Aug-2013.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ + = (π β πΈ, π β πΈ β¦ (π β π)) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
| Theorem | erngdvlem4 39857* | Lemma for erngdv 39859. (Contributed by NM, 11-Aug-2013.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ + = (π β πΈ, π β πΈ β¦ (π β π)) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) β β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β π· β DivRing) | ||
| Theorem | eringring 39858 | An endomorphism ring is a ring. TODO: fix comment. (Contributed by NM, 4-Aug-2013.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
| Theorem | erngdv 39859 | An endomorphism ring is a division ring. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π· β DivRing) | ||
| Theorem | erng0g 39860* | 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 39861 | 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 39862* | Lemma for eringring 39858. (Contributed by NM, 4-Aug-2013.) (New usage is discouraged.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Grp) | ||
| Theorem | erngdvlem2-rN 39863* | Lemma for eringring 39858. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Abel) | ||
| Theorem | erngdvlem3-rN 39864* | Lemma for eringring 39858. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |
| β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ π = (π β πΈ, π β πΈ β¦ (π β π)) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
| Theorem | erngdvlem4-rN 39865* | Lemma for erngdv 39859. (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 39866 | 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 39867 | 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 39868 | Extend class notation with constructed vector space A. |
| class DVecA | ||
| Definition | df-dveca 39869* | 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 39870* | 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 39871* | 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 39872 | 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 39873 | 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 39874* | 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 39875* | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ + = (+gβπΉ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π + π) = (π β π β¦ ((π βπ) β (πβπ)))) | ||
| Theorem | dvaplusgv 39876 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ + = (+gβπΉ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΊ β π)) β ((π + π)βπΊ) = ((π βπΊ) β (πβπΊ))) | ||
| Theorem | dvafmulr 39877* | 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 39878 | Ring multiplication operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ Β· = (.rβπΉ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π Β· π) = (π β π)) | ||
| Theorem | dvavbase 39879 | 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 39880* | 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 39881 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ + = (+gβπ) β β’ (((πΎ β π β§ π β π») β§ (πΉ β π β§ πΊ β π)) β (πΉ + πΊ) = (πΉ β πΊ)) | ||
| Theorem | dvafvsca 39882* | 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 39883 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β π)) β (π Β· πΉ) = (π βπΉ)) | ||
| Theorem | tendospcl 39884 | Closure of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ) β π) | ||
| Theorem | tendospass 39885 | Associative law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΉ β π)) β ((π β π)βπΉ) = (πβ(πβπΉ))) | ||
| Theorem | tendospdi1 39886 | Forward distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β π β§ πΊ β π)) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) | ||
| Theorem | tendocnv 39887 | Converse of a trace-preserving endomorphism value. (Contributed by NM, 7-Apr-2014.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β β‘(πβπΉ) = (πββ‘πΉ)) | ||
| Theorem | tendospdi2 39888* | Reverse distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
| β’ π = ((LTrnβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ ((π β πΈ β§ π β πΈ β§ πΉ β π) β ((πππ)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
| Theorem | tendospcanN 39889* | 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 39890 | 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 39891 | Lemma for dvalvec 39892. (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) | ||
| Theorem | dvalvec 39892 | The constructed partial vector space A for a lattice πΎ is a left vector space. (Contributed by NM, 11-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
| β’ π» = (LHypβπΎ) & β’ π = ((DVecAβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π β LVec) | ||
| Theorem | dva0g 39893 | The zero vector of partial vector space A. (Contributed by NM, 9-Sep-2014.) |
| β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ 0 = (0gβπ) β β’ ((πΎ β HL β§ π β π») β 0 = ( I βΎ π΅)) | ||
| Syntax | cdia 39894 | Extend class notation with partial isomorphism A. |
| class DIsoA | ||
| Definition | df-disoa 39895* | Define partial isomorphism A. (Contributed by NM, 15-Oct-2013.) |
| β’ DIsoA = (π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β {π¦ β (Baseβπ) β£ π¦(leβπ)π€} β¦ {π β ((LTrnβπ)βπ€) β£ (((trLβπ)βπ€)βπ)(leβπ)π₯}))) | ||
| Theorem | diaffval 39896* | The partial isomorphism A for a lattice πΎ. (Contributed by NM, 15-Oct-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β π β (DIsoAβπΎ) = (π€ β π» β¦ (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯}))) | ||
| Theorem | diafval 39897* | The partial isomorphism A for a lattice πΎ. (Contributed by NM, 15-Oct-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΌ = (π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π βπ) β€ π₯})) | ||
| Theorem | diaval 39898* | The partial isomorphism A for a lattice πΎ. Definition of isomorphism map in [Crawley] p. 120 line 24. (Contributed by NM, 15-Oct-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) = {π β π β£ (π βπ) β€ π}) | ||
| Theorem | diaelval 39899 | Member of the partial isomorphism A for a lattice πΎ. (Contributed by NM, 3-Dec-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΉ β (πΌβπ) β (πΉ β π β§ (π βπΉ) β€ π))) | ||
| Theorem | diafn 39900* | Functionality and domain of the partial isomorphism A. (Contributed by NM, 26-Nov-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΌ Fn {π₯ β π΅ β£ π₯ β€ π}) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |