Step | Hyp | Ref
| Expression |
1 | | simpr3 1197 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β (π β§ π) = 0 ) |
2 | | simpl 484 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β (πΎ β HL β§ π β π»)) |
3 | | simpr1 1195 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β π β π΅) |
4 | | simpr2 1196 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β π β 0 ) |
5 | | hllat 37871 |
. . . . . . . . . . 11
β’ (πΎ β HL β πΎ β Lat) |
6 | 5 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β πΎ β Lat) |
7 | | lhpm0at.b |
. . . . . . . . . . . 12
β’ π΅ = (BaseβπΎ) |
8 | | lhpm0at.h |
. . . . . . . . . . . 12
β’ π» = (LHypβπΎ) |
9 | 7, 8 | lhpbase 38507 |
. . . . . . . . . . 11
β’ (π β π» β π β π΅) |
10 | 9 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β π β π΅) |
11 | | eqid 2733 |
. . . . . . . . . . 11
β’
(leβπΎ) =
(leβπΎ) |
12 | | lhpm0at.m |
. . . . . . . . . . 11
β’ β§ =
(meetβπΎ) |
13 | 7, 11, 12 | latleeqm1 18361 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π(leβπΎ)π β (π β§ π) = π)) |
14 | 6, 3, 10, 13 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β (π(leβπΎ)π β (π β§ π) = π)) |
15 | 14 | biimpa 478 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β§ π(leβπΎ)π) β (π β§ π) = π) |
16 | | simplr3 1218 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β§ π(leβπΎ)π) β (π β§ π) = 0 ) |
17 | 15, 16 | eqtr3d 2775 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β§ π(leβπΎ)π) β π = 0 ) |
18 | 17 | ex 414 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β (π(leβπΎ)π β π = 0 )) |
19 | 18 | necon3ad 2953 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β (π β 0 β Β¬ π(leβπΎ)π)) |
20 | 4, 19 | mpd 15 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β Β¬ π(leβπΎ)π) |
21 | | eqid 2733 |
. . . . 5
β’ ( β
βπΎ) = ( β
βπΎ) |
22 | 7, 11, 12, 21, 8 | lhpmcvr 38532 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π(leβπΎ)π)) β (π β§ π)( β βπΎ)π) |
23 | 2, 3, 20, 22 | syl12anc 836 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β (π β§ π)( β βπΎ)π) |
24 | 1, 23 | eqbrtrrd 5130 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β 0 ( β
βπΎ)π) |
25 | | simpll 766 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β πΎ β HL) |
26 | | lhpm0at.o |
. . . 4
β’ 0 =
(0.βπΎ) |
27 | | lhpm0at.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
28 | 7, 26, 21, 27 | isat2 37795 |
. . 3
β’ ((πΎ β HL β§ π β π΅) β (π β π΄ β 0 ( β βπΎ)π)) |
29 | 25, 3, 28 | syl2anc 585 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β (π β π΄ β 0 ( β βπΎ)π)) |
30 | 24, 29 | mpbird 257 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β π β π΄) |