Home | Metamath
Proof Explorer Theorem List (p. 388 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 | cdleme22d 38701 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ π β€ (π β¨ π))) β π = ((π β¨ π) β§ π)) | ||
Theorem | cdleme22e 38702 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. πΉ, π, π represent f(z), fz(s), fz(t) respectively. When t β¨ v = p β¨ q, fz(s) β€ fz(t) β¨ v. (Contributed by NM, 6-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π§) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π΄)) β§ ((π β π΄ β§ π β€ π) β§ (π β π β§ (π β¨ π) = (π β¨ π)) β§ (π§ β π΄ β§ Β¬ π§ β€ π))) β π β€ (π β¨ π)) | ||
Theorem | cdleme22eALTN 38703 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. πΉ, π, π represent f(z), fz(s), fz(t) respectively. When t β¨ v = p β¨ q, fz(s) β€ fz(t) β¨ v. (Contributed by NM, 6-Dec-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π¦ β¨ π) β§ (π β¨ ((π β¨ π¦) β§ π))) & β’ πΊ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π¦) β§ π))) & β’ π = ((π β¨ π) β§ (πΊ β¨ ((π β¨ π§) β§ π))) β β’ (((πΎ β HL β§ π β π» β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ (π β π΄ β§ (π β π΄ β§ π β€ π β§ (π β¨ π) = (π β¨ π)) β§ ((π¦ β π΄ β§ Β¬ π¦ β€ π) β§ (π§ β π΄ β§ Β¬ π§ β€ π)))) β π β€ (π β¨ π)) | ||
Theorem | cdleme22f 38704 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. πΉ, π represent f(t), ft(s) respectively. If s β€ t β¨ v, then ft(s) β€ f(t) β¨ v. (Contributed by NM, 6-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ π β€ π)) β§ (π β π β§ π β€ (π β¨ π))) β π β€ (πΉ β¨ π)) | ||
Theorem | cdleme22f2 38705 | Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 38704 with s and t swapped (this case is not mentioned by them). If s β€ t β¨ v, then f(s) β€ fs(t) β¨ v. (Contributed by NM, 7-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π)) β§ (π β π΄ β§ π β€ π))) β πΉ β€ (π β¨ π)) | ||
Theorem | cdleme22g 38706 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. πΉ, πΊ represent f(s), f(t) respectively. If s β€ t β¨ v and Β¬ s β€ p β¨ q, then f(s) β€ f(t) β¨ v. (Contributed by NM, 6-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π)) β§ (π β π΄ β§ π β€ π))) β πΉ β€ (πΊ β¨ π)) | ||
Theorem | cdleme23a 38707 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ (π β§ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π β§ (π β¨ (π β§ π)) = π β§ (π β¨ (π β§ π)) = π)) β π β€ π) | ||
Theorem | cdleme23b 38708 | Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ (π β§ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π β§ (π β¨ (π β§ π)) = π β§ (π β¨ (π β§ π)) = π)) β π β π΄) | ||
Theorem | cdleme23c 38709 | Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ (π β§ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π β§ (π β¨ (π β§ π)) = π β§ (π β¨ (π β§ π)) = π)) β π β€ (π β¨ π)) | ||
Theorem | cdleme24 38710* | Quantified version of cdleme21k 38696. (Contributed by NM, 26-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (πΊ β¨ ((π β¨ π‘) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π))) β βπ β π΄ βπ‘ β π΄ (((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π))) β π = π)) | ||
Theorem | cdleme25a 38711* | Lemma for cdleme25b 38712. (Contributed by NM, 1-Jan-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π))) β βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ π β π΅)) | ||
Theorem | cdleme25b 38712* | Transform cdleme24 38710. TODO get rid of $d's on π, π (Contributed by NM, 1-Jan-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π))) β βπ’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β π’ = π)) | ||
Theorem | cdleme25c 38713* | Transform cdleme25b 38712. (Contributed by NM, 1-Jan-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π))) β β!π’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β π’ = π)) | ||
Theorem | cdleme25dN 38714* | Transform cdleme25c 38713. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π))) β β!π’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ π’ = π)) | ||
Theorem | cdleme25cl 38715* | Show closure of the unique element in cdleme25c 38713. (Contributed by NM, 2-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) & β’ πΌ = (β©π’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β π’ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π))) β πΌ β π΅) | ||
Theorem | cdleme25cv 38716* | Change bound variables in cdleme25c 38713. (Contributed by NM, 2-Feb-2013.) |
β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) & β’ πΊ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (πΊ β¨ ((π β¨ π§) β§ π))) & β’ πΌ = (β©π’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β π’ = π)) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) β β’ πΌ = πΈ | ||
Theorem | cdleme26e 38717* | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. πΉ, π, π represent f(z), fz(s), fz(t) respectively. When t β¨ v = p β¨ q, fz(s) β€ fz(t) β¨ v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π§) β§ π))) & β’ πΌ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ ((π β¨ π) = (π β¨ π) β§ Β¬ π§ β€ (π β¨ π)) β§ (π§ β π΄ β§ Β¬ π§ β€ π))) β πΌ β€ (πΈ β¨ π)) | ||
Theorem | cdleme26ee 38718* | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. πΉ, π, π represent f(z), fz(s), fz(t) respectively. When t β¨ v = p β¨ q, fz(s) β€ fz(t) β¨ v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π§) β§ π))) & β’ πΌ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ ((π β π β§ π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ (π β¨ π) = (π β¨ π))) β πΌ β€ (πΈ β¨ π)) | ||
Theorem | cdleme26eALTN 38719* | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. πΉ, π, π represent f(z), fz(s), fz(t) respectively. When t β¨ v = p β¨ q, fz(s) β€ fz(t) β¨ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π¦ β¨ π) β§ (π β¨ ((π β¨ π¦) β§ π))) & β’ πΊ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π¦) β§ π))) & β’ π = ((π β¨ π) β§ (πΊ β¨ ((π β¨ π§) β§ π))) & β’ πΌ = (β©π’ β π΅ βπ¦ β π΄ ((Β¬ π¦ β€ π β§ Β¬ π¦ β€ (π β¨ π)) β π’ = π)) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π β§ π β€ (π β¨ π)) β§ (π β π΄ β§ Β¬ π β€ π β§ π β€ (π β¨ π))) β§ ((π β π΄ β§ π β€ π β§ (π β¨ π) = (π β¨ π)) β§ (π¦ β π΄ β§ Β¬ π¦ β€ π β§ Β¬ π¦ β€ (π β¨ π)) β§ (π§ β π΄ β§ Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)))) β πΌ β€ (πΈ β¨ π)) | ||
Theorem | cdleme26fALTN 38720* | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. πΉ, π represent f(t), ft(s) respectively. If t β€ t β¨ v, then ft(s) β€ f(t) β¨ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π’ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π’ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β€ (π β¨ π)) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β§ (π β π‘ β§ π β€ (π‘ β¨ π)) β§ (π β π΄ β§ π β€ π))) β πΌ β€ (πΉ β¨ π)) | ||
Theorem | cdleme26f 38721* | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. πΉ, π represent f(t), ft(s) respectively. If t β€ t β¨ v, then ft(s) β€ f(t) β¨ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π’ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π’ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β€ (π β¨ π)) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (Β¬ π‘ β€ (π β¨ π) β§ (π β π‘ β§ π β€ (π‘ β¨ π)) β§ (π β π΄ β§ π β€ π))) β πΌ β€ (πΉ β¨ π)) | ||
Theorem | cdleme26f2ALTN 38722* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 38720 with s and t swapped (this case is not mentioned by them). If s β€ t β¨ v, then f(s) β€ fs(t) β¨ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΊ β¨ ((π β¨ π ) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β π’ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β€ (π β¨ π)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (π β π β§ π β€ (π β¨ π)) β§ (π β π΄ β§ π β€ π))) β πΊ β€ (πΈ β¨ π)) | ||
Theorem | cdleme26f2 38723* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 38720 with s and t swapped (this case is not mentioned by them). If s β€ t β¨ v, then f(s) β€ fs(t) β¨ v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΊ β¨ ((π β¨ π ) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β π’ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π β§ π β€ (π β¨ π)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (Β¬ π β€ (π β¨ π) β§ (π β π β§ π β€ (π β¨ π)) β§ (π β π΄ β§ π β€ π))) β πΊ β€ (πΈ β¨ π)) | ||
Theorem | cdleme27cl 38724* | Part of proof of Lemma E in [Crawley] p. 113. Closure of πΆ. (Contributed by NM, 6-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π)) β πΆ β π΅) | ||
Theorem | cdleme27a 38725* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 38721 with s and t swapped (this case is not mentioned by them). If s β€ t β¨ v, then f(s) β€ fs(t) β¨ v. TODO: FIX COMMENT. (Contributed by NM, 3-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) β β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ ((π β π‘ β§ π β€ (π‘ β¨ π)) β§ (π β π΄ β§ π β€ π))) β πΆ β€ (π β¨ π)) | ||
Theorem | cdleme27b 38726* | Lemma for cdleme27N 38727. (Contributed by NM, 3-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) β β’ (π = π‘ β πΆ = π) | ||
Theorem | cdleme27N 38727* | Part of proof of Lemma E in [Crawley] p. 113. Eliminate the π β π‘ antecedent in cdleme27a 38725. (Contributed by NM, 3-Feb-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) β β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β πΆ β€ (π β¨ π)) | ||
Theorem | cdleme28a 38728* | Lemma for cdleme25b 38712. TODO: FIX COMMENT. (Contributed by NM, 4-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) & β’ π = ((π β¨ π‘) β§ (π β§ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β π‘ β§ ((π β¨ (π β§ π)) = π β§ (π‘ β¨ (π β§ π)) = π) β§ (π β π΅ β§ Β¬ π β€ π))) β (πΆ β¨ (π β§ π)) β€ (π β¨ (π β§ π))) | ||
Theorem | cdleme28b 38729* | Lemma for cdleme25b 38712. TODO: FIX COMMENT. (Contributed by NM, 6-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β π‘ β§ ((π β¨ (π β§ π)) = π β§ (π‘ β¨ (π β§ π)) = π) β§ (π β π΅ β§ Β¬ π β€ π))) β (πΆ β¨ (π β§ π)) = (π β¨ (π β§ π))) | ||
Theorem | cdleme28c 38730* | Part of proof of Lemma E in [Crawley] p. 113. Eliminate the π β π‘ antecedent in cdleme28b 38729. TODO: FIX COMMENT. (Contributed by NM, 6-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ ((π β¨ (π β§ π)) = π β§ (π‘ β¨ (π β§ π)) = π β§ (π β π΅ β§ Β¬ π β€ π))) β (πΆ β¨ (π β§ π)) = (π β¨ (π β§ π))) | ||
Theorem | cdleme28 38731* | Quantified version of cdleme28c 38730. (Compare cdleme24 38710.) (Contributed by NM, 7-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β βπ β π΄ βπ‘ β π΄ (((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π)) β (πΆ β¨ (π β§ π)) = (π β¨ (π β§ π)))) | ||
Theorem | cdleme29ex 38732* | Lemma for cdleme29b 38733. (Compare cdleme25a 38711.) TODO: FIX COMMENT. (Contributed by NM, 7-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (πΆ β¨ (π β§ π)) β π΅)) | ||
Theorem | cdleme29b 38733* | Transform cdleme28 38731. (Compare cdleme25b 38712.) TODO: FIX COMMENT. (Contributed by NM, 7-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β βπ£ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π£ = (πΆ β¨ (π β§ π)))) | ||
Theorem | cdleme29c 38734* | Transform cdleme28b 38729. (Compare cdleme25c 38713.) TODO: FIX COMMENT. (Contributed by NM, 8-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β β!π£ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π£ = (πΆ β¨ (π β§ π)))) | ||
Theorem | cdleme29cl 38735* | Show closure of the unique element in cdleme28c 38730. (Contributed by NM, 8-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΌ = (β©π£ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π£ = (πΆ β¨ (π β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β πΌ β π΅) | ||
Theorem | cdleme30a 38736 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ (π β π΅ β§ Β¬ π β€ π) β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ π β€ π)) β (π β¨ (π β§ π)) = π) | ||
Theorem | cdleme31so 38737* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.) |
β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΆ = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π§ = (π β¨ (π β§ π)))) β β’ (π β π΅ β β¦π / π₯β¦π = πΆ) | ||
Theorem | cdleme31sn 38738* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ πΆ = if(π β€ (π β¨ π), β¦π / π β¦πΌ, β¦π / π β¦π·) β β’ (π β π΄ β β¦π / π β¦π = πΆ) | ||
Theorem | cdleme31sn1 38739* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ πΆ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = β¦π / π β¦πΊ)) β β’ ((π β π΄ β§ π β€ (π β¨ π)) β β¦π / π β¦π = πΆ) | ||
Theorem | cdleme31se 38740* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π· β¨ ((π β¨ π) β§ π))) β β’ (π β π΄ β β¦π / π β¦πΈ = π) | ||
Theorem | cdleme31se2 38741* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 3-Apr-2013.) |
β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (β¦π / π‘β¦π· β¨ ((π β¨ π) β§ π))) β β’ (π β π΄ β β¦π / π‘β¦πΈ = π) | ||
Theorem | cdleme31sc 38742* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) |
β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (π β π΄ β β¦π / π β¦πΆ = π) | ||
Theorem | cdleme31sde 38743* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) |
β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((π β π΄ β§ π β π΄) β β¦π / π β¦β¦π / π‘β¦πΈ = π) | ||
Theorem | cdleme31snd 38744* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Apr-2013.) |
β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (π β π΄ β β¦π / π£β¦β¦π / π‘β¦π· = πΈ) | ||
Theorem | cdleme31sdnN 38745* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) (New usage is discouraged.) |
β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ π = if(π β€ (π β¨ π), πΌ, β¦π / π‘β¦π·) | ||
Theorem | cdleme31sn1c 38746* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 1-Mar-2013.) |
β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΆ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) β β’ ((π β π΄ β§ π β€ (π β¨ π)) β β¦π / π β¦π = πΆ) | ||
Theorem | cdleme31sn2 38747* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ ((π β π΄ β§ Β¬ π β€ (π β¨ π)) β β¦π / π β¦π = πΆ) | ||
Theorem | cdleme31fv 38748* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.) |
β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ πΆ = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π§ = (π β¨ (π β§ π)))) β β’ (π β π΅ β (πΉβπ) = if((π β π β§ Β¬ π β€ π), πΆ, π)) | ||
Theorem | cdleme31fv1 38749* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.) |
β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ πΆ = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π§ = (π β¨ (π β§ π)))) β β’ ((π β π΅ β§ (π β π β§ Β¬ π β€ π)) β (πΉβπ) = πΆ) | ||
Theorem | cdleme31fv1s 38750* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.) |
β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((π β π΅ β§ (π β π β§ Β¬ π β€ π)) β (πΉβπ) = β¦π / π₯β¦π) | ||
Theorem | cdleme31fv2 38751* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 23-Feb-2013.) |
β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((π β π΅ β§ Β¬ (π β π β§ Β¬ π β€ π)) β (πΉβπ) = π) | ||
Theorem | cdleme31id 38752* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 18-Apr-2013.) |
β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((π β π΅ β§ π = π) β (πΉβπ) = π) | ||
Theorem | cdlemefrs29pre00 38753 | ***START OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW*** FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 38388. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π) β§ π β π΄) β (((Β¬ π β€ π β§ π) β§ (π β¨ (π β§ π)) = π ) β (Β¬ π β€ π β§ (π β¨ (π β§ π)) = π ))) | ||
Theorem | cdlemefrs29bpre0 38754* | TODO fix comment. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β (βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π))) β π§ = β¦π / π β¦π)) | ||
Theorem | cdlemefrs29bpre1 38755* | TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π β¦π β π΅) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β βπ§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) | ||
Theorem | cdlemefrs29cpre1 38756* | TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π β¦π β π΅) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β!π§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) | ||
Theorem | cdlemefrs29clN 38757* | TODO: NOT USED? Show closure of the unique element in cdlemefrs29cpre1 38756. (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π β¦π β π΅) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β π β π΅) | ||
Theorem | cdlemefrs32fva 38758* | Part of proof of Lemma E in [Crawley] p. 113. Value of πΉ at an atom not under π. TODO: FIX COMMENT. TODO: consolidate uses of lhpmat 38388 here and elsewhere, and presence/absence of π β€ (π β¨ π) term. Also, why can proof be shortened with cdleme29cl 38735? What is difference from cdlemefs27cl 38771? (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π β¦π β π΅) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π₯β¦π = β¦π / π β¦π) | ||
Theorem | cdlemefrs32fva1 38759* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π β¦π β π΅) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β (πΉβπ ) = β¦π / π β¦π) | ||
Theorem | cdlemefr29exN 38760* | Lemma for cdlemefs29bpre1N 38775. (Compare cdleme25a 38711.) TODO: FIX COMMENT. TODO: IS THIS NEEDED? (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ βπ β π΄ πΆ β π΅) β βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (πΆ β¨ (π β§ π)) β π΅)) | ||
Theorem | cdlemefr27cl 38761 | Part of proof of Lemma E in [Crawley] p. 113. Closure of π. (Contributed by NM, 23-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ (π β¨ π) β§ π β π)) β π β π΅) | ||
Theorem | cdlemefr32sn2aw 38762* | Show that β¦π / π β¦π is an atom not under π when Β¬ π β€ (π β¨ π). (Contributed by NM, 28-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (β¦π / π β¦π β π΄ β§ Β¬ β¦π / π β¦π β€ π)) | ||
Theorem | cdlemefr32snb 38763* | Show closure of β¦π / π β¦π. (Contributed by NM, 28-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β β¦π / π β¦π β π΅) | ||
Theorem | cdlemefr29bpre0N 38764* | TODO fix comment. (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (βπ β π΄ (((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π))) β π§ = β¦π / π β¦π)) | ||
Theorem | cdlemefr29clN 38765* | Show closure of the unique element in cdleme29c 38734. TODO fix comment. TODO Not needed? (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β π β π΅) | ||
Theorem | cdleme43frv1snN 38766* | Value of β¦π / π β¦π when Β¬ π β€ (π β¨ π). (Contributed by NM, 30-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ ((π β π΄ β§ Β¬ π β€ (π β¨ π)) β β¦π / π β¦π = π) | ||
Theorem | cdlemefr32fvaN 38767* | Part of proof of Lemma E in [Crawley] p. 113. Value of πΉ at an atom not under π. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β β¦π / π₯β¦π = β¦π / π β¦π) | ||
Theorem | cdlemefr32fva1 38768* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβπ ) = β¦π / π β¦π) | ||
Theorem | cdlemefr31fv1 38769* | Value of (πΉβπ ) when Β¬ π β€ (π β¨ π). TODO This may be useful for shortening others that now use riotasv 37316 3d . TODO: FIX COMMENT. (Contributed by NM, 30-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβπ ) = π) | ||
Theorem | cdlemefs29pre00N 38770 | FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 38388. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β§ π β π΄) β (((Β¬ π β€ π β§ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β (Β¬ π β€ π β§ (π β¨ (π β§ π)) = π ))) | ||
Theorem | cdlemefs27cl 38771* | Part of proof of Lemma E in [Crawley] p. 113. Closure of π. TODO FIX COMMENT This is the start of a re-proof of cdleme27cl 38724 etc. with the π β€ (π β¨ π) condition (so as to not have the πΆ hypothesis). (Contributed by NM, 24-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π’ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π’ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ π) β§ π β π)) β π β π΅) | ||
Theorem | cdlemefs32sn1aw 38772* | Show that β¦π / π β¦π is an atom not under π when π β€ (π β¨ π). (Contributed by NM, 24-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β (β¦π / π β¦π β π΄ β§ Β¬ β¦π / π β¦π β€ π)) | ||
Theorem | cdlemefs32snb 38773* | Show closure of β¦π / π β¦π. (Contributed by NM, 24-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β β¦π / π β¦π β π΅) | ||
Theorem | cdlemefs29bpre0N 38774* | TODO: FIX COMMENT. (Contributed by NM, 26-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β (βπ β π΄ (((Β¬ π β€ π β§ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π))) β π§ = β¦π / π β¦π)) | ||
Theorem | cdlemefs29bpre1N 38775* | TODO: FIX COMMENT. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β βπ§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) | ||
Theorem | cdlemefs29cpre1N 38776* | TODO: FIX COMMENT. (Contributed by NM, 26-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β β!π§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) | ||
Theorem | cdlemefs29clN 38777* | Show closure of the unique element in cdleme29c 38734. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β π β π΅) | ||
Theorem | cdleme43fsv1snlem 38778* | Value of β¦π / π β¦π when π β€ (π β¨ π). (Contributed by NM, 30-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β β¦π / π β¦π = π) | ||
Theorem | cdleme43fsv1sn 38779* | Value of β¦π / π β¦π when π β€ (π β¨ π). (Contributed by NM, 30-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β β¦π / π β¦π = π) | ||
Theorem | cdlemefs32fvaN 38780* | Part of proof of Lemma E in [Crawley] p. 113. Value of πΉ at an atom not under π. TODO: FIX COMMENT. TODO: consolidate uses of lhpmat 38388 here and elsewhere, and presence/absence of π β€ (π β¨ π) term. Also, why can proof be shortened with cdleme27cl 38724? What is difference from cdlemefs27cl 38771? (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β β¦π / π₯β¦π = β¦π / π β¦π) | ||
Theorem | cdlemefs32fva1 38781* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β (πΉβπ ) = β¦π / π β¦π) | ||
Theorem | cdlemefs31fv1 38782* |
Value of (πΉβπ
) when π
β€ (π β¨ π).
TODO This may be useful for shortening others that now use riotasv 37316
3d . TODO: FIX COMMENT.
***END OF VALUE AT ATOM STUFF TO REPLACE
ONES BELOW***
"cdleme3xsn1aw" decreased using "cdlemefs32sn1aw" "cdleme32sn1aw" decreased from 3302 to 36 using "cdlemefs32sn1aw". "cdleme32sn2aw" decreased from 1687 to 26 using "cdlemefr32sn2aw". "cdleme32snaw" decreased from 376 to 375 using "cdlemefs32sn1aw". "cdleme32snaw" decreased from 375 to 368 using "cdlemefr32sn2aw". "cdleme35sn3a" decreased from 547 to 523 using "cdleme43frv1sn".(Contributed by NM, 27-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΉβπ ) = π) | ||
Theorem | cdlemefr44 38783* | Value of f(r) when r is an atom not under pq, using more compact hypotheses. TODO: eliminate and use cdlemefr45 instead? TODO: FIX COMMENT. (Contributed by NM, 31-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), πΌ, β¦π / π‘β¦π·) β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβπ ) = β¦π / π‘β¦π·) | ||
Theorem | cdlemefs44 38784* | Value of fs(r) when r is an atom under pq and s is any atom not under pq, using more compact hypotheses. TODO: eliminate and use cdlemefs45 38787 instead TODO: FIX COMMENT. (Contributed by NM, 31-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), πΌ, β¦π / π‘β¦π·) β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΉβπ ) = β¦π / π β¦β¦π / π‘β¦πΈ) | ||
Theorem | cdlemefr45 38785* | Value of f(r) when r is an atom not under pq, using very compact hypotheses. TODO: FIX COMMENT. (Contributed by NM, 1-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβπ ) = β¦π / π‘β¦π·) | ||
Theorem | cdlemefr45e 38786* | Explicit expansion of cdlemefr45 38785. TODO: use to shorten cdlemefr45 38785 uses? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβπ ) = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π)))) | ||
Theorem | cdlemefs45 38787* | Value of fs(r) when r is an atom under pq and s is any atom not under pq, using very compact hypotheses. TODO: FIX COMMENT. (Contributed by NM, 1-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΉβπ ) = β¦π / π β¦β¦π / π‘β¦πΈ) | ||
Theorem | cdlemefs45ee 38788* | Explicit expansion of cdlemefs45 38787. TODO: use to shorten cdlemefs45 38787 uses? Should ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) be assigned to a hypothesis letter? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΉβπ ) = ((π β¨ π) β§ (((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemefs45eN 38789* | Explicit expansion of cdlemefs45 38787. TODO: use to shorten cdlemefs45 38787 uses? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΉβπ ) = ((π β¨ π) β§ ((πΉβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdleme32sn1awN 38790* | Show that β¦π / π β¦π is an atom not under π when π β€ (π β¨ π). (Contributed by NM, 6-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β (β¦π / π β¦π β π΄ β§ Β¬ β¦π / π β¦π β€ π)) | ||
Theorem | cdleme41sn3a 38791* | Show that β¦π / π β¦π is under π β¨ π when π β€ (π β¨ π). (Contributed by NM, 19-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β β¦π / π β¦π β€ (π β¨ π)) | ||
Theorem | cdleme32sn2awN 38792* | Show that β¦π / π β¦π is an atom not under π when Β¬ π β€ (π β¨ π). (Contributed by NM, 6-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (β¦π / π β¦π β π΄ β§ Β¬ β¦π / π β¦π β€ π)) | ||
Theorem | cdleme32snaw 38793* | Show that β¦π / π β¦π is an atom not under π. (Contributed by NM, 6-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π))) β (β¦π / π β¦π β π΄ β§ Β¬ β¦π / π β¦π β€ π)) | ||
Theorem | cdleme32snb 38794* | Show closure of β¦π / π β¦π. (Contributed by NM, 1-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π))) β β¦π / π β¦π β π΅) | ||
Theorem | cdleme32fva 38795* | Part of proof of Lemma D in [Crawley] p. 113. Value of πΉ at an atom not under π. (Contributed by NM, 2-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β β¦π / π₯β¦π = β¦π / π β¦π) | ||
Theorem | cdleme32fva1 38796* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β (πΉβπ ) = β¦π / π β¦π) | ||
Theorem | cdleme32fvaw 38797* | Show that (πΉβπ ) is an atom not under π when π is an atom not under π. (Contributed by NM, 18-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ ) β π΄ β§ Β¬ (πΉβπ ) β€ π)) | ||
Theorem | cdleme32fvcl 38798* | Part of proof of Lemma D in [Crawley] p. 113. Closure of the function πΉ. (Contributed by NM, 10-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π΅) β (πΉβπ) β π΅) | ||
Theorem | cdleme32a 38799* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π)) β (πΉβπ) = (π β¨ (π β§ π))) | ||
Theorem | cdleme32b 38800* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π β§ π β€ π)) β (πΉβπ) = (π β¨ (π β§ π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |