Step | Hyp | Ref
| Expression |
1 | | hlatl 37868 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β AtLat) |
2 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β πΎ β AtLat) |
3 | | simpr1 1195 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΅) |
4 | | cvrat4.b |
. . . . . . . . . . 11
β’ π΅ = (BaseβπΎ) |
5 | | cvrat4.l |
. . . . . . . . . . 11
β’ β€ =
(leβπΎ) |
6 | | cvrat4.z |
. . . . . . . . . . 11
β’ 0 =
(0.βπΎ) |
7 | | cvrat4.a |
. . . . . . . . . . 11
β’ π΄ = (AtomsβπΎ) |
8 | 4, 5, 6, 7 | atlex 37824 |
. . . . . . . . . 10
β’ ((πΎ β AtLat β§ π β π΅ β§ π β 0 ) β βπ β π΄ π β€ π) |
9 | 8 | 3exp 1120 |
. . . . . . . . 9
β’ (πΎ β AtLat β (π β π΅ β (π β 0 β βπ β π΄ π β€ π))) |
10 | 2, 3, 9 | sylc 65 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β 0 β βπ β π΄ π β€ π)) |
11 | 10 | adantr 482 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π = π) β (π β 0 β βπ β π΄ π β€ π)) |
12 | | simpll 766 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π΄) β πΎ β HL) |
13 | | simplr3 1218 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π΄) β π β π΄) |
14 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π΄) β π β π΄) |
15 | | cvrat4.j |
. . . . . . . . . . . . . . 15
β’ β¨ =
(joinβπΎ) |
16 | 5, 15, 7 | hlatlej1 37883 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
17 | 12, 13, 14, 16 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π΄) β π β€ (π β¨ π)) |
18 | | breq1 5109 |
. . . . . . . . . . . . 13
β’ (π = π β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
19 | 17, 18 | syl5ibr 246 |
. . . . . . . . . . . 12
β’ (π = π β (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β π΄) β π β€ (π β¨ π))) |
20 | 19 | expd 417 |
. . . . . . . . . . 11
β’ (π = π β ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β π΄ β π β€ (π β¨ π)))) |
21 | 20 | impcom 409 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π = π) β (π β π΄ β π β€ (π β¨ π))) |
22 | 21 | anim2d 613 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π = π) β ((π β€ π β§ π β π΄) β (π β€ π β§ π β€ (π β¨ π)))) |
23 | 22 | expcomd 418 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π = π) β (π β π΄ β (π β€ π β (π β€ π β§ π β€ (π β¨ π))))) |
24 | 23 | reximdvai 3159 |
. . . . . . 7
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π = π) β (βπ β π΄ π β€ π β βπ β π΄ (π β€ π β§ π β€ (π β¨ π)))) |
25 | 11, 24 | syld 47 |
. . . . . 6
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π = π) β (π β 0 β βπ β π΄ (π β€ π β§ π β€ (π β¨ π)))) |
26 | 25 | ex 414 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π = π β (π β 0 β βπ β π΄ (π β€ π β§ π β€ (π β¨ π))))) |
27 | 26 | a1i 11 |
. . . 4
β’ (π β€ (π β¨ π) β ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π = π β (π β 0 β βπ β π΄ (π β€ π β§ π β€ (π β¨ π)))))) |
28 | 27 | com4l 92 |
. . 3
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π = π β (π β 0 β (π β€ (π β¨ π) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π)))))) |
29 | 28 | imp4a 424 |
. 2
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π = π β ((π β 0 β§ π β€ (π β¨ π)) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π))))) |
30 | | hllat 37871 |
. . . . . . . . . . . . . 14
β’ (πΎ β HL β πΎ β Lat) |
31 | 30 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β πΎ β Lat) |
32 | | simpr3 1197 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΄) |
33 | 4, 7 | atbase 37797 |
. . . . . . . . . . . . . 14
β’ (π β π΄ β π β π΅) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΅) |
35 | 4, 5, 15 | latleeqj2 18346 |
. . . . . . . . . . . . 13
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β€ π β (π β¨ π) = π)) |
36 | 31, 34, 3, 35 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β€ π β (π β¨ π) = π)) |
37 | 36 | biimpa 478 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ π) β (π β¨ π) = π) |
38 | 37 | breq2d 5118 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ π) β (π β€ (π β¨ π) β π β€ π)) |
39 | 38 | biimpa 478 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ π) β§ π β€ (π β¨ π)) β π β€ π) |
40 | 39 | expl 459 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β€ π β§ π β€ (π β¨ π)) β π β€ π)) |
41 | | simpl 484 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β πΎ β HL) |
42 | | simpr2 1196 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΄) |
43 | 5, 15, 7 | hlatlej2 37884 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
44 | 41, 32, 42, 43 | syl3anc 1372 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) |
45 | 40, 44 | jctird 528 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β€ π β§ π β€ (π β¨ π)) β (π β€ π β§ π β€ (π β¨ π)))) |
46 | 45, 42 | jctild 527 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β€ π β§ π β€ (π β¨ π)) β (π β π΄ β§ (π β€ π β§ π β€ (π β¨ π))))) |
47 | 46 | impl 457 |
. . . . 5
β’ ((((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ π) β§ π β€ (π β¨ π)) β (π β π΄ β§ (π β€ π β§ π β€ (π β¨ π)))) |
48 | | breq1 5109 |
. . . . . . 7
β’ (π = π β (π β€ π β π β€ π)) |
49 | | oveq2 7366 |
. . . . . . . 8
β’ (π = π β (π β¨ π) = (π β¨ π)) |
50 | 49 | breq2d 5118 |
. . . . . . 7
β’ (π = π β (π β€ (π β¨ π) β π β€ (π β¨ π))) |
51 | 48, 50 | anbi12d 632 |
. . . . . 6
β’ (π = π β ((π β€ π β§ π β€ (π β¨ π)) β (π β€ π β§ π β€ (π β¨ π)))) |
52 | 51 | rspcev 3580 |
. . . . 5
β’ ((π β π΄ β§ (π β€ π β§ π β€ (π β¨ π))) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π))) |
53 | 47, 52 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ π) β§ π β€ (π β¨ π)) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π))) |
54 | 53 | adantrl 715 |
. . 3
β’ ((((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ π β€ π) β§ (π β 0 β§ π β€ (π β¨ π))) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π))) |
55 | 54 | exp31 421 |
. 2
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β€ π β ((π β 0 β§ π β€ (π β¨ π)) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π))))) |
56 | | simpr 486 |
. . 3
β’ ((π β 0 β§ π β€ (π β¨ π)) β π β€ (π β¨ π)) |
57 | | ioran 983 |
. . . . 5
β’ (Β¬
(π = π β¨ π β€ π) β (Β¬ π = π β§ Β¬ π β€ π)) |
58 | | df-ne 2941 |
. . . . . 6
β’ (π β π β Β¬ π = π) |
59 | 58 | anbi1i 625 |
. . . . 5
β’ ((π β π β§ Β¬ π β€ π) β (Β¬ π = π β§ Β¬ π β€ π)) |
60 | 57, 59 | bitr4i 278 |
. . . 4
β’ (Β¬
(π = π β¨ π β€ π) β (π β π β§ Β¬ π β€ π)) |
61 | | eqid 2733 |
. . . . . . . . . 10
β’
(meetβπΎ) =
(meetβπΎ) |
62 | 4, 5, 15, 61, 7 | cvrat3 37951 |
. . . . . . . . 9
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)) β (π(meetβπΎ)(π β¨ π)) β π΄)) |
63 | 62 | 3expd 1354 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β π β (Β¬ π β€ π β (π β€ (π β¨ π) β (π(meetβπΎ)(π β¨ π)) β π΄)))) |
64 | 63 | imp4c 425 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β (π(meetβπΎ)(π β¨ π)) β π΄)) |
65 | 4, 7 | atbase 37797 |
. . . . . . . . . . . . 13
β’ (π β π΄ β π β π΅) |
66 | 42, 65 | syl 17 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β π β π΅) |
67 | 4, 15 | latjcl 18333 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
68 | 31, 66, 34, 67 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β¨ π) β π΅) |
69 | 4, 5, 61 | latmle1 18358 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ π β π΅ β§ (π β¨ π) β π΅) β (π(meetβπΎ)(π β¨ π)) β€ π) |
70 | 31, 3, 68, 69 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π(meetβπΎ)(π β¨ π)) β€ π) |
71 | 70 | adantr 482 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β (π(meetβπΎ)(π β¨ π)) β€ π) |
72 | | simpll 766 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β πΎ β HL) |
73 | 63 | imp44 430 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β (π(meetβπΎ)(π β¨ π)) β π΄) |
74 | | simplr2 1217 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β π β π΄) |
75 | 34 | adantr 482 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β π β π΅) |
76 | 73, 74, 75 | 3jca 1129 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β ((π(meetβπΎ)(π β¨ π)) β π΄ β§ π β π΄ β§ π β π΅)) |
77 | 72, 76 | jca 513 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β (πΎ β HL β§ ((π(meetβπΎ)(π β¨ π)) β π΄ β§ π β π΄ β§ π β π΅))) |
78 | 4, 5, 61, 6, 7 | atnle 37825 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΅) β (Β¬ π β€ π β (π(meetβπΎ)π) = 0 )) |
79 | 2, 32, 3, 78 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (Β¬ π β€ π β (π(meetβπΎ)π) = 0 )) |
80 | 4, 61 | latmcom 18357 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π(meetβπΎ)π) = (π(meetβπΎ)π)) |
81 | 31, 34, 3, 80 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π(meetβπΎ)π) = (π(meetβπΎ)π)) |
82 | 81 | eqeq1d 2735 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π(meetβπΎ)π) = 0 β (π(meetβπΎ)π) = 0 )) |
83 | 79, 82 | bitrd 279 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (Β¬ π β€ π β (π(meetβπΎ)π) = 0 )) |
84 | 4, 61 | latmcl 18334 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΎ β Lat β§ π β π΅ β§ (π β¨ π) β π΅) β (π(meetβπΎ)(π β¨ π)) β π΅) |
85 | 31, 3, 68, 84 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π(meetβπΎ)(π β¨ π)) β π΅) |
86 | 85, 3, 34 | 3jca 1129 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π(meetβπΎ)(π β¨ π)) β π΅ β§ π β π΅ β§ π β π΅)) |
87 | 31, 86 | jca 513 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (πΎ β Lat β§ ((π(meetβπΎ)(π β¨ π)) β π΅ β§ π β π΅ β§ π β π΅))) |
88 | 4, 5, 61 | latmlem2 18364 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ β Lat β§ ((π(meetβπΎ)(π β¨ π)) β π΅ β§ π β π΅ β§ π β π΅)) β ((π(meetβπΎ)(π β¨ π)) β€ π β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) β€ (π(meetβπΎ)π))) |
89 | 87, 70, 88 | sylc 65 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) β€ (π(meetβπΎ)π)) |
90 | 89, 81 | breqtrd 5132 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) β€ (π(meetβπΎ)π)) |
91 | | breq2 5110 |
. . . . . . . . . . . . . . . 16
β’ ((π(meetβπΎ)π) = 0 β ((π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) β€ (π(meetβπΎ)π) β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) β€ 0 )) |
92 | 90, 91 | syl5ibcom 244 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π(meetβπΎ)π) = 0 β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) β€ 0 )) |
93 | | hlop 37870 |
. . . . . . . . . . . . . . . . 17
β’ (πΎ β HL β πΎ β OP) |
94 | 93 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β πΎ β OP) |
95 | 4, 61 | latmcl 18334 |
. . . . . . . . . . . . . . . . 17
β’ ((πΎ β Lat β§ π β π΅ β§ (π(meetβπΎ)(π β¨ π)) β π΅) β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) β π΅) |
96 | 31, 34, 85, 95 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) β π΅) |
97 | 4, 5, 6 | ople0 37695 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β OP β§ (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) β π΅) β ((π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) β€ 0 β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) = 0 )) |
98 | 94, 96, 97 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) β€ 0 β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) = 0 )) |
99 | 92, 98 | sylibd 238 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π(meetβπΎ)π) = 0 β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) = 0 )) |
100 | 83, 99 | sylbid 239 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (Β¬ π β€ π β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) = 0 )) |
101 | 100 | imp 408 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ Β¬ π β€ π) β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) = 0 ) |
102 | 101 | adantrl 715 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ Β¬ π β€ π)) β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) = 0 ) |
103 | 102 | adantrr 716 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) = 0 ) |
104 | 4, 5, 61 | latmle2 18359 |
. . . . . . . . . . . . 13
β’ ((πΎ β Lat β§ π β π΅ β§ (π β¨ π) β π΅) β (π(meetβπΎ)(π β¨ π)) β€ (π β¨ π)) |
105 | 31, 3, 68, 104 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π(meetβπΎ)(π β¨ π)) β€ (π β¨ π)) |
106 | 4, 15 | latjcom 18341 |
. . . . . . . . . . . . 13
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) = (π β¨ π)) |
107 | 31, 66, 34, 106 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π β¨ π) = (π β¨ π)) |
108 | 105, 107 | breqtrd 5132 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (π(meetβπΎ)(π β¨ π)) β€ (π β¨ π)) |
109 | 108 | adantr 482 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β (π(meetβπΎ)(π β¨ π)) β€ (π β¨ π)) |
110 | 30 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ ((π(meetβπΎ)(π β¨ π)) β π΄ β§ π β π΄ β§ π β π΅)) β πΎ β Lat) |
111 | | simpr3 1197 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ ((π(meetβπΎ)(π β¨ π)) β π΄ β§ π β π΄ β§ π β π΅)) β π β π΅) |
112 | | simpr1 1195 |
. . . . . . . . . . . . . 14
β’ ((πΎ β HL β§ ((π(meetβπΎ)(π β¨ π)) β π΄ β§ π β π΄ β§ π β π΅)) β (π(meetβπΎ)(π β¨ π)) β π΄) |
113 | 4, 7 | atbase 37797 |
. . . . . . . . . . . . . 14
β’ ((π(meetβπΎ)(π β¨ π)) β π΄ β (π(meetβπΎ)(π β¨ π)) β π΅) |
114 | 112, 113 | syl 17 |
. . . . . . . . . . . . 13
β’ ((πΎ β HL β§ ((π(meetβπΎ)(π β¨ π)) β π΄ β§ π β π΄ β§ π β π΅)) β (π(meetβπΎ)(π β¨ π)) β π΅) |
115 | 4, 61 | latmcom 18357 |
. . . . . . . . . . . . 13
β’ ((πΎ β Lat β§ π β π΅ β§ (π(meetβπΎ)(π β¨ π)) β π΅) β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) = ((π(meetβπΎ)(π β¨ π))(meetβπΎ)π)) |
116 | 110, 111,
114, 115 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ ((π(meetβπΎ)(π β¨ π)) β π΄ β§ π β π΄ β§ π β π΅)) β (π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) = ((π(meetβπΎ)(π β¨ π))(meetβπΎ)π)) |
117 | 116 | eqeq1d 2735 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ ((π(meetβπΎ)(π β¨ π)) β π΄ β§ π β π΄ β§ π β π΅)) β ((π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) = 0 β ((π(meetβπΎ)(π β¨ π))(meetβπΎ)π) = 0 )) |
118 | 4, 5, 15, 61, 6, 7 | hlexch3 37900 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ ((π(meetβπΎ)(π β¨ π)) β π΄ β§ π β π΄ β§ π β π΅) β§ ((π(meetβπΎ)(π β¨ π))(meetβπΎ)π) = 0 ) β ((π(meetβπΎ)(π β¨ π)) β€ (π β¨ π) β π β€ (π β¨ (π(meetβπΎ)(π β¨ π))))) |
119 | 118 | 3expia 1122 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ ((π(meetβπΎ)(π β¨ π)) β π΄ β§ π β π΄ β§ π β π΅)) β (((π(meetβπΎ)(π β¨ π))(meetβπΎ)π) = 0 β ((π(meetβπΎ)(π β¨ π)) β€ (π β¨ π) β π β€ (π β¨ (π(meetβπΎ)(π β¨ π)))))) |
120 | 117, 119 | sylbid 239 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ ((π(meetβπΎ)(π β¨ π)) β π΄ β§ π β π΄ β§ π β π΅)) β ((π(meetβπΎ)(π(meetβπΎ)(π β¨ π))) = 0 β ((π(meetβπΎ)(π β¨ π)) β€ (π β¨ π) β π β€ (π β¨ (π(meetβπΎ)(π β¨ π)))))) |
121 | 77, 103, 109, 120 | syl3c 66 |
. . . . . . . . 9
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β π β€ (π β¨ (π(meetβπΎ)(π β¨ π)))) |
122 | 71, 121 | jca 513 |
. . . . . . . 8
β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ ((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β ((π(meetβπΎ)(π β¨ π)) β€ π β§ π β€ (π β¨ (π(meetβπΎ)(π β¨ π))))) |
123 | 122 | ex 414 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β ((π(meetβπΎ)(π β¨ π)) β€ π β§ π β€ (π β¨ (π(meetβπΎ)(π β¨ π)))))) |
124 | 64, 123 | jcad 514 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β ((π(meetβπΎ)(π β¨ π)) β π΄ β§ ((π(meetβπΎ)(π β¨ π)) β€ π β§ π β€ (π β¨ (π(meetβπΎ)(π β¨ π))))))) |
125 | | breq1 5109 |
. . . . . . . 8
β’ (π = (π(meetβπΎ)(π β¨ π)) β (π β€ π β (π(meetβπΎ)(π β¨ π)) β€ π)) |
126 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = (π(meetβπΎ)(π β¨ π)) β (π β¨ π) = (π β¨ (π(meetβπΎ)(π β¨ π)))) |
127 | 126 | breq2d 5118 |
. . . . . . . 8
β’ (π = (π(meetβπΎ)(π β¨ π)) β (π β€ (π β¨ π) β π β€ (π β¨ (π(meetβπΎ)(π β¨ π))))) |
128 | 125, 127 | anbi12d 632 |
. . . . . . 7
β’ (π = (π(meetβπΎ)(π β¨ π)) β ((π β€ π β§ π β€ (π β¨ π)) β ((π(meetβπΎ)(π β¨ π)) β€ π β§ π β€ (π β¨ (π(meetβπΎ)(π β¨ π)))))) |
129 | 128 | rspcev 3580 |
. . . . . 6
β’ (((π(meetβπΎ)(π β¨ π)) β π΄ β§ ((π(meetβπΎ)(π β¨ π)) β€ π β§ π β€ (π β¨ (π(meetβπΎ)(π β¨ π))))) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π))) |
130 | 124, 129 | syl6 35 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (((π β π β§ Β¬ π β€ π) β§ π β€ (π β¨ π)) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π)))) |
131 | 130 | expd 417 |
. . . 4
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β π β§ Β¬ π β€ π) β (π β€ (π β¨ π) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π))))) |
132 | 60, 131 | biimtrid 241 |
. . 3
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (Β¬ (π = π β¨ π β€ π) β (π β€ (π β¨ π) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π))))) |
133 | 56, 132 | syl7 74 |
. 2
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (Β¬ (π = π β¨ π β€ π) β ((π β 0 β§ π β€ (π β¨ π)) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π))))) |
134 | 29, 55, 133 | ecase3d 1033 |
1
β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π β€ (π β¨ π)) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π)))) |