Step | Hyp | Ref
| Expression |
1 | | cvrat3.b |
. . . . . . . . . . . 12
β’ π΅ = (BaseβπΎ) |
2 | | cvrat3.l |
. . . . . . . . . . . 12
β’ β€ =
(leβπΎ) |
3 | | cvrat3.j |
. . . . . . . . . . . 12
β’ β¨ =
(joinβπΎ) |
4 | | eqid 2733 |
. . . . . . . . . . . 12
β’ ( β
βπΎ) = ( β
βπΎ) |
5 | | cvrat3.a |
. . . . . . . . . . . 12
β’ π΄ = (AtomsβπΎ) |
6 | 1, 2, 3, 4, 5 | cvr1 37919 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β π( β βπΎ)(π β¨ π))) |
7 | 6 | 3adant3r2 1184 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (Β¬ π β€ π β π( β βπΎ)(π β¨ π))) |
8 | 7 | biimpa 478 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ Β¬ π β€ π) β π( β βπΎ)(π β¨ π)) |
9 | 8 | adantrr 716 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ π β§ π β€ (π β¨ π))) β π( β βπΎ)(π β¨ π)) |
10 | | hllat 37871 |
. . . . . . . . . . . . . . . . . 18
β’ (πΎ β HL β πΎ β Lat) |
11 | 10 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β πΎ β Lat) |
12 | | simpr2 1196 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΄) |
13 | 1, 5 | atbase 37797 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΄ β π β π΅) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΅) |
15 | | simpr3 1197 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΄) |
16 | 1, 5 | atbase 37797 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π΄ β π β π΅) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΅) |
18 | 1, 3 | latjcom 18341 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) = (π β¨ π)) |
19 | 11, 14, 17, 18 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β¨ π) = (π β¨ π)) |
20 | 19 | oveq2d 7374 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β¨ (π β¨ π)) = (π β¨ (π β¨ π))) |
21 | | simpr1 1195 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΅) |
22 | 1, 3 | latjass 18377 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β¨ π) = (π β¨ (π β¨ π))) |
23 | 11, 21, 17, 14, 22 | syl13anc 1373 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ π) = (π β¨ (π β¨ π))) |
24 | 20, 23 | eqtr4d 2776 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β¨ (π β¨ π)) = ((π β¨ π) β¨ π)) |
25 | 24 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ (π β¨ π)) β (π β¨ (π β¨ π)) = ((π β¨ π) β¨ π)) |
26 | 1, 3 | latjcl 18333 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
27 | 11, 21, 17, 26 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β π΅) |
28 | 1, 2, 3 | latjlej2 18348 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β Lat β§ (π β π΅ β§ (π β¨ π) β π΅ β§ (π β¨ π) β π΅)) β (π β€ (π β¨ π) β ((π β¨ π) β¨ π) β€ ((π β¨ π) β¨ (π β¨ π)))) |
29 | 11, 14, 27, 27, 28 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β€ (π β¨ π) β ((π β¨ π) β¨ π) β€ ((π β¨ π) β¨ (π β¨ π)))) |
30 | 29 | imp 408 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ (π β¨ π)) β ((π β¨ π) β¨ π) β€ ((π β¨ π) β¨ (π β¨ π))) |
31 | 25, 30 | eqbrtrd 5128 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ (π β¨ π)) β (π β¨ (π β¨ π)) β€ ((π β¨ π) β¨ (π β¨ π))) |
32 | 1, 3 | latjidm 18356 |
. . . . . . . . . . . . . 14
β’ ((πΎ β Lat β§ (π β¨ π) β π΅) β ((π β¨ π) β¨ (π β¨ π)) = (π β¨ π)) |
33 | 11, 27, 32 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ (π β¨ π)) = (π β¨ π)) |
34 | 33 | adantr 482 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ (π β¨ π)) β ((π β¨ π) β¨ (π β¨ π)) = (π β¨ π)) |
35 | 31, 34 | breqtrd 5132 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ (π β¨ π)) β (π β¨ (π β¨ π)) β€ (π β¨ π)) |
36 | | simpl 484 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β πΎ β HL) |
37 | 2, 3, 5 | hlatlej2 37884 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
38 | 36, 12, 15, 37 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
39 | 1, 3 | latjcl 18333 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
40 | 11, 14, 17, 39 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β π΅) |
41 | 1, 2, 3 | latjlej2 18348 |
. . . . . . . . . . . . . 14
β’ ((πΎ β Lat β§ (π β π΅ β§ (π β¨ π) β π΅ β§ π β π΅)) β (π β€ (π β¨ π) β (π β¨ π) β€ (π β¨ (π β¨ π)))) |
42 | 11, 17, 40, 21, 41 | syl13anc 1373 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β€ (π β¨ π) β (π β¨ π) β€ (π β¨ (π β¨ π)))) |
43 | 38, 42 | mpd 15 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β€ (π β¨ (π β¨ π))) |
44 | 43 | adantr 482 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ (π β¨ π)) β (π β¨ π) β€ (π β¨ (π β¨ π))) |
45 | 1, 3 | latjcl 18333 |
. . . . . . . . . . . . . 14
β’ ((πΎ β Lat β§ π β π΅ β§ (π β¨ π) β π΅) β (π β¨ (π β¨ π)) β π΅) |
46 | 11, 21, 40, 45 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β¨ (π β¨ π)) β π΅) |
47 | 1, 2 | latasymb 18336 |
. . . . . . . . . . . . 13
β’ ((πΎ β Lat β§ (π β¨ (π β¨ π)) β π΅ β§ (π β¨ π) β π΅) β (((π β¨ (π β¨ π)) β€ (π β¨ π) β§ (π β¨ π) β€ (π β¨ (π β¨ π))) β (π β¨ (π β¨ π)) = (π β¨ π))) |
48 | 11, 46, 27, 47 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (((π β¨ (π β¨ π)) β€ (π β¨ π) β§ (π β¨ π) β€ (π β¨ (π β¨ π))) β (π β¨ (π β¨ π)) = (π β¨ π))) |
49 | 48 | adantr 482 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ (π β¨ π)) β (((π β¨ (π β¨ π)) β€ (π β¨ π) β§ (π β¨ π) β€ (π β¨ (π β¨ π))) β (π β¨ (π β¨ π)) = (π β¨ π))) |
50 | 35, 44, 49 | mpbi2and 711 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ (π β¨ π)) β (π β¨ (π β¨ π)) = (π β¨ π)) |
51 | 50 | breq2d 5118 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ (π β¨ π)) β (π( β βπΎ)(π β¨ (π β¨ π)) β π( β βπΎ)(π β¨ π))) |
52 | 51 | adantrl 715 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ π β§ π β€ (π β¨ π))) β (π( β βπΎ)(π β¨ (π β¨ π)) β π( β βπΎ)(π β¨ π))) |
53 | 9, 52 | mpbird 257 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ π β§ π β€ (π β¨ π))) β π( β βπΎ)(π β¨ (π β¨ π))) |
54 | 53 | ex 414 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((Β¬ π β€ π β§ π β€ (π β¨ π)) β π( β βπΎ)(π β¨ (π β¨ π)))) |
55 | | cvrat3.m |
. . . . . . . 8
β’ β§ =
(meetβπΎ) |
56 | 1, 3, 55, 4 | cvrexch 37929 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΅ β§ (π β¨ π) β π΅) β ((π β§ (π β¨ π))( β βπΎ)(π β¨ π) β π( β βπΎ)(π β¨ (π β¨ π)))) |
57 | 36, 21, 40, 56 | syl3anc 1372 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β§ (π β¨ π))( β βπΎ)(π β¨ π) β π( β βπΎ)(π β¨ (π β¨ π)))) |
58 | 54, 57 | sylibrd 259 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((Β¬ π β€ π β§ π β€ (π β¨ π)) β (π β§ (π β¨ π))( β βπΎ)(π β¨ π))) |
59 | 58 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π) β ((Β¬ π β€ π β§ π β€ (π β¨ π)) β (π β§ (π β¨ π))( β βπΎ)(π β¨ π))) |
60 | 1, 55 | latmcl 18334 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β π΅ β§ (π β¨ π) β π΅) β (π β§ (π β¨ π)) β π΅) |
61 | 11, 21, 40, 60 | syl3anc 1372 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β§ (π β¨ π)) β π΅) |
62 | 1, 3, 4, 5 | cvrat2 37938 |
. . . . . . 7
β’ ((πΎ β HL β§ ((π β§ (π β¨ π)) β π΅ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β§ (π β¨ π))( β βπΎ)(π β¨ π))) β (π β§ (π β¨ π)) β π΄) |
63 | 62 | 3expia 1122 |
. . . . . 6
β’ ((πΎ β HL β§ ((π β§ (π β¨ π)) β π΅ β§ π β π΄ β§ π β π΄)) β ((π β π β§ (π β§ (π β¨ π))( β βπΎ)(π β¨ π)) β (π β§ (π β¨ π)) β π΄)) |
64 | 36, 61, 12, 15, 63 | syl13anc 1373 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β π β§ (π β§ (π β¨ π))( β βπΎ)(π β¨ π)) β (π β§ (π β¨ π)) β π΄)) |
65 | 64 | expdimp 454 |
. . . 4
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π) β ((π β§ (π β¨ π))( β βπΎ)(π β¨ π) β (π β§ (π β¨ π)) β π΄)) |
66 | 59, 65 | syld 47 |
. . 3
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π) β ((Β¬ π β€ π β§ π β€ (π β¨ π)) β (π β§ (π β¨ π)) β π΄)) |
67 | 66 | exp4b 432 |
. 2
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β π β (Β¬ π β€ π β (π β€ (π β¨ π) β (π β§ (π β¨ π)) β π΄)))) |
68 | 67 | 3impd 1349 |
1
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)) β (π β§ (π β¨ π)) β π΄)) |