Step | Hyp | Ref
| Expression |
1 | | cdlemk4.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | cdlemk4.l |
. . 3
β’ β€ =
(leβπΎ) |
3 | | cdlemk4.j |
. . 3
β’ β¨ =
(joinβπΎ) |
4 | | cdlemk4.m |
. . 3
β’ β§ =
(meetβπΎ) |
5 | | cdlemk4.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
6 | | cdlemk4.h |
. . 3
β’ π» = (LHypβπΎ) |
7 | | cdlemk4.t |
. . 3
β’ π = ((LTrnβπΎ)βπ) |
8 | | cdlemk4.r |
. . 3
β’ π
= ((trLβπΎ)βπ) |
9 | | cdlemk4.z |
. . 3
β’ π = ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) |
10 | | cdlemk4.y |
. . 3
β’ π = ((π β¨ (π
βπΊ)) β§ (π β¨ (π
β(πΊ β β‘π)))) |
11 | | cdlemk4.x |
. . 3
β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)) β (π§βπ) = π)) |
12 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11 | cdlemk36 39422 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πβπ) = π) |
13 | | simp11l 1285 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β πΎ β HL) |
14 | 13 | hllatd 37872 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β πΎ β Lat) |
15 | | simp22l 1293 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β π β π΄) |
16 | | simp11 1204 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πΎ β HL β§ π β π»)) |
17 | | simp13l 1289 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β πΊ β π) |
18 | | simp13r 1290 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β πΊ β ( I βΎ π΅)) |
19 | 1, 5, 6, 7, 8 | trlnidat 38682 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ πΊ β ( I βΎ π΅)) β (π
βπΊ) β π΄) |
20 | 16, 17, 18, 19 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π
βπΊ) β π΄) |
21 | 1, 3, 5 | hlatjcl 37875 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ (π
βπΊ) β π΄) β (π β¨ (π
βπΊ)) β π΅) |
22 | 13, 15, 20, 21 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π β¨ (π
βπΊ)) β π΅) |
23 | | simp3l 1202 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β π β π) |
24 | | simp3r1 1282 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β π β ( I βΎ π΅)) |
25 | 1, 5, 6, 7, 8 | trlnidat 38682 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β ( I βΎ π΅)) β (π
βπ) β π΄) |
26 | 16, 23, 24, 25 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π
βπ) β π΄) |
27 | 1, 3, 5 | hlatjcl 37875 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄ β§ (π
βπ) β π΄) β (π β¨ (π
βπ)) β π΅) |
28 | 13, 15, 26, 27 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π β¨ (π
βπ)) β π΅) |
29 | | simp21 1207 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β π β π) |
30 | 2, 5, 6, 7 | ltrnat 38649 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π΄) β (πβπ) β π΄) |
31 | 16, 29, 15, 30 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πβπ) β π΄) |
32 | 1, 5 | atbase 37797 |
. . . . . . . . 9
β’ ((πβπ) β π΄ β (πβπ) β π΅) |
33 | 31, 32 | syl 17 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πβπ) β π΅) |
34 | | simp12l 1287 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β πΉ β π) |
35 | 6, 7 | ltrncnv 38655 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β β‘πΉ β π) |
36 | 16, 34, 35 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β β‘πΉ β π) |
37 | 6, 7 | ltrnco 39228 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ π β π β§ β‘πΉ β π) β (π β β‘πΉ) β π) |
38 | 16, 23, 36, 37 | syl3anc 1372 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π β β‘πΉ) β π) |
39 | 1, 6, 7, 8 | trlcl 38673 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β β‘πΉ) β π) β (π
β(π β β‘πΉ)) β π΅) |
40 | 16, 38, 39 | syl2anc 585 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π
β(π β β‘πΉ)) β π΅) |
41 | 1, 3 | latjcl 18333 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (πβπ) β π΅ β§ (π
β(π β β‘πΉ)) β π΅) β ((πβπ) β¨ (π
β(π β β‘πΉ))) β π΅) |
42 | 14, 33, 40, 41 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((πβπ) β¨ (π
β(π β β‘πΉ))) β π΅) |
43 | 1, 4 | latmcl 18334 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β¨ (π
βπ)) β π΅ β§ ((πβπ) β¨ (π
β(π β β‘πΉ))) β π΅) β ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β π΅) |
44 | 14, 28, 42, 43 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((π β¨ (π
βπ)) β§ ((πβπ) β¨ (π
β(π β β‘πΉ)))) β π΅) |
45 | 9, 44 | eqeltrid 2838 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β π β π΅) |
46 | 6, 7 | ltrncnv 38655 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β π) β β‘π β π) |
47 | 16, 23, 46 | syl2anc 585 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β β‘π β π) |
48 | 6, 7 | ltrnco 39228 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ β‘π β π) β (πΊ β β‘π) β π) |
49 | 16, 17, 47, 48 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πΊ β β‘π) β π) |
50 | 1, 6, 7, 8 | trlcl 38673 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΊ β β‘π) β π) β (π
β(πΊ β β‘π)) β π΅) |
51 | 16, 49, 50 | syl2anc 585 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π
β(πΊ β β‘π)) β π΅) |
52 | 1, 3 | latjcl 18333 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ (π
β(πΊ β β‘π)) β π΅) β (π β¨ (π
β(πΊ β β‘π))) β π΅) |
53 | 14, 45, 51, 52 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (π β¨ (π
β(πΊ β β‘π))) β π΅) |
54 | 1, 2, 4 | latmle1 18358 |
. . . 4
β’ ((πΎ β Lat β§ (π β¨ (π
βπΊ)) β π΅ β§ (π β¨ (π
β(πΊ β β‘π))) β π΅) β ((π β¨ (π
βπΊ)) β§ (π β¨ (π
β(πΊ β β‘π)))) β€ (π β¨ (π
βπΊ))) |
55 | 14, 22, 53, 54 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β ((π β¨ (π
βπΊ)) β§ (π β¨ (π
β(πΊ β β‘π)))) β€ (π β¨ (π
βπΊ))) |
56 | 10, 55 | eqbrtrid 5141 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β π β€ (π β¨ (π
βπΊ))) |
57 | 12, 56 | eqbrtrd 5128 |
1
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π
βπΉ) = (π
βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π
βπ) β (π
βπΉ) β§ (π
βπ) β (π
βπΊ)))) β (πβπ) β€ (π β¨ (π
βπΊ))) |