Step | Hyp | Ref
| Expression |
1 | | simp1 1133 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β (πΎ β HL β§ π β π»)) |
2 | | simp2r 1197 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β (π β π΄ β§ Β¬ π β€ π)) |
3 | | simp2l 1196 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β (π β π΄ β§ Β¬ π β€ π)) |
4 | | simp3 1135 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β πΉ β π) |
5 | | cdlemg2inv.h |
. . . 4
β’ π» = (LHypβπΎ) |
6 | | cdlemg2inv.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
7 | | cdlemg2j.l |
. . . 4
β’ β€ =
(leβπΎ) |
8 | | cdlemg2j.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
9 | | cdlemg2j.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
10 | | cdlemg2j.m |
. . . 4
β’ β§ =
(meetβπΎ) |
11 | | eqid 2726 |
. . . 4
β’ ((π β¨ π) β§ π) = ((π β¨ π) β§ π) |
12 | 5, 6, 7, 8, 9, 10,
11 | cdlemg2k 39985 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ ((π β¨ π) β§ π))) |
13 | 1, 2, 3, 4, 12 | syl121anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ ((π β¨ π) β§ π))) |
14 | | simp1l 1194 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β πΎ β HL) |
15 | | simp2ll 1237 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β π β π΄) |
16 | 7, 9, 5, 6 | ltrnat 39524 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π΄) β (πΉβπ) β π΄) |
17 | 1, 4, 15, 16 | syl3anc 1368 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β (πΉβπ) β π΄) |
18 | | simp2rl 1239 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β π β π΄) |
19 | 7, 9, 5, 6 | ltrnat 39524 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π΄) β (πΉβπ) β π΄) |
20 | 1, 4, 18, 19 | syl3anc 1368 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β (πΉβπ) β π΄) |
21 | 8, 9 | hlatjcom 38751 |
. . 3
β’ ((πΎ β HL β§ (πΉβπ) β π΄ β§ (πΉβπ) β π΄) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (πΉβπ))) |
22 | 14, 17, 20, 21 | syl3anc 1368 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ (πΉβπ))) |
23 | | cdlemg2j.u |
. . . 4
β’ π = ((π β¨ π) β§ π) |
24 | 8, 9 | hlatjcom 38751 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = (π β¨ π)) |
25 | 14, 15, 18, 24 | syl3anc 1368 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β (π β¨ π) = (π β¨ π)) |
26 | 25 | oveq1d 7420 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β ((π β¨ π) β§ π) = ((π β¨ π) β§ π)) |
27 | 23, 26 | eqtrid 2778 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β π = ((π β¨ π) β§ π)) |
28 | 27 | oveq2d 7421 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β ((πΉβπ) β¨ π) = ((πΉβπ) β¨ ((π β¨ π) β§ π))) |
29 | 13, 22, 28 | 3eqtr4d 2776 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ π)) |