Step | Hyp | Ref
| Expression |
1 | | cdlemi.b |
. 2
β’ π΅ = (BaseβπΎ) |
2 | | cdlemi.l |
. 2
β’ β€ =
(leβπΎ) |
3 | | simp1l 1198 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β HL) |
4 | 3 | hllatd 37829 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β Lat) |
5 | | simp1 1137 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΎ β HL β§ π β π»)) |
6 | | simp2l 1200 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β πΈ) |
7 | | simp2r 1201 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΊ β π) |
8 | | cdlemi.h |
. . . . 5
β’ π» = (LHypβπΎ) |
9 | | cdlemi.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
10 | | cdlemi.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
11 | 8, 9, 10 | tendocl 39233 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΊ β π) β (πβπΊ) β π) |
12 | 5, 6, 7, 11 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβπΊ) β π) |
13 | | simp3l 1202 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π΄) |
14 | | cdlemi.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
15 | 1, 14 | atbase 37754 |
. . . 4
β’ (π β π΄ β π β π΅) |
16 | 13, 15 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π΅) |
17 | 1, 8, 9 | ltrncl 38591 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πβπΊ) β π β§ π β π΅) β ((πβπΊ)βπ) β π΅) |
18 | 5, 12, 16, 17 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπΊ)βπ) β π΅) |
19 | | cdlemi.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
20 | 1, 8, 9, 19 | trlcl 38630 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πβπΊ) β π) β (π
β(πβπΊ)) β π΅) |
21 | 5, 12, 20 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π
β(πβπΊ)) β π΅) |
22 | | cdlemi.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
23 | 1, 22 | latjcl 18329 |
. . 3
β’ ((πΎ β Lat β§ π β π΅ β§ (π
β(πβπΊ)) β π΅) β (π β¨ (π
β(πβπΊ))) β π΅) |
24 | 4, 16, 21, 23 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
β(πβπΊ))) β π΅) |
25 | 1, 8, 9, 19 | trlcl 38630 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
βπΊ) β π΅) |
26 | 5, 7, 25 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΊ) β π΅) |
27 | 1, 22 | latjcl 18329 |
. . 3
β’ ((πΎ β Lat β§ π β π΅ β§ (π
βπΊ) β π΅) β (π β¨ (π
βπΊ)) β π΅) |
28 | 4, 16, 26, 27 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
βπΊ)) β π΅) |
29 | 1, 2, 22 | latlej2 18339 |
. . . 4
β’ ((πΎ β Lat β§ π β π΅ β§ ((πβπΊ)βπ) β π΅) β ((πβπΊ)βπ) β€ (π β¨ ((πβπΊ)βπ))) |
30 | 4, 16, 18, 29 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπΊ)βπ) β€ (π β¨ ((πβπΊ)βπ))) |
31 | | cdlemi.m |
. . . . . . 7
β’ β§ =
(meetβπΎ) |
32 | 2, 22, 31, 14, 8, 9, 19 | trlval2 38629 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πβπΊ) β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
β(πβπΊ)) = ((π β¨ ((πβπΊ)βπ)) β§ π)) |
33 | 12, 32 | syld3an2 1412 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π
β(πβπΊ)) = ((π β¨ ((πβπΊ)βπ)) β§ π)) |
34 | 33 | oveq2d 7374 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
β(πβπΊ))) = (π β¨ ((π β¨ ((πβπΊ)βπ)) β§ π))) |
35 | 1, 22 | latjcl 18329 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ ((πβπΊ)βπ) β π΅) β (π β¨ ((πβπΊ)βπ)) β π΅) |
36 | 4, 16, 18, 35 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ ((πβπΊ)βπ)) β π΅) |
37 | | simp1r 1199 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π») |
38 | 1, 8 | lhpbase 38464 |
. . . . . 6
β’ (π β π» β π β π΅) |
39 | 37, 38 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π΅) |
40 | 1, 2, 22 | latlej1 18338 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ ((πβπΊ)βπ) β π΅) β π β€ (π β¨ ((πβπΊ)βπ))) |
41 | 4, 16, 18, 40 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β€ (π β¨ ((πβπΊ)βπ))) |
42 | 1, 2, 22, 31, 14 | atmod3i1 38330 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ (π β¨ ((πβπΊ)βπ)) β π΅ β§ π β π΅) β§ π β€ (π β¨ ((πβπΊ)βπ))) β (π β¨ ((π β¨ ((πβπΊ)βπ)) β§ π)) = ((π β¨ ((πβπΊ)βπ)) β§ (π β¨ π))) |
43 | 3, 13, 36, 39, 41, 42 | syl131anc 1384 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ ((π β¨ ((πβπΊ)βπ)) β§ π)) = ((π β¨ ((πβπΊ)βπ)) β§ (π β¨ π))) |
44 | | eqid 2737 |
. . . . . . . 8
β’
(1.βπΎ) =
(1.βπΎ) |
45 | 2, 22, 44, 14, 8 | lhpjat2 38487 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ π) = (1.βπΎ)) |
46 | 45 | 3adant2 1132 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ π) = (1.βπΎ)) |
47 | 46 | oveq2d 7374 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ ((πβπΊ)βπ)) β§ (π β¨ π)) = ((π β¨ ((πβπΊ)βπ)) β§ (1.βπΎ))) |
48 | | hlol 37826 |
. . . . . . 7
β’ (πΎ β HL β πΎ β OL) |
49 | 3, 48 | syl 17 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β OL) |
50 | 1, 31, 44 | olm11 37692 |
. . . . . 6
β’ ((πΎ β OL β§ (π β¨ ((πβπΊ)βπ)) β π΅) β ((π β¨ ((πβπΊ)βπ)) β§ (1.βπΎ)) = (π β¨ ((πβπΊ)βπ))) |
51 | 49, 36, 50 | syl2anc 585 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ ((πβπΊ)βπ)) β§ (1.βπΎ)) = (π β¨ ((πβπΊ)βπ))) |
52 | 47, 51 | eqtrd 2777 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ ((πβπΊ)βπ)) β§ (π β¨ π)) = (π β¨ ((πβπΊ)βπ))) |
53 | 34, 43, 52 | 3eqtrd 2781 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
β(πβπΊ))) = (π β¨ ((πβπΊ)βπ))) |
54 | 30, 53 | breqtrrd 5134 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπΊ)βπ) β€ (π β¨ (π
β(πβπΊ)))) |
55 | 2, 8, 9, 19, 10 | tendotp 39227 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΊ β π) β (π
β(πβπΊ)) β€ (π
βπΊ)) |
56 | 5, 6, 7, 55 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π
β(πβπΊ)) β€ (π
βπΊ)) |
57 | 1, 2, 22 | latjlej2 18344 |
. . . 4
β’ ((πΎ β Lat β§ ((π
β(πβπΊ)) β π΅ β§ (π
βπΊ) β π΅ β§ π β π΅)) β ((π
β(πβπΊ)) β€ (π
βπΊ) β (π β¨ (π
β(πβπΊ))) β€ (π β¨ (π
βπΊ)))) |
58 | 4, 21, 26, 16, 57 | syl13anc 1373 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π
β(πβπΊ)) β€ (π
βπΊ) β (π β¨ (π
β(πβπΊ))) β€ (π β¨ (π
βπΊ)))) |
59 | 56, 58 | mpd 15 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
β(πβπΊ))) β€ (π β¨ (π
βπΊ))) |
60 | 1, 2, 4, 18, 24, 28, 54, 59 | lattrd 18336 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπΊ)βπ) β€ (π β¨ (π
βπΊ))) |