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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdleme24 38701* | Quantified version of cdleme21k 38687. (Contributed by NM, 26-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (πΊ β¨ ((π β¨ π‘) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π))) β βπ β π΄ βπ‘ β π΄ (((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π))) β π = π)) | ||
Theorem | cdleme25a 38702* | Lemma for cdleme25b 38703. (Contributed by NM, 1-Jan-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π))) β βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ π β π΅)) | ||
Theorem | cdleme25b 38703* | Transform cdleme24 38701. TODO get rid of $d's on π, π (Contributed by NM, 1-Jan-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π))) β βπ’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β π’ = π)) | ||
Theorem | cdleme25c 38704* | Transform cdleme25b 38703. (Contributed by NM, 1-Jan-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π))) β β!π’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β π’ = π)) | ||
Theorem | cdleme25dN 38705* | Transform cdleme25c 38704. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π))) β β!π’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ π’ = π)) | ||
Theorem | cdleme25cl 38706* | Show closure of the unique element in cdleme25c 38704. (Contributed by NM, 2-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) & β’ πΌ = (β©π’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β π’ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π))) β πΌ β π΅) | ||
Theorem | cdleme25cv 38707* | Change bound variables in cdleme25c 38704. (Contributed by NM, 2-Feb-2013.) |
β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π ) β§ π))) & β’ πΊ = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (πΊ β¨ ((π β¨ π§) β§ π))) & β’ πΌ = (β©π’ β π΅ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β π’ = π)) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) β β’ πΌ = πΈ | ||
Theorem | cdleme26e 38708* | 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 38709* | 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 38710* | 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 38711* | 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 38712* | 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 38713* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 38711 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 38714* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 38711 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 38715* | 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 38716* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 38712 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 38717* | Lemma for cdleme27N 38718. (Contributed by NM, 3-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) β β’ (π = π‘ β πΆ = π) | ||
Theorem | cdleme27N 38718* | Part of proof of Lemma E in [Crawley] p. 113. Eliminate the π β π‘ antecedent in cdleme27a 38716. (Contributed by NM, 3-Feb-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) β β’ ((((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β€ (π‘ β¨ π) β§ (π β π΄ β§ π β€ π))) β πΆ β€ (π β¨ π)) | ||
Theorem | cdleme28a 38719* | Lemma for cdleme25b 38703. TODO: FIX COMMENT. (Contributed by NM, 4-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) & β’ π = ((π β¨ π‘) β§ (π β§ π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β π‘ β§ ((π β¨ (π β§ π)) = π β§ (π‘ β¨ (π β§ π)) = π) β§ (π β π΅ β§ Β¬ π β€ π))) β (πΆ β¨ (π β§ π)) β€ (π β¨ (π β§ π))) | ||
Theorem | cdleme28b 38720* | Lemma for cdleme25b 38703. TODO: FIX COMMENT. (Contributed by NM, 6-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ (π β π‘ β§ ((π β¨ (π β§ π)) = π β§ (π‘ β¨ (π β§ π)) = π) β§ (π β π΅ β§ Β¬ π β€ π))) β (πΆ β¨ (π β§ π)) = (π β¨ (π β§ π))) | ||
Theorem | cdleme28c 38721* | Part of proof of Lemma E in [Crawley] p. 113. Eliminate the π β π‘ antecedent in cdleme28b 38720. TODO: FIX COMMENT. (Contributed by NM, 6-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π)) β§ ((π β¨ (π β§ π)) = π β§ (π‘ β¨ (π β§ π)) = π β§ (π β π΅ β§ Β¬ π β€ π))) β (πΆ β¨ (π β§ π)) = (π β¨ (π β§ π))) | ||
Theorem | cdleme28 38722* | Quantified version of cdleme28c 38721. (Compare cdleme24 38701.) (Contributed by NM, 7-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΊ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π‘ β¨ π§) β§ π))) & β’ πΈ = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ π = if(π‘ β€ (π β¨ π), πΈ, πΊ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β βπ β π΄ βπ‘ β π΄ (((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (Β¬ π‘ β€ π β§ (π‘ β¨ (π β§ π)) = π)) β (πΆ β¨ (π β§ π)) = (π β¨ (π β§ π)))) | ||
Theorem | cdleme29ex 38723* | Lemma for cdleme29b 38724. (Compare cdleme25a 38702.) TODO: FIX COMMENT. (Contributed by NM, 7-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β§ (πΆ β¨ (π β§ π)) β π΅)) | ||
Theorem | cdleme29b 38724* | Transform cdleme28 38722. (Compare cdleme25b 38703.) TODO: FIX COMMENT. (Contributed by NM, 7-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β βπ£ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π£ = (πΆ β¨ (π β§ π)))) | ||
Theorem | cdleme29c 38725* | Transform cdleme28b 38720. (Compare cdleme25c 38704.) TODO: FIX COMMENT. (Contributed by NM, 8-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β β!π£ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π£ = (πΆ β¨ (π β§ π)))) | ||
Theorem | cdleme29cl 38726* | Show closure of the unique element in cdleme28c 38721. (Contributed by NM, 8-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π§ β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π§) β§ π))) & β’ π· = (β©π’ β π΅ βπ§ β π΄ ((Β¬ π§ β€ π β§ Β¬ π§ β€ (π β¨ π)) β π’ = π)) & β’ πΆ = if(π β€ (π β¨ π), π·, πΉ) & β’ πΌ = (β©π£ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π£ = (πΆ β¨ (π β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΅ β§ Β¬ π β€ π)) β πΌ β π΅) | ||
Theorem | cdleme30a 38727 | 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 38728* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.) |
β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΆ = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π§ = (π β¨ (π β§ π)))) β β’ (π β π΅ β β¦π / π₯β¦π = πΆ) | ||
Theorem | cdleme31sn 38729* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ πΆ = if(π β€ (π β¨ π), β¦π / π β¦πΌ, β¦π / π β¦π·) β β’ (π β π΄ β β¦π / π β¦π = πΆ) | ||
Theorem | cdleme31sn1 38730* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ πΆ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = β¦π / π β¦πΊ)) β β’ ((π β π΄ β§ π β€ (π β¨ π)) β β¦π / π β¦π = πΆ) | ||
Theorem | cdleme31se 38731* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π· β¨ ((π β¨ π) β§ π))) β β’ (π β π΄ β β¦π / π β¦πΈ = π) | ||
Theorem | cdleme31se2 38732* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 3-Apr-2013.) |
β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (β¦π / π‘β¦π· β¨ ((π β¨ π) β§ π))) β β’ (π β π΄ β β¦π / π‘β¦πΈ = π) | ||
Theorem | cdleme31sc 38733* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) |
β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (π β π΄ β β¦π / π β¦πΆ = π) | ||
Theorem | cdleme31sde 38734* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) |
β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((π β π΄ β§ π β π΄) β β¦π / π β¦β¦π / π‘β¦πΈ = π) | ||
Theorem | cdleme31snd 38735* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Apr-2013.) |
β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ (π β π΄ β β¦π / π£β¦β¦π / π‘β¦π· = πΈ) | ||
Theorem | cdleme31sdnN 38736* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) (New usage is discouraged.) |
β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ π = if(π β€ (π β¨ π), πΌ, β¦π / π‘β¦π·) | ||
Theorem | cdleme31sn1c 38737* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 1-Mar-2013.) |
β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΆ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) β β’ ((π β π΄ β§ π β€ (π β¨ π)) β β¦π / π β¦π = πΆ) | ||
Theorem | cdleme31sn2 38738* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ ((π β π΄ β§ Β¬ π β€ (π β¨ π)) β β¦π / π β¦π = πΆ) | ||
Theorem | cdleme31fv 38739* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.) |
β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ πΆ = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π§ = (π β¨ (π β§ π)))) β β’ (π β π΅ β (πΉβπ) = if((π β π β§ Β¬ π β€ π), πΆ, π)) | ||
Theorem | cdleme31fv1 38740* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.) |
β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ πΆ = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π§ = (π β¨ (π β§ π)))) β β’ ((π β π΅ β§ (π β π β§ Β¬ π β€ π)) β (πΉβπ) = πΆ) | ||
Theorem | cdleme31fv1s 38741* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.) |
β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((π β π΅ β§ (π β π β§ Β¬ π β€ π)) β (πΉβπ) = β¦π / π₯β¦π) | ||
Theorem | cdleme31fv2 38742* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 23-Feb-2013.) |
β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((π β π΅ β§ Β¬ (π β π β§ Β¬ π β€ π)) β (πΉβπ) = π) | ||
Theorem | cdleme31id 38743* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 18-Apr-2013.) |
β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((π β π΅ β§ π = π) β (πΉβπ) = π) | ||
Theorem | cdlemefrs29pre00 38744 | ***START OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW*** FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 38379. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π) β§ π β π΄) β (((Β¬ π β€ π β§ π) β§ (π β¨ (π β§ π)) = π ) β (Β¬ π β€ π β§ (π β¨ (π β§ π)) = π ))) | ||
Theorem | cdlemefrs29bpre0 38745* | TODO fix comment. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β (βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π))) β π§ = β¦π / π β¦π)) | ||
Theorem | cdlemefrs29bpre1 38746* | TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π β¦π β π΅) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β βπ§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) | ||
Theorem | cdlemefrs29cpre1 38747* | TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π β¦π β π΅) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β!π§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) | ||
Theorem | cdlemefrs29clN 38748* | TODO: NOT USED? Show closure of the unique element in cdlemefrs29cpre1 38747. (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π β¦π β π΅) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β π β π΅) | ||
Theorem | cdlemefrs32fva 38749* | 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 38379 here and elsewhere, and presence/absence of π β€ (π β¨ π) term. Also, why can proof be shortened with cdleme29cl 38726? What is difference from cdlemefs27cl 38762? (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π β¦π β π΅) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π₯β¦π = β¦π / π β¦π) | ||
Theorem | cdlemefrs32fva1 38750* | 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 38751* | Lemma for cdlemefs29bpre1N 38766. (Compare cdleme25a 38702.) 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 38752 | 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 38753* | Show that β¦π / π β¦π is an atom not under π when Β¬ π β€ (π β¨ π). (Contributed by NM, 28-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (β¦π / π β¦π β π΄ β§ Β¬ β¦π / π β¦π β€ π)) | ||
Theorem | cdlemefr32snb 38754* | Show closure of β¦π / π β¦π. (Contributed by NM, 28-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β β¦π / π β¦π β π΅) | ||
Theorem | cdlemefr29bpre0N 38755* | TODO fix comment. (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (βπ β π΄ (((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π))) β π§ = β¦π / π β¦π)) | ||
Theorem | cdlemefr29clN 38756* | Show closure of the unique element in cdleme29c 38725. 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 38757* | Value of β¦π / π β¦π when Β¬ π β€ (π β¨ π). (Contributed by NM, 30-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ ((π β π΄ β§ Β¬ π β€ (π β¨ π)) β β¦π / π β¦π = π) | ||
Theorem | cdlemefr32fvaN 38758* | 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 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βπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβπ ) = β¦π / π β¦π) | ||
Theorem | cdlemefr31fv1 38760* | Value of (πΉβπ ) when Β¬ π β€ (π β¨ π). TODO This may be useful for shortening others that now use riotasv 37307 3d . TODO: FIX COMMENT. (Contributed by NM, 30-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβπ ) = π) | ||
Theorem | cdlemefs29pre00N 38761 | FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 38379. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β§ π β π΄) β (((Β¬ π β€ π β§ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β (Β¬ π β€ π β§ (π β¨ (π β§ π)) = π ))) | ||
Theorem | cdlemefs27cl 38762* | 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 38715 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 38763* | Show that β¦π / π β¦π is an atom not under π when π β€ (π β¨ π). (Contributed by NM, 24-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β (β¦π / π β¦π β π΄ β§ Β¬ β¦π / π β¦π β€ π)) | ||
Theorem | cdlemefs32snb 38764* | Show closure of β¦π / π β¦π. (Contributed by NM, 24-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β β¦π / π β¦π β π΅) | ||
Theorem | cdlemefs29bpre0N 38765* | TODO: FIX COMMENT. (Contributed by NM, 26-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β (βπ β π΄ (((Β¬ π β€ π β§ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π))) β π§ = β¦π / π β¦π)) | ||
Theorem | cdlemefs29bpre1N 38766* | TODO: FIX COMMENT. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β βπ§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) | ||
Theorem | cdlemefs29cpre1N 38767* | TODO: FIX COMMENT. (Contributed by NM, 26-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β β!π§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) | ||
Theorem | cdlemefs29clN 38768* | Show closure of the unique element in cdleme29c 38725. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β π β π΅) | ||
Theorem | cdleme43fsv1snlem 38769* | Value of β¦π / π β¦π when π β€ (π β¨ π). (Contributed by NM, 30-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β β¦π / π β¦π = π) | ||
Theorem | cdleme43fsv1sn 38770* | Value of β¦π / π β¦π when π β€ (π β¨ π). (Contributed by NM, 30-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β β¦π / π β¦π = π) | ||
Theorem | cdlemefs32fvaN 38771* | 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 38379 here and elsewhere, and presence/absence of π β€ (π β¨ π) term. Also, why can proof be shortened with cdleme27cl 38715? What is difference from cdlemefs27cl 38762? (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β β¦π / π₯β¦π = β¦π / π β¦π) | ||
Theorem | cdlemefs32fva1 38772* | 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 38773* |
Value of (πΉβπ
) when π
β€ (π β¨ π).
TODO This may be useful for shortening others that now use riotasv 37307
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 38774* | 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 38775* | 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 38778 instead TODO: FIX COMMENT. (Contributed by NM, 31-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), πΌ, β¦π / π‘β¦π·) β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΉβπ ) = β¦π / π β¦β¦π / π‘β¦πΈ) | ||
Theorem | cdlemefr45 38776* | 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 38777* | Explicit expansion of cdlemefr45 38776. TODO: use to shorten cdlemefr45 38776 uses? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβπ ) = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π)))) | ||
Theorem | cdlemefs45 38778* | 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 38779* | Explicit expansion of cdlemefs45 38778. TODO: use to shorten cdlemefs45 38778 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 38780* | Explicit expansion of cdlemefs45 38778. TODO: use to shorten cdlemefs45 38778 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 38781* | 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 38782* | Show that β¦π / π β¦π is under π β¨ π when π β€ (π β¨ π). (Contributed by NM, 19-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β β¦π / π β¦π β€ (π β¨ π)) | ||
Theorem | cdleme32sn2awN 38783* | 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 38784* | Show that β¦π / π β¦π is an atom not under π. (Contributed by NM, 6-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π))) β (β¦π / π β¦π β π΄ β§ Β¬ β¦π / π β¦π β€ π)) | ||
Theorem | cdleme32snb 38785* | Show closure of β¦π / π β¦π. (Contributed by NM, 1-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π))) β β¦π / π β¦π β π΅) | ||
Theorem | cdleme32fva 38786* | 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 38787* | 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 38788* | 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 38789* | 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 38790* | 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 38791* | 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 | cdleme32c 38792* | 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 | cdleme32d 38793* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ π β€ π) β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | cdleme32e 38794* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΅ β§ π β π΅) β§ Β¬ (π β π β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π β§ π β€ π)) β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | cdleme32f 38795* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΅ β§ π β π΅) β§ Β¬ (π β π β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ π)) β§ π β€ π) β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | cdleme32le 38796* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ π β π΅) β§ π β€ π) β (πΉβπ) β€ (πΉβπ)) | ||
Theorem | cdleme35a 38797 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉ β¨ π) = (π β¨ π)) | ||
Theorem | cdleme35fnpq 38798 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β Β¬ πΉ β€ (π β¨ π)) | ||
Theorem | cdleme35b 38799 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (π β¨ ((π β¨ π ) β§ π)) β€ (π β¨ (π β¨ π))) | ||
Theorem | cdleme35c 38800 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 10-Mar-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (π β¨ πΉ) = (π β¨ ((π β¨ π ) β§ π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |