![]() |
Metamath
Proof Explorer Theorem List (p. 397 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemc1 39601 | Part of proof of Lemma C in [Crawley] p. 112. TODO: shorten with atmod3i1 39274? (Contributed by NM, 29-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅ β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ ((π β¨ π) β§ π)) = (π β¨ π)) | ||
Theorem | cdlemc2 39602 | Part of proof of Lemma C in [Crawley] p. 112. (Contributed by NM, 25-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β (πΉβπ) β€ ((πΉβπ) β¨ ((π β¨ π) β§ π))) | ||
Theorem | cdlemc3 39603 | Part of proof of Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πΉβπ) β€ (π β¨ (π βπΉ)) β π β€ (π β¨ (πΉβπ)))) | ||
Theorem | cdlemc4 39604 | Part of proof of Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ (πΉβπ))) β (π β¨ (π βπΉ)) β ((πΉβπ) β¨ ((π β¨ π) β§ π))) | ||
Theorem | cdlemc5 39605 | Lemma for cdlemc 39607. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (Β¬ π β€ (π β¨ (πΉβπ)) β§ (πΉβπ) β π)) β (πΉβπ) = ((π β¨ (π βπΉ)) β§ ((πΉβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemc6 39606 | Lemma for cdlemc 39607. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (πΉβπ) = ((π β¨ (π βπΉ)) β§ ((πΉβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemc 39607 | Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ (πΉβπ))) β (πΉβπ) = ((π β¨ (π βπΉ)) β§ ((πΉβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemd1 39608 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π β§ Β¬ π β€ (π β¨ π)))) β π = ((π β¨ ((π β¨ π ) β§ π)) β§ (π β¨ ((π β¨ π ) β§ π)))) | ||
Theorem | cdlemd2 39609 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = (πΊβπ))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd3 39610 | Part of proof of Lemma D in [Crawley] p. 113. The π β π requirement is not mentioned in their proof. (Contributed by NM, 29-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π) β§ π β π)) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π)) | ||
Theorem | cdlemd4 39611 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π) β§ π β π)) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = (πΊβπ))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd5 39612 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = (πΊβπ))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd6 39613 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ Β¬ π β€ (π β¨ (πΉβπ))) β§ (πΉβπ) = (πΊβπ)) β (πΉβπ) = (πΊβπ)) | ||
Theorem | cdlemd7 39614 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = (πΊβπ) β§ Β¬ π β€ (π β¨ (πΉβπ)))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd8 39615 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = π)) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd9 39616 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd 39617 | If two translations agree at any atom not under the fiducial co-atom π, then they are equal. Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β πΉ = πΊ) | ||
Theorem | ltrneq3 39618 | Two translations agree at any atom not under the fiducial co-atom π iff they are equal. (Contributed by NM, 25-Jul-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) = (πΊβπ) β πΉ = πΊ)) | ||
Theorem | cdleme00a 39619 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ Β¬ π β€ (π β¨ π)) β π β π) | ||
Theorem | cdleme0aa 39620 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π΅ = (BaseβπΎ) β β’ (((πΎ β HL β§ π β π») β§ π β π΄ β§ π β π΄) β π β π΅) | ||
Theorem | cdleme0a 39621 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π΄) | ||
Theorem | cdleme0b 39622 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β π β π) | ||
Theorem | cdleme0c 39623 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π ) | ||
Theorem | cdleme0cp 39624 | Part of proof of Lemma E in [Crawley] p. 113. TODO: Reformat as in cdlemg3a 40007- swap consequent equality; make antecedent use df-3an 1087. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄)) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdleme0cq 39625 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π))) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdleme0dN 39626 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π )) β π β π΄) | ||
Theorem | cdleme0e 39627 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π) | ||
Theorem | cdleme0fN 39628 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π΄)) β π β π) | ||
Theorem | cdleme0gN 39629 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π) | ||
Theorem | cdlemeulpq 39630 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) | ||
Theorem | cdleme01N 39631 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β ((π β π β§ π β π β§ π β€ (π β¨ π)) β§ π β€ π)) | ||
Theorem | cdleme02N 39632 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β ((π β¨ π) = (π β¨ π) β§ π β€ π)) | ||
Theorem | cdleme0ex1N 39633* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ π β π) β βπ’ β π΄ (π’ β€ (π β¨ π) β§ π’ β€ π)) | ||
Theorem | cdleme0ex2N 39634* | Part of proof of Lemma E in [Crawley] p. 113. Note that (π β¨ π’) = (π β¨ π’) is a shorter way to express π’ β π β§ π’ β π β§ π’ β€ (π β¨ π). (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β βπ’ β π΄ ((π β¨ π’) = (π β¨ π’) β§ π’ β€ π)) | ||
Theorem | cdleme0moN 39635* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ β*π(π β π΄ β§ (π β¨ π) = (π β¨ π)))) β (π = π β¨ π = π)) | ||
Theorem | cdleme1b 39636 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma showing πΉ is a lattice element. πΉ represents their f(r). (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π΅ = (BaseβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β πΉ β π΅) | ||
Theorem | cdleme1 39637 | Part of proof of Lemma E in [Crawley] p. 113. πΉ represents their f(r). Here we show r β¨ f(r) = r β¨ u (7th through 5th lines from bottom on p. 113). (Contributed by NM, 4-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π))) β (π β¨ πΉ) = (π β¨ π)) | ||
Theorem | cdleme2 39638 | Part of proof of Lemma E in [Crawley] p. 113. πΉ represents f(r). π is the fiducial co-atom (hyperplane) w. Here we show that (r β¨ f(r)) β§ w = u in their notation (4th line from bottom on p. 113). (Contributed by NM, 5-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π))) β ((π β¨ πΉ) β§ π) = π) | ||
Theorem | cdleme3b 39639 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 39646 and cdleme3 39647. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π))) β πΉ β π ) | ||
Theorem | cdleme3c 39640 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 39646 and cdleme3 39647. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ 0 = (0.βπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π))) β πΉ β 0 ) | ||
Theorem | cdleme3d 39641 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 39646 and cdleme3 39647. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ πΉ = ((π β¨ π) β§ (π β¨ π)) | ||
Theorem | cdleme3e 39642 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 39646 and cdleme3 39647. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ (π β¨ π)))) β π β π΄) | ||
Theorem | cdleme3fN 39643 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 39646 and cdleme3 39647. TODO: Delete - duplicates cdleme0e 39627. (Contributed by NM, 6-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π) | ||
Theorem | cdleme3g 39644 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 39646 and cdleme3 39647. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π) | ||
Theorem | cdleme3h 39645 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 39646 and cdleme3 39647. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π΄) | ||
Theorem | cdleme3fa 39646 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 39647. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π΄) | ||
Theorem | cdleme3 39647 | Part of proof of Lemma E in [Crawley] p. 113. πΉ represents f(r). π is the fiducial co-atom (hyperplane) w. Here and in cdleme3fa 39646 above, we show that f(r) β W (4th line from bottom on p. 113), meaning it is an atom and not under w, which in our notation is expressed as πΉ β π΄ β§ Β¬ πΉ β€ π. Their proof provides no details of our lemmas cdleme3b 39639 through cdleme3 39647, so there may be a simpler proof that we have overlooked. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ πΉ β€ π) | ||
Theorem | cdleme4 39648 | Part of proof of Lemma E in [Crawley] p. 113. πΉ and πΊ represent f(s) and fs(r). Here show p β¨ q = r β¨ u at the top of p. 114. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdleme4a 39649 | Part of proof of Lemma E in [Crawley] p. 114 top. πΊ represents fs(r). Auxiliary lemma derived from cdleme5 39650. We show fs(r) β€ p β¨ q. (Contributed by NM, 10-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π΄) β πΊ β€ (π β¨ π)) | ||
Theorem | cdleme5 39650 | Part of proof of Lemma E in [Crawley] p. 113. πΊ represents fs(r). We show r β¨ fs(r)) = p β¨ q at the top of p. 114. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β (π β¨ πΊ) = (π β¨ π)) | ||
Theorem | cdleme6 39651 | Part of proof of Lemma E in [Crawley] p. 113. This expresses (r β¨ fs(r)) β§ w = u at the top of p. 114. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β ((π β¨ πΊ) β§ π) = π) | ||
Theorem | cdleme7aa 39652 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 39658 and cdleme7 39659. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π)) | ||
Theorem | cdleme7a 39653 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 39658 and cdleme7 39659. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ πΊ = ((π β¨ π) β§ (πΉ β¨ π)) | ||
Theorem | cdleme7b 39654 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 39658 and cdleme7 39659. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β π β π΄) | ||
Theorem | cdleme7c 39655 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 39658 and cdleme7 39659. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π) | ||
Theorem | cdleme7d 39656 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 39658 and cdleme7 39659. (Contributed by NM, 8-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΊ β π) | ||
Theorem | cdleme7e 39657 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 39658 and cdleme7 39659. (Contributed by NM, 8-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΊ β (0.βπΎ)) | ||
Theorem | cdleme7ga 39658 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme7 39659. (Contributed by NM, 8-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΊ β π΄) | ||
Theorem | cdleme7 39659 | 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 39658 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 39652 through cdleme7 39659, 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 39660 | 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 39661 | 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 39662 | Utility lemma for Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Oct-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΆ = ((π β¨ π) β§ π) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π»)) β πΆ β π΅) | ||
Theorem | cdleme9 39663 | 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 39664 | 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 39665 | 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 39666 | 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 39667 | 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 39668 | 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 39669 | 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 39670 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 39680. (Contributed by NM, 12-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ (π β¨ π)))) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdleme11c 39671 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 39680. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π) β§ (Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π)) | ||
Theorem | cdleme11dN 39672 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 39680. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β (π β¨ π) β (π β¨ π)) | ||
Theorem | cdleme11e 39673 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 39680. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β πΆ β π·) | ||
Theorem | cdleme11fN 39674 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 39680. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β πΆ) | ||
Theorem | cdleme11g 39675 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 39680. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ π β π) β (π β¨ πΉ) = (π β¨ πΆ)) | ||
Theorem | cdleme11h 39676 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 39680. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π) | ||
Theorem | cdleme11j 39677 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 39680. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΆ β€ (π β¨ πΉ)) | ||
Theorem | cdleme11k 39678 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 39680. (Contributed by NM, 15-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΆ = ((π β¨ πΉ) β§ π)) | ||
Theorem | cdleme11l 39679 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 39680. (Contributed by NM, 15-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β πΉ β πΊ) | ||
Theorem | cdleme11 39680 | 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 39670 through cdleme11 39680, 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 39681 | 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 39682 | 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 39683 | 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 39296 to cdleme13 39682. πΉ and πΊ represent f(s) and f(t) respectively. (Contributed by NM, 8-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β§ (πΉ β¨ πΊ)) β€ (((π β¨ π) β§ (πΊ β¨ π)) β¨ ((π β¨ π) β§ (π β¨ πΉ)))) | ||
Theorem | cdleme15a 39684 | 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 39685 | 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 39686 | 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 39687 | 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 39688 | 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 39689 | 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 39690 | 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 39691 | 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 39692 | 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 39693 | 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 39694 | 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 39695 | 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 39696 | 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 39697 | Lemma leading to cdleme17c 39698. (Contributed by NM, 11-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ πΆ = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ (π β¨ π))) β Β¬ πΆ β€ (π β¨ π)) | ||
Theorem | cdleme17c 39698 | 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 39699 | 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 39700* | 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 39621- which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 38752, 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 β§ π β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π = π β¨ π = π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |