Step | Hyp | Ref
| Expression |
1 | | hllat 37871 |
. . . . . . 7
β’ (πΎ β HL β πΎ β Lat) |
2 | | cvrexch.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
3 | | cvrexch.m |
. . . . . . . 8
β’ β§ =
(meetβπΎ) |
4 | 2, 3 | latmcl 18334 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
5 | 1, 4 | syl3an1 1164 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
6 | | eqid 2733 |
. . . . . . . 8
β’
(ltβπΎ) =
(ltβπΎ) |
7 | | cvrexch.c |
. . . . . . . 8
β’ πΆ = ( β βπΎ) |
8 | 2, 6, 7 | cvrlt 37778 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β§ π) β π΅ β§ π β π΅) β§ (π β§ π)πΆπ) β (π β§ π)(ltβπΎ)π) |
9 | 8 | ex 414 |
. . . . . 6
β’ ((πΎ β HL β§ (π β§ π) β π΅ β§ π β π΅) β ((π β§ π)πΆπ β (π β§ π)(ltβπΎ)π)) |
10 | 5, 9 | syld3an2 1412 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β (π β§ π)(ltβπΎ)π)) |
11 | | eqid 2733 |
. . . . . . 7
β’
(leβπΎ) =
(leβπΎ) |
12 | | eqid 2733 |
. . . . . . 7
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
13 | 2, 11, 6, 12 | hlrelat1 37909 |
. . . . . 6
β’ ((πΎ β HL β§ (π β§ π) β π΅ β§ π β π΅) β ((π β§ π)(ltβπΎ)π β βπ β (AtomsβπΎ)(Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π))) |
14 | 5, 13 | syld3an2 1412 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)(ltβπΎ)π β βπ β (AtomsβπΎ)(Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π))) |
15 | 10, 14 | syld 47 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β βπ β (AtomsβπΎ)(Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π))) |
16 | 15 | imp 408 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β§ π)πΆπ) β βπ β (AtomsβπΎ)(Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π)) |
17 | | simpl1 1192 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β πΎ β HL) |
18 | 17 | hllatd 37872 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β πΎ β Lat) |
19 | 2, 12 | atbase 37797 |
. . . . . . . . . . . . . . . . 17
β’ (π β (AtomsβπΎ) β π β π΅) |
20 | 19 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β π β π΅) |
21 | | simpl2 1193 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β π β π΅) |
22 | | simpl3 1194 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β π β π΅) |
23 | 2, 11, 3 | latlem12 18360 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)(π β§ π))) |
24 | 18, 20, 21, 22, 23 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)(π β§ π))) |
25 | 24 | biimpd 228 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β ((π(leβπΎ)π β§ π(leβπΎ)π) β π(leβπΎ)(π β§ π))) |
26 | 25 | expcomd 418 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β (π(leβπΎ)π β (π(leβπΎ)π β π(leβπΎ)(π β§ π)))) |
27 | | con3 153 |
. . . . . . . . . . . . 13
β’ ((π(leβπΎ)π β π(leβπΎ)(π β§ π)) β (Β¬ π(leβπΎ)(π β§ π) β Β¬ π(leβπΎ)π)) |
28 | 26, 27 | syl6 35 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β (π(leβπΎ)π β (Β¬ π(leβπΎ)(π β§ π) β Β¬ π(leβπΎ)π))) |
29 | 28 | com23 86 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β (Β¬ π(leβπΎ)(π β§ π) β (π(leβπΎ)π β Β¬ π(leβπΎ)π))) |
30 | 29 | a1d 25 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β ((π β§ π)πΆπ β (Β¬ π(leβπΎ)(π β§ π) β (π(leβπΎ)π β Β¬ π(leβπΎ)π)))) |
31 | 30 | imp4d 426 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β (((π β§ π)πΆπ β§ (Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π)) β Β¬ π(leβπΎ)π)) |
32 | | simpr 486 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β π β (AtomsβπΎ)) |
33 | | cvrexch.j |
. . . . . . . . . . 11
β’ β¨ =
(joinβπΎ) |
34 | 2, 11, 33, 7, 12 | cvr1 37919 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΅ β§ π β (AtomsβπΎ)) β (Β¬ π(leβπΎ)π β ππΆ(π β¨ π))) |
35 | 17, 21, 32, 34 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β (Β¬ π(leβπΎ)π β ππΆ(π β¨ π))) |
36 | 31, 35 | sylibd 238 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β (((π β§ π)πΆπ β§ (Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π)) β ππΆ(π β¨ π))) |
37 | 36 | imp 408 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β§ ((π β§ π)πΆπ β§ (Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π))) β ππΆ(π β¨ π)) |
38 | | simpl1 1192 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β πΎ β HL) |
39 | 38 | hllatd 37872 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β πΎ β Lat) |
40 | | simpl2 1193 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β π β π΅) |
41 | | simpl3 1194 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β π β π΅) |
42 | 39, 40, 41, 4 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β (π β§ π) β π΅) |
43 | | simpr 486 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β π β π΅) |
44 | 2, 33 | latjass 18377 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ (π β π΅ β§ (π β§ π) β π΅ β§ π β π΅)) β ((π β¨ (π β§ π)) β¨ π) = (π β¨ ((π β§ π) β¨ π))) |
45 | 39, 40, 42, 43, 44 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β ((π β¨ (π β§ π)) β¨ π) = (π β¨ ((π β§ π) β¨ π))) |
46 | 2, 33, 3 | latabs1 18369 |
. . . . . . . . . . . . . 14
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ (π β§ π)) = π) |
47 | 1, 46 | syl3an1 1164 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β¨ (π β§ π)) = π) |
48 | 47 | adantr 482 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β (π β¨ (π β§ π)) = π) |
49 | 48 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β ((π β¨ (π β§ π)) β¨ π) = (π β¨ π)) |
50 | 45, 49 | eqtr3d 2775 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β (π β¨ ((π β§ π) β¨ π)) = (π β¨ π)) |
51 | 50 | adantr 482 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β§ ((π β§ π)πΆπ β§ (Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π))) β (π β¨ ((π β§ π) β¨ π)) = (π β¨ π)) |
52 | 2, 11, 6, 33 | latnle 18367 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β Lat β§ (π β§ π) β π΅ β§ π β π΅) β (Β¬ π(leβπΎ)(π β§ π) β (π β§ π)(ltβπΎ)((π β§ π) β¨ π))) |
53 | 39, 42, 43, 52 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β (Β¬ π(leβπΎ)(π β§ π) β (π β§ π)(ltβπΎ)((π β§ π) β¨ π))) |
54 | 2, 11, 3 | latmle2 18359 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π)(leβπΎ)π) |
55 | 39, 40, 41, 54 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β (π β§ π)(leβπΎ)π) |
56 | 55 | biantrurd 534 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β (π(leβπΎ)π β ((π β§ π)(leβπΎ)π β§ π(leβπΎ)π))) |
57 | 2, 11, 33 | latjle12 18344 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β Lat β§ ((π β§ π) β π΅ β§ π β π΅ β§ π β π΅)) β (((π β§ π)(leβπΎ)π β§ π(leβπΎ)π) β ((π β§ π) β¨ π)(leβπΎ)π)) |
58 | 39, 42, 43, 41, 57 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β (((π β§ π)(leβπΎ)π β§ π(leβπΎ)π) β ((π β§ π) β¨ π)(leβπΎ)π)) |
59 | 56, 58 | bitrd 279 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β (π(leβπΎ)π β ((π β§ π) β¨ π)(leβπΎ)π)) |
60 | 53, 59 | anbi12d 632 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β ((Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π) β ((π β§ π)(ltβπΎ)((π β§ π) β¨ π) β§ ((π β§ π) β¨ π)(leβπΎ)π))) |
61 | | hlpos 37874 |
. . . . . . . . . . . . . . . 16
β’ (πΎ β HL β πΎ β Poset) |
62 | 38, 61 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β πΎ β Poset) |
63 | 2, 33 | latjcl 18333 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β Lat β§ (π β§ π) β π΅ β§ π β π΅) β ((π β§ π) β¨ π) β π΅) |
64 | 39, 42, 43, 63 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β ((π β§ π) β¨ π) β π΅) |
65 | 42, 41, 64 | 3jca 1129 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β ((π β§ π) β π΅ β§ π β π΅ β§ ((π β§ π) β¨ π) β π΅)) |
66 | 2, 11, 6, 7 | cvrnbtwn2 37783 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β Poset β§ ((π β§ π) β π΅ β§ π β π΅ β§ ((π β§ π) β¨ π) β π΅) β§ (π β§ π)πΆπ) β (((π β§ π)(ltβπΎ)((π β§ π) β¨ π) β§ ((π β§ π) β¨ π)(leβπΎ)π) β ((π β§ π) β¨ π) = π)) |
67 | 66 | biimpd 228 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β Poset β§ ((π β§ π) β π΅ β§ π β π΅ β§ ((π β§ π) β¨ π) β π΅) β§ (π β§ π)πΆπ) β (((π β§ π)(ltβπΎ)((π β§ π) β¨ π) β§ ((π β§ π) β¨ π)(leβπΎ)π) β ((π β§ π) β¨ π) = π)) |
68 | 67 | 3exp 1120 |
. . . . . . . . . . . . . . 15
β’ (πΎ β Poset β (((π β§ π) β π΅ β§ π β π΅ β§ ((π β§ π) β¨ π) β π΅) β ((π β§ π)πΆπ β (((π β§ π)(ltβπΎ)((π β§ π) β¨ π) β§ ((π β§ π) β¨ π)(leβπΎ)π) β ((π β§ π) β¨ π) = π)))) |
69 | 62, 65, 68 | sylc 65 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β ((π β§ π)πΆπ β (((π β§ π)(ltβπΎ)((π β§ π) β¨ π) β§ ((π β§ π) β¨ π)(leβπΎ)π) β ((π β§ π) β¨ π) = π))) |
70 | 69 | com23 86 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β (((π β§ π)(ltβπΎ)((π β§ π) β¨ π) β§ ((π β§ π) β¨ π)(leβπΎ)π) β ((π β§ π)πΆπ β ((π β§ π) β¨ π) = π))) |
71 | 60, 70 | sylbid 239 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β ((Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π) β ((π β§ π)πΆπ β ((π β§ π) β¨ π) = π))) |
72 | 71 | com23 86 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β ((π β§ π)πΆπ β ((Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π) β ((π β§ π) β¨ π) = π))) |
73 | 72 | imp32 420 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β§ ((π β§ π)πΆπ β§ (Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π))) β ((π β§ π) β¨ π) = π) |
74 | 73 | oveq2d 7374 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β§ ((π β§ π)πΆπ β§ (Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π))) β (π β¨ ((π β§ π) β¨ π)) = (π β¨ π)) |
75 | 51, 74 | eqtr3d 2775 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β π΅) β§ ((π β§ π)πΆπ β§ (Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π))) β (π β¨ π) = (π β¨ π)) |
76 | 19, 75 | sylanl2 680 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β§ ((π β§ π)πΆπ β§ (Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π))) β (π β¨ π) = (π β¨ π)) |
77 | 37, 76 | breqtrd 5132 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β§ ((π β§ π)πΆπ β§ (Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π))) β ππΆ(π β¨ π)) |
78 | 77 | expr 458 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β (AtomsβπΎ)) β§ (π β§ π)πΆπ) β ((Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π) β ππΆ(π β¨ π))) |
79 | 78 | an32s 651 |
. . . 4
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β§ π)πΆπ) β§ π β (AtomsβπΎ)) β ((Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π) β ππΆ(π β¨ π))) |
80 | 79 | rexlimdva 3149 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β§ π)πΆπ) β (βπ β (AtomsβπΎ)(Β¬ π(leβπΎ)(π β§ π) β§ π(leβπΎ)π) β ππΆ(π β¨ π))) |
81 | 16, 80 | mpd 15 |
. 2
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β§ π)πΆπ) β ππΆ(π β¨ π)) |
82 | 81 | ex 414 |
1
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β ππΆ(π β¨ π))) |