Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π΅) β πΎ β HL) |
2 | | simpr 486 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π΅) β π β π΅) |
3 | | lhpj1.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
4 | | lhpj1.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
5 | 3, 4 | lhpbase 38507 |
. . . . 5
β’ (π β π» β π β π΅) |
6 | 5 | ad2antlr 726 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π΅) β π β π΅) |
7 | | lhpj1.l |
. . . . 5
β’ β€ =
(leβπΎ) |
8 | | eqid 2733 |
. . . . 5
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
9 | 3, 7, 8 | hlrelat2 37912 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β βπ β (AtomsβπΎ)(π β€ π β§ Β¬ π β€ π))) |
10 | 1, 2, 6, 9 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (Β¬ π β€ π β βπ β (AtomsβπΎ)(π β€ π β§ Β¬ π β€ π))) |
11 | | simp1l 1198 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β (πΎ β HL β§ π β π»)) |
12 | | simp2 1138 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β π β (AtomsβπΎ)) |
13 | | simp3r 1203 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β Β¬ π β€ π) |
14 | | lhpj1.j |
. . . . . . . 8
β’ β¨ =
(joinβπΎ) |
15 | | lhpj1.u |
. . . . . . . 8
β’ 1 =
(1.βπΎ) |
16 | 7, 14, 15, 8, 4 | lhpjat1 38529 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β (AtomsβπΎ) β§ Β¬ π β€ π)) β (π β¨ π) = 1 ) |
17 | 11, 12, 13, 16 | syl12anc 836 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β (π β¨ π) = 1 ) |
18 | | simp3l 1202 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β π β€ π) |
19 | | simp1ll 1237 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β πΎ β HL) |
20 | 19 | hllatd 37872 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β πΎ β Lat) |
21 | 3, 8 | atbase 37797 |
. . . . . . . . 9
β’ (π β (AtomsβπΎ) β π β π΅) |
22 | 21 | 3ad2ant2 1135 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β π β π΅) |
23 | | simp1r 1199 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β π β π΅) |
24 | 6 | 3ad2ant1 1134 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β π β π΅) |
25 | 3, 7, 14 | latjlej2 18348 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β€ π β (π β¨ π) β€ (π β¨ π))) |
26 | 20, 22, 23, 24, 25 | syl13anc 1373 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β (π β€ π β (π β¨ π) β€ (π β¨ π))) |
27 | 18, 26 | mpd 15 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β (π β¨ π) β€ (π β¨ π)) |
28 | 17, 27 | eqbrtrrd 5130 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β 1 β€ (π β¨ π)) |
29 | | hlop 37870 |
. . . . . . 7
β’ (πΎ β HL β πΎ β OP) |
30 | 19, 29 | syl 17 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β πΎ β OP) |
31 | 3, 14 | latjcl 18333 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
32 | 20, 24, 23, 31 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β (π β¨ π) β π΅) |
33 | 3, 7, 15 | op1le 37700 |
. . . . . 6
β’ ((πΎ β OP β§ (π β¨ π) β π΅) β ( 1 β€ (π β¨ π) β (π β¨ π) = 1 )) |
34 | 30, 32, 33 | syl2anc 585 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β ( 1 β€ (π β¨ π) β (π β¨ π) = 1 )) |
35 | 28, 34 | mpbid 231 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β π΅) β§ π β (AtomsβπΎ) β§ (π β€ π β§ Β¬ π β€ π)) β (π β¨ π) = 1 ) |
36 | 35 | rexlimdv3a 3153 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (βπ β (AtomsβπΎ)(π β€ π β§ Β¬ π β€ π) β (π β¨ π) = 1 )) |
37 | 10, 36 | sylbid 239 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (Β¬ π β€ π β (π β¨ π) = 1 )) |
38 | 37 | impr 456 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π)) β (π β¨ π) = 1 ) |