Step | Hyp | Ref
| Expression |
1 | | hllat 38233 |
. . 3
β’ (πΎ β HL β πΎ β Lat) |
2 | 1 | anim1i 616 |
. 2
β’ ((πΎ β HL β§ π β π») β (πΎ β Lat β§ π β π»)) |
3 | | eqid 2733 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
4 | | trlval2.l |
. . . . 5
β’ β€ =
(leβπΎ) |
5 | | trlval2.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
6 | | trlval2.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
7 | | trlval2.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
8 | | trlval2.h |
. . . . 5
β’ π» = (LHypβπΎ) |
9 | | trlval2.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
10 | | trlval2.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
11 | 3, 4, 5, 6, 7, 8, 9, 10 | trlval 39033 |
. . . 4
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π) β (π
βπΉ) = (β©π₯ β (BaseβπΎ)βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)))) |
12 | 11 | 3adant3 1133 |
. . 3
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΉ) = (β©π₯ β (BaseβπΎ)βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)))) |
13 | | simp1l 1198 |
. . . . 5
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β Lat) |
14 | | simp3l 1202 |
. . . . . . 7
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β π β π΄) |
15 | 3, 7 | atbase 38159 |
. . . . . . 7
β’ (π β π΄ β π β (BaseβπΎ)) |
16 | 14, 15 | syl 17 |
. . . . . 6
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β π β (BaseβπΎ)) |
17 | 3, 8, 9 | ltrncl 38996 |
. . . . . . 7
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ π β (BaseβπΎ)) β (πΉβπ) β (BaseβπΎ)) |
18 | 16, 17 | syld3an3 1410 |
. . . . . 6
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) β (BaseβπΎ)) |
19 | 3, 5 | latjcl 18392 |
. . . . . 6
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (πΉβπ) β (BaseβπΎ)) β (π β¨ (πΉβπ)) β (BaseβπΎ)) |
20 | 13, 16, 18, 19 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (πΉβπ)) β (BaseβπΎ)) |
21 | | simp1r 1199 |
. . . . . 6
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β π β π») |
22 | 3, 8 | lhpbase 38869 |
. . . . . 6
β’ (π β π» β π β (BaseβπΎ)) |
23 | 21, 22 | syl 17 |
. . . . 5
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β π β (BaseβπΎ)) |
24 | 3, 6 | latmcl 18393 |
. . . . 5
β’ ((πΎ β Lat β§ (π β¨ (πΉβπ)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ (πΉβπ)) β§ π) β (BaseβπΎ)) |
25 | 13, 20, 23, 24 | syl3anc 1372 |
. . . 4
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ (πΉβπ)) β§ π) β (BaseβπΎ)) |
26 | | simpl3l 1229 |
. . . . . 6
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π₯ β (BaseβπΎ)) β π β π΄) |
27 | | simpl3r 1230 |
. . . . . 6
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π₯ β (BaseβπΎ)) β Β¬ π β€ π) |
28 | | breq1 5152 |
. . . . . . . . . 10
β’ (π = π β (π β€ π β π β€ π)) |
29 | 28 | notbid 318 |
. . . . . . . . 9
β’ (π = π β (Β¬ π β€ π β Β¬ π β€ π)) |
30 | | id 22 |
. . . . . . . . . . . 12
β’ (π = π β π = π) |
31 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π = π β (πΉβπ) = (πΉβπ)) |
32 | 30, 31 | oveq12d 7427 |
. . . . . . . . . . 11
β’ (π = π β (π β¨ (πΉβπ)) = (π β¨ (πΉβπ))) |
33 | 32 | oveq1d 7424 |
. . . . . . . . . 10
β’ (π = π β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)) |
34 | 33 | eqeq2d 2744 |
. . . . . . . . 9
β’ (π = π β (π₯ = ((π β¨ (πΉβπ)) β§ π) β π₯ = ((π β¨ (πΉβπ)) β§ π))) |
35 | 29, 34 | imbi12d 345 |
. . . . . . . 8
β’ (π = π β ((Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)) β (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)))) |
36 | 35 | rspcv 3609 |
. . . . . . 7
β’ (π β π΄ β (βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)) β (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)))) |
37 | 36 | com23 86 |
. . . . . 6
β’ (π β π΄ β (Β¬ π β€ π β (βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)) β π₯ = ((π β¨ (πΉβπ)) β§ π)))) |
38 | 26, 27, 37 | sylc 65 |
. . . . 5
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π₯ β (BaseβπΎ)) β (βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)) β π₯ = ((π β¨ (πΉβπ)) β§ π))) |
39 | | simp11 1204 |
. . . . . . . . . . 11
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ π β§ π β π΄) β (πΎ β Lat β§ π β π»)) |
40 | | simp12 1205 |
. . . . . . . . . . 11
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ π β§ π β π΄) β πΉ β π) |
41 | | simp13l 1289 |
. . . . . . . . . . 11
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ π β§ π β π΄) β π β π΄) |
42 | | simp13r 1290 |
. . . . . . . . . . 11
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ π β§ π β π΄) β Β¬ π β€ π) |
43 | | simp3 1139 |
. . . . . . . . . . 11
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ π β§ π β π΄) β π β π΄) |
44 | | simp2 1138 |
. . . . . . . . . . 11
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ π β§ π β π΄) β Β¬ π β€ π) |
45 | 4, 5, 6, 7, 8, 9 | ltrnu 38992 |
. . . . . . . . . . 11
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)) |
46 | 39, 40, 41, 42, 43, 44, 45 | syl222anc 1387 |
. . . . . . . . . 10
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ π β§ π β π΄) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)) |
47 | | eqeq2 2745 |
. . . . . . . . . . 11
β’ (((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π) β (π₯ = ((π β¨ (πΉβπ)) β§ π) β π₯ = ((π β¨ (πΉβπ)) β§ π))) |
48 | 47 | biimpd 228 |
. . . . . . . . . 10
β’ (((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π) β (π₯ = ((π β¨ (πΉβπ)) β§ π) β π₯ = ((π β¨ (πΉβπ)) β§ π))) |
49 | 46, 48 | syl 17 |
. . . . . . . . 9
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ π β§ π β π΄) β (π₯ = ((π β¨ (πΉβπ)) β§ π) β π₯ = ((π β¨ (πΉβπ)) β§ π))) |
50 | 49 | 3exp 1120 |
. . . . . . . 8
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (Β¬ π β€ π β (π β π΄ β (π₯ = ((π β¨ (πΉβπ)) β§ π) β π₯ = ((π β¨ (πΉβπ)) β§ π))))) |
51 | 50 | com24 95 |
. . . . . . 7
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π₯ = ((π β¨ (πΉβπ)) β§ π) β (π β π΄ β (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π))))) |
52 | 51 | ralrimdv 3153 |
. . . . . 6
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π₯ = ((π β¨ (πΉβπ)) β§ π) β βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)))) |
53 | 52 | adantr 482 |
. . . . 5
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π₯ β (BaseβπΎ)) β (π₯ = ((π β¨ (πΉβπ)) β§ π) β βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)))) |
54 | 38, 53 | impbid 211 |
. . . 4
β’ ((((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π₯ β (BaseβπΎ)) β (βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)) β π₯ = ((π β¨ (πΉβπ)) β§ π))) |
55 | 25, 54 | riota5 7395 |
. . 3
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (β©π₯ β (BaseβπΎ)βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π))) = ((π β¨ (πΉβπ)) β§ π)) |
56 | 12, 55 | eqtrd 2773 |
. 2
β’ (((πΎ β Lat β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΉ) = ((π β¨ (πΉβπ)) β§ π)) |
57 | 2, 56 | syl3an1 1164 |
1
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΉ) = ((π β¨ (πΉβπ)) β§ π)) |