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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdleme7a 38601 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 38606 and cdleme7 38607. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ πΊ = ((π β¨ π) β§ (πΉ β¨ π)) | ||
Theorem | cdleme7b 38602 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 38606 and cdleme7 38607. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β π β π΄) | ||
Theorem | cdleme7c 38603 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 38606 and cdleme7 38607. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π) | ||
Theorem | cdleme7d 38604 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 38606 and cdleme7 38607. (Contributed by NM, 8-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΊ β π) | ||
Theorem | cdleme7e 38605 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 38606 and cdleme7 38607. (Contributed by NM, 8-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΊ β (0.βπΎ)) | ||
Theorem | cdleme7ga 38606 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme7 38607. (Contributed by NM, 8-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΊ β π΄) | ||
Theorem | cdleme7 38607 | Part of proof of Lemma E in [Crawley] p. 113. πΊ and πΉ represent fs(r) and f(s) respectively. π is the fiducial co-atom (hyperplane) that they call w. Here and in cdleme7ga 38606 above, we show that fs(r) β W (top of p. 114), meaning it is an atom and not under w, which in our notation is expressed as πΊ β π΄ β§ Β¬ πΊ β€ π. (Note that we do not have a symbol for their W.) Their proof provides no details of our cdleme7aa 38600 through cdleme7 38607, so there may be a simpler proof that we have overlooked. (Contributed by NM, 9-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β Β¬ πΊ β€ π) | ||
Theorem | cdleme8 38608 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. πΆ represents s1. In their notation, we prove p β¨ s1 = p β¨ s. (Contributed by NM, 9-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΆ = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β (π β¨ πΆ) = (π β¨ π)) | ||
Theorem | cdleme9a 38609 | Part of proof of Lemma E in [Crawley] p. 113. πΆ represents s1, which we prove is an atom. (Contributed by NM, 10-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΆ = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β πΆ β π΄) | ||
Theorem | cdleme9b 38610 | Utility lemma for Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Oct-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΆ = ((π β¨ π) β§ π) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π»)) β πΆ β π΅) | ||
Theorem | cdleme9 38611 | 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 38612 | 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 38613 | 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 38614 | 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 38615 | 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 38616 | 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 38617 | 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 38618 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38628. (Contributed by NM, 12-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ (π β¨ π)))) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdleme11c 38619 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38628. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π)) | ||
Theorem | cdleme11dN 38620 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38628. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β (π β¨ π) β (π β¨ π)) | ||
Theorem | cdleme11e 38621 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38628. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β πΆ β π·) | ||
Theorem | cdleme11fN 38622 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38628. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β πΆ) | ||
Theorem | cdleme11g 38623 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38628. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ π β π) β (π β¨ πΉ) = (π β¨ πΆ)) | ||
Theorem | cdleme11h 38624 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38628. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π) | ||
Theorem | cdleme11j 38625 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38628. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΆ β€ (π β¨ πΉ)) | ||
Theorem | cdleme11k 38626 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38628. (Contributed by NM, 15-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΆ = ((π β¨ πΉ) β§ π)) | ||
Theorem | cdleme11l 38627 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 38628. (Contributed by NM, 15-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β πΉ β πΊ) | ||
Theorem | cdleme11 38628 | 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 38618 through cdleme11 38628, 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 38629 | 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 38630 | 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 38631 | 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 38244 to cdleme13 38630. πΉ and πΊ represent f(s) and f(t) respectively. (Contributed by NM, 8-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β§ (πΉ β¨ πΊ)) β€ (((π β¨ π) β§ (πΊ β¨ π)) β¨ ((π β¨ π) β§ (π β¨ πΉ)))) | ||
Theorem | cdleme15a 38632 | 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 38633 | 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 38634 | 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 38635 | 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 38636 | 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 38637 | 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 38638 | 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 38639 | 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 38640 | 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 38641 | 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 38642 | 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 38643 | 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 38644 | 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 38645 | Lemma leading to cdleme17c 38646. (Contributed by NM, 11-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ πΆ = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ (π β¨ π))) β Β¬ πΆ β€ (π β¨ π)) | ||
Theorem | cdleme17c 38646 | 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 38647 | 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 38648* | 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 38569- which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 37700, 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 38649 | 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 38650 | 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 38651* | 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 38652 | Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π΅ = (BaseβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β πΊ β π΅) | ||
Theorem | cdleme18d 38653* | 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 38654 | 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 38655 | 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 38656 | 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 38657 | 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 38658 | 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 38659 | 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 38660 | 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 38661 | 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 38662 | 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 38663 | 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 38664 | 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 38665 | 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 38666 | 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 38667 | 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 38668 | 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 38669 | 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 38670 | 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 38671 | 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 38672 | 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 38673 | 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 38674 | 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 38675 | 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 38676 | 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 38677 | 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 38678 | 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 38679 | 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 38680 | 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 38681 | 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 38682 | Combine cdleme19f 38666 and cdleme20m 38681 to eliminate Β¬ π β€ (π β¨ π) condition. (Contributed by NM, 28-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ Β¬ π β€ (π β¨ π))) β π = π) | ||
Theorem | cdleme21a 38683 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ (π β¨ π)) β§ (π§ β π΄ β§ (π β¨ π§) = (π β¨ π§))) β π β π§) | ||
Theorem | cdleme21b 38684 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π β§ Β¬ π β€ (π β¨ π)) β§ (π§ β π΄ β§ (π β¨ π§) = (π β¨ π§))) β Β¬ π§ β€ (π β¨ π)) | ||
Theorem | cdleme21c 38685 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π΄ β§ π β π β§ Β¬ π β€ (π β¨ π)) β§ (π§ β π΄ β§ (π β¨ π§) = (π β¨ π§))) β Β¬ π β€ (π β¨ π§)) | ||
Theorem | cdleme21at 38686 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ π β π β§ Β¬ π β€ (π β¨ π)) β§ π β€ (π β¨ π)) β§ (π§ β π΄ β§ (π β¨ π§) = (π β¨ π§))) β π β π§) | ||
Theorem | cdleme21ct 38687 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β§ ((π§ β π΄ β§ Β¬ π§ β€ π) β§ (π β¨ π§) = (π β¨ π§))) β Β¬ π β€ (π β¨ π§)) | ||
Theorem | cdleme21d 38688 | 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 38689 | 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 38690 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π΅ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ πΈ = ((π β¨ π§) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (π΅ β¨ πΈ)) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ ((π§ β π΄ β§ Β¬ π§ β€ π) β§ (π β¨ π§) = (π β¨ π§)))) β π = π) | ||
Theorem | cdleme21g 38691 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ ((π§ β π΄ β§ Β¬ π§ β€ π) β§ (π β¨ π§) = (π β¨ π§)))) β π = π) | ||
Theorem | cdleme21h 38692* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)))) β (βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§)) β π = π)) | ||
Theorem | cdleme21i 38693* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)))) β (βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)) β π = π)) | ||
Theorem | cdleme21j 38694* | Combine cdleme20 38682 and cdleme21i 38693 to eliminate π β€ (π β¨ π) condition. (Contributed by NM, 29-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π = π) | ||
Theorem | cdleme21 38695 | 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 38653 and cdleme21j 38694 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 38696 | Eliminate π β π condition in cdleme21 38695. (Contributed by NM, 26-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ (πΉ β¨ π·)) & β’ π = ((π β¨ π) β§ (πΊ β¨ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π)))) β π = π) | ||
Theorem | cdleme22aa 38697 | 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 38698 | 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 38699 | 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 38700 | 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 β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β π) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) β (π β¨ π))) β Β¬ π β€ (π β¨ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |