![]() |
Metamath
Proof Explorer Theorem List (p. 391 of 475) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-29964) |
![]() (29965-31487) |
![]() (31488-47412) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemefr44 39001* | 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 39002* | 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 39005 instead TODO: FIX COMMENT. (Contributed by NM, 31-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), πΌ, β¦π / π‘β¦π·) β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΉβπ ) = β¦π / π β¦β¦π / π‘β¦πΈ) | ||
Theorem | cdlemefr45 39003* | 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 39004* | Explicit expansion of cdlemefr45 39003. TODO: use to shorten cdlemefr45 39003 uses? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβπ ) = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π)))) | ||
Theorem | cdlemefs45 39005* | 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 39006* | Explicit expansion of cdlemefs45 39005. TODO: use to shorten cdlemefs45 39005 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 39007* | Explicit expansion of cdlemefs45 39005. TODO: use to shorten cdlemefs45 39005 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 39008* | 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 39009* | Show that β¦π / π β¦π is under π β¨ π when π β€ (π β¨ π). (Contributed by NM, 19-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β β¦π / π β¦π β€ (π β¨ π)) | ||
Theorem | cdleme32sn2awN 39010* | 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 39011* | Show that β¦π / π β¦π is an atom not under π. (Contributed by NM, 6-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π))) β (β¦π / π β¦π β π΄ β§ Β¬ β¦π / π β¦π β€ π)) | ||
Theorem | cdleme32snb 39012* | Show closure of β¦π / π β¦π. (Contributed by NM, 1-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π))) β β¦π / π β¦π β π΅) | ||
Theorem | cdleme32fva 39013* | 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 39014* | 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 39015* | 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 39016* | 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 39017* | 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 39018* | 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 39019* | 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 39020* | 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 39021* | 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 39022* | 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 39023* | 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 39024 | 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 39025 | 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 39026 | 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 39027 | 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 | cdleme35d 39028 | 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 | cdleme35e 39029 | 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 | cdleme35f 39030 | 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 | cdleme35g 39031 | 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 | cdleme35h 39032 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of π β¨ π line. TODO: FIX COMMENT. (Contributed by NM, 11-Mar-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ πΉ = πΊ)) β π = π) | ||
Theorem | cdleme35h2 39033 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of π β¨ π line. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β π)) β πΉ β πΊ) | ||
Theorem | cdleme35sn2aw 39034* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of π β¨ π line case; compare cdleme32sn2awN 39010. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, π·) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β π)) β β¦π / π β¦π β β¦π / π β¦π) | ||
Theorem | cdleme35sn3a 39035* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, π·) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β Β¬ β¦π / π β¦π β€ (π β¨ π)) | ||
Theorem | cdleme36a 39036 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 11-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π))) β Β¬ π β€ (π‘ β¨ πΈ)) | ||
Theorem | cdleme36m 39037 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on π β¨ π line. TODO: FIX COMMENT. (Contributed by NM, 11-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π‘ β¨ πΈ) β§ π) & β’ πΉ = ((π β¨ π) β§ (πΈ β¨ ((π‘ β¨ π ) β§ π))) & β’ πΆ = ((π β¨ π) β§ (πΈ β¨ ((π‘ β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ πΉ = πΆ) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)))) β π = π) | ||
Theorem | cdleme37m 39038 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on π β¨ π line. TODO: FIX COMMENT. (Contributed by NM, 13-Mar-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π· = ((π’ β¨ π) β§ (π β¨ ((π β¨ π’) β§ π))) & β’ π = ((π‘ β¨ πΈ) β§ π) & β’ π = ((π’ β¨ π·) β§ π) & β’ πΆ = ((π β¨ π) β§ (πΈ β¨ ((π‘ β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π· β¨ ((π’ β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β€ (π β¨ π) β§ π β€ (π β¨ π)) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β πΆ = πΊ) | ||
Theorem | cdleme38m 39039 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on π β¨ π line. TODO: FIX COMMENT. (Contributed by NM, 13-Mar-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π· = ((π’ β¨ π) β§ (π β¨ ((π β¨ π’) β§ π))) & β’ π = ((π‘ β¨ πΈ) β§ π) & β’ π = ((π’ β¨ π·) β§ π) & β’ πΉ = ((π β¨ π) β§ (πΈ β¨ ((π‘ β¨ π ) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π· β¨ ((π’ β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ πΉ = πΊ) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β π = π) | ||
Theorem | cdleme38n 39040 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on π β¨ π line. TODO: FIX COMMENT. TODO shorter if proved directly from cdleme36m 39037 and cdleme37m 39038? (Contributed by NM, 14-Mar-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π· = ((π’ β¨ π) β§ (π β¨ ((π β¨ π’) β§ π))) & β’ π = ((π‘ β¨ πΈ) β§ π) & β’ π = ((π’ β¨ π·) β§ π) & β’ πΉ = ((π β¨ π) β§ (πΈ β¨ ((π‘ β¨ π ) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π· β¨ ((π’ β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β πΉ β πΊ) | ||
Theorem | cdleme39a 39041 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on π β¨ π line. TODO: FIX COMMENT. πΈ, π, πΊ, π serve as f(t), f(u), ft(π ), ft(π). Put hypotheses of cdleme38n 39040 in convention of cdleme32sn1awN 39008. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π‘ β¨ πΈ) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β€ (π β¨ π) β§ (π‘ β π΄ β§ Β¬ π‘ β€ π))) β πΊ = ((π β¨ π) β§ (πΈ β¨ ((π‘ β¨ π ) β§ π)))) | ||
Theorem | cdleme39n 39042 | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on π β¨ π line. TODO: FIX COMMENT. πΈ, π, πΊ, π serve as f(t), f(u), ft(π ), ft(π). Put hypotheses of cdleme38n 39040 in convention of cdleme32sn1awN 39008. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ π = ((π’ β¨ π) β§ (π β¨ ((π β¨ π’) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π’) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β πΊ β π) | ||
Theorem | cdleme40m 39043* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on π β¨ π line. TODO: FIX COMMENT Use proof idea from cdleme32sn1awN 39008. (Contributed by NM, 18-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΆ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π β π) β§ (π£ β π΄ β§ Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β β¦π / π β¦π β πΉ) | ||
Theorem | cdleme40n 39044* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on π β¨ π line. TODO: FIX COMMENT. TODO get rid of '.<' class? (Contributed by NM, 18-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΆ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ π = (β©π§ β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π§ = π)) & β’ π = if(π’ β€ (π β¨ π), π, < ) & β’ π = (β©π§ β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π§ = πΉ)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π β π)) β β¦π / π β¦π β β¦π / π’β¦π) | ||
Theorem | cdleme40v 39045* | Part of proof of Lemma E in [Crawley] p. 113. Change bound variables in β¦π / π’β¦π (but we use β¦π / π’β¦π for convenience since we have its hypotheses available). (Contributed by NM, 18-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π’ β¨ π) β§ (π β¨ ((π β¨ π’) β§ π))) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ π = (β©π§ β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π§ = π)) & β’ π = if(π’ β€ (π β¨ π), π, π) β β’ (π β π΄ β β¦π / π β¦π = β¦π / π’β¦π) | ||
Theorem | cdleme40w 39046* | Part of proof of Lemma E in [Crawley] p. 113. Apply cdleme40v 39045 bound variable change to β¦π / π’β¦π. TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π’ β¨ π) β§ (π β¨ ((π β¨ π’) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π β π)) β β¦π / π β¦π β β¦π / π β¦π) | ||
Theorem | cdleme42a 39047 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 3-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdleme42c 39048 | Part of proof of Lemma E in [Crawley] p. 113. Match Β¬ π₯ β€ π. (Contributed by NM, 6-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β Β¬ (π β¨ π) β€ π) | ||
Theorem | cdleme42d 39049 | Part of proof of Lemma E in [Crawley] p. 113. Match (π β¨ (π₯ β§ π)) = π₯. (Contributed by NM, 6-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ ((π β¨ π) β§ π)) = (π β¨ π)) | ||
Theorem | cdleme41sn3aw 39050* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is different on and off the π β¨ π line. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β π)) β β¦π / π β¦π β β¦π / π β¦π) | ||
Theorem | cdleme41sn4aw 39051* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for on and off π β¨ π line. TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π β π)) β β¦π / π β¦π β β¦π / π β¦π) | ||
Theorem | cdleme41snaw 39052* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for combined cases; compare cdleme32snaw 39011. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β β¦π / π β¦π β β¦π / π β¦π) | ||
Theorem | cdleme41fva11 39053* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is one-to-one for r in W (r an atom not under w). TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β (πΉβπ ) β (πΉβπ)) | ||
Theorem | cdleme42b 39054* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 6-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β π β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π)) β (πΉβπ) = (β¦π / π β¦π β¨ (π β§ π))) | ||
Theorem | cdleme42e 39055* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β (πΉβ(π β¨ π)) = (β¦π / π β¦π β¨ ((π β¨ π) β§ π))) | ||
Theorem | cdleme42f 39056* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β (πΉβ(π β¨ π)) = ((πΉβπ ) β¨ π)) | ||
Theorem | cdleme42g 39057* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β (πΉβ(π β¨ π)) = ((πΉβπ ) β¨ π)) | ||
Theorem | cdleme42h 39058* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β (πΉβπ) β€ ((πΉβπ ) β¨ π)) | ||
Theorem | cdleme42i 39059* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β ((πΉβπ ) β¨ (πΉβπ)) β€ ((πΉβπ ) β¨ π)) | ||
Theorem | cdleme42k 39060* | Part of proof of Lemma E in [Crawley] p. 113. Since F ' S =/= F'R when S =/= R (i.e. 1-1); then ( ( F ' R ) .\/ ( F ' S ) ) is 2-dim therefore = ( ( F ' R ) .\/ V ) by cdleme42i 39059 and ps-1 38053 TODO: FIX COMMENT. (Contributed by NM, 20-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β ((πΉβπ ) β¨ (πΉβπ)) = ((πΉβπ ) β¨ π)) | ||
Theorem | cdleme42ke 39061* | Part of proof of Lemma E in [Crawley] p. 113. Remove π β π condition. TODO: FIX COMMENT. (Contributed by NM, 2-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πΉβπ ) β¨ (πΉβπ)) = ((πΉβπ ) β¨ π)) | ||
Theorem | cdleme42keg 39062* | Part of proof of Lemma E in [Crawley] p. 113. Remove π β π condition. TODO: FIX COMMENT. TODO: Use instead of cdleme42ke 39061 and even combine with it? (Contributed by NM, 22-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πΉβπ ) β¨ (πΉβπ)) = ((πΉβπ ) β¨ π)) | ||
Theorem | cdleme42mN 39063* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT . f preserves join: f(r β¨ s) = f(r) β¨ s, p. 115 10th line from bottom. (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β (πΉβ(π β¨ π)) = ((πΉβπ ) β¨ (πΉβπ))) | ||
Theorem | cdleme42mgN 39064* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT . f preserves join: f(r β¨ s) = f(r) β¨ s, p. 115 10th line from bottom. TODO: Use instead of cdleme42mN 39063? Combine with cdleme42mN 39063? (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β (πΉβ(π β¨ π)) = ((πΉβπ ) β¨ (πΉβπ))) | ||
Theorem | cdleme43aN 39065 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT p. 115 penultimate line: g(f(r)) = (p v q) ^ (g(s) v v1). (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (πΆ β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π· β¨ ((π β¨ π) β§ π))) & β’ πΈ = ((π· β¨ π) β§ (π β¨ ((π β¨ π·) β§ π))) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π·) β§ π) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β πΊ = ((π β¨ π) β§ (π· β¨ π))) | ||
Theorem | cdleme43bN 39066 | Lemma for Lemma E in [Crawley] p. 113. g(s) is an atom not under w. (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (πΆ β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π· β¨ ((π β¨ π) β§ π))) & β’ πΈ = ((π· β¨ π) β§ (π β¨ ((π β¨ π·) β§ π))) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π·) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (π· β π΄ β§ Β¬ π· β€ π)) | ||
Theorem | cdleme43cN 39067 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT p. 115 last line: r v g(s) = r v v2. (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (πΆ β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π· β¨ ((π β¨ π) β§ π))) & β’ πΈ = ((π· β¨ π) β§ (π β¨ ((π β¨ π·) β§ π))) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π·) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (π β¨ π·) = (π β¨ π)) | ||
Theorem | cdleme43dN 39068 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT p. 116 2nd line: f(r) v s = f(r) v f(g(s)). (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (πΆ β¨ ((π β¨ π) β§ π))) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π· β¨ ((π β¨ π) β§ π))) & β’ πΈ = ((π· β¨ π) β§ (π β¨ ((π β¨ π·) β§ π))) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π·) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (π β¨ π) = (π β¨ πΈ)) | ||
Theorem | cdleme46f2g2 39069 | Conversion for πΊ to reuse πΉ theorems. TODO FIX COMMENT. TODO What other conversion theorems would be reused? e.g. cdlemeg46nlpq 39093? Find other hlatjcom 37943 uses giving π β¨ π. (Contributed by NM, 1-Apr-2013.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π))) | ||
Theorem | cdleme46f2g1 39070 | Conversion for πΊ to reuse πΉ theorems. TODO FIX COMMENT. (Contributed by NM, 1-Apr-2013.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)))) | ||
Theorem | cdleme17d2 39071* | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. πΉ, πΊ represent f(s), fs(p) respectively. We show, in their notation, fs(p)=q. TODO: FIX COMMENT. (Contributed by NM, 5-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβπ) = π) | ||
Theorem | cdleme17d3 39072* | TODO: FIX COMMENT. (Contributed by NM, 5-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β (πΉβπ) = π) | ||
Theorem | cdleme17d4 39073* | TODO: FIX COMMENT. (Contributed by NM, 11-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π = π) β (πΉβπ) = π) | ||
Theorem | cdleme17d 39074* | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. We show, in their notation, fs(p)=q. TODO FIX COMMENT. (Contributed by NM, 11-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) = π) | ||
Theorem | cdleme48fv 39075* | Part of proof of Lemma D in [Crawley] p. 113. TODO: Can this replace uses of cdleme32a 39017? TODO: Can this be used to help prove the π or π case where π is an atom? (Contributed by NM, 8-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π)) β (πΉβπ) = ((πΉβπ) β¨ (π β§ π))) | ||
Theorem | cdleme48fvg 39076* | Remove π β π condition in cdleme48fv 39075. TODO: Can this replace uses of cdleme32a 39017? TODO: Can this be used to help prove the π or π case where π is an atom? TODO: Can this be proved more directly by eliminating π β π in earlier theorems? Should this replace uses of cdleme48fv 39075? (Contributed by NM, 23-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π)) β (πΉβπ) = ((πΉβπ) β¨ (π β§ π))) | ||
Theorem | cdleme46fvaw 39077* | 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 | cdleme48bw 39078* | TODO: fix comment. TODO: Remove unnecessary π β π from cdleme48bw 39078 cdlemeg46c 39089 cdlemeg46fvaw 39092 cdlemeg46rgv 39104 cdlemeg46gfv 39106? cdleme48d 39111? and possibly others they affect. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π)) β Β¬ (πΉβπ) β€ π) | ||
Theorem | cdleme48b 39079* | TODO: fix comment. (Contributed by NM, 8-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π)) β ((πΉβπ) β§ π) = (π β§ π)) | ||
Theorem | cdleme46frvlpq 39080* | Show that (πΉβπ) is not under π β¨ π when π isn't. (Contributed by NM, 1-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β Β¬ (πΉβπ) β€ (π β¨ π)) | ||
Theorem | cdleme46fsvlpq 39081* | Show that (πΉβπ ) is under π β¨ π when π is. (Contributed by NM, 1-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β (πΉβπ ) β€ (π β¨ π)) | ||
Theorem | cdlemeg46fvcl 39082* | TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π΅) β (πΊβπ) β π΅) | ||
Theorem | cdleme4gfv 39083* | Part of proof of Lemma D in [Crawley] p. 113. TODO: Can this replace uses of cdleme32a 39017? TODO: Can this be used to help prove the π or π case where π is an atom? TODO: Would an antecedent transformer like cdleme46f2g2 39069 help? (Contributed by NM, 8-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π)) β (πΊβπ) = ((πΊβπ) β¨ (π β§ π))) | ||
Theorem | cdlemeg47b 39084* | TODO: FIX COMMENT. (Contributed by NM, 1-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΊβπ) = β¦π / π£β¦π) | ||
Theorem | cdlemeg47rv 39085* | Value of gs(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, 3-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΊβπ ) = β¦π / π’β¦β¦π / π£β¦π) | ||
Theorem | cdlemeg47rv2 39086* | Value of gs(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 | cdlemeg49le 39087* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ π β π΅) β§ π β€ π) β (πΊβπ) β€ (πΊβπ)) | ||
Theorem | cdlemeg46bOLDN 39088* | TODO FIX COMMENT. (Contributed by NM, 1-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΊβπ) = β¦π / π£β¦π) | ||
Theorem | cdlemeg46c 39089* | TODO FIX COMMENT. (Contributed by NM, 1-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβ(πΊβπ)) = β¦π / π£β¦β¦π / π‘β¦π·) | ||
Theorem | cdlemeg46rvOLDN 39090* | Value of gs(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, 3-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΊβπ ) = β¦π / π’β¦β¦π / π£β¦π) | ||
Theorem | cdlemeg46rv2OLDN 39091* | Value of gs(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, 3-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΊβπ ) = ((π β¨ π) β§ ((πΊβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemeg46fvaw 39092* | Show that (πΉβπ ) is an atom not under π when π is an atom not under π. (Contributed by NM, 1-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β ((πΊβπ ) β π΄ β§ Β¬ (πΊβπ ) β€ π)) | ||
Theorem | cdlemeg46nlpq 39093* | Show that (πΊβπ) is not under π β¨ π when π isn't. (Contributed by NM, 3-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β Β¬ (πΊβπ) β€ (π β¨ π)) | ||
Theorem | cdlemeg46ngfr 39094* | TODO FIX COMMENT g(f(s))=s p. 115 4th line from bottom. (Contributed by NM, 4-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΊβ(πΉβπ )) = π ) | ||
Theorem | cdlemeg46nfgr 39095* | TODO FIX COMMENT f(g(s))=s p. 115 antepenultimate line. (Contributed by NM, 4-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβ(πΊβπ )) = π ) | ||
Theorem | cdlemeg46sfg 39096* | TODO FIX COMMENT f(r) β¨ s = f(r) β¨ g(s) p. 116 2nd line TODO: eliminate eqcomd? (Contributed by NM, 4-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((πΉβπ ) β¨ π) = ((πΉβπ ) β¨ (πΉβ(πΊβπ)))) | ||
Theorem | cdlemeg46fjgN 39097* | NOT NEEDED? TODO FIX COMMENT. TODO eliminate eqcomd 2737? p. 116 2nd line. (Contributed by NM, 2-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((πΉβπ ) β¨ (πΉβ(πΊβπ))) = (πΉβ(π β¨ (πΊβπ)))) | ||
Theorem | cdlemeg46rjgN 39098* | NOT NEEDED? TODO FIX COMMENT. r β¨ g(s) = r β¨ v2 p. 115 last line. (Contributed by NM, 2-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) & β’ π = ((π β¨ (πΊβπ)) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (π β¨ (πΊβπ)) = (π β¨ π)) | ||
Theorem | cdlemeg46fjv 39099* | TODO FIX COMMENT f(r) β¨ f(g(s)) = f(r) β¨ v2 p. 116 2nd line. (Contributed by NM, 2-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) & β’ π = ((π β¨ (πΊβπ)) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((πΉβπ ) β¨ (πΉβ(πΊβπ))) = ((πΉβπ ) β¨ π)) | ||
Theorem | cdlemeg46fsfv 39100* | TODO FIX COMMENT f(r) β¨ s = f(r) β¨ v2 p. 116 2nd line. (Contributed by NM, 2-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) & β’ π = ((π β¨ (πΊβπ)) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((πΉβπ ) β¨ π) = ((πΉβπ ) β¨ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |