Step | Hyp | Ref
| Expression |
1 | | simpl11 1249 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β πΎ β HL) |
2 | | simpl21 1252 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β π β π΄) |
3 | | simpl12 1250 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β π β π) |
4 | | eqid 2737 |
. . . . . . . 8
β’
(BaseβπΎ) =
(BaseβπΎ) |
5 | | llnexch.n |
. . . . . . . 8
β’ π = (LLinesβπΎ) |
6 | 4, 5 | llnbase 37975 |
. . . . . . 7
β’ (π β π β π β (BaseβπΎ)) |
7 | 3, 6 | syl 17 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β π β (BaseβπΎ)) |
8 | 1 | hllatd 37829 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β πΎ β Lat) |
9 | | simpl13 1251 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β π β π) |
10 | 4, 5 | llnbase 37975 |
. . . . . . . 8
β’ (π β π β π β (BaseβπΎ)) |
11 | 9, 10 | syl 17 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β π β (BaseβπΎ)) |
12 | | llnexch.m |
. . . . . . . 8
β’ β§ =
(meetβπΎ) |
13 | 4, 12 | latmcl 18330 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β§ π) β (BaseβπΎ)) |
14 | 8, 7, 11, 13 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (π β§ π) β (BaseβπΎ)) |
15 | | llnexch.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
16 | 4, 15, 12 | latmle1 18354 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β§ π) β€ π) |
17 | 8, 7, 11, 16 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (π β§ π) β€ π) |
18 | | llnexch.j |
. . . . . . 7
β’ β¨ =
(joinβπΎ) |
19 | | llnexch.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
20 | 4, 15, 18, 12, 19 | atmod2i2 38328 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β (BaseβπΎ) β§ (π β§ π) β (BaseβπΎ)) β§ (π β§ π) β€ π) β ((π β§ π) β¨ (π β§ π)) = (π β§ (π β¨ (π β§ π)))) |
21 | 1, 2, 7, 14, 17, 20 | syl131anc 1384 |
. . . . 5
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β ((π β§ π) β¨ (π β§ π)) = (π β§ (π β¨ (π β§ π)))) |
22 | 4, 19 | atbase 37754 |
. . . . . . . . 9
β’ (π β π΄ β π β (BaseβπΎ)) |
23 | 2, 22 | syl 17 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β π β (BaseβπΎ)) |
24 | 4, 12 | latmcom 18353 |
. . . . . . . 8
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β§ π) = (π β§ π)) |
25 | 8, 7, 23, 24 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (π β§ π) = (π β§ π)) |
26 | | simpl23 1254 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β Β¬ π β€ π) |
27 | | hlatl 37825 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β AtLat) |
28 | 1, 27 | syl 17 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β πΎ β AtLat) |
29 | | eqid 2737 |
. . . . . . . . . 10
β’
(0.βπΎ) =
(0.βπΎ) |
30 | 4, 15, 12, 29, 19 | atnle 37782 |
. . . . . . . . 9
β’ ((πΎ β AtLat β§ π β π΄ β§ π β (BaseβπΎ)) β (Β¬ π β€ π β (π β§ π) = (0.βπΎ))) |
31 | 28, 2, 7, 30 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (Β¬ π β€ π β (π β§ π) = (0.βπΎ))) |
32 | 26, 31 | mpbid 231 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (π β§ π) = (0.βπΎ)) |
33 | 25, 32 | eqtrd 2777 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (π β§ π) = (0.βπΎ)) |
34 | 33 | oveq1d 7373 |
. . . . 5
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β ((π β§ π) β¨ (π β§ π)) = ((0.βπΎ) β¨ (π β§ π))) |
35 | | simpr 486 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (π β§ π) β€ (π β¨ π)) |
36 | | hlcvl 37824 |
. . . . . . . . 9
β’ (πΎ β HL β πΎ β CvLat) |
37 | 1, 36 | syl 17 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β πΎ β CvLat) |
38 | | simpl3 1194 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (π β§ π) β π΄) |
39 | | simpl22 1253 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β π β π΄) |
40 | | breq1 5109 |
. . . . . . . . . . . 12
β’ (π = (π β§ π) β (π β€ π β (π β§ π) β€ π)) |
41 | 17, 40 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (π = (π β§ π) β π β€ π)) |
42 | 41 | necon3bd 2958 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (Β¬ π β€ π β π β (π β§ π))) |
43 | 26, 42 | mpd 15 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β π β (π β§ π)) |
44 | 43 | necomd 3000 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (π β§ π) β π) |
45 | 15, 18, 19 | cvlatexchb1 37799 |
. . . . . . . 8
β’ ((πΎ β CvLat β§ ((π β§ π) β π΄ β§ π β π΄ β§ π β π΄) β§ (π β§ π) β π) β ((π β§ π) β€ (π β¨ π) β (π β¨ (π β§ π)) = (π β¨ π))) |
46 | 37, 38, 39, 2, 44, 45 | syl131anc 1384 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β ((π β§ π) β€ (π β¨ π) β (π β¨ (π β§ π)) = (π β¨ π))) |
47 | 35, 46 | mpbid 231 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (π β¨ (π β§ π)) = (π β¨ π)) |
48 | 47 | oveq2d 7374 |
. . . . 5
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (π β§ (π β¨ (π β§ π))) = (π β§ (π β¨ π))) |
49 | 21, 34, 48 | 3eqtr3rd 2786 |
. . . 4
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (π β§ (π β¨ π)) = ((0.βπΎ) β¨ (π β§ π))) |
50 | | hlol 37826 |
. . . . . 6
β’ (πΎ β HL β πΎ β OL) |
51 | 1, 50 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β πΎ β OL) |
52 | 4, 18, 29 | olj02 37691 |
. . . . 5
β’ ((πΎ β OL β§ (π β§ π) β (BaseβπΎ)) β ((0.βπΎ) β¨ (π β§ π)) = (π β§ π)) |
53 | 51, 14, 52 | syl2anc 585 |
. . . 4
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β ((0.βπΎ) β¨ (π β§ π)) = (π β§ π)) |
54 | 49, 53 | eqtr2d 2778 |
. . 3
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β§ (π β§ π) β€ (π β¨ π)) β (π β§ π) = (π β§ (π β¨ π))) |
55 | 54 | ex 414 |
. 2
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π)))) |
56 | | simp11 1204 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β πΎ β HL) |
57 | 56 | hllatd 37829 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β πΎ β Lat) |
58 | | simp12 1205 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β π β π) |
59 | 58, 6 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β π β (BaseβπΎ)) |
60 | | simp21 1207 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β π β π΄) |
61 | | simp22 1208 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β π β π΄) |
62 | 4, 18, 19 | hlatjcl 37832 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
63 | 56, 60, 61, 62 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β (π β¨ π) β (BaseβπΎ)) |
64 | 4, 15, 12 | latmle2 18355 |
. . . 4
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β (π β§ (π β¨ π)) β€ (π β¨ π)) |
65 | 57, 59, 63, 64 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β (π β§ (π β¨ π)) β€ (π β¨ π)) |
66 | | breq1 5109 |
. . 3
β’ ((π β§ π) = (π β§ (π β¨ π)) β ((π β§ π) β€ (π β¨ π) β (π β§ (π β¨ π)) β€ (π β¨ π))) |
67 | 65, 66 | syl5ibrcom 247 |
. 2
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β ((π β§ π) = (π β§ (π β¨ π)) β (π β§ π) β€ (π β¨ π))) |
68 | 55, 67 | impbid 211 |
1
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π)))) |