Step | Hyp | Ref
| Expression |
1 | | 2dim.j |
. . 3
β’ β¨ =
(joinβπΎ) |
2 | | eqid 2737 |
. . 3
β’
(leβπΎ) =
(leβπΎ) |
3 | | 2dim.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
4 | 1, 2, 3 | 3dim1 37959 |
. 2
β’ ((πΎ β HL β§ π β π΄) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π(leβπΎ)(π β¨ π) β§ Β¬ π (leβπΎ)((π β¨ π) β¨ π))) |
5 | | df-3an 1090 |
. . . . . . . 8
β’ ((π β π β§ Β¬ π(leβπΎ)(π β¨ π) β§ Β¬ π (leβπΎ)((π β¨ π) β¨ π)) β ((π β π β§ Β¬ π(leβπΎ)(π β¨ π)) β§ Β¬ π (leβπΎ)((π β¨ π) β¨ π))) |
6 | 5 | rexbii 3098 |
. . . . . . 7
β’
(βπ β
π΄ (π β π β§ Β¬ π(leβπΎ)(π β¨ π) β§ Β¬ π (leβπΎ)((π β¨ π) β¨ π)) β βπ β π΄ ((π β π β§ Β¬ π(leβπΎ)(π β¨ π)) β§ Β¬ π (leβπΎ)((π β¨ π) β¨ π))) |
7 | | r19.42v 3188 |
. . . . . . 7
β’
(βπ β
π΄ ((π β π β§ Β¬ π(leβπΎ)(π β¨ π)) β§ Β¬ π (leβπΎ)((π β¨ π) β¨ π)) β ((π β π β§ Β¬ π(leβπΎ)(π β¨ π)) β§ βπ β π΄ Β¬ π (leβπΎ)((π β¨ π) β¨ π))) |
8 | 6, 7 | bitri 275 |
. . . . . 6
β’
(βπ β
π΄ (π β π β§ Β¬ π(leβπΎ)(π β¨ π) β§ Β¬ π (leβπΎ)((π β¨ π) β¨ π)) β ((π β π β§ Β¬ π(leβπΎ)(π β¨ π)) β§ βπ β π΄ Β¬ π (leβπΎ)((π β¨ π) β¨ π))) |
9 | 8 | simplbi 499 |
. . . . 5
β’
(βπ β
π΄ (π β π β§ Β¬ π(leβπΎ)(π β¨ π) β§ Β¬ π (leβπΎ)((π β¨ π) β¨ π)) β (π β π β§ Β¬ π(leβπΎ)(π β¨ π))) |
10 | | simplll 774 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β πΎ β HL) |
11 | | hlatl 37851 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β AtLat) |
12 | 10, 11 | syl 17 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β πΎ β AtLat) |
13 | | simplr 768 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β π β π΄) |
14 | | simpllr 775 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β π β π΄) |
15 | 2, 3 | atncmp 37803 |
. . . . . . . . 9
β’ ((πΎ β AtLat β§ π β π΄ β§ π β π΄) β (Β¬ π(leβπΎ)π β π β π)) |
16 | 12, 13, 14, 15 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β (Β¬ π(leβπΎ)π β π β π)) |
17 | | necom 2998 |
. . . . . . . 8
β’ (π β π β π β π) |
18 | 16, 17 | bitr2di 288 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β (π β π β Β¬ π(leβπΎ)π)) |
19 | | eqid 2737 |
. . . . . . . . . 10
β’
(BaseβπΎ) =
(BaseβπΎ) |
20 | 19, 3 | atbase 37780 |
. . . . . . . . 9
β’ (π β π΄ β π β (BaseβπΎ)) |
21 | 14, 20 | syl 17 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β π β (BaseβπΎ)) |
22 | | 2dim.c |
. . . . . . . . 9
β’ πΆ = ( β βπΎ) |
23 | 19, 2, 1, 22, 3 | cvr1 37902 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β (BaseβπΎ) β§ π β π΄) β (Β¬ π(leβπΎ)π β ππΆ(π β¨ π))) |
24 | 10, 21, 13, 23 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β (Β¬ π(leβπΎ)π β ππΆ(π β¨ π))) |
25 | 18, 24 | bitrd 279 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β (π β π β ππΆ(π β¨ π))) |
26 | 19, 1, 3 | hlatjcl 37858 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
27 | 10, 14, 13, 26 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
28 | | simpr 486 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β π β π΄) |
29 | 19, 2, 1, 22, 3 | cvr1 37902 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β¨ π) β (BaseβπΎ) β§ π β π΄) β (Β¬ π(leβπΎ)(π β¨ π) β (π β¨ π)πΆ((π β¨ π) β¨ π))) |
30 | 10, 27, 28, 29 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β (Β¬ π(leβπΎ)(π β¨ π) β (π β¨ π)πΆ((π β¨ π) β¨ π))) |
31 | 25, 30 | anbi12d 632 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β ((π β π β§ Β¬ π(leβπΎ)(π β¨ π)) β (ππΆ(π β¨ π) β§ (π β¨ π)πΆ((π β¨ π) β¨ π)))) |
32 | 9, 31 | imbitrid 243 |
. . . 4
β’ ((((πΎ β HL β§ π β π΄) β§ π β π΄) β§ π β π΄) β (βπ β π΄ (π β π β§ Β¬ π(leβπΎ)(π β¨ π) β§ Β¬ π (leβπΎ)((π β¨ π) β¨ π)) β (ππΆ(π β¨ π) β§ (π β¨ π)πΆ((π β¨ π) β¨ π)))) |
33 | 32 | reximdva 3166 |
. . 3
β’ (((πΎ β HL β§ π β π΄) β§ π β π΄) β (βπ β π΄ βπ β π΄ (π β π β§ Β¬ π(leβπΎ)(π β¨ π) β§ Β¬ π (leβπΎ)((π β¨ π) β¨ π)) β βπ β π΄ (ππΆ(π β¨ π) β§ (π β¨ π)πΆ((π β¨ π) β¨ π)))) |
34 | 33 | reximdva 3166 |
. 2
β’ ((πΎ β HL β§ π β π΄) β (βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π(leβπΎ)(π β¨ π) β§ Β¬ π (leβπΎ)((π β¨ π) β¨ π)) β βπ β π΄ βπ β π΄ (ππΆ(π β¨ π) β§ (π β¨ π)πΆ((π β¨ π) β¨ π)))) |
35 | 4, 34 | mpd 15 |
1
β’ ((πΎ β HL β§ π β π΄) β βπ β π΄ βπ β π΄ (ππΆ(π β¨ π) β§ (π β¨ π)πΆ((π β¨ π) β¨ π))) |