Home | Metamath
Proof Explorer Theorem List (p. 391 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemg12a 39001 | TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ π β π β§ (π β¨ π) β ((πΊβπ) β¨ π))) β ((π β¨ π) β§ ((πΊβπ) β¨ π)) β€ ((πΉβ(πΊβπ)) β¨ π)) | ||
Theorem | cdlemg12b 39002 | The triples β¨π, (πΉβπ), (πΉβ(πΊβπ))β© and β¨π, (πΉβπ), (πΉβ(πΊβπ))β© are centrally perspective. TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ π β π β§ Β¬ (π βπΊ) β€ (π β¨ π))) β ((π β¨ π) β§ ((πΊβπ) β¨ (πΊβπ))) β€ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ)))) | ||
Theorem | cdlemg12c 39003 | The triples β¨π, (πΉβπ), (πΉβ(πΊβπ))β© and β¨π, (πΉβπ), (πΉβ(πΊβπ))β© are axially perspective by dalaw 38244. TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ π β π β§ Β¬ (π βπΊ) β€ (π β¨ π))) β ((π β¨ (πΊβπ)) β§ (π β¨ (πΊβπ))) β€ ((((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ ((πΊβπ) β¨ (πΉβ(πΊβπ)))) β¨ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)))) | ||
Theorem | cdlemg12d 39004 | TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ (π β π β§ Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π))) β (π βπΊ) β€ ((π βπΉ) β¨ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)))) | ||
Theorem | cdlemg12e 39005 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ 0 = (0.βπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π) β§ (π βπΉ) β (π βπΊ))) β (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) β 0 ) | ||
Theorem | cdlemg12f 39006 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π)) β§ (π βπΉ) β (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β€ ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg12g 39007 | TODO: FIX COMMENT. TODO: Combine with cdlemg12f 39006. (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π)) β§ (π βπΉ) β (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg12 39008 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π)) β§ (π βπΉ) β (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg13a 39009 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π βπΉ) = (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π β¨ (πΉβ(πΊβπ))) = ((πΊβπ) β¨ (πΉβ(πΊβπ)))) | ||
Theorem | cdlemg13 39010 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π βπΉ) = (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg14f 39011 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ (πΉβπ) = π)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg14g 39012 | TODO: FIX COMMENT. (Contributed by NM, 22-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ (πΊβπ) = π)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg15a 39013 | Eliminate the (πΉβπ) β π condition from cdlemg13 39010. TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((π βπΉ) = (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg15 39014 | Eliminate the ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) condition from cdlemg13 39010. TODO: FIX COMMENT. (Contributed by NM, 25-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ (π βπΉ) = (π βπΊ)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg16 39015 | Part of proof of Lemma G of [Crawley] p. 116; 2nd line p. 117, which says that (our) cdlemg10 38999 "implies (2)" (of p. 116). No details are provided by the authors, so there may be a shorter proof; but ours requires the 14 lemmas, one using Desargues's law dalaw 38244, in order to make this inference. This final step eliminates the (π βπΉ) β (π βπΊ) condition from cdlemg12 39008. TODO: FIX COMMENT. TODO: should we also eliminate π β π here (or earlier)? Do it if we don't need to add it in for something else later. (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg16ALTN 39016 | This version of cdlemg16 39015 uses cdlemg15a 39013 instead of cdlemg15 39014, in case cdlemg15 39014 ends up not being needed. TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π» β§ (πΉ β π β§ πΊ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg16z 39017 | Eliminate ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) condition from cdlemg16 39015. TODO: would it help to also eliminate π β π here or later? (Contributed by NM, 25-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg16zz 39018 | Eliminate π β π from cdlemg16z 39017. TODO: Use this only if needed. (Contributed by NM, 26-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg17a 39019 | TODO: FIX COMMENT. (Contributed by NM, 8-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΊ β π β§ (π βπΊ) β€ (π β¨ π))) β (πΊβπ) β€ (π β¨ π)) | ||
Theorem | cdlemg17b 39020* | Part of proof of Lemma G in [Crawley] p. 117, 4th line. Whenever (in their terminology) p β¨ q/0 (i.e. the sublattice from 0 to p β¨ q) contains precisely three atoms and g is not the identity, g(p) = q. See also comments under cdleme0nex 38648. (Contributed by NM, 8-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβπ) = π) | ||
Theorem | cdlemg17dN 39021* | TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π» β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ ((π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)) β§ (πΊβπ) β π)) β (π βπΊ) = ((π β¨ π) β§ π)) | ||
Theorem | cdlemg17dALTN 39022 | Same as cdlemg17dN 39021 with fewer antecedents but longer proof TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π» β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ π β π) β§ ((π βπΊ) β€ (π β¨ π) β§ (πΊβπ) β π)) β (π βπΊ) = ((π β¨ π) β§ π)) | ||
Theorem | cdlemg17e 39023* | TODO: fix comment. (Contributed by NM, 8-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (π βπΊ))) | ||
Theorem | cdlemg17f 39024* | TODO: fix comment. (Contributed by NM, 8-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (πΊβ(πΉβπ)))) | ||
Theorem | cdlemg17g 39025* | TODO: fix comment. (Contributed by NM, 9-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ(πΉβπ)) β€ ((πΉβπ) β¨ (πΉβπ))) | ||
Theorem | cdlemg17h 39026* | TODO: fix comment. (Contributed by NM, 10-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ πΊ β π) β§ (π β π β§ π β€ ((πΉβπ) β¨ (πΉβπ)))) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π = (πΉβπ) β¨ π = (πΉβπ))) | ||
Theorem | cdlemg17i 39027* | TODO: fix comment. (Contributed by NM, 10-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ(πΉβπ)) = (πΉβπ)) | ||
Theorem | cdlemg17ir 39028* | TODO: fix comment. (Contributed by NM, 13-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΉβ(πΊβπ)) = (πΉβπ)) | ||
Theorem | cdlemg17j 39029* | TODO: fix comment. (Contributed by NM, 11-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ(πΉβπ)) = (πΉβ(πΊβπ))) | ||
Theorem | cdlemg17pq 39030* | Utility theorem for swapping π and π. TODO: fix comment. (Contributed by NM, 11-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))))) | ||
Theorem | cdlemg17bq 39031* | cdlemg17b 39020 with π and π swapped. Antecedent πΉ β (πβπ) is redundant for easier use. TODO: should we have redundant antecedent for cdlemg17b 39020 also? (Contributed by NM, 13-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβπ) = π) | ||
Theorem | cdlemg17iqN 39032* | cdlemg17i 39027 with π and π swapped. (Contributed by NM, 13-May-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π» β§ (πΉ β π β§ πΊ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ ((π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)) β§ (πΊβπ) β π)) β (πΊβ(πΉβπ)) = (πΉβπ)) | ||
Theorem | cdlemg17irq 39033* | cdlemg17ir 39028 with π and π swapped. (Contributed by NM, 13-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΉβ(πΊβπ)) = (πΉβπ)) | ||
Theorem | cdlemg17jq 39034* | cdlemg17j 39029 with π and π swapped. (Contributed by NM, 13-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ(πΉβπ)) = (πΉβ(πΊβπ))) | ||
Theorem | cdlemg17 39035* | Part of Lemma G of [Crawley] p. 117, lines 7 and 8. We show an argument whose value at πΊ equals itself. TODO: fix comment. (Contributed by NM, 12-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ))))) = ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ))))) | ||
Theorem | cdlemg18a 39036 | Show two lines are different. TODO: fix comment. (Contributed by NM, 14-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ πΉ β π) β§ (π β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (π β¨ (πΉβπ)) β (π β¨ (πΉβπ))) | ||
Theorem | cdlemg18b 39037 | Lemma for cdlemg18c 39038. TODO: fix comment. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β Β¬ π β€ (π β¨ (πΉβπ))) | ||
Theorem | cdlemg18c 39038 | Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ))) β π΄) | ||
Theorem | cdlemg18d 39039* | Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β π΄) | ||
Theorem | cdlemg18 39040* | Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β€ π) | ||
Theorem | cdlemg19a 39041* | Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg19 39042* | Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg20 39043* | Show two lines intersect at an atom. TODO: fix comment. (Contributed by NM, 23-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((π βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg21 39044* | Version of cdlemg19 with (π βπΉ) β€ (π β¨ π) instead of (π βπΊ) β€ (π β¨ π) as a condition. (Contributed by NM, 23-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΉβπ) β π) β§ ((π βπΉ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg22 39045* | cdlemg21 39044 with (πΉβπ) β π condition removed. (Contributed by NM, 23-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((π βπΉ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg24 39046* | Combine cdlemg16z 39017 and cdlemg22 39045. TODO: Fix comment. (Contributed by NM, 24-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg37 39047* | Use cdlemg8 38989 to eliminate the β (π β¨ π) condition of cdlemg24 39046. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ π β π β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg25zz 39048 | cdlemg16zz 39018 restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π§ β π΄ β§ Β¬ π§ β€ π) β§ πΉ β π) β§ (πΊ β π β§ Β¬ (π βπΉ) β€ (π β¨ π§) β§ Β¬ (π βπΊ) β€ (π β¨ π§))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π§ β¨ (πΉβ(πΊβπ§))) β§ π)) | ||
Theorem | cdlemg26zz 39049 | cdlemg16zz 39018 restated for easier studying. TODO: Discard this after everything is figured out. (Contributed by NM, 26-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π§ β π΄ β§ Β¬ π§ β€ π) β§ πΉ β π) β§ (πΊ β π β§ Β¬ (π βπΉ) β€ (π β¨ π§) β§ Β¬ (π βπΊ) β€ (π β¨ π§))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π§ β¨ (πΉβ(πΊβπ§))) β§ π)) | ||
Theorem | cdlemg27a 39050 | For use with case when (π β¨ π£) β§ (π β¨ (π βπΉ)) or (π β¨ π£) β§ (π β¨ (π βπΉ)) is zero, letting us establish Β¬ π§ β€ π β§ π§ β€ (π β¨ π£) via 4atex 38434. TODO: Fix comment. (Contributed by NM, 28-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β Β¬ (π βπΉ) β€ (π β¨ π§)) | ||
Theorem | cdlemg28a 39051 | Part of proof of Lemma G of [Crawley] p. 116. First equality of the equation of line 14 on p. 117. (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ ((π§ β π΄ β§ Β¬ π§ β€ π) β§ πΉ β π β§ πΊ β π) β§ ((π£ β (π βπΉ) β§ π£ β (π βπΊ)) β§ π§ β€ (π β¨ π£) β§ ((πΉβπ) β π β§ (πΊβπ) β π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π§ β¨ (πΉβ(πΊβπ§))) β§ π)) | ||
Theorem | cdlemg31b0N 39052 | TODO: Fix comment. (Contributed by NM, 30-May-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π» β§ πΉ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ π£ β (π βπΉ) β§ (πΉβπ) β π)) β (π β π΄ β¨ π = (0.βπΎ))) | ||
Theorem | cdlemg31b0a 39053 | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (πΉ β π β§ π£ β (π βπΉ))) β (π β π΄ β¨ π = (0.βπΎ))) | ||
Theorem | cdlemg27b 39054 | TODO: Fix comment. (Contributed by NM, 28-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π§ β π΄ β§ (π£ β π΄ β§ π£ β€ π) β§ (πΉ β π β§ π§ β π)) β§ (π£ β (π βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β Β¬ (π βπΉ) β€ (π β¨ π§)) | ||
Theorem | cdlemg31a 39055 | TODO: fix comment. (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π£ β π΄ β§ πΉ β π)) β π β€ (π β¨ π£)) | ||
Theorem | cdlemg31b 39056 | TODO: fix comment. (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π£ β π΄ β§ πΉ β π)) β π β€ (π β¨ (π βπΉ))) | ||
Theorem | cdlemg31c 39057 | Show that when π is an atom, it is not under π. TODO: Is there a shorter direct proof? TODO: should we eliminate (πΉβπ) β π here? (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π£ β (π βπΉ) β§ (πΉβπ) β π β§ π β π΄)) β Β¬ π β€ π) | ||
Theorem | cdlemg31d 39058 | Eliminate (πΉβπ) β π from cdlemg31c 39057. TODO: Prove directly. TODO: do we need to eliminate (πΉβπ) β π? It might be better to do this all at once at the end. See also cdlemg29 39063 versus cdlemg28 39062. (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (πΉ β π β§ π£ β (π βπΉ) β§ π β π΄)) β Β¬ π β€ π) | ||
Theorem | cdlemg33b0 39059* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ π β π΄ β§ πΉ β π) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg33c0 39060* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ π§ β€ (π β¨ π£))) | ||
Theorem | cdlemg28b 39061* | Part of proof of Lemma G of [Crawley] p. 116. Second equality of the equation of line 14 on p. 117. Note that Β¬ π§ β€ π is redundant here (but simplifies cdlemg28 39062.) (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π§ β π΄ β§ Β¬ π§ β€ π) β§ (πΉ β π β§ πΊ β π)) β§ ((π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)) β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ)) β§ ((πΉβπ) β π β§ (πΊβπ) β π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π§ β¨ (πΉβ(πΊβπ§))) β§ π)) | ||
Theorem | cdlemg28 39062* | Part of proof of Lemma G of [Crawley] p. 116. Chain the equalities of line 14 on p. 117. TODO: rearrange hypotheses in the order of cdlemg29 39063 (and maybe leading up to this too)? (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π§ β π΄ β§ Β¬ π§ β€ π) β§ (πΉ β π β§ πΊ β π)) β§ ((π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)) β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ)) β§ ((πΉβπ) β π β§ (πΊβπ) β π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg29 39063* | Eliminate (πΉβπ) β π and (πΊβπ) β π from cdlemg28 39062. TODO: would it be better to do this later? (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π§ β π΄ β§ Β¬ π§ β€ π) β§ (πΉ β π β§ πΊ β π)) β§ ((π§ β π β§ π§ β π) β§ π§ β€ (π β¨ π£) β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg33a 39064* | TODO: Fix comment. (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π β π΄ β§ π β π΄) β§ (πΉ β π β§ πΊ β π)) β§ ((π β π β§ π β π) β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg33b 39065* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π β π΄ β§ π β π΄) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg33c 39066* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π β π΄ β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg33d 39067* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π β π΄) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π βπΊ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg33e 39068* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg33 39069* | Combine cdlemg33b 39065, cdlemg33c 39066, cdlemg33d 39067, cdlemg33e 39068. TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (πΉ β π β§ πΊ β π) β§ π β π) β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg34 39070* | Use cdlemg33 to eliminate π§ from cdlemg29 39063. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (πΉ β π β§ πΊ β π) β§ π β π) β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg35 39071* | TODO: Fix comment. TODO: should we have a more general version of hlsupr 37744 to avoid the β conditions? (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (πΊβπ) β π β§ (π βπΉ) β (π βπΊ))) β βπ£ β π΄ (π£ β€ π β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ)))) | ||
Theorem | cdlemg36 39072* | Use cdlemg35 to eliminate π£ from cdlemg34 39070. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβπ) β π β§ (πΊβπ) β π) β§ (π βπΉ) β (π βπΊ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg38 39073 | Use cdlemg37 39047 to eliminate βπ β π΄ from cdlemg36 39072. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβπ) β π β§ (πΊβπ) β π) β§ (π βπΉ) β (π βπΊ))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg39 39074 | Eliminate β conditions from cdlemg38 39073. TODO: Would this better be done at cdlemg35 39071? TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg40 39075 | Eliminate π β π conditions from cdlemg39 39074. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg41 39076 | Convert cdlemg40 39075 to function composition. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((π β¨ ((πΉ β πΊ)βπ)) β§ π) = ((π β¨ ((πΉ β πΊ)βπ)) β§ π)) | ||
Theorem | ltrnco 39077 | The composition of two translations is a translation. Part of proof of Lemma G of [Crawley] p. 116, line 15 on p. 117. (Contributed by NM, 31-May-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (πΉ β πΊ) β π) | ||
Theorem | trlcocnv 39078 | Swap the arguments of the trace of a composition with converse. (Contributed by NM, 1-Jul-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (π β(πΉ β β‘πΊ)) = (π β(πΊ β β‘πΉ))) | ||
Theorem | trlcoabs 39079 | Absorption into a composition by joining with trace. (Contributed by NM, 22-Jul-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΉ β πΊ)βπ) β¨ (π βπΉ)) = ((πΊβπ) β¨ (π βπΉ))) | ||
Theorem | trlcoabs2N 39080 | Absorption of the trace of a composition. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β¨ (π β(πΊ β β‘πΉ))) = ((πΉβπ) β¨ (πΊβπ))) | ||
Theorem | trlcoat 39081 | The trace of a composition of two translations is an atom if their traces are different. (Contributed by NM, 15-Jun-2013.) |
β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π βπΉ) β (π βπΊ)) β (π β(πΉ β πΊ)) β π΄) | ||
Theorem | trlcocnvat 39082 | Commonly used special case of trlcoat 39081. (Contributed by NM, 1-Jul-2013.) |
β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π βπΉ) β (π βπΊ)) β (π β(πΉ β β‘πΊ)) β π΄) | ||
Theorem | trlconid 39083 | The composition of two different translations is not the identity translation. (Contributed by NM, 22-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π βπΉ) β (π βπΊ)) β (πΉ β πΊ) β ( I βΎ π΅)) | ||
Theorem | trlcolem 39084 | Lemma for trlco 39085. (Contributed by NM, 1-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β(πΉ β πΊ)) β€ ((π βπΉ) β¨ (π βπΊ))) | ||
Theorem | trlco 39085 | The trace of a composition of translations is less than or equal to the join of their traces. Part of proof of Lemma G of [Crawley] p. 116, second paragraph on p. 117. (Contributed by NM, 2-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (π β(πΉ β πΊ)) β€ ((π βπΉ) β¨ (π βπΊ))) | ||
Theorem | trlcone 39086 | If two translations have different traces, the trace of their composition is also different. (Contributed by NM, 14-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ ((π βπΉ) β (π βπΊ) β§ πΊ β ( I βΎ π΅))) β (π βπΉ) β (π β(πΉ β πΊ))) | ||
Theorem | cdlemg42 39087 | Part of proof of Lemma G of [Crawley] p. 116, first line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (πΊβπ) β π β§ (π βπΉ) β (π βπΊ))) β Β¬ (πΊβπ) β€ (π β¨ (πΉβπ))) | ||
Theorem | cdlemg43 39088 | Part of proof of Lemma G of [Crawley] p. 116, third line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (πΊβπ) β π β§ (π βπΉ) β (π βπΊ))) β (πΉβ(πΊβπ)) = (((πΊβπ) β¨ (π βπΉ)) β§ ((πΉβπ) β¨ (π βπΊ)))) | ||
Theorem | cdlemg44a 39089 | Part of proof of Lemma G of [Crawley] p. 116, fourth line of third paragraph on p. 117: "so fg(p) = gf(p)." (Contributed by NM, 3-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) β π β§ (πΊβπ) β π β§ (π βπΉ) β (π βπΊ))) β (πΉβ(πΊβπ)) = (πΊβ(πΉβπ))) | ||
Theorem | cdlemg44b 39090 | Eliminate (πΉβπ) β π, (πΊβπ) β π from cdlemg44a 39089. (Contributed by NM, 3-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π βπΉ) β (π βπΊ)) β (πΉβ(πΊβπ)) = (πΊβ(πΉβπ))) | ||
Theorem | cdlemg44 39091 | Part of proof of Lemma G of [Crawley] p. 116, fifth line of third paragraph on p. 117: "and hence fg = gf." (Contributed by NM, 3-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π βπΉ) β (π βπΊ)) β (πΉ β πΊ) = (πΊ β πΉ)) | ||
Theorem | cdlemg47a 39092 | TODO: fix comment. TODO: Use this above in place of (πΉβπ) = π antecedents? (Contributed by NM, 5-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ πΉ = ( I βΎ π΅)) β (πΉ β πΊ) = (πΊ β πΉ)) | ||
Theorem | cdlemg46 39093* | Part of proof of Lemma G of [Crawley] p. 116, seventh line of third paragraph on p. 117: "hf and f have different traces." (Contributed by NM, 5-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ β β π) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π ββ) β (π βπΉ))) β (π β(β β πΉ)) β (π βπΉ)) | ||
Theorem | cdlemg47 39094* | Part of proof of Lemma G of [Crawley] p. 116, ninth line of third paragraph on p. 117: "we conclude that gf = fg." (Contributed by NM, 5-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (β β π β§ (π βπΉ) = (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ β β ( I βΎ π΅) β§ (π ββ) β (π βπΉ))) β (πΉ β πΊ) = (πΊ β πΉ)) | ||
Theorem | cdlemg48 39095 | Eliminate β from cdlemg47 39094. (Contributed by NM, 5-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (πΉ β ( I βΎ π΅) β§ (π βπΉ) = (π βπΊ))) β (πΉ β πΊ) = (πΊ β πΉ)) | ||
Theorem | ltrncom 39096 | Composition is commutative for translations. Part of proof of Lemma G of [Crawley] p. 116. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (πΉ β πΊ) = (πΊ β πΉ)) | ||
Theorem | ltrnco4 39097 | Rearrange a composition of 4 translations, analogous to an4 654. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΈ β π β§ πΉ β π) β ((π· β πΈ) β (πΉ β πΊ)) = ((π· β πΉ) β (πΈ β πΊ))) | ||
Theorem | trljco 39098 | Trace joined with trace of composition. (Contributed by NM, 15-Jun-2013.) |
β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β ((π βπΉ) β¨ (π β(πΉ β πΊ))) = ((π βπΉ) β¨ (π βπΊ))) | ||
Theorem | trljco2 39099 | Trace joined with trace of composition. (Contributed by NM, 16-Jun-2013.) |
β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β ((π βπΉ) β¨ (π β(πΉ β πΊ))) = ((π βπΊ) β¨ (π β(πΉ β πΊ)))) | ||
Syntax | ctgrp 39100 | Extend class notation with translation group. |
class TGrp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |