![]() |
Metamath
Proof Explorer Theorem List (p. 399 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdleme31fv1 39801* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.) |
β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ πΆ = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π§ = (π β¨ (π β§ π)))) β β’ ((π β π΅ β§ (π β π β§ Β¬ π β€ π)) β (πΉβπ) = πΆ) | ||
Theorem | cdleme31fv1s 39802* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.) |
β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((π β π΅ β§ (π β π β§ Β¬ π β€ π)) β (πΉβπ) = β¦π / π₯β¦π) | ||
Theorem | cdleme31fv2 39803* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 23-Feb-2013.) |
β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((π β π΅ β§ Β¬ (π β π β§ Β¬ π β€ π)) β (πΉβπ) = π) | ||
Theorem | cdleme31id 39804* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 18-Apr-2013.) |
β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((π β π΅ β§ π = π) β (πΉβπ) = π) | ||
Theorem | cdlemefrs29pre00 39805 | ***START OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW*** FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 39440. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π) β§ π β π΄) β (((Β¬ π β€ π β§ π) β§ (π β¨ (π β§ π)) = π ) β (Β¬ π β€ π β§ (π β¨ (π β§ π)) = π ))) | ||
Theorem | cdlemefrs29bpre0 39806* | TODO fix comment. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β (βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π))) β π§ = β¦π / π β¦π)) | ||
Theorem | cdlemefrs29bpre1 39807* | TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π β¦π β π΅) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β βπ§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) | ||
Theorem | cdlemefrs29cpre1 39808* | TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π β¦π β π΅) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β!π§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) | ||
Theorem | cdlemefrs29clN 39809* | TODO: NOT USED? Show closure of the unique element in cdlemefrs29cpre1 39808. (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π β¦π β π΅) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β π β π΅) | ||
Theorem | cdlemefrs32fva 39810* | 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 39440 here and elsewhere, and presence/absence of π β€ (π β¨ π) term. Also, why can proof be shortened with cdleme29cl 39787? What is difference from cdlemefs27cl 39823? (Contributed by NM, 29-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ (π = π β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π β§ (π β π΄ β§ (Β¬ π β€ π β§ π))) β π β π΅) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π β¦π β π΅) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β β¦π / π₯β¦π = β¦π / π β¦π) | ||
Theorem | cdlemefrs32fva1 39811* | 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 39812* | Lemma for cdlemefs29bpre1N 39827. (Compare cdleme25a 39763.) 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 39813 | 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 39814* | Show that β¦π / π β¦π is an atom not under π when Β¬ π β€ (π β¨ π). (Contributed by NM, 28-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (β¦π / π β¦π β π΄ β§ Β¬ β¦π / π β¦π β€ π)) | ||
Theorem | cdlemefr32snb 39815* | Show closure of β¦π / π β¦π. (Contributed by NM, 28-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β β¦π / π β¦π β π΅) | ||
Theorem | cdlemefr29bpre0N 39816* | TODO fix comment. (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (βπ β π΄ (((Β¬ π β€ π β§ Β¬ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π))) β π§ = β¦π / π β¦π)) | ||
Theorem | cdlemefr29clN 39817* | Show closure of the unique element in cdleme29c 39786. 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 39818* | Value of β¦π / π β¦π when Β¬ π β€ (π β¨ π). (Contributed by NM, 30-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ ((π β π΄ β§ Β¬ π β€ (π β¨ π)) β β¦π / π β¦π = π) | ||
Theorem | cdlemefr32fvaN 39819* | 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 39820* | 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 39821* | Value of (πΉβπ ) when Β¬ π β€ (π β¨ π). TODO This may be useful for shortening others that now use riotasv 38368 3d . TODO: FIX COMMENT. (Contributed by NM, 30-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβπ ) = π) | ||
Theorem | cdlemefs29pre00N 39822 | FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 39440. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β§ π β π΄) β (((Β¬ π β€ π β§ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β (Β¬ π β€ π β§ (π β¨ (π β§ π)) = π ))) | ||
Theorem | cdlemefs27cl 39823* | 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 39776 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 39824* | Show that β¦π / π β¦π is an atom not under π when π β€ (π β¨ π). (Contributed by NM, 24-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β (β¦π / π β¦π β π΄ β§ Β¬ β¦π / π β¦π β€ π)) | ||
Theorem | cdlemefs32snb 39825* | Show closure of β¦π / π β¦π. (Contributed by NM, 24-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β β¦π / π β¦π β π΅) | ||
Theorem | cdlemefs29bpre0N 39826* | TODO: FIX COMMENT. (Contributed by NM, 26-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β (βπ β π΄ (((Β¬ π β€ π β§ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π))) β π§ = β¦π / π β¦π)) | ||
Theorem | cdlemefs29bpre1N 39827* | TODO: FIX COMMENT. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β βπ§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) | ||
Theorem | cdlemefs29cpre1N 39828* | TODO: FIX COMMENT. (Contributed by NM, 26-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β β!π§ β π΅ βπ β π΄ (((Β¬ π β€ π β§ π β€ (π β¨ π)) β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) | ||
Theorem | cdlemefs29clN 39829* | Show closure of the unique element in cdleme29c 39786. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π ) β π§ = (π β¨ (π β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β π β π΅) | ||
Theorem | cdleme43fsv1snlem 39830* | Value of β¦π / π β¦π when π β€ (π β¨ π). (Contributed by NM, 30-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β β¦π / π β¦π = π) | ||
Theorem | cdleme43fsv1sn 39831* | Value of β¦π / π β¦π when π β€ (π β¨ π). (Contributed by NM, 30-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β β¦π / π β¦π = π) | ||
Theorem | cdlemefs32fvaN 39832* | 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 39440 here and elsewhere, and presence/absence of π β€ (π β¨ π) term. Also, why can proof be shortened with cdleme27cl 39776? What is difference from cdlemefs27cl 39823? (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β β¦π / π₯β¦π = β¦π / π β¦π) | ||
Theorem | cdlemefs32fva1 39833* | 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 39834* |
Value of (πΉβπ
) when π
β€ (π β¨ π).
TODO This may be useful for shortening others that now use riotasv 38368
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 39835* | 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 39836* | 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 39839 instead TODO: FIX COMMENT. (Contributed by NM, 31-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), πΌ, β¦π / π‘β¦π·) β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΉβπ ) = β¦π / π β¦β¦π / π‘β¦πΈ) | ||
Theorem | cdlemefr45 39837* | 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 39838* | Explicit expansion of cdlemefr45 39837. TODO: use to shorten cdlemefr45 39837 uses? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (πΉβπ ) = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π)))) | ||
Theorem | cdlemefs45 39839* | 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 39840* | Explicit expansion of cdlemefs45 39839. TODO: use to shorten cdlemefs45 39839 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 39841* | Explicit expansion of cdlemefs45 39839. TODO: use to shorten cdlemefs45 39839 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 39842* | 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 39843* | Show that β¦π / π β¦π is under π β¨ π when π β€ (π β¨ π). (Contributed by NM, 19-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) & β’ π = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ π = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β β¦π / π β¦π β€ (π β¨ π)) | ||
Theorem | cdleme32sn2awN 39844* | 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 39845* | Show that β¦π / π β¦π is an atom not under π. (Contributed by NM, 6-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π))) β (β¦π / π β¦π β π΄ β§ Β¬ β¦π / π β¦π β€ π)) | ||
Theorem | cdleme32snb 39846* | Show closure of β¦π / π β¦π. (Contributed by NM, 1-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)) & β’ π = if(π β€ (π β¨ π), πΌ, πΆ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π))) β β¦π / π β¦π β π΅) | ||
Theorem | cdleme32fva 39847* | 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 39848* | 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 39849* | 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 39850* | 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 39851* | 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 39852* | 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 39853* | 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 39854* | 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 39855* | 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 39856* | 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 39857* | 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 39858 | 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 39859 | 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 39860 | 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 39861 | 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 39862 | 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 39863 | 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 39864 | 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 39865 | 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 39866 | 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 39867 | 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 39868* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of π β¨ π line case; compare cdleme32sn2awN 39844. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = if(π β€ (π β¨ π), πΌ, π·) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ π β π)) β β¦π / π β¦π β β¦π / π β¦π) | ||
Theorem | cdleme35sn3a 39869* | 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 39870 | 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 39871 | 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 39872 | 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 39873 | 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 39874 | 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 39871 and cdleme37m 39872? (Contributed by NM, 14-Mar-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ π· = ((π’ β¨ π) β§ (π β¨ ((π β¨ π’) β§ π))) & β’ π = ((π‘ β¨ πΈ) β§ π) & β’ π = ((π’ β¨ π·) β§ π) & β’ πΉ = ((π β¨ π) β§ (πΈ β¨ ((π‘ β¨ π ) β§ π))) & β’ πΊ = ((π β¨ π) β§ (π· β¨ ((π’ β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π β π) β§ ((π‘ β π΄ β§ Β¬ π‘ β€ π) β§ Β¬ π‘ β€ (π β¨ π)) β§ ((π’ β π΄ β§ Β¬ π’ β€ π) β§ Β¬ π’ β€ (π β¨ π)))) β πΉ β πΊ) | ||
Theorem | cdleme39a 39875 | 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 39874 in convention of cdleme32sn1awN 39842. 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 39876 | 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 39874 in convention of cdleme32sn1awN 39842. 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 39877* | 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 39842. (Contributed by NM, 18-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΆ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = π)) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π β π) β§ (π£ β π΄ β§ Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)))) β β¦π / π β¦π β πΉ) | ||
Theorem | cdleme40n 39878* | 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 39879* | 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 39880* | Part of proof of Lemma E in [Crawley] p. 113. Apply cdleme40v 39879 bound variable change to β¦π / π’β¦π. TODO: FIX COMMENT. (Contributed by NM, 19-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π’ β¨ π) β§ (π β¨ ((π β¨ π’) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ π β π)) β β¦π / π β¦π β β¦π / π β¦π) | ||
Theorem | cdleme42a 39881 | 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 39882 | 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 39883 | 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 39884* | 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 39885* | 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 39886* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for combined cases; compare cdleme32snaw 39845. TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β β¦π / π β¦π β β¦π / π β¦π) | ||
Theorem | cdleme41fva11 39887* | 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 39888* | 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 39889* | 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 39890* | 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 39891* | 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 39892* | 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 39893* | 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 39894* | 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 39893 and ps-1 38887 TODO: FIX COMMENT. (Contributed by NM, 20-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β ((πΉβπ ) β¨ (πΉβπ)) = ((πΉβπ ) β¨ π)) | ||
Theorem | cdleme42ke 39895* | 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 39896* | Part of proof of Lemma E in [Crawley] p. 113. Remove π β π condition. TODO: FIX COMMENT. TODO: Use instead of cdleme42ke 39895 and even combine with it? (Contributed by NM, 22-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πΉβπ ) β¨ (πΉβπ)) = ((πΉβπ ) β¨ π)) | ||
Theorem | cdleme42mN 39897* | 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 39898* | 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 39897? Combine with cdleme42mN 39897? (Contributed by NM, 20-Mar-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ πΈ = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΈ β¨ ((π β¨ π‘) β§ π))) & β’ πΌ = (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΊ)) & β’ π = if(π β€ (π β¨ π), πΌ, π·) & β’ π = (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (π β¨ (π₯ β§ π)))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), π, π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β (πΉβ(π β¨ π)) = ((πΉβπ ) β¨ (πΉβπ))) | ||
Theorem | cdleme43aN 39899 | 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 39900 | 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 β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β (π· β π΄ β§ Β¬ π· β€ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |