Step | Hyp | Ref
| Expression |
1 | | hlatl 38533 |
. . . . . . 7
β’ (πΎ β HL β πΎ β AtLat) |
2 | 1 | 3ad2ant1 1133 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β πΎ β AtLat) |
3 | 2 | ad2antrr 724 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β πΎ β AtLat) |
4 | | eqid 2732 |
. . . . . 6
β’
(0.βπΎ) =
(0.βπΎ) |
5 | | intnat.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
6 | 4, 5 | atn0 38481 |
. . . . 5
β’ ((πΎ β AtLat β§ (π β§ π) β π΄) β (π β§ π) β (0.βπΎ)) |
7 | 3, 6 | sylancom 588 |
. . . 4
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β (π β§ π) β (0.βπΎ)) |
8 | 7 | ex 413 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β ((π β§ π) β π΄ β (π β§ π) β (0.βπΎ))) |
9 | | simpll1 1212 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β πΎ β HL) |
10 | 9 | hllatd 38537 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β πΎ β Lat) |
11 | | simpll2 1213 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β π β π΅) |
12 | | simpll3 1214 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β π β π΅) |
13 | | intnat.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
14 | | intnat.m |
. . . . . . . 8
β’ β§ =
(meetβπΎ) |
15 | 13, 14 | latmcom 18420 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) = (π β§ π)) |
16 | 10, 11, 12, 15 | syl3anc 1371 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β (π β§ π) = (π β§ π)) |
17 | | simplr 767 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β Β¬ π β€ π) |
18 | 9, 1 | syl 17 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β πΎ β AtLat) |
19 | | simpr 485 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β π β π΄) |
20 | | intnat.l |
. . . . . . . . 9
β’ β€ =
(leβπΎ) |
21 | 13, 20, 14, 4, 5 | atnle 38490 |
. . . . . . . 8
β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΅) β (Β¬ π β€ π β (π β§ π) = (0.βπΎ))) |
22 | 18, 19, 11, 21 | syl3anc 1371 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β (Β¬ π β€ π β (π β§ π) = (0.βπΎ))) |
23 | 17, 22 | mpbid 231 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β (π β§ π) = (0.βπΎ)) |
24 | 16, 23 | eqtrd 2772 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β§ π β π΄) β (π β§ π) = (0.βπΎ)) |
25 | 24 | ex 413 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β (π β π΄ β (π β§ π) = (0.βπΎ))) |
26 | 25 | necon3ad 2953 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β ((π β§ π) β (0.βπΎ) β Β¬ π β π΄)) |
27 | 8, 26 | syld 47 |
. 2
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ Β¬ π β€ π) β ((π β§ π) β π΄ β Β¬ π β π΄)) |
28 | 27 | impr 455 |
1
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ (π β§ π) β π΄)) β Β¬ π β π΄) |