HomeTheorem List (p. 396 of 479)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 396 of 479) | < 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-30166) |
Hilbert Space Explorer
(30167-31689) |
Users' Mathboxes
(31690-47842) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdlemg10b 39501 | TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in ltrn* area? (Contributed by NM, 4-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β (((πΉβπ) β¨ (πΉβπ)) β§ π) = ((π β¨ π) β§ π)) | ||
| Theorem | cdlemg10bALTN 39502 | TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in ltrn* area? TODO: Compare this proof to cdlemg2m 39470 and pick best, if moved to ltrn* area. (Contributed by NM, 4-May-2013.) (New usage is discouraged.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΉβπ) β¨ (πΉβπ)) β§ π) = ((π β¨ π) β§ π)) | ||
| Theorem | cdlemg11a 39503 | TODO: FIX COMMENT. (Contributed by NM, 4-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΉβ(πΊβπ)) β π) | ||
| Theorem | cdlemg11aq 39504 | TODO: FIX COMMENT. TODO: can proof using this be restructured to use cdlemg11a 39503? (Contributed by NM, 4-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (πΉβ(πΊβπ)) β π) | ||
| Theorem | cdlemg10c 39505 | TODO: FIX COMMENT. TODO: Can this be moved up as a stand-alone theorem in trl* area? (Contributed by NM, 4-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((π βπΉ) β€ ((πΊβπ) β¨ (πΊβπ)) β (π βπΉ) β€ (π β¨ π))) | ||
| Theorem | cdlemg10a 39506 | TODO: FIX COMMENT. (Contributed by NM, 3-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β€ ((π βπΉ) β¨ (π βπΊ))) | ||
| Theorem | cdlemg10 39507 | TODO: FIX COMMENT. (Contributed by NM, 4-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β€ π) | ||
| Theorem | cdlemg11b 39508 | TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (πΊ β π β§ π β π β§ Β¬ (π βπΊ) β€ (π β¨ π))) β (π β¨ π) β ((πΊβπ) β¨ (πΊβπ))) | ||
| Theorem | cdlemg12a 39509 | TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ π β π β§ (π β¨ π) β ((πΊβπ) β¨ π))) β ((π β¨ π) β§ ((πΊβπ) β¨ π)) β€ ((πΉβ(πΊβπ)) β¨ π)) | ||
| Theorem | cdlemg12b 39510 | 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 39511 | The triples β¨π, (πΉβπ), (πΉβ(πΊβπ))β© and β¨π, (πΉβπ), (πΉβ(πΊβπ))β© are axially perspective by dalaw 38752. TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ π β π β§ Β¬ (π βπΊ) β€ (π β¨ π))) β ((π β¨ (πΊβπ)) β§ (π β¨ (πΊβπ))) β€ ((((πΊβπ) β¨ (πΉβ(πΊβπ))) β§ ((πΊβπ) β¨ (πΉβ(πΊβπ)))) β¨ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)))) | ||
| Theorem | cdlemg12d 39512 | TODO: FIX COMMENT. (Contributed by NM, 5-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ (π β π β§ Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π))) β (π βπΊ) β€ ((π βπΉ) β¨ (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)))) | ||
| Theorem | cdlemg12e 39513 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ 0 = (0.βπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π) β§ (π βπΉ) β (π βπΊ))) β (((πΉβ(πΊβπ)) β¨ π) β§ ((πΉβ(πΊβπ)) β¨ π)) β 0 ) | ||
| Theorem | cdlemg12f 39514 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π)) β§ (π βπΉ) β (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β€ ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg12g 39515 | TODO: FIX COMMENT. TODO: Combine with cdlemg12f 39514. (Contributed by NM, 6-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π)) β§ (π βπΉ) β (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg12 39516 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π)) β§ (π βπΉ) β (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg13a 39517 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π βπΉ) = (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β (π β¨ (πΉβ(πΊβπ))) = ((πΊβπ) β¨ (πΉβ(πΊβπ)))) | ||
| Theorem | cdlemg13 39518 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (π βπΉ) = (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg14f 39519 | TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ (πΉβπ) = π)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg14g 39520 | TODO: FIX COMMENT. (Contributed by NM, 22-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ (πΊβπ) = π)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg15a 39521 | Eliminate the (πΉβπ) β π condition from cdlemg13 39518. TODO: FIX COMMENT. (Contributed by NM, 6-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ ((π βπΉ) = (π βπΊ) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg15 39522 | Eliminate the ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) condition from cdlemg13 39518. TODO: FIX COMMENT. (Contributed by NM, 25-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π) β§ (π βπΉ) = (π βπΊ)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg16 39523 | Part of proof of Lemma G of [Crawley] p. 116; 2nd line p. 117, which says that (our) cdlemg10 39507 "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 38752, in order to make this inference. This final step eliminates the (π βπΉ) β (π βπΊ) condition from cdlemg12 39516. 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 39524 | This version of cdlemg16 39523 uses cdlemg15a 39521 instead of cdlemg15 39522, in case cdlemg15 39522 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 39525 | Eliminate ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) condition from cdlemg16 39523. 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 39526 | Eliminate π β π from cdlemg16z 39525. TODO: Use this only if needed. (Contributed by NM, 26-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ Β¬ (π βπΉ) β€ (π β¨ π) β§ Β¬ (π βπΊ) β€ (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg17a 39527 | TODO: FIX COMMENT. (Contributed by NM, 8-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΊ β π β§ (π βπΊ) β€ (π β¨ π))) β (πΊβπ) β€ (π β¨ π)) | ||
| Theorem | cdlemg17b 39528* | 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 39156. (Contributed by NM, 8-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβπ) = π) | ||
| Theorem | cdlemg17dN 39529* | TODO: fix comment. (Contributed by NM, 9-May-2013.) (New usage is discouraged.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π» β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ ((π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)) β§ (πΊβπ) β π)) β (π βπΊ) = ((π β¨ π) β§ π)) | ||
| Theorem | cdlemg17dALTN 39530 | Same as cdlemg17dN 39529 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 39531* | TODO: fix comment. (Contributed by NM, 8-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (π βπΊ))) | ||
| Theorem | cdlemg17f 39532* | TODO: fix comment. (Contributed by NM, 8-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (πΊβ(πΉβπ)))) | ||
| Theorem | cdlemg17g 39533* | TODO: fix comment. (Contributed by NM, 9-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ(πΉβπ)) β€ ((πΉβπ) β¨ (πΉβπ))) | ||
| Theorem | cdlemg17h 39534* | TODO: fix comment. (Contributed by NM, 10-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ πΊ β π) β§ (π β π β§ π β€ ((πΉβπ) β¨ (πΉβπ)))) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π = (πΉβπ) β¨ π = (πΉβπ))) | ||
| Theorem | cdlemg17i 39535* | TODO: fix comment. (Contributed by NM, 10-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ(πΉβπ)) = (πΉβπ)) | ||
| Theorem | cdlemg17ir 39536* | TODO: fix comment. (Contributed by NM, 13-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΉβ(πΊβπ)) = (πΉβπ)) | ||
| Theorem | cdlemg17j 39537* | TODO: fix comment. (Contributed by NM, 11-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ(πΉβπ)) = (πΉβ(πΊβπ))) | ||
| Theorem | cdlemg17pq 39538* | 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 39539* | cdlemg17b 39528 with π and π swapped. Antecedent πΉ β (πβπ) is redundant for easier use. TODO: should we have redundant antecedent for cdlemg17b 39528 also? (Contributed by NM, 13-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβπ) = π) | ||
| Theorem | cdlemg17iqN 39540* | cdlemg17i 39535 with π and π swapped. (Contributed by NM, 13-May-2013.) (New usage is discouraged.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π» β§ (πΉ β π β§ πΊ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ ((π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)) β§ (πΊβπ) β π)) β (πΊβ(πΉβπ)) = (πΉβπ)) | ||
| Theorem | cdlemg17irq 39541* | cdlemg17ir 39536 with π and π swapped. (Contributed by NM, 13-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΉβ(πΊβπ)) = (πΉβπ)) | ||
| Theorem | cdlemg17jq 39542* | cdlemg17j 39537 with π and π swapped. (Contributed by NM, 13-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ(πΉβπ)) = (πΉβ(πΊβπ))) | ||
| Theorem | cdlemg17 39543* | 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 39544 | Show two lines are different. TODO: fix comment. (Contributed by NM, 14-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ πΉ β π) β§ (π β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β (π β¨ (πΉβπ)) β (π β¨ (πΉβπ))) | ||
| Theorem | cdlemg18b 39545 | Lemma for cdlemg18c 39546. TODO: fix comment. (Contributed by NM, 15-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (π β π β§ (πΉβπ) β π β§ ((πΉβπ) β¨ (πΉβπ)) β (π β¨ π))) β Β¬ π β€ (π β¨ (πΉβπ))) | ||
| Theorem | cdlemg18c 39546 | 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 39547* | 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 39548* | 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 39549* | 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 39550* | 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 39551* | 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 39552* | 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 39553* | cdlemg21 39552 with (πΉβπ) β π condition removed. (Contributed by NM, 23-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((π βπΉ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg24 39554* | Combine cdlemg16z 39525 and cdlemg22 39553. TODO: Fix comment. (Contributed by NM, 24-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg37 39555* | Use cdlemg8 39497 to eliminate the β (π β¨ π) condition of cdlemg24 39554. (Contributed by NM, 31-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ π β π β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg25zz 39556 | cdlemg16zz 39526 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 39557 | cdlemg16zz 39526 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 39558 | For use with case when (π β¨ π£) β§ (π β¨ (π βπΉ)) or (π β¨ π£) β§ (π β¨ (π βπΉ)) is zero, letting us establish Β¬ π§ β€ π β§ π§ β€ (π β¨ π£) via 4atex 38942. TODO: Fix comment. (Contributed by NM, 28-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (π§ β π΄ β§ πΉ β π) β§ (π£ β (π βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β Β¬ (π βπΉ) β€ (π β¨ π§)) | ||
| Theorem | cdlemg28a 39559 | 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 39560 | TODO: Fix comment. (Contributed by NM, 30-May-2013.) (New usage is discouraged.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π» β§ πΉ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ π£ β (π βπΉ) β§ (πΉβπ) β π)) β (π β π΄ β¨ π = (0.βπΎ))) | ||
| Theorem | cdlemg31b0a 39561 | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (πΉ β π β§ π£ β (π βπΉ))) β (π β π΄ β¨ π = (0.βπΎ))) | ||
| Theorem | cdlemg27b 39562 | TODO: Fix comment. (Contributed by NM, 28-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π§ β π΄ β§ (π£ β π΄ β§ π£ β€ π) β§ (πΉ β π β§ π§ β π)) β§ (π£ β (π βπΉ) β§ π§ β€ (π β¨ π£) β§ (πΉβπ) β π)) β Β¬ (π βπΉ) β€ (π β¨ π§)) | ||
| Theorem | cdlemg31a 39563 | TODO: fix comment. (Contributed by NM, 29-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π£ β π΄ β§ πΉ β π)) β π β€ (π β¨ π£)) | ||
| Theorem | cdlemg31b 39564 | TODO: fix comment. (Contributed by NM, 29-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π£ β π΄ β§ πΉ β π)) β π β€ (π β¨ (π βπΉ))) | ||
| Theorem | cdlemg31c 39565 | 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 39566 | Eliminate (πΉβπ) β π from cdlemg31c 39565. 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 39571 versus cdlemg28 39570. (Contributed by NM, 29-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π£ β π΄ β§ π£ β€ π)) β§ (πΉ β π β§ π£ β (π βπΉ) β§ π β π΄)) β Β¬ π β€ π) | ||
| Theorem | cdlemg33b0 39567* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ π β π΄ β§ πΉ β π) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β€ (π β¨ π£)))) | ||
| Theorem | cdlemg33c0 39568* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ π§ β€ (π β¨ π£))) | ||
| Theorem | cdlemg28b 39569* | 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 39570.) (Contributed by NM, 29-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π§ β π΄ β§ Β¬ π§ β€ π) β§ (πΉ β π β§ πΊ β π)) β§ ((π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)) β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ)) β§ ((πΉβπ) β π β§ (πΊβπ) β π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π§ β¨ (πΉβ(πΊβπ§))) β§ π)) | ||
| Theorem | cdlemg28 39570* | 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 39571 (and maybe leading up to this too)? (Contributed by NM, 29-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π§ β π΄ β§ Β¬ π§ β€ π) β§ (πΉ β π β§ πΊ β π)) β§ ((π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)) β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ)) β§ ((πΉβπ) β π β§ (πΊβπ) β π))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg29 39571* | Eliminate (πΉβπ) β π and (πΊβπ) β π from cdlemg28 39570. 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 39572* | TODO: Fix comment. (Contributed by NM, 29-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π β π΄ β§ π β π΄) β§ (πΉ β π β§ πΊ β π)) β§ ((π β π β§ π β π) β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
| Theorem | cdlemg33b 39573* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π β π΄ β§ π β π΄) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
| Theorem | cdlemg33c 39574* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π β π΄ β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
| Theorem | cdlemg33d 39575* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π β π΄) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π βπΊ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
| Theorem | cdlemg33e 39576* | TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
| Theorem | cdlemg33 39577* | Combine cdlemg33b 39573, cdlemg33c 39574, cdlemg33d 39575, cdlemg33e 39576. TODO: Fix comment. (Contributed by NM, 30-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (πΉ β π β§ πΊ β π) β§ π β π) β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) | ||
| Theorem | cdlemg34 39578* | Use cdlemg33 to eliminate π§ from cdlemg29 39571. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΉ))) & β’ π = ((π β¨ π£) β§ (π β¨ (π βπΊ))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (πΉ β π β§ πΊ β π) β§ π β π) β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg35 39579* | TODO: Fix comment. TODO: should we have a more general version of hlsupr 38252 to avoid the β conditions? (Contributed by NM, 31-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ ((πΉβπ) β π β§ (πΊβπ) β π β§ (π βπΉ) β (π βπΊ))) β βπ£ β π΄ (π£ β€ π β§ (π£ β (π βπΉ) β§ π£ β (π βπΊ)))) | ||
| Theorem | cdlemg36 39580* | Use cdlemg35 to eliminate π£ from cdlemg34 39578. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβπ) β π β§ (πΊβπ) β π) β§ (π βπΉ) β (π βπΊ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg38 39581 | Use cdlemg37 39555 to eliminate βπ β π΄ from cdlemg36 39580. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβπ) β π β§ (πΊβπ) β π) β§ (π βπΉ) β (π βπΊ))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg39 39582 | Eliminate β conditions from cdlemg38 39581. TODO: Would this better be done at cdlemg35 39579? TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg40 39583 | Eliminate π β π conditions from cdlemg39 39582. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) | ||
| Theorem | cdlemg41 39584 | Convert cdlemg40 39583 to function composition. TODO: Fix comment. (Contributed by NM, 31-May-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((π β¨ ((πΉ β πΊ)βπ)) β§ π) = ((π β¨ ((πΉ β πΊ)βπ)) β§ π)) | ||
| Theorem | ltrnco 39585 | 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 39586 | Swap the arguments of the trace of a composition with converse. (Contributed by NM, 1-Jul-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (π β(πΉ β β‘πΊ)) = (π β(πΊ β β‘πΉ))) | ||
| Theorem | trlcoabs 39587 | Absorption into a composition by joining with trace. (Contributed by NM, 22-Jul-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΉ β πΊ)βπ) β¨ (π βπΉ)) = ((πΊβπ) β¨ (π βπΉ))) | ||
| Theorem | trlcoabs2N 39588 | 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 39589 | 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 39590 | Commonly used special case of trlcoat 39589. (Contributed by NM, 1-Jul-2013.) |
| β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π βπΉ) β (π βπΊ)) β (π β(πΉ β β‘πΊ)) β π΄) | ||
| Theorem | trlconid 39591 | 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 39592 | Lemma for trlco 39593. (Contributed by NM, 1-Jun-2013.) |
| β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β(πΉ β πΊ)) β€ ((π βπΉ) β¨ (π βπΊ))) | ||
| Theorem | trlco 39593 | 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 39594 | 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 39595 | 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 39596 | 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 39597 | 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 39598 | Eliminate (πΉβπ) β π, (πΊβπ) β π from cdlemg44a 39597. (Contributed by NM, 3-Jun-2013.) |
| β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π βπΉ) β (π βπΊ)) β (πΉβ(πΊβπ)) = (πΊβ(πΉβπ))) | ||
| Theorem | cdlemg44 39599 | 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 39600 | TODO: fix comment. TODO: Use this above in place of (πΉβπ) = π antecedents? (Contributed by NM, 5-Jun-2013.) |
| β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ πΉ = ( I βΎ π΅)) β (πΉ β πΊ) = (πΊ β πΉ)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |