Step | Hyp | Ref
| Expression |
1 | | cdlemg12.l |
. . 3
β’ β€ =
(leβπΎ) |
2 | | cdlemg12.j |
. . 3
β’ β¨ =
(joinβπΎ) |
3 | | cdlemg12.m |
. . 3
β’ β§ =
(meetβπΎ) |
4 | | cdlemg12.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
5 | | cdlemg12.h |
. . 3
β’ π» = (LHypβπΎ) |
6 | | cdlemg12.t |
. . 3
β’ π = ((LTrnβπΎ)βπ) |
7 | | cdlemg12b.r |
. . 3
β’ π
= ((trLβπΎ)βπ) |
8 | 1, 2, 3, 4, 5, 6, 7 | cdlemg17e 39157 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π
βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (π
βπΊ))) |
9 | | simp11 1204 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π
βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΎ β HL β§ π β π»)) |
10 | | simp22 1208 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π
βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β πΊ β π) |
11 | | simp21 1207 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π
βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β πΉ β π) |
12 | | simp12 1205 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π
βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π β π΄ β§ Β¬ π β€ π)) |
13 | 1, 4, 5, 6 | ltrnel 38631 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) |
14 | 9, 11, 12, 13 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π
βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) |
15 | 1, 2, 3, 4, 5, 6, 7 | trlval2 38655 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) β (π
βπΊ) = (((πΉβπ) β¨ (πΊβ(πΉβπ))) β§ π)) |
16 | 9, 10, 14, 15 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π
βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π
βπΊ) = (((πΉβπ) β¨ (πΊβ(πΉβπ))) β§ π)) |
17 | 16 | oveq2d 7378 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π
βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβπ) β¨ (π
βπΊ)) = ((πΉβπ) β¨ (((πΉβπ) β¨ (πΊβ(πΉβπ))) β§ π))) |
18 | | simp12l 1287 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π
βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π β π΄) |
19 | 1, 4, 5, 6 | ltrncoat 38636 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ πΉ β π) β§ π β π΄) β (πΊβ(πΉβπ)) β π΄) |
20 | 9, 10, 11, 18, 19 | syl121anc 1376 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π
βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβ(πΉβπ)) β π΄) |
21 | | eqid 2737 |
. . . 4
β’ (((πΉβπ) β¨ (πΊβ(πΉβπ))) β§ π) = (((πΉβπ) β¨ (πΊβ(πΉβπ))) β§ π) |
22 | 1, 2, 3, 4, 5, 21 | cdleme0cp 38706 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π) β§ (πΊβ(πΉβπ)) β π΄)) β ((πΉβπ) β¨ (((πΉβπ) β¨ (πΊβ(πΉβπ))) β§ π)) = ((πΉβπ) β¨ (πΊβ(πΉβπ)))) |
23 | 9, 14, 20, 22 | syl12anc 836 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π
βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβπ) β¨ (((πΉβπ) β¨ (πΊβ(πΉβπ))) β§ π)) = ((πΉβπ) β¨ (πΊβ(πΉβπ)))) |
24 | 8, 17, 23 | 3eqtrd 2781 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((πΊβπ) β π β§ (π
βπΊ) β€ (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (πΊβ(πΉβπ)))) |