Step | Hyp | Ref
| Expression |
1 | | simpl3 1194 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β π β π) |
2 | 1 | necomd 2996 |
. . . 4
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β π β π) |
3 | | simplr 768 |
. . . . . . . . 9
β’ ((((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β§ π
= π) β (π β¨ π
) = (π β¨ π
)) |
4 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π
= π β (π β¨ π
) = (π β¨ π)) |
5 | | oveq2 7366 |
. . . . . . . . . . . 12
β’ (π
= π β (π β¨ π
) = (π β¨ π)) |
6 | 4, 5 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (π
= π β ((π β¨ π
) = (π β¨ π
) β (π β¨ π) = (π β¨ π))) |
7 | | eqcom 2740 |
. . . . . . . . . . 11
β’ ((π β¨ π) = (π β¨ π) β (π β¨ π) = (π β¨ π)) |
8 | 6, 7 | bitrdi 287 |
. . . . . . . . . 10
β’ (π
= π β ((π β¨ π
) = (π β¨ π
) β (π β¨ π) = (π β¨ π))) |
9 | 8 | adantl 483 |
. . . . . . . . 9
β’ ((((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β§ π
= π) β ((π β¨ π
) = (π β¨ π
) β (π β¨ π) = (π β¨ π))) |
10 | 3, 9 | mpbid 231 |
. . . . . . . 8
β’ ((((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β§ π
= π) β (π β¨ π) = (π β¨ π)) |
11 | | simpl1 1192 |
. . . . . . . . . . 11
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β πΎ β CvLat) |
12 | | cvllat 37834 |
. . . . . . . . . . 11
β’ (πΎ β CvLat β πΎ β Lat) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β πΎ β Lat) |
14 | | simpl21 1252 |
. . . . . . . . . . 11
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β π β π΄) |
15 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(BaseβπΎ) =
(BaseβπΎ) |
16 | | cvlsupr2.a |
. . . . . . . . . . . 12
β’ π΄ = (AtomsβπΎ) |
17 | 15, 16 | atbase 37797 |
. . . . . . . . . . 11
β’ (π β π΄ β π β (BaseβπΎ)) |
18 | 14, 17 | syl 17 |
. . . . . . . . . 10
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β π β (BaseβπΎ)) |
19 | | cvlsupr2.j |
. . . . . . . . . . 11
β’ β¨ =
(joinβπΎ) |
20 | 15, 19 | latjidm 18356 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π β (BaseβπΎ)) β (π β¨ π) = π) |
21 | 13, 18, 20 | syl2anc 585 |
. . . . . . . . 9
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π β¨ π) = π) |
22 | 21 | adantr 482 |
. . . . . . . 8
β’ ((((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β§ π
= π) β (π β¨ π) = π) |
23 | 10, 22 | eqtrd 2773 |
. . . . . . 7
β’ ((((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β§ π
= π) β (π β¨ π) = π) |
24 | 23 | ex 414 |
. . . . . 6
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π
= π β (π β¨ π) = π)) |
25 | | simpl22 1253 |
. . . . . . . . 9
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β π β π΄) |
26 | 15, 16 | atbase 37797 |
. . . . . . . . 9
β’ (π β π΄ β π β (BaseβπΎ)) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β π β (BaseβπΎ)) |
28 | | cvlsupr2.l |
. . . . . . . . 9
β’ β€ =
(leβπΎ) |
29 | 15, 28, 19 | latleeqj1 18345 |
. . . . . . . 8
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β€ π β (π β¨ π) = π)) |
30 | 13, 27, 18, 29 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π β€ π β (π β¨ π) = π)) |
31 | | cvlatl 37833 |
. . . . . . . . 9
β’ (πΎ β CvLat β πΎ β AtLat) |
32 | 11, 31 | syl 17 |
. . . . . . . 8
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β πΎ β AtLat) |
33 | 28, 16 | atcmp 37819 |
. . . . . . . 8
β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β (π β€ π β π = π)) |
34 | 32, 25, 14, 33 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π β€ π β π = π)) |
35 | 30, 34 | bitr3d 281 |
. . . . . 6
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β ((π β¨ π) = π β π = π)) |
36 | 24, 35 | sylibd 238 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π
= π β π = π)) |
37 | 36 | necon3d 2961 |
. . . 4
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π β π β π
β π)) |
38 | 2, 37 | mpd 15 |
. . 3
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β π
β π) |
39 | | simplr 768 |
. . . . . . . . 9
β’ ((((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β§ π
= π) β (π β¨ π
) = (π β¨ π
)) |
40 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π
= π β (π β¨ π
) = (π β¨ π)) |
41 | | oveq2 7366 |
. . . . . . . . . . 11
β’ (π
= π β (π β¨ π
) = (π β¨ π)) |
42 | 40, 41 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (π
= π β ((π β¨ π
) = (π β¨ π
) β (π β¨ π) = (π β¨ π))) |
43 | 42 | adantl 483 |
. . . . . . . . 9
β’ ((((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β§ π
= π) β ((π β¨ π
) = (π β¨ π
) β (π β¨ π) = (π β¨ π))) |
44 | 39, 43 | mpbid 231 |
. . . . . . . 8
β’ ((((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β§ π
= π) β (π β¨ π) = (π β¨ π)) |
45 | 15, 19 | latjidm 18356 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π β (BaseβπΎ)) β (π β¨ π) = π) |
46 | 13, 27, 45 | syl2anc 585 |
. . . . . . . . 9
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π β¨ π) = π) |
47 | 46 | adantr 482 |
. . . . . . . 8
β’ ((((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β§ π
= π) β (π β¨ π) = π) |
48 | 44, 47 | eqtrd 2773 |
. . . . . . 7
β’ ((((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β§ π
= π) β (π β¨ π) = π) |
49 | 48 | ex 414 |
. . . . . 6
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π
= π β (π β¨ π) = π)) |
50 | 15, 28, 19 | latleeqj1 18345 |
. . . . . . . 8
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β€ π β (π β¨ π) = π)) |
51 | 13, 18, 27, 50 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π β€ π β (π β¨ π) = π)) |
52 | 28, 16 | atcmp 37819 |
. . . . . . . 8
β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β (π β€ π β π = π)) |
53 | 32, 14, 25, 52 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π β€ π β π = π)) |
54 | 51, 53 | bitr3d 281 |
. . . . . 6
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β ((π β¨ π) = π β π = π)) |
55 | 49, 54 | sylibd 238 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π
= π β π = π)) |
56 | 55 | necon3d 2961 |
. . . 4
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π β π β π
β π)) |
57 | 1, 56 | mpd 15 |
. . 3
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β π
β π) |
58 | | simpl23 1254 |
. . . . . . 7
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β π
β π΄) |
59 | 15, 16 | atbase 37797 |
. . . . . . 7
β’ (π
β π΄ β π
β (BaseβπΎ)) |
60 | 58, 59 | syl 17 |
. . . . . 6
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β π
β (BaseβπΎ)) |
61 | 15, 28, 19 | latlej1 18342 |
. . . . . 6
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π
β (BaseβπΎ)) β π β€ (π β¨ π
)) |
62 | 13, 27, 60, 61 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β π β€ (π β¨ π
)) |
63 | | simpr 486 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π β¨ π
) = (π β¨ π
)) |
64 | 62, 63 | breqtrrd 5134 |
. . . 4
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β π β€ (π β¨ π
)) |
65 | 28, 19, 16 | cvlatexch1 37844 |
. . . . 5
β’ ((πΎ β CvLat β§ (π β π΄ β§ π
β π΄ β§ π β π΄) β§ π β π) β (π β€ (π β¨ π
) β π
β€ (π β¨ π))) |
66 | 11, 25, 58, 14, 2, 65 | syl131anc 1384 |
. . . 4
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π β€ (π β¨ π
) β π
β€ (π β¨ π))) |
67 | 64, 66 | mpd 15 |
. . 3
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β π
β€ (π β¨ π)) |
68 | 38, 57, 67 | 3jca 1129 |
. 2
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π β¨ π
) = (π β¨ π
)) β (π
β π β§ π
β π β§ π
β€ (π β¨ π))) |
69 | | simpr3 1197 |
. . 3
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β π
β€ (π β¨ π)) |
70 | | simpl1 1192 |
. . . . . . 7
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β πΎ β CvLat) |
71 | 70, 12 | syl 17 |
. . . . . 6
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β πΎ β Lat) |
72 | | simpl21 1252 |
. . . . . . 7
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β π β π΄) |
73 | 72, 17 | syl 17 |
. . . . . 6
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β π β (BaseβπΎ)) |
74 | | simpl22 1253 |
. . . . . . 7
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β π β π΄) |
75 | 74, 26 | syl 17 |
. . . . . 6
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β π β (BaseβπΎ)) |
76 | 15, 19 | latjcom 18341 |
. . . . . 6
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β¨ π) = (π β¨ π)) |
77 | 71, 73, 75, 76 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β (π β¨ π) = (π β¨ π)) |
78 | 77 | breq2d 5118 |
. . . 4
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β (π
β€ (π β¨ π) β π
β€ (π β¨ π))) |
79 | | simpl23 1254 |
. . . . . 6
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β π
β π΄) |
80 | | simpr2 1196 |
. . . . . 6
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β π
β π) |
81 | 28, 19, 16 | cvlatexch1 37844 |
. . . . . 6
β’ ((πΎ β CvLat β§ (π
β π΄ β§ π β π΄ β§ π β π΄) β§ π
β π) β (π
β€ (π β¨ π) β π β€ (π β¨ π
))) |
82 | 70, 79, 72, 74, 80, 81 | syl131anc 1384 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β (π
β€ (π β¨ π) β π β€ (π β¨ π
))) |
83 | | simpr1 1195 |
. . . . . . 7
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β π
β π) |
84 | 83 | necomd 2996 |
. . . . . 6
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β π β π
) |
85 | 28, 19, 16 | cvlatexchb2 37843 |
. . . . . 6
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π
) β (π β€ (π β¨ π
) β (π β¨ π
) = (π β¨ π
))) |
86 | 70, 72, 74, 79, 84, 85 | syl131anc 1384 |
. . . . 5
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β (π β€ (π β¨ π
) β (π β¨ π
) = (π β¨ π
))) |
87 | 82, 86 | sylibd 238 |
. . . 4
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β (π
β€ (π β¨ π) β (π β¨ π
) = (π β¨ π
))) |
88 | 78, 87 | sylbid 239 |
. . 3
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β (π
β€ (π β¨ π) β (π β¨ π
) = (π β¨ π
))) |
89 | 69, 88 | mpd 15 |
. 2
β’ (((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β§ (π
β π β§ π
β π β§ π
β€ (π β¨ π))) β (π β¨ π
) = (π β¨ π
)) |
90 | 68, 89 | impbida 800 |
1
β’ ((πΎ β CvLat β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β ((π β¨ π
) = (π β¨ π
) β (π
β π β§ π
β π β§ π
β€ (π β¨ π)))) |