Step | Hyp | Ref
| Expression |
1 | | hlatl 38230 |
. . . . 5
β’ (πΎ β HL β πΎ β AtLat) |
2 | 1 | adantr 482 |
. . . 4
β’ ((πΎ β HL β§ π β π») β πΎ β AtLat) |
3 | | simpr 486 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β π β π») |
4 | | eqid 2733 |
. . . . . . 7
β’
(BaseβπΎ) =
(BaseβπΎ) |
5 | | lhpocnle.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
6 | 4, 5 | lhpbase 38869 |
. . . . . 6
β’ (π β π» β π β (BaseβπΎ)) |
7 | | lhpocnle.o |
. . . . . . 7
β’ β₯ =
(ocβπΎ) |
8 | | eqid 2733 |
. . . . . . 7
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
9 | 4, 7, 8, 5 | lhpoc 38885 |
. . . . . 6
β’ ((πΎ β HL β§ π β (BaseβπΎ)) β (π β π» β ( β₯ βπ) β (AtomsβπΎ))) |
10 | 6, 9 | sylan2 594 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (π β π» β ( β₯ βπ) β (AtomsβπΎ))) |
11 | 3, 10 | mpbid 231 |
. . . 4
β’ ((πΎ β HL β§ π β π») β ( β₯ βπ) β (AtomsβπΎ)) |
12 | | eqid 2733 |
. . . . 5
β’
(0.βπΎ) =
(0.βπΎ) |
13 | 12, 8 | atn0 38178 |
. . . 4
β’ ((πΎ β AtLat β§ ( β₯
βπ) β
(AtomsβπΎ)) β (
β₯
βπ) β
(0.βπΎ)) |
14 | 2, 11, 13 | syl2anc 585 |
. . 3
β’ ((πΎ β HL β§ π β π») β ( β₯ βπ) β (0.βπΎ)) |
15 | 14 | neneqd 2946 |
. 2
β’ ((πΎ β HL β§ π β π») β Β¬ ( β₯ βπ) = (0.βπΎ)) |
16 | | simpr 486 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β€ π) β ( β₯ βπ) β€ π) |
17 | | hllat 38233 |
. . . . . . 7
β’ (πΎ β HL β πΎ β Lat) |
18 | 17 | ad2antrr 725 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β€ π) β πΎ β Lat) |
19 | | hlop 38232 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β OP) |
20 | 19 | ad2antrr 725 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β€ π) β πΎ β OP) |
21 | 6 | ad2antlr 726 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β€ π) β π β (BaseβπΎ)) |
22 | 4, 7 | opoccl 38064 |
. . . . . . 7
β’ ((πΎ β OP β§ π β (BaseβπΎ)) β ( β₯ βπ) β (BaseβπΎ)) |
23 | 20, 21, 22 | syl2anc 585 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β€ π) β ( β₯ βπ) β (BaseβπΎ)) |
24 | | lhpocnle.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
25 | 4, 24 | latref 18394 |
. . . . . 6
β’ ((πΎ β Lat β§ ( β₯
βπ) β
(BaseβπΎ)) β (
β₯
βπ) β€ ( β₯
βπ)) |
26 | 18, 23, 25 | syl2anc 585 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β€ π) β ( β₯ βπ) β€ ( β₯ βπ)) |
27 | | eqid 2733 |
. . . . . . 7
β’
(meetβπΎ) =
(meetβπΎ) |
28 | 4, 24, 27 | latlem12 18419 |
. . . . . 6
β’ ((πΎ β Lat β§ (( β₯
βπ) β
(BaseβπΎ) β§ π β (BaseβπΎ) β§ ( β₯ βπ) β (BaseβπΎ))) β ((( β₯
βπ) β€ π β§ ( β₯ βπ) β€ ( β₯ βπ)) β ( β₯ βπ) β€ (π(meetβπΎ)( β₯ βπ)))) |
29 | 18, 23, 21, 23, 28 | syl13anc 1373 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β€ π) β ((( β₯ βπ) β€ π β§ ( β₯ βπ) β€ ( β₯ βπ)) β ( β₯ βπ) β€ (π(meetβπΎ)( β₯ βπ)))) |
30 | 16, 26, 29 | mpbi2and 711 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β€ π) β ( β₯ βπ) β€ (π(meetβπΎ)( β₯ βπ))) |
31 | 4, 7, 27, 12 | opnoncon 38078 |
. . . . 5
β’ ((πΎ β OP β§ π β (BaseβπΎ)) β (π(meetβπΎ)( β₯ βπ)) = (0.βπΎ)) |
32 | 20, 21, 31 | syl2anc 585 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β€ π) β (π(meetβπΎ)( β₯ βπ)) = (0.βπΎ)) |
33 | 30, 32 | breqtrd 5175 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β€ π) β ( β₯ βπ) β€ (0.βπΎ)) |
34 | 4, 24, 12 | ople0 38057 |
. . . 4
β’ ((πΎ β OP β§ ( β₯
βπ) β
(BaseβπΎ)) β ((
β₯
βπ) β€
(0.βπΎ) β ( β₯
βπ) = (0.βπΎ))) |
35 | 20, 23, 34 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β€ π) β (( β₯ βπ) β€ (0.βπΎ) β ( β₯ βπ) = (0.βπΎ))) |
36 | 33, 35 | mpbid 231 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ( β₯ βπ) β€ π) β ( β₯ βπ) = (0.βπΎ)) |
37 | 15, 36 | mtand 815 |
1
β’ ((πΎ β HL β§ π β π») β Β¬ ( β₯ βπ) β€ π) |