Step | Hyp | Ref
| Expression |
1 | | simpl1 1191 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β πΎ β HL) |
2 | | hlatl 37416 |
. . . . 5
β’ (πΎ β HL β πΎ β AtLat) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β πΎ β AtLat) |
4 | 1 | hllatd 37420 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β πΎ β Lat) |
5 | | simpl2 1192 |
. . . . . 6
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β π β π) |
6 | | eqid 2736 |
. . . . . . 7
β’
(BaseβπΎ) =
(BaseβπΎ) |
7 | | 2llnmat.n |
. . . . . . 7
β’ π = (LLinesβπΎ) |
8 | 6, 7 | llnbase 37565 |
. . . . . 6
β’ (π β π β π β (BaseβπΎ)) |
9 | 5, 8 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β π β (BaseβπΎ)) |
10 | | simpl3 1193 |
. . . . . 6
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β π β π) |
11 | 6, 7 | llnbase 37565 |
. . . . . 6
β’ (π β π β π β (BaseβπΎ)) |
12 | 10, 11 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β π β (BaseβπΎ)) |
13 | | 2llnmat.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
14 | 6, 13 | latmcl 18203 |
. . . . 5
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β§ π) β (BaseβπΎ)) |
15 | 4, 9, 12, 14 | syl3anc 1371 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β (π β§ π) β (BaseβπΎ)) |
16 | | simprr 771 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β (π β§ π) β 0 ) |
17 | | eqid 2736 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
18 | | 2llnmat.z |
. . . . 5
β’ 0 =
(0.βπΎ) |
19 | | 2llnmat.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
20 | 6, 17, 18, 19 | atlex 37372 |
. . . 4
β’ ((πΎ β AtLat β§ (π β§ π) β (BaseβπΎ) β§ (π β§ π) β 0 ) β βπ β π΄ π(leβπΎ)(π β§ π)) |
21 | 3, 15, 16, 20 | syl3anc 1371 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β βπ β π΄ π(leβπΎ)(π β§ π)) |
22 | | simp1rl 1238 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β π β π) |
23 | | simp1l 1197 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β (πΎ β HL β§ π β π β§ π β π)) |
24 | 17, 7 | llncmp 37578 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π β§ π β π) β (π(leβπΎ)π β π = π)) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β (π(leβπΎ)π β π = π)) |
26 | | simp1l1 1266 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β πΎ β HL) |
27 | 26 | hllatd 37420 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β πΎ β Lat) |
28 | | simp1l2 1267 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β π β π) |
29 | 28, 8 | syl 17 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β π β (BaseβπΎ)) |
30 | | simp1l3 1268 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β π β π) |
31 | 30, 11 | syl 17 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β π β (BaseβπΎ)) |
32 | 6, 17, 13 | latleeqm1 18230 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π(leβπΎ)π β (π β§ π) = π)) |
33 | 27, 29, 31, 32 | syl3anc 1371 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β (π(leβπΎ)π β (π β§ π) = π)) |
34 | 25, 33 | bitr3d 281 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β (π = π β (π β§ π) = π)) |
35 | 34 | necon3bid 2986 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β (π β π β (π β§ π) β π)) |
36 | 22, 35 | mpbid 231 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β (π β§ π) β π) |
37 | | simp3 1138 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β π(leβπΎ)(π β§ π)) |
38 | 6, 17, 13 | latmle1 18227 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β§ π)(leβπΎ)π) |
39 | 27, 29, 31, 38 | syl3anc 1371 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β (π β§ π)(leβπΎ)π) |
40 | | hlpos 37422 |
. . . . . . . . . . 11
β’ (πΎ β HL β πΎ β Poset) |
41 | 26, 40 | syl 17 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β πΎ β Poset) |
42 | 6, 19 | atbase 37345 |
. . . . . . . . . . 11
β’ (π β π΄ β π β (BaseβπΎ)) |
43 | 42 | 3ad2ant2 1134 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β π β (BaseβπΎ)) |
44 | 27, 29, 31, 14 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β (π β§ π) β (BaseβπΎ)) |
45 | | simp2 1137 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β π β π΄) |
46 | 6, 17, 27, 43, 44, 29, 37, 39 | lattrd 18209 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β π(leβπΎ)π) |
47 | | eqid 2736 |
. . . . . . . . . . . 12
β’ ( β
βπΎ) = ( β
βπΎ) |
48 | 17, 47, 19, 7 | atcvrlln2 37575 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π΄ β§ π β π) β§ π(leβπΎ)π) β π( β βπΎ)π) |
49 | 26, 45, 28, 46, 48 | syl31anc 1373 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β π( β βπΎ)π) |
50 | 6, 17, 47 | cvrnbtwn4 37335 |
. . . . . . . . . 10
β’ ((πΎ β Poset β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ (π β§ π) β (BaseβπΎ)) β§ π( β βπΎ)π) β ((π(leβπΎ)(π β§ π) β§ (π β§ π)(leβπΎ)π) β (π = (π β§ π) β¨ (π β§ π) = π))) |
51 | 41, 43, 29, 44, 49, 50 | syl131anc 1383 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β ((π(leβπΎ)(π β§ π) β§ (π β§ π)(leβπΎ)π) β (π = (π β§ π) β¨ (π β§ π) = π))) |
52 | 37, 39, 51 | mpbi2and 710 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β (π = (π β§ π) β¨ (π β§ π) = π)) |
53 | | neor 3034 |
. . . . . . . 8
β’ ((π = (π β§ π) β¨ (π β§ π) = π) β (π β (π β§ π) β (π β§ π) = π)) |
54 | 52, 53 | sylib 217 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β (π β (π β§ π) β (π β§ π) = π)) |
55 | 54 | necon1d 2963 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β ((π β§ π) β π β π = (π β§ π))) |
56 | 36, 55 | mpd 15 |
. . . . 5
β’ ((((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β§ π β π΄ β§ π(leβπΎ)(π β§ π)) β π = (π β§ π)) |
57 | 56 | 3exp 1119 |
. . . 4
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β (π β π΄ β (π(leβπΎ)(π β§ π) β π = (π β§ π)))) |
58 | 57 | reximdvai 3159 |
. . 3
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β (βπ β π΄ π(leβπΎ)(π β§ π) β βπ β π΄ π = (π β§ π))) |
59 | 21, 58 | mpd 15 |
. 2
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β βπ β π΄ π = (π β§ π)) |
60 | | risset 3218 |
. 2
β’ ((π β§ π) β π΄ β βπ β π΄ π = (π β§ π)) |
61 | 59, 60 | sylibr 233 |
1
β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β (π β§ π) β π΄) |