Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β πΎ β HL) |
2 | | simpl2 1193 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
3 | | eqid 2733 |
. . . . . . 7
β’
(0.βπΎ) =
(0.βπΎ) |
4 | | eqid 2733 |
. . . . . . 7
β’ ( β
βπΎ) = ( β
βπΎ) |
5 | | lnnat.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
6 | 3, 4, 5 | atcvr0 37796 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄) β (0.βπΎ)( β βπΎ)π) |
7 | 1, 2, 6 | syl2anc 585 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β (0.βπΎ)( β βπΎ)π) |
8 | | lnnat.j |
. . . . . . 7
β’ β¨ =
(joinβπΎ) |
9 | 8, 4, 5 | atcvr1 37926 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β π( β βπΎ)(π β¨ π))) |
10 | 9 | biimpa 478 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π( β βπΎ)(π β¨ π)) |
11 | | hlop 37870 |
. . . . . . 7
β’ (πΎ β HL β πΎ β OP) |
12 | | eqid 2733 |
. . . . . . . 8
β’
(BaseβπΎ) =
(BaseβπΎ) |
13 | 12, 3 | op0cl 37692 |
. . . . . . 7
β’ (πΎ β OP β
(0.βπΎ) β
(BaseβπΎ)) |
14 | 1, 11, 13 | 3syl 18 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β (0.βπΎ) β (BaseβπΎ)) |
15 | 12, 5 | atbase 37797 |
. . . . . . 7
β’ (π β π΄ β π β (BaseβπΎ)) |
16 | 2, 15 | syl 17 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β (BaseβπΎ)) |
17 | 1 | hllatd 37872 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β πΎ β Lat) |
18 | | simpl3 1194 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β π΄) |
19 | 12, 5 | atbase 37797 |
. . . . . . . 8
β’ (π β π΄ β π β (BaseβπΎ)) |
20 | 18, 19 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β (BaseβπΎ)) |
21 | 12, 8 | latjcl 18333 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β¨ π) β (BaseβπΎ)) |
22 | 17, 16, 20, 21 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β (π β¨ π) β (BaseβπΎ)) |
23 | 12, 4 | cvrntr 37934 |
. . . . . 6
β’ ((πΎ β HL β§
((0.βπΎ) β
(BaseβπΎ) β§ π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β (((0.βπΎ)( β βπΎ)π β§ π( β βπΎ)(π β¨ π)) β Β¬ (0.βπΎ)( β βπΎ)(π β¨ π))) |
24 | 1, 14, 16, 22, 23 | syl13anc 1373 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β (((0.βπΎ)( β βπΎ)π β§ π( β βπΎ)(π β¨ π)) β Β¬ (0.βπΎ)( β βπΎ)(π β¨ π))) |
25 | 7, 10, 24 | mp2and 698 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β Β¬ (0.βπΎ)( β βπΎ)(π β¨ π)) |
26 | | simpll1 1213 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β§ (π β¨ π) β π΄) β πΎ β HL) |
27 | 3, 4, 5 | atcvr0 37796 |
. . . . 5
β’ ((πΎ β HL β§ (π β¨ π) β π΄) β (0.βπΎ)( β βπΎ)(π β¨ π)) |
28 | 26, 27 | sylancom 589 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β§ (π β¨ π) β π΄) β (0.βπΎ)( β βπΎ)(π β¨ π)) |
29 | 25, 28 | mtand 815 |
. . 3
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β Β¬ (π β¨ π) β π΄) |
30 | 29 | ex 414 |
. 2
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β Β¬ (π β¨ π) β π΄)) |
31 | 8, 5 | hlatjidm 37877 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄) β (π β¨ π) = π) |
32 | 31 | 3adant3 1133 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = π) |
33 | | simp2 1138 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β π΄) |
34 | 32, 33 | eqeltrd 2834 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β π΄) |
35 | | oveq2 7366 |
. . . . 5
β’ (π = π β (π β¨ π) = (π β¨ π)) |
36 | 35 | eleq1d 2819 |
. . . 4
β’ (π = π β ((π β¨ π) β π΄ β (π β¨ π) β π΄)) |
37 | 34, 36 | syl5ibcom 244 |
. . 3
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π = π β (π β¨ π) β π΄)) |
38 | 37 | necon3bd 2954 |
. 2
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (Β¬ (π β¨ π) β π΄ β π β π)) |
39 | 30, 38 | impbid 211 |
1
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β Β¬ (π β¨ π) β π΄)) |