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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemg13 39001 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π βπΉ) = (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg14f 39002 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ (πΉβπ) = π)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg14g 39003 | TODO: FIX COMMENT. (Contributed by NM, 22-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ (πΊβπ) = π)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg15a 39004 | Eliminate the (πΉβπ) β π condition from cdlemg13 39001. TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((π βπΉ) = (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg15 39005 | Eliminate the ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) condition from cdlemg13 39001. TODO: FIX COMMENT. (Contributed by NM, 25-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ (π βπΉ) = (π βπΊ)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg16 39006 | Part of proof of Lemma G of [Crawley] p. 116; 2nd line p. 117, which says that (our) cdlemg10 38990 "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 38235, in order to make this inference. This final step eliminates the (π βπΉ) β (π βπΊ) condition from cdlemg12 38999. 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 39007 | This version of cdlemg16 39006 uses cdlemg15a 39004 instead of cdlemg15 39005, in case cdlemg15 39005 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 39008 | Eliminate ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) condition from cdlemg16 39006. 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 39009 | Eliminate π β π from cdlemg16z 39008. TODO: Use this only if needed. (Contributed by NM, 26-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg17a 39010 | TODO: FIX COMMENT. (Contributed by NM, 8-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΊ β π β§ (π βπΊ) β€ (π β¨ π))) β (πΊβπ) β€ (π β¨ π)) | ||
Theorem | cdlemg17b 39011* | 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 38639. (Contributed by NM, 8-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβπ) = π) | ||
Theorem | cdlemg17dN 39012* | TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π» β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ ((π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)) β§ (πΊβπ) β π)) β (π βπΊ) = ((π β¨ π) β§ π)) | ||
Theorem | cdlemg17dALTN 39013 | Same as cdlemg17dN 39012 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 39014* | TODO: fix comment. (Contributed by NM, 8-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (π βπΊ))) | ||
Theorem | cdlemg17f 39015* | TODO: fix comment. (Contributed by NM, 8-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (πΊβ(πΉβπ)))) | ||
Theorem | cdlemg17g 39016* | TODO: fix comment. (Contributed by NM, 9-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ(πΉβπ)) β€ ((πΉβπ) β¨ (πΉβπ))) | ||
Theorem | cdlemg17h 39017* | TODO: fix comment. (Contributed by NM, 10-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ πΊ β π) β§ (π β π β§ π β€ ((πΉβπ) β¨ (πΉβπ)))) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π = (πΉβπ) β¨ π = (πΉβπ))) | ||
Theorem | cdlemg17i 39018* | TODO: fix comment. (Contributed by NM, 10-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ(πΉβπ)) = (πΉβπ)) | ||
Theorem | cdlemg17ir 39019* | TODO: fix comment. (Contributed by NM, 13-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΉβ(πΊβπ)) = (πΉβπ)) | ||
Theorem | cdlemg17j 39020* | TODO: fix comment. (Contributed by NM, 11-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ(πΉβπ)) = (πΉβ(πΊβπ))) | ||
Theorem | cdlemg17pq 39021* | 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 39022* | cdlemg17b 39011 with π and π swapped. Antecedent πΉ β (πβπ) is redundant for easier use. TODO: should we have redundant antecedent for cdlemg17b 39011 also? (Contributed by NM, 13-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβπ) = π) | ||
Theorem | cdlemg17iqN 39023* | cdlemg17i 39018 with π and π swapped. (Contributed by NM, 13-May-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π» β§ (πΉ β π β§ πΊ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ ((π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)) β§ (πΊβπ) β π)) β (πΊβ(πΉβπ)) = (πΉβπ)) | ||
Theorem | cdlemg17irq 39024* | cdlemg17ir 39019 with π and π swapped. (Contributed by NM, 13-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΉβ(πΊβπ)) = (πΉβπ)) | ||
Theorem | cdlemg17jq 39025* | cdlemg17j 39020 with π and π swapped. (Contributed by NM, 13-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ(πΉβπ)) = (πΉβ(πΊβπ))) | ||
Theorem | cdlemg17 39026* | 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 39027 | Show two lines are different. TODO: fix comment. (Contributed by NM, 14-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ πΉ β π) β§ (π β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (π β¨ (πΉβπ)) β (π β¨ (πΉβπ))) | ||
Theorem | cdlemg18b 39028 | Lemma for cdlemg18c 39029. TODO: fix comment. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β Β¬ π β€ (π β¨ (πΉβπ))) | ||
Theorem | cdlemg18c 39029 | 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 39030* | 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 39031* | 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 39032* | 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 39033* | 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 39034* | 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 39035* | 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 39036* | cdlemg21 39035 with (πΉβπ) β π condition removed. (Contributed by NM, 23-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((π βπΉ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg24 39037* | Combine cdlemg16z 39008 and cdlemg22 39036. TODO: Fix comment. (Contributed by NM, 24-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg37 39038* | Use cdlemg8 38980 to eliminate the β (π β¨ π) condition of cdlemg24 39037. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ π β π β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg25zz 39039 | cdlemg16zz 39009 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 39040 | cdlemg16zz 39009 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 39041 | For use with case when (π β¨ π£) β§ (π β¨ (π βπΉ)) or (π β¨ π£) β§ (π β¨ (π βπΉ)) is zero, letting us establish Β¬ π§ β€ π β§ π§ β€ (π β¨ π£) via 4atex 38425. TODO: Fix comment. (Contributed by NM, 28-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β Β¬ (π βπΉ) β€ (π β¨ π§)) | ||
Theorem | cdlemg28a 39042 | 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 39043 | TODO: Fix comment. (Contributed by NM, 30-May-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π» β§ πΉ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ π£ β (π βπΉ) β§ (πΉβπ) β π)) β (π β π΄ β¨ π = (0.βπΎ))) | ||
Theorem | cdlemg31b0a 39044 | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (πΉ β π β§ π£ β (π βπΉ))) β (π β π΄ β¨ π = (0.βπΎ))) | ||
Theorem | cdlemg27b 39045 | TODO: Fix comment. (Contributed by NM, 28-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π§ β π΄ β§ (π£ β π΄ β§ π£ β€ π) β§ (πΉ β π β§ π§ β π)) β§ (π£ β (π βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β Β¬ (π βπΉ) β€ (π β¨ π§)) | ||
Theorem | cdlemg31a 39046 | TODO: fix comment. (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π£ β π΄ β§ πΉ β π)) β π β€ (π β¨ π£)) | ||
Theorem | cdlemg31b 39047 | TODO: fix comment. (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π£ β π΄ β§ πΉ β π)) β π β€ (π β¨ (π βπΉ))) | ||
Theorem | cdlemg31c 39048 | 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 39049 | Eliminate (πΉβπ) β π from cdlemg31c 39048. 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 39054 versus cdlemg28 39053. (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (πΉ β π β§ π£ β (π βπΉ) β§ π β π΄)) β Β¬ π β€ π) | ||
Theorem | cdlemg33b0 39050* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ π β π΄ β§ πΉ β π) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg33c0 39051* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ π§ β€ (π β¨ π£))) | ||
Theorem | cdlemg28b 39052* | 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 39053.) (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π§ β π΄ β§ Β¬ π§ β€ π) β§ (πΉ β π β§ πΊ β π)) β§ ((π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)) β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ)) β§ ((πΉβπ) β π β§ (πΊβπ) β π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π§ β¨ (πΉβ(πΊβπ§))) β§ π)) | ||
Theorem | cdlemg28 39053* | 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 39054 (and maybe leading up to this too)? (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π§ β π΄ β§ Β¬ π§ β€ π) β§ (πΉ β π β§ πΊ β π)) β§ ((π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)) β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ)) β§ ((πΉβπ) β π β§ (πΊβπ) β π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg29 39054* | Eliminate (πΉβπ) β π and (πΊβπ) β π from cdlemg28 39053. 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 39055* | TODO: Fix comment. (Contributed by NM, 29-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π β π΄ β§ π β π΄) β§ (πΉ β π β§ πΊ β π)) β§ ((π β π β§ π β π) β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg33b 39056* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π β π΄ β§ π β π΄) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg33c 39057* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π β π΄ β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg33d 39058* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π β π΄) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π βπΊ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg33e 39059* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg33 39060* | Combine cdlemg33b 39056, cdlemg33c 39057, cdlemg33d 39058, cdlemg33e 39059. TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (πΉ β π β§ πΊ β π) β§ π β π) β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
Theorem | cdlemg34 39061* | Use cdlemg33 to eliminate π§ from cdlemg29 39054. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (πΉ β π β§ πΊ β π) β§ π β π) β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg35 39062* | TODO: Fix comment. TODO: should we have a more general version of hlsupr 37735 to avoid the β conditions? (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (πΊβπ) β π β§ (π βπΉ) β (π βπΊ))) β βπ£ β π΄ (π£ β€ π β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ)))) | ||
Theorem | cdlemg36 39063* | Use cdlemg35 to eliminate π£ from cdlemg34 39061. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβπ) β π β§ (πΊβπ) β π) β§ (π βπΉ) β (π βπΊ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg38 39064 | Use cdlemg37 39038 to eliminate βπ β π΄ from cdlemg36 39063. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβπ) β π β§ (πΊβπ) β π) β§ (π βπΉ) β (π βπΊ))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg39 39065 | Eliminate β conditions from cdlemg38 39064. TODO: Would this better be done at cdlemg35 39062? TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg40 39066 | Eliminate π β π conditions from cdlemg39 39065. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
Theorem | cdlemg41 39067 | Convert cdlemg40 39066 to function composition. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((π β¨ ((πΉ β πΊ)βπ)) β§ π) = ((π β¨ ((πΉ β πΊ)βπ)) β§ π)) | ||
Theorem | ltrnco 39068 | 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 39069 | Swap the arguments of the trace of a composition with converse. (Contributed by NM, 1-Jul-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (π β(πΉ β β‘πΊ)) = (π β(πΊ β β‘πΉ))) | ||
Theorem | trlcoabs 39070 | Absorption into a composition by joining with trace. (Contributed by NM, 22-Jul-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΉ β πΊ)βπ) β¨ (π βπΉ)) = ((πΊβπ) β¨ (π βπΉ))) | ||
Theorem | trlcoabs2N 39071 | 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 39072 | 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 39073 | Commonly used special case of trlcoat 39072. (Contributed by NM, 1-Jul-2013.) |
β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π βπΉ) β (π βπΊ)) β (π β(πΉ β β‘πΊ)) β π΄) | ||
Theorem | trlconid 39074 | 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 39075 | Lemma for trlco 39076. (Contributed by NM, 1-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β(πΉ β πΊ)) β€ ((π βπΉ) β¨ (π βπΊ))) | ||
Theorem | trlco 39076 | 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 39077 | 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 39078 | 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 39079 | 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 39080 | 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 39081 | Eliminate (πΉβπ) β π, (πΊβπ) β π from cdlemg44a 39080. (Contributed by NM, 3-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π βπΉ) β (π βπΊ)) β (πΉβ(πΊβπ)) = (πΊβ(πΉβπ))) | ||
Theorem | cdlemg44 39082 | 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 39083 | TODO: fix comment. TODO: Use this above in place of (πΉβπ) = π antecedents? (Contributed by NM, 5-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ πΉ = ( I βΎ π΅)) β (πΉ β πΊ) = (πΊ β πΉ)) | ||
Theorem | cdlemg46 39084* | 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 39085* | 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 39086 | Eliminate β from cdlemg47 39085. (Contributed by NM, 5-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (πΉ β ( I βΎ π΅) β§ (π βπΉ) = (π βπΊ))) β (πΉ β πΊ) = (πΊ β πΉ)) | ||
Theorem | ltrncom 39087 | 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 39088 | Rearrange a composition of 4 translations, analogous to an4 655. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΈ β π β§ πΉ β π) β ((π· β πΈ) β (πΉ β πΊ)) = ((π· β πΉ) β (πΈ β πΊ))) | ||
Theorem | trljco 39089 | Trace joined with trace of composition. (Contributed by NM, 15-Jun-2013.) |
β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β ((π βπΉ) β¨ (π β(πΉ β πΊ))) = ((π βπΉ) β¨ (π βπΊ))) | ||
Theorem | trljco2 39090 | Trace joined with trace of composition. (Contributed by NM, 16-Jun-2013.) |
β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β ((π βπΉ) β¨ (π β(πΉ β πΊ))) = ((π βπΊ) β¨ (π β(πΉ β πΊ)))) | ||
Syntax | ctgrp 39091 | Extend class notation with translation group. |
class TGrp | ||
Definition | df-tgrp 39092* | Define the class of all translation groups. π is normally a member of HL. Each base set is the set of all lattice translations with respect to a hyperplane π€, and the operation is function composition. Similar to definition of G in [Crawley] p. 116, third paragraph (which defines this for geomodular lattices). (Contributed by NM, 5-Jun-2013.) |
β’ TGrp = (π β V β¦ (π€ β (LHypβπ) β¦ {β¨(Baseβndx), ((LTrnβπ)βπ€)β©, β¨(+gβndx), (π β ((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©})) | ||
Theorem | tgrpfset 39093* | The translation group maps for a lattice πΎ. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (TGrpβπΎ) = (π€ β π» β¦ {β¨(Baseβndx), ((LTrnβπΎ)βπ€)β©, β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©})) | ||
Theorem | tgrpset 39094* | The translation group for a fiducial co-atom π. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΊ = ((TGrpβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΊ = {β¨(Baseβndx), πβ©, β¨(+gβndx), (π β π, π β π β¦ (π β π))β©}) | ||
Theorem | tgrpbase 39095 | The base set of the translation group is the set of all translations (for a fiducial co-atom π). (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΊ = ((TGrpβπΎ)βπ) & β’ πΆ = (BaseβπΊ) β β’ ((πΎ β π β§ π β π») β πΆ = π) | ||
Theorem | tgrpopr 39096* | The group operation of the translation group is function composition. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΊ = ((TGrpβπΎ)βπ) & β’ + = (+gβπΊ) β β’ ((πΎ β π β§ π β π») β + = (π β π, π β π β¦ (π β π))) | ||
Theorem | tgrpov 39097 | The group operation value of the translation group is the composition of translations. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΊ = ((TGrpβπΎ)βπ) & β’ + = (+gβπΊ) β β’ ((πΎ β π β§ π β π» β§ (π β π β§ π β π)) β (π + π) = (π β π)) | ||
Theorem | tgrpgrplem 39098 | Lemma for tgrpgrp 39099. (Contributed by NM, 6-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΊ = ((TGrpβπΎ)βπ) & β’ + = (+gβπΊ) & β’ π΅ = (BaseβπΎ) β β’ ((πΎ β HL β§ π β π») β πΊ β Grp) | ||
Theorem | tgrpgrp 39099 | The translation group is a group. (Contributed by NM, 6-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ πΊ = ((TGrpβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β πΊ β Grp) | ||
Theorem | tgrpabl 39100 | The translation group is an Abelian group. Lemma G of [Crawley] p. 116. (Contributed by NM, 6-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ πΊ = ((TGrpβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β πΊ β Abel) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |