Step | Hyp | Ref
| Expression |
1 | | hlatl 37868 |
. . . . . . 7
β’ (πΎ β HL β πΎ β AtLat) |
2 | 1 | 3ad2ant1 1134 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β πΎ β AtLat) |
3 | 2 | ad2antrr 725 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β πΎ β AtLat) |
4 | | eqid 2733 |
. . . . . 6
β’
(0.βπΎ) =
(0.βπΎ) |
5 | | intnat.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
6 | 4, 5 | atn0 37816 |
. . . . 5
β’ ((πΎ β AtLat β§ (π β§ π) β π΄) β (π β§ π) β (0.βπΎ)) |
7 | 3, 6 | sylancom 589 |
. . . 4
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β (π β§ π) β (0.βπΎ)) |
8 | 7 | ex 414 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β ((π β§ π) β π΄ β (π β§ π) β (0.βπΎ))) |
9 | | simpll1 1213 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β πΎ β HL) |
10 | 9 | hllatd 37872 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β πΎ β Lat) |
11 | | simpll2 1214 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β π β π΅) |
12 | | simpll3 1215 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β π β π΅) |
13 | | intnat.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
14 | | intnat.m |
. . . . . . . 8
β’ β§ =
(meetβπΎ) |
15 | 13, 14 | latmcom 18357 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) = (π β§ π)) |
16 | 10, 11, 12, 15 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β (π β§ π) = (π β§ π)) |
17 | | simplr 768 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β Β¬ π β€ π) |
18 | 9, 1 | syl 17 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β πΎ β AtLat) |
19 | | simpr 486 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β π β π΄) |
20 | | intnat.l |
. . . . . . . . 9
β’ β€ =
(leβπΎ) |
21 | 13, 20, 14, 4, 5 | atnle 37825 |
. . . . . . . 8
β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΅) β (Β¬ π β€ π β (π β§ π) = (0.βπΎ))) |
22 | 18, 19, 11, 21 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β (Β¬ π β€ π β (π β§ π) = (0.βπΎ))) |
23 | 17, 22 | mpbid 231 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β (π β§ π) = (0.βπΎ)) |
24 | 16, 23 | eqtrd 2773 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β (π β§ π) = (0.βπΎ)) |
25 | 24 | ex 414 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β (π β π΄ β (π β§ π) = (0.βπΎ))) |
26 | 25 | necon3ad 2953 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β ((π β§ π) β (0.βπΎ) β Β¬ π β π΄)) |
27 | 8, 26 | syld 47 |
. 2
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β ((π β§ π) β π΄ β Β¬ π β π΄)) |
28 | 27 | impr 456 |
1
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ (π β§ π) β π΄)) β Β¬ π β π΄) |