Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | dalawlem.l |
. . . 4
β’ β€ =
(leβπΎ) |
3 | | simp11 1204 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β πΎ β HL) |
4 | 3 | hllatd 37829 |
. . . 4
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β πΎ β Lat) |
5 | | simp21 1207 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
6 | | simp22 1208 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
7 | | dalawlem.j |
. . . . . . 7
β’ β¨ =
(joinβπΎ) |
8 | | dalawlem.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
9 | 1, 7, 8 | hlatjcl 37832 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
10 | 3, 5, 6, 9 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
11 | | simp31 1210 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
12 | | simp32 1211 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
13 | 1, 7, 8 | hlatjcl 37832 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
14 | 3, 11, 12, 13 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
15 | | dalawlem.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
16 | 1, 15 | latmcl 18330 |
. . . . 5
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
17 | 4, 10, 14, 16 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
18 | 1, 8 | atbase 37754 |
. . . . . . . 8
β’ (π β π΄ β π β (BaseβπΎ)) |
19 | 11, 18 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
20 | 1, 7 | latjcl 18329 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ π) β¨ π) β (BaseβπΎ)) |
21 | 4, 10, 19, 20 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π) β (BaseβπΎ)) |
22 | 1, 8 | atbase 37754 |
. . . . . . 7
β’ (π β π΄ β π β (BaseβπΎ)) |
23 | 12, 22 | syl 17 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
24 | 1, 15 | latmcl 18330 |
. . . . . 6
β’ ((πΎ β Lat β§ ((π β¨ π) β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β (((π β¨ π) β¨ π) β§ π) β (BaseβπΎ)) |
25 | 4, 21, 23, 24 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β (BaseβπΎ)) |
26 | 1, 7 | latjcl 18329 |
. . . . 5
β’ ((πΎ β Lat β§ (((π β¨ π) β¨ π) β§ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((((π β¨ π) β¨ π) β§ π) β¨ π) β (BaseβπΎ)) |
27 | 4, 25, 19, 26 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π) β§ π) β¨ π) β (BaseβπΎ)) |
28 | 1, 8 | atbase 37754 |
. . . . . . 7
β’ (π β π΄ β π β (BaseβπΎ)) |
29 | 6, 28 | syl 17 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
30 | | simp33 1212 |
. . . . . . 7
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β π΄) |
31 | 1, 7, 8 | hlatjcl 37832 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
32 | 3, 12, 30, 31 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
33 | 1, 15 | latmcl 18330 |
. . . . . 6
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β (π β§ (π β¨ π)) β (BaseβπΎ)) |
34 | 4, 29, 32, 33 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β§ (π β¨ π)) β (BaseβπΎ)) |
35 | 1, 7, 8 | hlatjcl 37832 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
36 | 3, 30, 11, 35 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
37 | 1, 7 | latjcl 18329 |
. . . . 5
β’ ((πΎ β Lat β§ (π β§ (π β¨ π)) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β§ (π β¨ π)) β¨ (π β¨ π)) β (BaseβπΎ)) |
38 | 4, 34, 36, 37 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β§ (π β¨ π)) β¨ (π β¨ π)) β (BaseβπΎ)) |
39 | 1, 2, 7 | latlej1 18338 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β¨ π) β€ ((π β¨ π) β¨ π)) |
40 | 4, 10, 19, 39 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β€ ((π β¨ π) β¨ π)) |
41 | 1, 7, 8 | hlatjcl 37832 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
42 | 3, 12, 11, 41 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
43 | 1, 2, 15 | latmlem1 18359 |
. . . . . . 7
β’ ((πΎ β Lat β§ ((π β¨ π) β (BaseβπΎ) β§ ((π β¨ π) β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β ((π β¨ π) β€ ((π β¨ π) β¨ π) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π) β¨ π) β§ (π β¨ π)))) |
44 | 4, 10, 21, 42, 43 | syl13anc 1373 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β€ ((π β¨ π) β¨ π) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π) β¨ π) β§ (π β¨ π)))) |
45 | 40, 44 | mpd 15 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π) β¨ π) β§ (π β¨ π))) |
46 | 7, 8 | hlatjcom 37833 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = (π β¨ π)) |
47 | 3, 11, 12, 46 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) = (π β¨ π)) |
48 | 47 | oveq2d 7374 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) = ((π β¨ π) β§ (π β¨ π))) |
49 | 1, 2, 7 | latlej2 18339 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β π β€ ((π β¨ π) β¨ π)) |
50 | 4, 10, 19, 49 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ ((π β¨ π) β¨ π)) |
51 | 1, 2, 7, 15, 8 | atmod2i2 38328 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ ((π β¨ π) β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ π β€ ((π β¨ π) β¨ π)) β ((((π β¨ π) β¨ π) β§ π) β¨ π) = (((π β¨ π) β¨ π) β§ (π β¨ π))) |
52 | 3, 12, 21, 19, 50, 51 | syl131anc 1384 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π) β§ π) β¨ π) = (((π β¨ π) β¨ π) β§ (π β¨ π))) |
53 | 45, 48, 52 | 3brtr4d 5138 |
. . . 4
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ ((((π β¨ π) β¨ π) β§ π) β¨ π)) |
54 | | hlol 37826 |
. . . . . . . . . . 11
β’ (πΎ β HL β πΎ β OL) |
55 | 3, 54 | syl 17 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β πΎ β OL) |
56 | 1, 7, 8 | hlatjcl 37832 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
57 | 3, 5, 11, 56 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
58 | 1, 7 | latjcl 18329 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β (π β¨ (π β¨ π)) β (BaseβπΎ)) |
59 | 4, 29, 57, 58 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π β¨ π)) β (BaseβπΎ)) |
60 | 1, 7, 8 | hlatjcl 37832 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
61 | 3, 6, 12, 60 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
62 | 1, 15 | latmassOLD 37694 |
. . . . . . . . . 10
β’ ((πΎ β OL β§ ((π β¨ (π β¨ π)) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((π β¨ (π β¨ π)) β§ (π β¨ π)) β§ π) = ((π β¨ (π β¨ π)) β§ ((π β¨ π) β§ π))) |
63 | 55, 59, 61, 23, 62 | syl13anc 1373 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ (π β¨ π)) β§ (π β¨ π)) β§ π) = ((π β¨ (π β¨ π)) β§ ((π β¨ π) β§ π))) |
64 | 7, 8 | hlatjass 37835 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π) = (π β¨ (π β¨ π))) |
65 | 3, 5, 6, 11, 64 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π) = (π β¨ (π β¨ π))) |
66 | 7, 8 | hlatj12 37836 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π β¨ π)) = (π β¨ (π β¨ π))) |
67 | 3, 5, 6, 11, 66 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π β¨ π)) = (π β¨ (π β¨ π))) |
68 | 65, 67 | eqtr2d 2778 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π β¨ π)) = ((π β¨ π) β¨ π)) |
69 | 2, 7, 8 | hlatlej2 37841 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
70 | 3, 6, 12, 69 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
71 | 1, 2, 15 | latleeqm2 18358 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β (π β€ (π β¨ π) β ((π β¨ π) β§ π) = π)) |
72 | 4, 23, 61, 71 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β€ (π β¨ π) β ((π β¨ π) β§ π) = π)) |
73 | 70, 72 | mpbid 231 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ π) = π) |
74 | 68, 73 | oveq12d 7376 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ (π β¨ π)) β§ ((π β¨ π) β§ π)) = (((π β¨ π) β¨ π) β§ π)) |
75 | 63, 74 | eqtr2d 2778 |
. . . . . . . 8
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) = (((π β¨ (π β¨ π)) β§ (π β¨ π)) β§ π)) |
76 | 2, 7, 8 | hlatlej1 37840 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
77 | 3, 6, 12, 76 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
78 | 1, 2, 7, 15, 8 | atmod1i1 38323 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (π β π΄ β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β§ π β€ (π β¨ π)) β (π β¨ ((π β¨ π) β§ (π β¨ π))) = ((π β¨ (π β¨ π)) β§ (π β¨ π))) |
79 | 3, 6, 57, 61, 77, 78 | syl131anc 1384 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β¨ π) β§ (π β¨ π))) = ((π β¨ (π β¨ π)) β§ (π β¨ π))) |
80 | 2, 7, 8 | hlatlej2 37841 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
81 | 3, 30, 6, 80 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
82 | | simp13 1206 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) |
83 | | simp12 1205 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π = π
) |
84 | 83 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) = (π
β¨ π)) |
85 | 7, 8 | hlatjcom 37833 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = (π β¨ π)) |
86 | 3, 6, 30, 85 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) = (π β¨ π)) |
87 | 84, 86 | eqtr3d 2779 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π
β¨ π) = (π β¨ π)) |
88 | 82, 87 | breqtrd 5132 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
89 | 1, 15 | latmcl 18330 |
. . . . . . . . . . . . 13
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
90 | 4, 57, 61, 89 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ)) |
91 | 1, 7, 8 | hlatjcl 37832 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
92 | 3, 30, 6, 91 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β (BaseβπΎ)) |
93 | 1, 2, 7 | latjle12 18340 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ ((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β ((π β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β (π β¨ ((π β¨ π) β§ (π β¨ π))) β€ (π β¨ π))) |
94 | 4, 29, 90, 92, 93 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β (π β¨ ((π β¨ π) β§ (π β¨ π))) β€ (π β¨ π))) |
95 | 81, 88, 94 | mpbi2and 711 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ ((π β¨ π) β§ (π β¨ π))) β€ (π β¨ π)) |
96 | 79, 95 | eqbrtrrd 5130 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ (π β¨ π)) β§ (π β¨ π)) β€ (π β¨ π)) |
97 | 2, 7, 8 | hlatlej1 37840 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
98 | 3, 12, 30, 97 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
99 | 1, 15 | latmcl 18330 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ (π β¨ (π β¨ π)) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ (π β¨ π)) β§ (π β¨ π)) β (BaseβπΎ)) |
100 | 4, 59, 61, 99 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ (π β¨ π)) β§ (π β¨ π)) β (BaseβπΎ)) |
101 | 1, 2, 15 | latmlem12 18361 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (((π β¨ (π β¨ π)) β§ (π β¨ π)) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β§ (π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β ((((π β¨ (π β¨ π)) β§ (π β¨ π)) β€ (π β¨ π) β§ π β€ (π β¨ π)) β (((π β¨ (π β¨ π)) β§ (π β¨ π)) β§ π) β€ ((π β¨ π) β§ (π β¨ π)))) |
102 | 4, 100, 92, 23, 32, 101 | syl122anc 1380 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((((π β¨ (π β¨ π)) β§ (π β¨ π)) β€ (π β¨ π) β§ π β€ (π β¨ π)) β (((π β¨ (π β¨ π)) β§ (π β¨ π)) β§ π) β€ ((π β¨ π) β§ (π β¨ π)))) |
103 | 96, 98, 102 | mp2and 698 |
. . . . . . . 8
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ (π β¨ π)) β§ (π β¨ π)) β§ π) β€ ((π β¨ π) β§ (π β¨ π))) |
104 | 75, 103 | eqbrtrd 5128 |
. . . . . . 7
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ ((π β¨ π) β§ (π β¨ π))) |
105 | 2, 7, 8 | hlatlej2 37841 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
106 | 3, 12, 30, 105 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
107 | 1, 2, 7, 15, 8 | atmod1i1 38323 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΄ β§ π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β§ π β€ (π β¨ π)) β (π β¨ (π β§ (π β¨ π))) = ((π β¨ π) β§ (π β¨ π))) |
108 | 3, 30, 29, 32, 106, 107 | syl131anc 1384 |
. . . . . . . 8
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π β§ (π β¨ π))) = ((π β¨ π) β§ (π β¨ π))) |
109 | 1, 8 | atbase 37754 |
. . . . . . . . . 10
β’ (π β π΄ β π β (BaseβπΎ)) |
110 | 30, 109 | syl 17 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
111 | 1, 7 | latjcom 18337 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (π β§ (π β¨ π)) β (BaseβπΎ)) β (π β¨ (π β§ (π β¨ π))) = ((π β§ (π β¨ π)) β¨ π)) |
112 | 4, 110, 34, 111 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ (π β§ (π β¨ π))) = ((π β§ (π β¨ π)) β¨ π)) |
113 | 108, 112 | eqtr3d 2779 |
. . . . . . 7
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) = ((π β§ (π β¨ π)) β¨ π)) |
114 | 104, 113 | breqtrd 5132 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ ((π β§ (π β¨ π)) β¨ π)) |
115 | 1, 7 | latjcl 18329 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β§ (π β¨ π)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β§ (π β¨ π)) β¨ π) β (BaseβπΎ)) |
116 | 4, 34, 110, 115 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β§ (π β¨ π)) β¨ π) β (BaseβπΎ)) |
117 | 1, 2, 7 | latjlej1 18343 |
. . . . . . 7
β’ ((πΎ β Lat β§ ((((π β¨ π) β¨ π) β§ π) β (BaseβπΎ) β§ ((π β§ (π β¨ π)) β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((((π β¨ π) β¨ π) β§ π) β€ ((π β§ (π β¨ π)) β¨ π) β ((((π β¨ π) β¨ π) β§ π) β¨ π) β€ (((π β§ (π β¨ π)) β¨ π) β¨ π))) |
118 | 4, 25, 116, 19, 117 | syl13anc 1373 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π) β§ π) β€ ((π β§ (π β¨ π)) β¨ π) β ((((π β¨ π) β¨ π) β§ π) β¨ π) β€ (((π β§ (π β¨ π)) β¨ π) β¨ π))) |
119 | 114, 118 | mpd 15 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π) β§ π) β¨ π) β€ (((π β§ (π β¨ π)) β¨ π) β¨ π)) |
120 | 1, 7 | latjass 18373 |
. . . . . 6
β’ ((πΎ β Lat β§ ((π β§ (π β¨ π)) β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((π β§ (π β¨ π)) β¨ π) β¨ π) = ((π β§ (π β¨ π)) β¨ (π β¨ π))) |
121 | 4, 34, 110, 19, 120 | syl13anc 1373 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β§ (π β¨ π)) β¨ π) β¨ π) = ((π β§ (π β¨ π)) β¨ (π β¨ π))) |
122 | 119, 121 | breqtrd 5132 |
. . . 4
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π) β§ π) β¨ π) β€ ((π β§ (π β¨ π)) β¨ (π β¨ π))) |
123 | 1, 2, 4, 17, 27, 38, 53, 122 | lattrd 18336 |
. . 3
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ ((π β§ (π β¨ π)) β¨ (π β¨ π))) |
124 | 1, 2, 15 | latmle1 18354 |
. . . 4
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
125 | 4, 10, 14, 124 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) |
126 | 1, 2, 15 | latlem12 18356 |
. . . 4
β’ ((πΎ β Lat β§ (((π β¨ π) β§ (π β¨ π)) β (BaseβπΎ) β§ ((π β§ (π β¨ π)) β¨ (π β¨ π)) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β ((((π β¨ π) β§ (π β¨ π)) β€ ((π β§ (π β¨ π)) β¨ (π β¨ π)) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β§ (π β¨ π)) β¨ (π β¨ π)) β§ (π β¨ π)))) |
127 | 4, 17, 38, 10, 126 | syl13anc 1373 |
. . 3
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((((π β¨ π) β§ (π β¨ π)) β€ ((π β§ (π β¨ π)) β¨ (π β¨ π)) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β§ (π β¨ π)) β¨ (π β¨ π)) β§ (π β¨ π)))) |
128 | 123, 125,
127 | mpbi2and 711 |
. 2
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β§ (π β¨ π)) β¨ (π β¨ π)) β§ (π β¨ π))) |
129 | 1, 8 | atbase 37754 |
. . . . . 6
β’ (π β π΄ β π β (BaseβπΎ)) |
130 | 5, 129 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π β (BaseβπΎ)) |
131 | 1, 2, 7, 15 | latmlej12 18369 |
. . . . 5
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ))) β (π β§ (π β¨ π)) β€ (π β¨ π)) |
132 | 4, 29, 32, 130, 131 | syl13anc 1373 |
. . . 4
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β§ (π β¨ π)) β€ (π β¨ π)) |
133 | 1, 2, 7, 15, 8 | llnmod1i2 38326 |
. . . 4
β’ (((πΎ β HL β§ (π β§ (π β¨ π)) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄) β§ (π β§ (π β¨ π)) β€ (π β¨ π)) β ((π β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π))) = (((π β§ (π β¨ π)) β¨ (π β¨ π)) β§ (π β¨ π))) |
134 | 3, 34, 10, 30, 11, 132, 133 | syl321anc 1393 |
. . 3
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π))) = (((π β§ (π β¨ π)) β¨ (π β¨ π)) β§ (π β¨ π))) |
135 | 7, 8 | hlatjidm 37834 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄) β (π β¨ π) = π) |
136 | 3, 6, 135 | syl2anc 585 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) = π) |
137 | 83 | oveq2d 7374 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) = (π β¨ π
)) |
138 | 136, 137 | eqtr3d 2779 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β π = (π β¨ π
)) |
139 | 138 | oveq1d 7373 |
. . . 4
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β§ (π β¨ π)) = ((π β¨ π
) β§ (π β¨ π))) |
140 | 1, 15 | latmcom 18353 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β¨ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β ((π β¨ π) β§ (π β¨ π)) = ((π β¨ π) β§ (π β¨ π))) |
141 | 4, 36, 10, 140 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) = ((π β¨ π) β§ (π β¨ π))) |
142 | 7, 8 | hlatjcom 37833 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = (π β¨ π)) |
143 | 3, 5, 6, 142 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) = (π β¨ π)) |
144 | 83 | oveq1d 7373 |
. . . . . . 7
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) = (π
β¨ π)) |
145 | 143, 144 | eqtrd 2777 |
. . . . . 6
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β¨ π) = (π
β¨ π)) |
146 | 145 | oveq1d 7373 |
. . . . 5
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) = ((π
β¨ π) β§ (π β¨ π))) |
147 | 141, 146 | eqtrd 2777 |
. . . 4
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) = ((π
β¨ π) β§ (π β¨ π))) |
148 | 139, 147 | oveq12d 7376 |
. . 3
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π))) = (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π)))) |
149 | 134, 148 | eqtr3d 2779 |
. 2
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β§ (π β¨ π)) β¨ (π β¨ π)) β§ (π β¨ π)) = (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π)))) |
150 | 128, 149 | breqtrd 5132 |
1
β’ (((πΎ β HL β§ π = π
β§ ((π β¨ π) β§ (π β¨ π)) β€ (π
β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π
) β§ (π β¨ π)) β¨ ((π
β¨ π) β§ (π β¨ π)))) |