Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. 2
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | dalawlem.l |
. 2
β’ β€ =
(leβπΎ) |
3 | | simp11 1204 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β πΎ β HL) |
4 | 3 | hllatd 37829 |
. 2
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β πΎ β Lat) |
5 | | simp21 1207 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
6 | | simp22 1208 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
7 | | dalawlem.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
8 | | dalawlem.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
9 | 1, 7, 8 | hlatjcl 37832 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
10 | 3, 5, 6, 9 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
11 | | simp32 1211 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
12 | 1, 8 | atbase 37754 |
. . . . 5
β’ (π β π΄ β π β (BaseβπΎ)) |
13 | 11, 12 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
14 | 1, 7 | latjcl 18329 |
. . . 4
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ π) β¨ π) β (BaseβπΎ)) |
15 | 4, 10, 13, 14 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π) β (BaseβπΎ)) |
16 | | simp31 1210 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
17 | 1, 8 | atbase 37754 |
. . . 4
β’ (π β π΄ β π β (BaseβπΎ)) |
18 | 16, 17 | syl 17 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
19 | | dalawlem.m |
. . . 4
β’ β§ =
(meetβπΎ) |
20 | 1, 19 | latmcl 18330 |
. . 3
β’ ((πΎ β Lat β§ ((π β¨ π) β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β (((π β¨ π) β¨ π) β§ π) β (BaseβπΎ)) |
21 | 4, 15, 18, 20 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β (BaseβπΎ)) |
22 | | simp23 1209 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π
β π΄) |
23 | 1, 7, 8 | hlatjcl 37832 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π
β π΄) β (π β¨ π
) β (BaseβπΎ)) |
24 | 3, 6, 22, 23 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π
) β (BaseβπΎ)) |
25 | | simp33 1212 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
26 | 1, 8 | atbase 37754 |
. . . . 5
β’ (π β π΄ β π β (BaseβπΎ)) |
27 | 25, 26 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
28 | 1, 19 | latmcl 18330 |
. . . 4
β’ ((πΎ β Lat β§ (π β¨ π
) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ π
) β§ π) β (BaseβπΎ)) |
29 | 4, 24, 27, 28 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π
) β§ π) β (BaseβπΎ)) |
30 | 1, 7, 8 | hlatjcl 37832 |
. . . . 5
β’ ((πΎ β HL β§ π
β π΄ β§ π β π΄) β (π
β¨ π) β (BaseβπΎ)) |
31 | 3, 22, 5, 30 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π
β¨ π) β (BaseβπΎ)) |
32 | 1, 7, 8 | hlatjcl 37832 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
33 | 3, 25, 16, 32 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
34 | 1, 19 | latmcl 18330 |
. . . 4
β’ ((πΎ β Lat β§ (π
β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π
β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
35 | 4, 31, 33, 34 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π
β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
36 | 1, 7 | latjcl 18329 |
. . 3
β’ ((πΎ β Lat β§ ((π β¨ π
) β§ π) β (BaseβπΎ) β§ ((π
β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) β (BaseβπΎ)) |
37 | 4, 29, 35, 36 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) β (BaseβπΎ)) |
38 | 1, 7, 8 | hlatjcl 37832 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
39 | 3, 11, 25, 38 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
40 | 1, 19 | latmcl 18330 |
. . . 4
β’ ((πΎ β Lat β§ (π β¨ π
) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ)) |
41 | 4, 24, 39, 40 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ)) |
42 | 1, 7 | latjcl 18329 |
. . 3
β’ ((πΎ β Lat β§ ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ) β§ ((π
β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) β (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π))) β (BaseβπΎ)) |
43 | 4, 41, 35, 42 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π))) β (BaseβπΎ)) |
44 | 1, 8 | atbase 37754 |
. . . . . . . 8
β’ (π β π΄ β π β (BaseβπΎ)) |
45 | 5, 44 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
46 | 1, 7, 8 | hlatjcl 37832 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
47 | 3, 5, 16, 46 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
48 | 1, 7, 8 | hlatjcl 37832 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
49 | 3, 6, 11, 48 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
50 | 1, 19 | latmcl 18330 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π β¨ π
) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ)) |
51 | 4, 24, 49, 50 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ)) |
52 | 1, 19 | latmcl 18330 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ)) β ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π))) β (BaseβπΎ)) |
53 | 4, 47, 51, 52 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π))) β (BaseβπΎ)) |
54 | 1, 7 | latjcl 18329 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π))) β (BaseβπΎ)) β (π β¨ ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π)))) β (BaseβπΎ)) |
55 | 4, 45, 53, 54 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π)))) β (BaseβπΎ)) |
56 | 1, 8 | atbase 37754 |
. . . . . . . . 9
β’ (π
β π΄ β π
β (BaseβπΎ)) |
57 | 22, 56 | syl 17 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π
β (BaseβπΎ)) |
58 | 1, 7 | latjcl 18329 |
. . . . . . . 8
β’ ((πΎ β Lat β§ π
β (BaseβπΎ) β§ ((π β¨ π
) β§ π) β (BaseβπΎ)) β (π
β¨ ((π β¨ π
) β§ π)) β (BaseβπΎ)) |
59 | 4, 57, 29, 58 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π
β¨ ((π β¨ π
) β§ π)) β (BaseβπΎ)) |
60 | 1, 7 | latjcl 18329 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (π
β¨ ((π β¨ π
) β§ π)) β (BaseβπΎ)) β (π β¨ (π
β¨ ((π β¨ π
) β§ π))) β (BaseβπΎ)) |
61 | 4, 45, 59, 60 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π
β¨ ((π β¨ π
) β§ π))) β (BaseβπΎ)) |
62 | 1, 2, 7, 19 | latmlej22 18371 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ ((π β¨ π) β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((π β¨ π) β¨ π) β§ π) β€ (π β¨ π)) |
63 | 4, 18, 15, 45, 62 | syl13anc 1373 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (π β¨ π)) |
64 | 1, 19 | latmcl 18330 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
65 | 4, 49, 47, 64 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
66 | 1, 7 | latjcl 18329 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) β (π β¨ ((π β¨ π) β§ (π β¨ π))) β (BaseβπΎ)) |
67 | 4, 45, 65, 66 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β¨ π) β§ (π β¨ π))) β (BaseβπΎ)) |
68 | 1, 7 | latjcl 18329 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ)) β (π β¨ ((π β¨ π
) β§ (π β¨ π))) β (BaseβπΎ)) |
69 | 4, 45, 51, 68 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β¨ π
) β§ (π β¨ π))) β (BaseβπΎ)) |
70 | 2, 7, 8 | hlatlej2 37841 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
71 | 3, 5, 16, 70 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
72 | 1, 7 | latjcl 18329 |
. . . . . . . . . . . . 13
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β (π β¨ (π β¨ π)) β (BaseβπΎ)) |
73 | 4, 45, 49, 72 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π β¨ π)) β (BaseβπΎ)) |
74 | 1, 2, 19 | latmlem2 18360 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ (π β¨ π)) β (BaseβπΎ))) β (π β€ (π β¨ π) β ((π β¨ (π β¨ π)) β§ π) β€ ((π β¨ (π β¨ π)) β§ (π β¨ π)))) |
75 | 4, 18, 47, 73, 74 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β€ (π β¨ π) β ((π β¨ (π β¨ π)) β§ π) β€ ((π β¨ (π β¨ π)) β§ (π β¨ π)))) |
76 | 71, 75 | mpd 15 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ (π β¨ π)) β§ π) β€ ((π β¨ (π β¨ π)) β§ (π β¨ π))) |
77 | 7, 8 | hlatjass 37835 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π) = (π β¨ (π β¨ π))) |
78 | 3, 5, 6, 11, 77 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π) = (π β¨ (π β¨ π))) |
79 | 78 | oveq1d 7373 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) = ((π β¨ (π β¨ π)) β§ π)) |
80 | 2, 7, 8 | hlatlej1 37840 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
81 | 3, 5, 16, 80 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
82 | 1, 2, 7, 19, 8 | atmod1i1 38323 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (π β π΄ β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β§ π β€ (π β¨ π)) β (π β¨ ((π β¨ π) β§ (π β¨ π))) = ((π β¨ (π β¨ π)) β§ (π β¨ π))) |
83 | 3, 5, 49, 47, 81, 82 | syl131anc 1384 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β¨ π) β§ (π β¨ π))) = ((π β¨ (π β¨ π)) β§ (π β¨ π))) |
84 | 76, 79, 83 | 3brtr4d 5138 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (π β¨ ((π β¨ π) β§ (π β¨ π)))) |
85 | 1, 19 | latmcom 18353 |
. . . . . . . . . . . . 13
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) = ((π β¨ π) β§ (π β¨ π))) |
86 | 4, 49, 47, 85 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) = ((π β¨ π) β§ (π β¨ π))) |
87 | | simp12 1205 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
)) |
88 | 86, 87 | eqbrtrd 5128 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
)) |
89 | 1, 2, 19 | latmle1 18354 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
90 | 4, 49, 47, 89 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
91 | 1, 2, 19 | latlem12 18356 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ (((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β ((((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β ((π β¨ π) β§ (π β¨ π)) β€ ((π β¨ π
) β§ (π β¨ π)))) |
92 | 4, 65, 24, 49, 91 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β ((π β¨ π) β§ (π β¨ π)) β€ ((π β¨ π
) β§ (π β¨ π)))) |
93 | 88, 90, 92 | mpbi2and 711 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ ((π β¨ π
) β§ (π β¨ π))) |
94 | 1, 2, 7 | latjlej2 18344 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ (((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ) β§ ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((π β¨ π) β§ (π β¨ π)) β€ ((π β¨ π
) β§ (π β¨ π)) β (π β¨ ((π β¨ π) β§ (π β¨ π))) β€ (π β¨ ((π β¨ π
) β§ (π β¨ π))))) |
95 | 4, 65, 51, 45, 94 | syl13anc 1373 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β§ (π β¨ π)) β€ ((π β¨ π
) β§ (π β¨ π)) β (π β¨ ((π β¨ π) β§ (π β¨ π))) β€ (π β¨ ((π β¨ π
) β§ (π β¨ π))))) |
96 | 93, 95 | mpd 15 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β¨ π) β§ (π β¨ π))) β€ (π β¨ ((π β¨ π
) β§ (π β¨ π)))) |
97 | 1, 2, 4, 21, 67, 69, 84, 96 | lattrd 18336 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (π β¨ ((π β¨ π
) β§ (π β¨ π)))) |
98 | 1, 2, 19 | latlem12 18356 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ ((((π β¨ π) β¨ π) β§ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ ((π β¨ π
) β§ (π β¨ π))) β (BaseβπΎ))) β (((((π β¨ π) β¨ π) β§ π) β€ (π β¨ π) β§ (((π β¨ π) β¨ π) β§ π) β€ (π β¨ ((π β¨ π
) β§ (π β¨ π)))) β (((π β¨ π) β¨ π) β§ π) β€ ((π β¨ π) β§ (π β¨ ((π β¨ π
) β§ (π β¨ π)))))) |
99 | 4, 21, 47, 69, 98 | syl13anc 1373 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((((π β¨ π) β¨ π) β§ π) β€ (π β¨ π) β§ (((π β¨ π) β¨ π) β§ π) β€ (π β¨ ((π β¨ π
) β§ (π β¨ π)))) β (((π β¨ π) β¨ π) β§ π) β€ ((π β¨ π) β§ (π β¨ ((π β¨ π
) β§ (π β¨ π)))))) |
100 | 63, 97, 99 | mpbi2and 711 |
. . . . . . 7
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ ((π β¨ π) β§ (π β¨ ((π β¨ π
) β§ (π β¨ π))))) |
101 | 1, 2, 7, 19, 8 | atmod3i1 38330 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΄ β§ (π β¨ π) β (BaseβπΎ) β§ ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ)) β§ π β€ (π β¨ π)) β (π β¨ ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π)))) = ((π β¨ π) β§ (π β¨ ((π β¨ π
) β§ (π β¨ π))))) |
102 | 3, 5, 47, 51, 81, 101 | syl131anc 1384 |
. . . . . . 7
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π)))) = ((π β¨ π) β§ (π β¨ ((π β¨ π
) β§ (π β¨ π))))) |
103 | 100, 102 | breqtrrd 5134 |
. . . . . 6
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (π β¨ ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π))))) |
104 | | simp13 1206 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) |
105 | 1, 19 | latmcl 18330 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
106 | 4, 47, 49, 105 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
107 | 1, 7, 8 | hlatjcl 37832 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π
β π΄ β§ π β π΄) β (π
β¨ π) β (BaseβπΎ)) |
108 | 3, 22, 25, 107 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π
β¨ π) β (BaseβπΎ)) |
109 | 1, 2, 19 | latmlem2 18360 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ) β§ (π
β¨ π) β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ))) β (((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π) β ((π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π))) β€ ((π β¨ π
) β§ (π
β¨ π)))) |
110 | 4, 106, 108, 24, 109 | syl13anc 1373 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π) β ((π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π))) β€ ((π β¨ π
) β§ (π
β¨ π)))) |
111 | 104, 110 | mpd 15 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π))) β€ ((π β¨ π
) β§ (π
β¨ π))) |
112 | | hlol 37826 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β OL) |
113 | 3, 112 | syl 17 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β πΎ β OL) |
114 | 1, 19 | latm12 37695 |
. . . . . . . . 9
β’ ((πΎ β OL β§ ((π β¨ π) β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π))) = ((π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)))) |
115 | 113, 47, 24, 49, 114 | syl13anc 1373 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π))) = ((π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)))) |
116 | 2, 7, 8 | hlatlej2 37841 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄ β§ π
β π΄) β π
β€ (π β¨ π
)) |
117 | 3, 6, 22, 116 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π
β€ (π β¨ π
)) |
118 | 1, 2, 7, 19, 8 | atmod3i1 38330 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π
β π΄ β§ (π β¨ π
) β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ π
β€ (π β¨ π
)) β (π
β¨ ((π β¨ π
) β§ π)) = ((π β¨ π
) β§ (π
β¨ π))) |
119 | 3, 22, 24, 27, 117, 118 | syl131anc 1384 |
. . . . . . . 8
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π
β¨ ((π β¨ π
) β§ π)) = ((π β¨ π
) β§ (π
β¨ π))) |
120 | 111, 115,
119 | 3brtr4d 5138 |
. . . . . . 7
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π))) β€ (π
β¨ ((π β¨ π
) β§ π))) |
121 | 1, 2, 7 | latjlej2 18344 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π))) β (BaseβπΎ) β§ (π
β¨ ((π β¨ π
) β§ π)) β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π))) β€ (π
β¨ ((π β¨ π
) β§ π)) β (π β¨ ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π)))) β€ (π β¨ (π
β¨ ((π β¨ π
) β§ π))))) |
122 | 4, 53, 59, 45, 121 | syl13anc 1373 |
. . . . . . 7
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π))) β€ (π
β¨ ((π β¨ π
) β§ π)) β (π β¨ ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π)))) β€ (π β¨ (π
β¨ ((π β¨ π
) β§ π))))) |
123 | 120, 122 | mpd 15 |
. . . . . 6
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β¨ π) β§ ((π β¨ π
) β§ (π β¨ π)))) β€ (π β¨ (π
β¨ ((π β¨ π
) β§ π)))) |
124 | 1, 2, 4, 21, 55, 61, 103, 123 | lattrd 18336 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (π β¨ (π
β¨ ((π β¨ π
) β§ π)))) |
125 | 1, 7 | latj13 18376 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π
β (BaseβπΎ) β§ ((π β¨ π
) β§ π) β (BaseβπΎ))) β (π β¨ (π
β¨ ((π β¨ π
) β§ π))) = (((π β¨ π
) β§ π) β¨ (π
β¨ π))) |
126 | 4, 45, 57, 29, 125 | syl13anc 1373 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π
β¨ ((π β¨ π
) β§ π))) = (((π β¨ π
) β§ π) β¨ (π
β¨ π))) |
127 | 124, 126 | breqtrd 5132 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π
) β§ π) β¨ (π
β¨ π))) |
128 | 1, 2, 7, 19 | latmlej22 18371 |
. . . . 5
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ ((π β¨ π) β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((π β¨ π) β¨ π) β§ π) β€ (π β¨ π)) |
129 | 4, 18, 15, 27, 128 | syl13anc 1373 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (π β¨ π)) |
130 | 1, 7 | latjcl 18329 |
. . . . . 6
β’ ((πΎ β Lat β§ ((π β¨ π
) β§ π) β (BaseβπΎ) β§ (π
β¨ π) β (BaseβπΎ)) β (((π β¨ π
) β§ π) β¨ (π
β¨ π)) β (BaseβπΎ)) |
131 | 4, 29, 31, 130 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π
) β§ π) β¨ (π
β¨ π)) β (BaseβπΎ)) |
132 | 1, 2, 19 | latlem12 18356 |
. . . . 5
β’ ((πΎ β Lat β§ ((((π β¨ π) β¨ π) β§ π) β (BaseβπΎ) β§ (((π β¨ π
) β§ π) β¨ (π
β¨ π)) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β (((((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (((π β¨ π) β¨ π) β§ π) β€ (π β¨ π)) β (((π β¨ π) β¨ π) β§ π) β€ ((((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (π β¨ π)))) |
133 | 4, 21, 131, 33, 132 | syl13anc 1373 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (((π β¨ π) β¨ π) β§ π) β€ (π β¨ π)) β (((π β¨ π) β¨ π) β§ π) β€ ((((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (π β¨ π)))) |
134 | 127, 129,
133 | mpbi2and 711 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ ((((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (π β¨ π))) |
135 | 1, 2, 7, 19 | latmlej21 18370 |
. . . . 5
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π β¨ π
) β§ π) β€ (π β¨ π)) |
136 | 4, 27, 24, 18, 135 | syl13anc 1373 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π
) β§ π) β€ (π β¨ π)) |
137 | 1, 2, 7, 19, 8 | atmod1i1m 38324 |
. . . 4
β’ (((πΎ β HL β§ π β π΄) β§ ((π β¨ π
) β (BaseβπΎ) β§ (π
β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β§ ((π β¨ π
) β§ π) β€ (π β¨ π)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) = ((((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (π β¨ π))) |
138 | 3, 25, 24, 31, 33, 136, 137 | syl231anc 1391 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) = ((((π β¨ π
) β§ π) β¨ (π
β¨ π)) β§ (π β¨ π))) |
139 | 134, 138 | breqtrrd 5134 |
. 2
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π)))) |
140 | 2, 7, 8 | hlatlej2 37841 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
141 | 3, 11, 25, 140 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
142 | 1, 2, 19 | latmlem2 18360 |
. . . . 5
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π
) β (BaseβπΎ))) β (π β€ (π β¨ π) β ((π β¨ π
) β§ π) β€ ((π β¨ π
) β§ (π β¨ π)))) |
143 | 4, 27, 39, 24, 142 | syl13anc 1373 |
. . . 4
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β€ (π β¨ π) β ((π β¨ π
) β§ π) β€ ((π β¨ π
) β§ (π β¨ π)))) |
144 | 141, 143 | mpd 15 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π
) β§ π) β€ ((π β¨ π
) β§ (π β¨ π))) |
145 | 1, 2, 7 | latjlej1 18343 |
. . . 4
β’ ((πΎ β Lat β§ (((π β¨ π
) β§ π) β (BaseβπΎ) β§ ((π β¨ π
) β§ (π β¨ π)) β (BaseβπΎ) β§ ((π
β¨ π) β§ (π β¨ π)) β (BaseβπΎ))) β (((π β¨ π
) β§ π) β€ ((π β¨ π
) β§ (π β¨ π)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) β€ (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π))))) |
146 | 4, 29, 41, 35, 145 | syl13anc 1373 |
. . 3
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π
) β§ π) β€ ((π β¨ π
) β§ (π β¨ π)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) β€ (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π))))) |
147 | 144, 146 | mpd 15 |
. 2
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π
) β§ π) β¨ ((π
β¨ π) β§ (π β¨ π))) β€ (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π)))) |
148 | 1, 2, 4, 21, 37, 43, 139, 147 | lattrd 18336 |
1
β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π
) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π)))) |