Step | Hyp | Ref
| Expression |
1 | | simp23 1208 |
. . 3
β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β π β π) |
2 | | simp1 1136 |
. . . 4
β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β πΎ β HL) |
3 | | eqid 2732 |
. . . . . 6
β’
(BaseβπΎ) =
(BaseβπΎ) |
4 | | llnexch.n |
. . . . . 6
β’ π = (LLinesβπΎ) |
5 | 3, 4 | llnbase 38368 |
. . . . 5
β’ (π β π β π β (BaseβπΎ)) |
6 | 1, 5 | syl 17 |
. . . 4
β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β π β (BaseβπΎ)) |
7 | | llnexch.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
8 | | llnexch.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
9 | 3, 7, 8, 4 | islln3 38369 |
. . . 4
β’ ((πΎ β HL β§ π β (BaseβπΎ)) β (π β π β βπ β π΄ βπ β π΄ (π β π β§ π = (π β¨ π)))) |
10 | 2, 6, 9 | syl2anc 584 |
. . 3
β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β (π β π β βπ β π΄ βπ β π΄ (π β π β§ π = (π β¨ π)))) |
11 | 1, 10 | mpbid 231 |
. 2
β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β βπ β π΄ βπ β π΄ (π β π β§ π = (π β¨ π))) |
12 | | simp3r 1202 |
. . 3
β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β π β π) |
13 | 12 | necomd 2996 |
. 2
β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β π β π) |
14 | | simp11 1203 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β πΎ β HL) |
15 | 14 | hllatd 38222 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β πΎ β Lat) |
16 | | simp2l 1199 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
17 | 3, 8 | atbase 38147 |
. . . . . . . . . . . 12
β’ (π β π΄ β π β (BaseβπΎ)) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β π β (BaseβπΎ)) |
19 | | simp2r 1200 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
20 | 3, 8 | atbase 38147 |
. . . . . . . . . . . 12
β’ (π β π΄ β π β (BaseβπΎ)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β π β (BaseβπΎ)) |
22 | | simp121 1305 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β π β π) |
23 | 3, 4 | llnbase 38368 |
. . . . . . . . . . . 12
β’ (π β π β π β (BaseβπΎ)) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β π β (BaseβπΎ)) |
25 | | llnexch.l |
. . . . . . . . . . . 12
β’ β€ =
(leβπΎ) |
26 | 3, 25, 7 | latjle12 18399 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π β€ π β§ π β€ π) β (π β¨ π) β€ π)) |
27 | 15, 18, 21, 24, 26 | syl13anc 1372 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β ((π β€ π β§ π β€ π) β (π β¨ π) β€ π)) |
28 | | simp3 1138 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β π β π) |
29 | 7, 8, 4 | llni2 38371 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β (π β¨ π) β π) |
30 | 14, 16, 19, 28, 29 | syl31anc 1373 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β (π β¨ π) β π) |
31 | 25, 4 | llncmp 38381 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (π β¨ π) β π β§ π β π) β ((π β¨ π) β€ π β (π β¨ π) = π)) |
32 | 14, 30, 22, 31 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β ((π β¨ π) β€ π β (π β¨ π) = π)) |
33 | 27, 32 | bitr2d 279 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β ((π β¨ π) = π β (π β€ π β§ π β€ π))) |
34 | 33 | necon3abid 2977 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β ((π β¨ π) β π β Β¬ (π β€ π β§ π β€ π))) |
35 | | ianor 980 |
. . . . . . . 8
β’ (Β¬
(π β€ π β§ π β€ π) β (Β¬ π β€ π β¨ Β¬ π β€ π)) |
36 | 34, 35 | bitrdi 286 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β ((π β¨ π) β π β (Β¬ π β€ π β¨ Β¬ π β€ π))) |
37 | | simpl11 1248 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β πΎ β HL) |
38 | 22 | adantr 481 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β π β π) |
39 | | simp122 1306 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β π β π) |
40 | 39 | adantr 481 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β π β π) |
41 | | simpl2l 1226 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β π β π΄) |
42 | | simpl2r 1227 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β π β π΄) |
43 | | simpr 485 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β Β¬ π β€ π) |
44 | | simp13l 1288 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β (π β§ π) β π΄) |
45 | 44 | adantr 481 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β (π β§ π) β π΄) |
46 | | llnexch.m |
. . . . . . . . . . 11
β’ β§ =
(meetβπΎ) |
47 | 25, 7, 46, 8, 4 | llnexchb2lem 38727 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π)))) |
48 | 37, 38, 40, 41, 42, 43, 45, 47 | syl331anc 1395 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π)))) |
49 | 48 | ex 413 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β (Β¬ π β€ π β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π))))) |
50 | | simpl11 1248 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β πΎ β HL) |
51 | 22 | adantr 481 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β π β π) |
52 | 39 | adantr 481 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β π β π) |
53 | | simpl2r 1227 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β π β π΄) |
54 | | simpl2l 1226 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β π β π΄) |
55 | | simpr 485 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β Β¬ π β€ π) |
56 | 44 | adantr 481 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β (π β§ π) β π΄) |
57 | 25, 7, 46, 8, 4 | llnexchb2lem 38727 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π)))) |
58 | 50, 51, 52, 53, 54, 55, 56, 57 | syl331anc 1395 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π)))) |
59 | 7, 8 | hlatjcom 38226 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = (π β¨ π)) |
60 | 50, 54, 53, 59 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β (π β¨ π) = (π β¨ π)) |
61 | 60 | breq2d 5159 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β ((π β§ π) β€ (π β¨ π) β (π β§ π) β€ (π β¨ π))) |
62 | 60 | oveq2d 7421 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β (π β§ (π β¨ π)) = (π β§ (π β¨ π))) |
63 | 62 | eqeq2d 2743 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β ((π β§ π) = (π β§ (π β¨ π)) β (π β§ π) = (π β§ (π β¨ π)))) |
64 | 58, 61, 63 | 3bitr4d 310 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β§ Β¬ π β€ π) β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π)))) |
65 | 64 | ex 413 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β (Β¬ π β€ π β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π))))) |
66 | 49, 65 | jaod 857 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β ((Β¬ π β€ π β¨ Β¬ π β€ π) β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π))))) |
67 | 36, 66 | sylbid 239 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β ((π β¨ π) β π β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π))))) |
68 | | neeq1 3003 |
. . . . . . 7
β’ (π = (π β¨ π) β (π β π β (π β¨ π) β π)) |
69 | | breq2 5151 |
. . . . . . . 8
β’ (π = (π β¨ π) β ((π β§ π) β€ π β (π β§ π) β€ (π β¨ π))) |
70 | | oveq2 7413 |
. . . . . . . . 9
β’ (π = (π β¨ π) β (π β§ π) = (π β§ (π β¨ π))) |
71 | 70 | eqeq2d 2743 |
. . . . . . . 8
β’ (π = (π β¨ π) β ((π β§ π) = (π β§ π) β (π β§ π) = (π β§ (π β¨ π)))) |
72 | 69, 71 | bibi12d 345 |
. . . . . . 7
β’ (π = (π β¨ π) β (((π β§ π) β€ π β (π β§ π) = (π β§ π)) β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π))))) |
73 | 68, 72 | imbi12d 344 |
. . . . . 6
β’ (π = (π β¨ π) β ((π β π β ((π β§ π) β€ π β (π β§ π) = (π β§ π))) β ((π β¨ π) β π β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π)))))) |
74 | 67, 73 | syl5ibrcom 246 |
. . . . 5
β’ (((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β§ (π β π΄ β§ π β π΄) β§ π β π) β (π = (π β¨ π) β (π β π β ((π β§ π) β€ π β (π β§ π) = (π β§ π))))) |
75 | 74 | 3exp 1119 |
. . . 4
β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β ((π β π΄ β§ π β π΄) β (π β π β (π = (π β¨ π) β (π β π β ((π β§ π) β€ π β (π β§ π) = (π β§ π))))))) |
76 | 75 | imp4a 423 |
. . 3
β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β ((π β π΄ β§ π β π΄) β ((π β π β§ π = (π β¨ π)) β (π β π β ((π β§ π) β€ π β (π β§ π) = (π β§ π)))))) |
77 | 76 | rexlimdvv 3210 |
. 2
β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β (βπ β π΄ βπ β π΄ (π β π β§ π = (π β¨ π)) β (π β π β ((π β§ π) β€ π β (π β§ π) = (π β§ π))))) |
78 | 11, 13, 77 | mp2d 49 |
1
β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β ((π β§ π) β€ π β (π β§ π) = (π β§ π))) |