Step | Hyp | Ref
| Expression |
1 | | ltrncnv.h |
. . . 4
β’ π» = (LHypβπΎ) |
2 | | eqid 2733 |
. . . 4
β’
((LDilβπΎ)βπ) = ((LDilβπΎ)βπ) |
3 | | ltrncnv.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
4 | 1, 2, 3 | ltrnldil 38635 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ β ((LDilβπΎ)βπ)) |
5 | 1, 2 | ldilcnv 38628 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β ((LDilβπΎ)βπ)) β β‘πΉ β ((LDilβπΎ)βπ)) |
6 | 4, 5 | syldan 592 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β β‘πΉ β ((LDilβπΎ)βπ)) |
7 | | simp1 1137 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((πΎ β HL β§ π β π») β§ πΉ β π)) |
8 | | simp1l 1198 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (πΎ β HL β§ π β π»)) |
9 | | simp1r 1199 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β πΉ β π) |
10 | | simp2l 1200 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β π β (AtomsβπΎ)) |
11 | | simp3l 1202 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β Β¬ π(leβπΎ)π) |
12 | | eqid 2733 |
. . . . . . . 8
β’
(leβπΎ) =
(leβπΎ) |
13 | | eqid 2733 |
. . . . . . . 8
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
14 | 12, 13, 1, 3 | ltrncnvel 38655 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β ((β‘πΉβπ) β (AtomsβπΎ) β§ Β¬ (β‘πΉβπ)(leβπΎ)π)) |
15 | 8, 9, 10, 11, 14 | syl112anc 1375 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((β‘πΉβπ) β (AtomsβπΎ) β§ Β¬ (β‘πΉβπ)(leβπΎ)π)) |
16 | | simp2r 1201 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β π β (AtomsβπΎ)) |
17 | | simp3r 1203 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β Β¬ π(leβπΎ)π) |
18 | 12, 13, 1, 3 | ltrncnvel 38655 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β ((β‘πΉβπ) β (AtomsβπΎ) β§ Β¬ (β‘πΉβπ)(leβπΎ)π)) |
19 | 8, 9, 16, 17, 18 | syl112anc 1375 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((β‘πΉβπ) β (AtomsβπΎ) β§ Β¬ (β‘πΉβπ)(leβπΎ)π)) |
20 | | eqid 2733 |
. . . . . . 7
β’
(joinβπΎ) =
(joinβπΎ) |
21 | | eqid 2733 |
. . . . . . 7
β’
(meetβπΎ) =
(meetβπΎ) |
22 | 12, 20, 21, 13, 1, 3 | ltrnu 38634 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ ((β‘πΉβπ) β (AtomsβπΎ) β§ Β¬ (β‘πΉβπ)(leβπΎ)π) β§ ((β‘πΉβπ) β (AtomsβπΎ) β§ Β¬ (β‘πΉβπ)(leβπΎ)π)) β (((β‘πΉβπ)(joinβπΎ)(πΉβ(β‘πΉβπ)))(meetβπΎ)π) = (((β‘πΉβπ)(joinβπΎ)(πΉβ(β‘πΉβπ)))(meetβπΎ)π)) |
23 | 7, 15, 19, 22 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (((β‘πΉβπ)(joinβπΎ)(πΉβ(β‘πΉβπ)))(meetβπΎ)π) = (((β‘πΉβπ)(joinβπΎ)(πΉβ(β‘πΉβπ)))(meetβπΎ)π)) |
24 | | eqid 2733 |
. . . . . . . . . . 11
β’
(BaseβπΎ) =
(BaseβπΎ) |
25 | 24, 1, 3 | ltrn1o 38637 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
26 | 25 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
27 | 24, 13 | atbase 37801 |
. . . . . . . . . 10
β’ (π β (AtomsβπΎ) β π β (BaseβπΎ)) |
28 | 10, 27 | syl 17 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β π β (BaseβπΎ)) |
29 | | f1ocnvfv2 7227 |
. . . . . . . . 9
β’ ((πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ) β§ π β (BaseβπΎ)) β (πΉβ(β‘πΉβπ)) = π) |
30 | 26, 28, 29 | syl2anc 585 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (πΉβ(β‘πΉβπ)) = π) |
31 | 30 | oveq2d 7377 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((β‘πΉβπ)(joinβπΎ)(πΉβ(β‘πΉβπ))) = ((β‘πΉβπ)(joinβπΎ)π)) |
32 | | simp1ll 1237 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β πΎ β HL) |
33 | 12, 13, 1, 3 | ltrncnvat 38654 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β (AtomsβπΎ)) β (β‘πΉβπ) β (AtomsβπΎ)) |
34 | 8, 9, 10, 33 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (β‘πΉβπ) β (AtomsβπΎ)) |
35 | 20, 13 | hlatjcom 37880 |
. . . . . . . 8
β’ ((πΎ β HL β§ (β‘πΉβπ) β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β ((β‘πΉβπ)(joinβπΎ)π) = (π(joinβπΎ)(β‘πΉβπ))) |
36 | 32, 34, 10, 35 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((β‘πΉβπ)(joinβπΎ)π) = (π(joinβπΎ)(β‘πΉβπ))) |
37 | 31, 36 | eqtrd 2773 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((β‘πΉβπ)(joinβπΎ)(πΉβ(β‘πΉβπ))) = (π(joinβπΎ)(β‘πΉβπ))) |
38 | 37 | oveq1d 7376 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (((β‘πΉβπ)(joinβπΎ)(πΉβ(β‘πΉβπ)))(meetβπΎ)π) = ((π(joinβπΎ)(β‘πΉβπ))(meetβπΎ)π)) |
39 | 24, 13 | atbase 37801 |
. . . . . . . . . 10
β’ (π β (AtomsβπΎ) β π β (BaseβπΎ)) |
40 | 16, 39 | syl 17 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β π β (BaseβπΎ)) |
41 | | f1ocnvfv2 7227 |
. . . . . . . . 9
β’ ((πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ) β§ π β (BaseβπΎ)) β (πΉβ(β‘πΉβπ)) = π) |
42 | 26, 40, 41 | syl2anc 585 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (πΉβ(β‘πΉβπ)) = π) |
43 | 42 | oveq2d 7377 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((β‘πΉβπ)(joinβπΎ)(πΉβ(β‘πΉβπ))) = ((β‘πΉβπ)(joinβπΎ)π)) |
44 | 12, 13, 1, 3 | ltrncnvat 38654 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β (AtomsβπΎ)) β (β‘πΉβπ) β (AtomsβπΎ)) |
45 | 8, 9, 16, 44 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (β‘πΉβπ) β (AtomsβπΎ)) |
46 | 20, 13 | hlatjcom 37880 |
. . . . . . . 8
β’ ((πΎ β HL β§ (β‘πΉβπ) β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β ((β‘πΉβπ)(joinβπΎ)π) = (π(joinβπΎ)(β‘πΉβπ))) |
47 | 32, 45, 16, 46 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((β‘πΉβπ)(joinβπΎ)π) = (π(joinβπΎ)(β‘πΉβπ))) |
48 | 43, 47 | eqtrd 2773 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((β‘πΉβπ)(joinβπΎ)(πΉβ(β‘πΉβπ))) = (π(joinβπΎ)(β‘πΉβπ))) |
49 | 48 | oveq1d 7376 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β (((β‘πΉβπ)(joinβπΎ)(πΉβ(β‘πΉβπ)))(meetβπΎ)π) = ((π(joinβπΎ)(β‘πΉβπ))(meetβπΎ)π)) |
50 | 23, 38, 49 | 3eqtr3d 2781 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β§ (Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π)) β ((π(joinβπΎ)(β‘πΉβπ))(meetβπΎ)π) = ((π(joinβπΎ)(β‘πΉβπ))(meetβπΎ)π)) |
51 | 50 | 3exp 1120 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β ((π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β ((Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π) β ((π(joinβπΎ)(β‘πΉβπ))(meetβπΎ)π) = ((π(joinβπΎ)(β‘πΉβπ))(meetβπΎ)π)))) |
52 | 51 | ralrimivv 3192 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)((Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π) β ((π(joinβπΎ)(β‘πΉβπ))(meetβπΎ)π) = ((π(joinβπΎ)(β‘πΉβπ))(meetβπΎ)π))) |
53 | 12, 20, 21, 13, 1, 2, 3 | isltrn 38632 |
. . 3
β’ ((πΎ β HL β§ π β π») β (β‘πΉ β π β (β‘πΉ β ((LDilβπΎ)βπ) β§ βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)((Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π) β ((π(joinβπΎ)(β‘πΉβπ))(meetβπΎ)π) = ((π(joinβπΎ)(β‘πΉβπ))(meetβπΎ)π))))) |
54 | 53 | adantr 482 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (β‘πΉ β π β (β‘πΉ β ((LDilβπΎ)βπ) β§ βπ β (AtomsβπΎ)βπ β (AtomsβπΎ)((Β¬ π(leβπΎ)π β§ Β¬ π(leβπΎ)π) β ((π(joinβπΎ)(β‘πΉβπ))(meetβπΎ)π) = ((π(joinβπΎ)(β‘πΉβπ))(meetβπΎ)π))))) |
55 | 6, 52, 54 | mpbir2and 712 |
1
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β β‘πΉ β π) |