Step | Hyp | Ref
| Expression |
1 | | simp11l 1285 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β πΎ β HL) |
2 | | simp22l 1293 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β π β π΄) |
3 | | simp11 1204 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (πΎ β HL β§ π β π»)) |
4 | | simp21 1207 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β π β π) |
5 | | cdlemk1.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
6 | | cdlemk1.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
7 | | cdlemk1.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
8 | | cdlemk1.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
9 | 5, 6, 7, 8 | ltrnat 38649 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π΄) β (πβπ) β π΄) |
10 | 3, 4, 2, 9 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (πβπ) β π΄) |
11 | | cdlemk1.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
12 | 5, 11, 6 | hlatlej2 37884 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ (πβπ) β π΄) β (πβπ) β€ (π β¨ (πβπ))) |
13 | 1, 2, 10, 12 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (πβπ) β€ (π β¨ (πβπ))) |
14 | | simp23 1209 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (π
βπΉ) = (π
βπ)) |
15 | 14 | oveq2d 7374 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (π β¨ (π
βπΉ)) = (π β¨ (π
βπ))) |
16 | | simp22 1208 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (π β π΄ β§ Β¬ π β€ π)) |
17 | | cdlemk1.r |
. . . . . 6
β’ π
= ((trLβπΎ)βπ) |
18 | 5, 11, 6, 7, 8, 17 | trljat1 38675 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π
βπ)) = (π β¨ (πβπ))) |
19 | 3, 4, 16, 18 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (π β¨ (π
βπ)) = (π β¨ (πβπ))) |
20 | 15, 19 | eqtr2d 2774 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (π β¨ (πβπ)) = (π β¨ (π
βπΉ))) |
21 | 13, 20 | breqtrd 5132 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (πβπ) β€ (π β¨ (π
βπΉ))) |
22 | | cdlemk1.b |
. . 3
β’ π΅ = (BaseβπΎ) |
23 | | cdlemk1.m |
. . 3
β’ β§ =
(meetβπΎ) |
24 | | cdlemk1.s |
. . 3
β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))))) |
25 | | cdlemk1.o |
. . 3
β’ π = (πβπ·) |
26 | 22, 5, 11, 23, 6, 7, 8, 17, 24, 25 | cdlemk14 39363 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (πβπ) β€ ((πβπ) β¨ (π
β(πΉ β β‘π·)))) |
27 | 1 | hllatd 37872 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β πΎ β Lat) |
28 | 22, 6 | atbase 37797 |
. . . 4
β’ ((πβπ) β π΄ β (πβπ) β π΅) |
29 | 10, 28 | syl 17 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (πβπ) β π΅) |
30 | | simp12 1205 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β πΉ β π) |
31 | | simp31 1210 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β πΉ β ( I βΎ π΅)) |
32 | 22, 6, 7, 8, 17 | trlnidat 38682 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΉ β ( I βΎ π΅)) β (π
βπΉ) β π΄) |
33 | 3, 30, 31, 32 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (π
βπΉ) β π΄) |
34 | 22, 11, 6 | hlatjcl 37875 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ (π
βπΉ) β π΄) β (π β¨ (π
βπΉ)) β π΅) |
35 | 1, 2, 33, 34 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (π β¨ (π
βπΉ)) β π΅) |
36 | 25 | fveq1i 6844 |
. . . . 5
β’ (πβπ) = ((πβπ·)βπ) |
37 | 22, 5, 11, 6, 7, 8,
17, 23, 24 | cdlemksat 39355 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β ((πβπ·)βπ) β π΄) |
38 | 36, 37 | eqeltrid 2838 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (πβπ) β π΄) |
39 | | simp13 1206 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β π· β π) |
40 | | simp33 1212 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (π
βπ·) β (π
βπΉ)) |
41 | 40 | necomd 2996 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (π
βπΉ) β (π
βπ·)) |
42 | 6, 7, 8, 17 | trlcocnvat 39233 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π· β π) β§ (π
βπΉ) β (π
βπ·)) β (π
β(πΉ β β‘π·)) β π΄) |
43 | 3, 30, 39, 41, 42 | syl121anc 1376 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (π
β(πΉ β β‘π·)) β π΄) |
44 | 22, 11, 6 | hlatjcl 37875 |
. . . 4
β’ ((πΎ β HL β§ (πβπ) β π΄ β§ (π
β(πΉ β β‘π·)) β π΄) β ((πβπ) β¨ (π
β(πΉ β β‘π·))) β π΅) |
45 | 1, 38, 43, 44 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β ((πβπ) β¨ (π
β(πΉ β β‘π·))) β π΅) |
46 | 22, 5, 23 | latlem12 18360 |
. . 3
β’ ((πΎ β Lat β§ ((πβπ) β π΅ β§ (π β¨ (π
βπΉ)) β π΅ β§ ((πβπ) β¨ (π
β(πΉ β β‘π·))) β π΅)) β (((πβπ) β€ (π β¨ (π
βπΉ)) β§ (πβπ) β€ ((πβπ) β¨ (π
β(πΉ β β‘π·)))) β (πβπ) β€ ((π β¨ (π
βπΉ)) β§ ((πβπ) β¨ (π
β(πΉ β β‘π·)))))) |
47 | 27, 29, 35, 45, 46 | syl13anc 1373 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (((πβπ) β€ (π β¨ (π
βπΉ)) β§ (πβπ) β€ ((πβπ) β¨ (π
β(πΉ β β‘π·)))) β (πβπ) β€ ((π β¨ (π
βπΉ)) β§ ((πβπ) β¨ (π
β(πΉ β β‘π·)))))) |
48 | 21, 26, 47 | mpbi2and 711 |
1
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π
βπ·) β (π
βπΉ))) β (πβπ) β€ ((π β¨ (π
βπΉ)) β§ ((πβπ) β¨ (π
β(πΉ β β‘π·))))) |