Home | Metamath
Proof Explorer Theorem List (p. 387 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdleme9b 38601 | Utility lemma for Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Oct-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΆ = ((π β¨ π) β§ π) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π»)) β πΆ β π΅) | ||
Theorem | cdleme9 38602 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. πΆ and πΉ represent s1 and f(s) respectively. In their notation, we prove f(s) β¨ s1 = q β¨ s1. (Contributed by NM, 10-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΆ = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉ β¨ πΆ) = (π β¨ πΆ)) | ||
Theorem | cdleme10 38603 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. π· represents s2. In their notation, we prove s β¨ s2 = s β¨ r. (Contributed by NM, 9-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π· = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ π·) = (π β¨ π )) | ||
Theorem | cdleme8tN 38604 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. π represents t1. In their notation, we prove p β¨ t1 = p β¨ t. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdleme9taN 38605 | Part of proof of Lemma E in [Crawley] p. 113. π represents t1, which we prove is an atom. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π΄) | ||
Theorem | cdleme9tN 38606 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. π and πΉ represent t1 and f(t) respectively. In their notation, we prove f(t) β¨ t1 = q β¨ t1. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉ β¨ π) = (π β¨ π)) | ||
Theorem | cdleme10tN 38607 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. π represents t2. In their notation, we prove t β¨ t2 = t β¨ r. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ π) = (π β¨ π )) | ||
Theorem | cdleme16aN 38608 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, s β¨ u β t β¨ u. (Contributed by NM, 9-Oct-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ Β¬ π β€ (π β¨ π))) β (π β¨ π) β (π β¨ π)) | ||
Theorem | cdleme11a 38609 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38619. (Contributed by NM, 12-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ (π β¨ π)))) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdleme11c 38610 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38619. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π)) | ||
Theorem | cdleme11dN 38611 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38619. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β (π β¨ π) β (π β¨ π)) | ||
Theorem | cdleme11e 38612 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38619. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β πΆ β π·) | ||
Theorem | cdleme11fN 38613 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38619. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β πΆ) | ||
Theorem | cdleme11g 38614 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38619. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ π β π) β (π β¨ πΉ) = (π β¨ πΆ)) | ||
Theorem | cdleme11h 38615 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38619. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π) | ||
Theorem | cdleme11j 38616 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38619. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΆ β€ (π β¨ πΉ)) | ||
Theorem | cdleme11k 38617 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38619. (Contributed by NM, 15-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΆ = ((π β¨ πΉ) β§ π)) | ||
Theorem | cdleme11l 38618 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38619. (Contributed by NM, 15-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β πΉ β πΊ) | ||
Theorem | cdleme11 38619 | Part of proof of Lemma E in [Crawley] p. 113, 1st sentence of 3rd paragraph on p. 114. πΉ and πΊ represent f(s) and f(t) respectively. Their proof provides no details of our cdleme11a 38609 through cdleme11 38619, so there may be a simpler proof that we have overlooked. (Contributed by NM, 15-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β (πΉ β¨ πΊ) = (π β¨ π)) | ||
Theorem | cdleme12 38620 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, first part of 3rd sentence. πΉ and πΊ represent f(s) and f(t) respectively. (Contributed by NM, 16-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β ((π β¨ πΉ) β§ (π β¨ πΊ)) = π) | ||
Theorem | cdleme13 38621 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, "<s,t,p> and <f(s),f(t),q> are centrally perspective." πΉ and πΊ represent f(s) and f(t) respectively. (Contributed by NM, 7-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β ((π β¨ πΉ) β§ (π β¨ πΊ)) β€ (π β¨ π)) | ||
Theorem | cdleme14 38622 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, "<s,t,p> and <f(s),f(t),q> ... are axially perspective." We apply dalaw 38235 to cdleme13 38621. πΉ and πΊ represent f(s) and f(t) respectively. (Contributed by NM, 8-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β§ (πΉ β¨ πΊ)) β€ (((π β¨ π) β§ (πΊ β¨ π)) β¨ ((π β¨ π) β§ (π β¨ πΉ)))) | ||
Theorem | cdleme15a 38623 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, ((s β¨ p) β§ (f(s) β¨ q)) β¨ ((t β¨ p) β§ (f(t) β¨ q))=((p β¨ s1) β§ (q β¨ s1)) β¨ ((p β¨ t1) β§ (q β¨ t1)). We represent f(s), f(t), s1, and t1 with πΉ, πΊ, πΆ, and π respectively. The order of our operations is slightly different. (Contributed by NM, 9-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΆ = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (((π β¨ π) β§ (πΊ β¨ π)) β¨ ((π β¨ π) β§ (π β¨ πΉ))) = (((π β¨ π) β§ (π β¨ π)) β¨ ((π β¨ πΆ) β§ (π β¨ πΆ)))) | ||
Theorem | cdleme15b 38624 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, (p β¨ s1) β§ (q β¨ s1)=s1. We represent s1 with πΆ. (Contributed by NM, 10-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΆ = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ πΆ) β§ (π β¨ πΆ)) = πΆ) | ||
Theorem | cdleme15c 38625 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, ((p β¨ s1) β§ (q β¨ s1)) β¨ ((p β¨ t1) β§ (q β¨ t1))=s1 β¨ t1. πΆ and π represent s1 and t1 respectively. The order of our operations is slightly different. (Contributed by NM, 10-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΆ = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (((π β¨ π) β§ (π β¨ π)) β¨ ((π β¨ πΆ) β§ (π β¨ πΆ))) = (π β¨ πΆ)) | ||
Theorem | cdleme15d 38626 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, s1 β¨ t1 β€ w. πΆ and π represent s1 and t1 respectively. The order of our operations is slightly different. (Contributed by NM, 10-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΆ = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (π β¨ πΆ) β€ π) | ||
Theorem | cdleme15 38627 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, (s β¨ t) β§ (f(s) β¨ f(t)) β€ w. We use πΉ, πΊ for f(s), f(t) respectively. (Contributed by NM, 10-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β§ (πΉ β¨ πΊ)) β€ π) | ||
Theorem | cdleme16b 38628 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, first part of 3rd sentence. πΉ and πΊ represent f(s) and f(t) respectively. It is unclear how this follows from s β¨ u β t β¨ u, as the authors state, and we used a different proof. (Note: the antecedent Β¬ π β€ (π β¨ π) is not used.) (Contributed by NM, 11-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΉ β πΊ) | ||
Theorem | cdleme16c 38629 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, 2nd part of 3rd sentence. πΉ and πΊ represent f(s) and f(t) respectively. We show, in their notation, s β¨ t β¨ f(s) β¨ f(t)=s β¨ t β¨ u. (Contributed by NM, 11-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β¨ (πΉ β¨ πΊ)) = ((π β¨ π) β¨ π)) | ||
Theorem | cdleme16d 38630 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, 3rd part of 3rd sentence. πΉ and πΊ represent f(s) and f(t) respectively. We show, in their notation, (s β¨ t) β§ (f(s) β¨ f(t)) is an atom. (Contributed by NM, 11-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β§ (πΉ β¨ πΊ)) β π΄) | ||
Theorem | cdleme16e 38631 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, 3rd part of 3rd sentence. πΉ and πΊ represent f(s) and f(t) respectively. We show, in their notation, (s β¨ t) β§ (f(s) β¨ f(t))=(s β¨ t) β§ w. (Contributed by NM, 11-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β§ (πΉ β¨ πΊ)) = ((π β¨ π) β§ π)) | ||
Theorem | cdleme16f 38632 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, 3rd part of 3rd sentence. πΉ and πΊ represent f(s) and f(t) respectively. We show, in their notation, (s β¨ t) β§ (f(s) β¨ f(t))=(f(s) β¨ f(t)) β§ w. (Contributed by NM, 11-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β§ (πΉ β¨ πΊ)) = ((πΉ β¨ πΊ) β§ π)) | ||
Theorem | cdleme16g 38633 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, Eq. (1). πΉ and πΊ represent f(s) and f(t) respectively. We show, in their notation, (s β¨ t) β§ w=(f(s) β¨ f(t)) β§ w. (Contributed by NM, 11-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β§ π) = ((πΉ β¨ πΊ) β§ π)) | ||
Theorem | cdleme16 38634 | Part of proof of Lemma E in [Crawley] p. 113, conclusion of 3rd paragraph on p. 114. πΉ and πΊ represent f(s) and f(t) respectively. We show, in their notation, (s β¨ t) β§ w=(f(s) β¨ f(t)) β§ w, whether or not u β€ s β¨ t. (Contributed by NM, 11-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β§ π) = ((πΉ β¨ πΊ) β§ π)) | ||
Theorem | cdleme17a 38635 | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. πΉ, πΊ, and πΆ represent f(s), fs(p), and s1 respectively. We show, in their notation, fs(p)=(p β¨ q) β§ (q β¨ s1). (Contributed by NM, 11-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ πΆ = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β πΊ = ((π β¨ π) β§ (π β¨ πΆ))) | ||
Theorem | cdleme17b 38636 | Lemma leading to cdleme17c 38637. (Contributed by NM, 11-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ πΆ = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ (π β¨ π))) β Β¬ πΆ β€ (π β¨ π)) | ||
Theorem | cdleme17c 38637 | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. πΆ represents s1. We show, in their notation, (p β¨ q) β§ (q β¨ s1)=q. (Contributed by NM, 11-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ πΆ = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β§ (π β¨ πΆ)) = π) | ||
Theorem | cdleme17d1 38638 | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. πΉ, πΊ represent f(s), fs(p) respectively. We show, in their notation, fs(p)=q. (Contributed by NM, 11-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β πΊ = π) | ||
Theorem | cdleme0nex 38639* | Part of proof of Lemma E in [Crawley] p. 114, 4th line of 4th paragraph. Whenever (in their terminology) p β¨ q/0 (i.e. the sublattice from 0 to p β¨ q) contains precisely three atoms, any atom not under w must equal either p or q. (In case of 3 atoms, one of them must be u - see cdleme0a 38560- which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 37691, our (π β¨ π) = (π β¨ π) is a shorter way to express π β π β§ π β π β§ π β€ (π β¨ π). Thus, the negated existential condition states there are no atoms different from p or q that are also not under w. (Contributed by NM, 12-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π = π β¨ π = π)) | ||
Theorem | cdleme18a 38640 | Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph. πΉ, πΊ represent f(s), fs(q) respectively. We show Β¬ fs(q) β€ w. (Contributed by NM, 12-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ πΊ β€ π) | ||
Theorem | cdleme18b 38641 | Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph. πΉ, πΊ represent f(s), fs(q) respectively. We show Β¬ fs(q) β q. (Contributed by NM, 12-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΊ β π) | ||
Theorem | cdleme18c 38642* | Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph. πΉ, πΊ represent f(s), fs(q) respectively. We show Β¬ fs(q) = p whenever p β¨ q has three atoms under it (implied by the negated existential condition). (Contributed by NM, 10-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β πΊ = π) | ||
Theorem | cdleme22gb 38643 | Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π΅ = (BaseβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β πΊ β π΅) | ||
Theorem | cdleme18d 38644* | Part of proof of Lemma E in [Crawley] p. 114, 4th sentence of 4th paragraph. πΉ, πΊ, π·, πΈ represent f(s), fs(r), f(t), ft(r) respectively. We show fs(r) = ft(r) for all possible r (which must equal p or q in the case of exactly 3 atoms in p β¨ q/0 , i.e., when Β¬ βπ β π΄...). (Contributed by NM, 12-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β πΊ = πΈ) | ||
Theorem | cdlemesner 38645 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π ) | ||
Theorem | cdlemedb 38646 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. π· represents s2. (Contributed by NM, 20-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π· = ((π β¨ π) β§ π) & β’ π΅ = (BaseβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄)) β π· β π΅) | ||
Theorem | cdlemeda 38647 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. π· represents s2. (Contributed by NM, 13-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π· = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π· β π΄) | ||
Theorem | cdlemednpq 38648 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. π· represents s2. (Contributed by NM, 18-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π· = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β Β¬ π· β€ (π β¨ π)) | ||
Theorem | cdlemednuN 38649 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. π· represents s2. (Contributed by NM, 18-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π· β π) | ||
Theorem | cdleme20zN 38650 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π ) β§ π) = (0.βπΎ)) | ||
Theorem | cdleme20y 38651 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (Proof shortened by OpenAI, 25-Mar-2020.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π ) β§ (π β¨ π )) = π ) | ||
Theorem | cdleme19a 38652 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line. π· represents s2. In their notation, we prove that if r β€ s β¨ t, then s2=(s β¨ t) β§ w. (Contributed by NM, 13-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β π· = ((π β¨ π) β§ π)) | ||
Theorem | cdleme19b 38653 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line. π·, πΉ, πΊ represent s2, f(s), f(t). In their notation, we prove that if r β€ s β¨ t, then s2 β€ f(s) β¨ f(t). (Contributed by NM, 13-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)))) β π· β€ (πΉ β¨ πΊ)) | ||
Theorem | cdleme19c 38654 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line. π·, πΉ represent s2, f(s). We prove f(s) β s2. (Contributed by NM, 13-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π·) | ||
Theorem | cdleme19d 38655 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114. π·, πΉ, πΊ represent s2, f(s), f(t). We prove f(s) β¨ s2 = f(s) β¨ f(t). (Contributed by NM, 14-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)))) β (πΉ β¨ π·) = (πΉ β¨ πΊ)) | ||
Theorem | cdleme19e 38656 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, line 2. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t). We prove f(s) β¨ s2=f(t) β¨ t2. (Contributed by NM, 14-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)))) β (πΉ β¨ π·) = (πΊ β¨ π)) | ||
Theorem | cdleme19f 38657 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, line 3. π·, πΉ, π, π, πΊ, π represent s2, f(s), fs(r), t2, f(t), ft(r). We prove that if r β€ s β¨ t, then ft(r) = ft(r). (Contributed by NM, 14-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)))) β π = π) | ||
Theorem | cdleme20aN 38658 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t). (Contributed by NM, 14-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β (π β¨ π·) = (((π β¨ π ) β¨ π) β§ π)) | ||
Theorem | cdleme20bN 38659 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t). We show v β¨ s2 = v β¨ t2. (Contributed by NM, 15-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β (π β¨ π·) = (π β¨ π)) | ||
Theorem | cdleme20c 38660 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t). (Contributed by NM, 15-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β (π· β¨ π) = (((π β¨ π) β¨ π) β§ π)) | ||
Theorem | cdleme20d 38661 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t). (Contributed by NM, 17-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)) β§ π β€ (π β¨ π))) β ((πΉ β¨ πΊ) β§ (π· β¨ π)) = π) | ||
Theorem | cdleme20e 38662 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, 4th line. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t). We show <f(s),s2,s> and <f(t),t2,t> are centrally perspective. (Contributed by NM, 17-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)) β§ π β€ (π β¨ π))) β ((πΉ β¨ πΊ) β§ (π· β¨ π)) β€ (π β¨ π)) | ||
Theorem | cdleme20f 38663 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, 4th line. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t). We show <f(s),s2,s> and <f(t),t2,t> are axially perspective. (Contributed by NM, 17-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)) β§ π β€ (π β¨ π))) β ((πΉ β¨ π·) β§ (πΊ β¨ π)) β€ (((π· β¨ π) β§ (π β¨ π)) β¨ ((π β¨ πΉ) β§ (π β¨ πΊ)))) | ||
Theorem | cdleme20g 38664 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t). (Contributed by NM, 18-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)) β§ π β€ (π β¨ π))) β (((π· β¨ π) β§ (π β¨ π)) β¨ ((π β¨ πΉ) β§ (π β¨ πΊ))) = (((π β¨ π ) β§ (π β¨ π )) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | cdleme20h 38665 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t). (Contributed by NM, 18-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)))) β (((π β¨ π ) β§ (π β¨ π )) β¨ ((π β¨ π) β§ (π β¨ π))) = (π β¨ π)) | ||
Theorem | cdleme20i 38666 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t). We show (f(s) β¨ s2) β§ (f(t) β¨ t2) β€ p β¨ q. (Contributed by NM, 18-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)))) β ((πΉ β¨ π·) β§ (πΊ β¨ π)) β€ (π β¨ π)) | ||
Theorem | cdleme20j 38667 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t). We show s2 β t2. (Contributed by NM, 18-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ Β¬ π β€ (π β¨ π))) β π· β π) | ||
Theorem | cdleme20k 38668 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t). (Contributed by NM, 20-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ π β π΄ β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β (πΉ β¨ π·) β (π β¨ π)) | ||
Theorem | cdleme20l1 38669 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t) respectively. (Contributed by NM, 20-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β (πΉ β¨ π·) β (LLinesβπΎ)) | ||
Theorem | cdleme20l2 38670 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t) respectively. (Contributed by NM, 20-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)))) β ((πΉ β¨ π·) β§ (πΊ β¨ π)) β π΄) | ||
Theorem | cdleme20l 38671 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. π·, πΉ, π, πΊ represent s2, f(s), t2, f(t) respectively. (Contributed by NM, 20-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)))) β ((πΉ β¨ π·) β§ (πΊ β¨ π)) = ((π β¨ π) β§ (πΉ β¨ π·))) | ||
Theorem | cdleme20m 38672 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. π·, πΉ, π, π, πΊ, π represent s2, f(s), fs(r), t2, f(t), ft(r) respectively. We prove that if Β¬ r β€ s β¨ t and Β¬ u β€ s β¨ t, then fs(r) = ft(r). (Contributed by NM, 20-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)))) β π = π) | ||
Theorem | cdleme20 38673 | Combine cdleme19f 38657 and cdleme20m 38672 to eliminate Β¬ π β€ (π β¨ π) condition. (Contributed by NM, 28-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ Β¬ π β€ (π β¨ π))) β π = π) | ||
Theorem | cdleme21a 38674 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ (π β¨ π)) β§ (π§ β π΄ β§ (π β¨ π§) = (π β¨ π§))) β π β π§) | ||
Theorem | cdleme21b 38675 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π β§ Β¬ π β€ (π β¨ π)) β§ (π§ β π΄ β§ (π β¨ π§) = (π β¨ π§))) β Β¬ π§ β€ (π β¨ π)) | ||
Theorem | cdleme21c 38676 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π΄ β§ π β π β§ Β¬ π β€ (π β¨ π)) β§ (π§ β π΄ β§ (π β¨ π§) = (π β¨ π§))) β Β¬ π β€ (π β¨ π§)) | ||
Theorem | cdleme21at 38677 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ π β π β§ Β¬ π β€ (π β¨ π)) β§ π β€ (π β¨ π)) β§ (π§ β π΄ β§ (π β¨ π§) = (π β¨ π§))) β π β π§) | ||
Theorem | cdleme21ct 38678 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β§ ((π§ β π΄ β§ Β¬ π§ β€ π) β§ (π β¨ π§) = (π β¨ π§))) β Β¬ π β€ (π β¨ π§)) | ||
Theorem | cdleme21d 38679 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 115, 3rd line. π·, πΉ, π, πΈ, π΅, π represent s2, f(s), fs(r), z2, f(z), fz(r) respectively. We prove fs(r) = fz(r). (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π΅ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ πΈ = ((π β¨ π§) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (π΅ β¨ πΈ)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ ((π§ β π΄ β§ Β¬ π§ β€ π) β§ (π β¨ π§) = (π β¨ π§)))) β π = π) | ||
Theorem | cdleme21e 38680 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 115, 3rd line. π, πΊ, π, πΈ, π΅, π represent s2, f(s), fs(r), z2, f(z), fz(r) respectively. We prove that if u β€ s β¨ z, then ft(r) = fz(r). (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π΅ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ πΈ = ((π β¨ π§) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (π΅ β¨ πΈ)) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ ((π§ β π΄ β§ Β¬ π§ β€ π) β§ (π β¨ π§) = (π β¨ π§)))) β π = π) | ||
Theorem | cdleme21f 38681 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π΅ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ πΈ = ((π β¨ π§) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (π΅ β¨ πΈ)) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ ((π§ β π΄ β§ Β¬ π§ β€ π) β§ (π β¨ π§) = (π β¨ π§)))) β π = π) | ||
Theorem | cdleme21g 38682 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ ((π§ β π΄ β§ Β¬ π§ β€ π) β§ (π β¨ π§) = (π β¨ π§)))) β π = π) | ||
Theorem | cdleme21h 38683* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)))) β (βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§)) β π = π)) | ||
Theorem | cdleme21i 38684* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)))) β (βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)) β π = π)) | ||
Theorem | cdleme21j 38685* | Combine cdleme20 38673 and cdleme21i 38684 to eliminate π β€ (π β¨ π) condition. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π = π) | ||
Theorem | cdleme21 38686 | Part of proof of Lemma E in [Crawley] p. 113, 3rd line on p. 115. π·, πΉ, π, π, πΊ, π represent s2, f(s), fs(r), t2, f(t), ft(r) respectively. Combine cdleme18d 38644 and cdleme21j 38685 to eliminate existence condition, proving fs(r) = ft(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)))) β π = π) | ||
Theorem | cdleme21k 38687 | Eliminate π β π condition in cdleme21 38686. (Contributed by NM, 26-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)))) β π = π) | ||
Theorem | cdleme22aa 38688 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 3rd line on p. 115. Show that t β¨ v = p β¨ q implies v = u. (Contributed by NM, 2-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π) β§ (π β π΄ β§ π β€ π β§ π β€ (π β¨ π))) β π = π) | ||
Theorem | cdleme22a 38689 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 3rd line on p. 115. Show that t β¨ v = p β¨ q implies v = u. (Contributed by NM, 30-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π΄) β§ ((π β π΄ β§ π β€ π) β§ π β π β§ (π β¨ π) = (π β¨ π))) β π = π) | ||
Theorem | cdleme22b 38690 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t β¨ v =/= p β¨ q and s β€ p β¨ q implies Β¬ t β€ p β¨ q. (Contributed by NM, 2-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π β π΄ β§ ((π β¨ π) β (π β¨ π) β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)))) β Β¬ π β€ (π β¨ π)) | ||
Theorem | cdleme22cN 38691 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t β¨ v =/= p β¨ q and s β€ p β¨ q implies Β¬ v β€ p β¨ q. (Contributed by NM, 3-Dec-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β π) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) β (π β¨ π))) β Β¬ π β€ (π β¨ π)) | ||
Theorem | cdleme22d 38692 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ π β€ (π β¨ π))) β π = ((π β¨ π) β§ π)) | ||
Theorem | cdleme22e 38693 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. πΉ, π, π represent f(z), fz(s), fz(t) respectively. When t β¨ v = p β¨ q, fz(s) β€ fz(t) β¨ v. (Contributed by NM, 6-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π§) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π΄)) β§ ((π β π΄ β§ π β€ π) β§ (π β π β§ (π β¨ π) = (π β¨ π)) β§ (π§ β π΄ β§ Β¬ π§ β€ π))) β π β€ (π β¨ π)) | ||
Theorem | cdleme22eALTN 38694 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. πΉ, π, π represent f(z), fz(s), fz(t) respectively. When t β¨ v = p β¨ q, fz(s) β€ fz(t) β¨ v. (Contributed by NM, 6-Dec-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π¦ β¨ π) β§ (π β¨ ((π β¨ π¦) β§ π))) & β’ πΊ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π¦) β§ π))) & β’ π = ((π β¨ π) β§ (πΊ β¨ ((π β¨ π§) β§ π))) β β’ (((πΎ β HL β§ π β π» β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ (π β π΄ β§ (π β π΄ β§ π β€ π β§ (π β¨ π) = (π β¨ π)) β§ ((π¦ β π΄ β§ Β¬ π¦ β€ π) β§ (π§ β π΄ β§ Β¬ π§ β€ π)))) β π β€ (π β¨ π)) | ||
Theorem | cdleme22f 38695 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. πΉ, π represent f(t), ft(s) respectively. If s β€ t β¨ v, then ft(s) β€ f(t) β¨ v. (Contributed by NM, 6-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ π β€ (π β¨ π))) β π β€ (πΉ β¨ π)) | ||
Theorem | cdleme22f2 38696 | Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 38695 with s and t swapped (this case is not mentioned by them). If s β€ t β¨ v, then f(s) β€ fs(t) β¨ v. (Contributed by NM, 7-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π)) β§ (π β π΄ β§ π β€ π))) β πΉ β€ (π β¨ π)) | ||
Theorem | cdleme22g 38697 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. πΉ, πΊ represent f(s), f(t) respectively. If s β€ t β¨ v and Β¬ s β€ p β¨ q, then f(s) β€ f(t) β¨ v. (Contributed by NM, 6-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π)) β§ (π β π΄ β§ π β€ π))) β πΉ β€ (πΊ β¨ π)) | ||
Theorem | cdleme23a 38698 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ (π β§ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π β§ (π β¨ (π β§ π)) = π β§ (π β¨ (π β§ π)) = π)) β π β€ π) | ||
Theorem | cdleme23b 38699 | Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ (π β§ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π β§ (π β¨ (π β§ π)) = π β§ (π β¨ (π β§ π)) = π)) β π β π΄) | ||
Theorem | cdleme23c 38700 | Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ (π β§ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π β§ (π β¨ (π β§ π)) = π β§ (π β¨ (π β§ π)) = π)) β π β€ (π β¨ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |