Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΎ β HL β§ π β π»)) |
2 | | simp2r 1201 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΊ β π) |
3 | | simp2l 1200 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) |
4 | | trlcoabs.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
5 | | trlcoabs.t |
. . . . . . 7
β’ π = ((LTrnβπΎ)βπ) |
6 | 4, 5 | ltrncnv 38638 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β β‘πΉ β π) |
7 | 1, 3, 6 | syl2anc 585 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β β‘πΉ β π) |
8 | 4, 5 | ltrnco 39211 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ β‘πΉ β π) β (πΊ β β‘πΉ) β π) |
9 | 1, 2, 7, 8 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊ β β‘πΉ) β π) |
10 | | trlcoabs.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
11 | | trlcoabs.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
12 | 10, 11, 4, 5 | ltrnel 38631 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) |
13 | 12 | 3adant2r 1180 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) |
14 | | trlcoabs.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
15 | | eqid 2737 |
. . . . 5
β’
(meetβπΎ) =
(meetβπΎ) |
16 | | trlcoabs.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
17 | 10, 14, 15, 11, 4, 5, 16 | trlval2 38655 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΊ β β‘πΉ) β π β§ ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) β (π
β(πΊ β β‘πΉ)) = (((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ)))(meetβπΎ)π)) |
18 | 1, 9, 13, 17 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π
β(πΊ β β‘πΉ)) = (((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ)))(meetβπΎ)π)) |
19 | 18 | oveq2d 7378 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β¨ (π
β(πΊ β β‘πΉ))) = ((πΉβπ) β¨ (((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ)))(meetβπΎ)π))) |
20 | | simp1l 1198 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β HL) |
21 | | simp3l 1202 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π΄) |
22 | 10, 11, 4, 5 | ltrnat 38632 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π΄) β (πΉβπ) β π΄) |
23 | 1, 3, 21, 22 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) β π΄) |
24 | 10, 11, 4, 5 | ltrnat 38632 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΊ β β‘πΉ) β π β§ (πΉβπ) β π΄) β ((πΊ β β‘πΉ)β(πΉβπ)) β π΄) |
25 | 1, 9, 23, 24 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊ β β‘πΉ)β(πΉβπ)) β π΄) |
26 | | eqid 2737 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
27 | 26, 14, 11 | hlatjcl 37858 |
. . . 4
β’ ((πΎ β HL β§ (πΉβπ) β π΄ β§ ((πΊ β β‘πΉ)β(πΉβπ)) β π΄) β ((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ))) β (BaseβπΎ)) |
28 | 20, 23, 25, 27 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ))) β (BaseβπΎ)) |
29 | | simp1r 1199 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π») |
30 | 26, 4 | lhpbase 38490 |
. . . 4
β’ (π β π» β π β (BaseβπΎ)) |
31 | 29, 30 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β (BaseβπΎ)) |
32 | 10, 14, 11 | hlatlej1 37866 |
. . . 4
β’ ((πΎ β HL β§ (πΉβπ) β π΄ β§ ((πΊ β β‘πΉ)β(πΉβπ)) β π΄) β (πΉβπ) β€ ((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ)))) |
33 | 20, 23, 25, 32 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) β€ ((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ)))) |
34 | 26, 10, 14, 15, 11 | atmod3i1 38356 |
. . 3
β’ ((πΎ β HL β§ ((πΉβπ) β π΄ β§ ((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ))) β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ (πΉβπ) β€ ((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ)))) β ((πΉβπ) β¨ (((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ)))(meetβπΎ)π)) = (((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ)))(meetβπΎ)((πΉβπ) β¨ π))) |
35 | 20, 23, 28, 31, 33, 34 | syl131anc 1384 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β¨ (((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ)))(meetβπΎ)π)) = (((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ)))(meetβπΎ)((πΉβπ) β¨ π))) |
36 | 10, 11, 4, 5 | ltrncoval 38637 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ((πΊ β β‘πΉ) β π β§ πΉ β π) β§ π β π΄) β (((πΊ β β‘πΉ) β πΉ)βπ) = ((πΊ β β‘πΉ)β(πΉβπ))) |
37 | 1, 9, 3, 21, 36 | syl121anc 1376 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΊ β β‘πΉ) β πΉ)βπ) = ((πΊ β β‘πΉ)β(πΉβπ))) |
38 | | coass 6222 |
. . . . . . . 8
β’ ((πΊ β β‘πΉ) β πΉ) = (πΊ β (β‘πΉ β πΉ)) |
39 | 26, 4, 5 | ltrn1o 38616 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
40 | 1, 3, 39 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
41 | | f1ococnv1 6818 |
. . . . . . . . . . 11
β’ (πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ) β (β‘πΉ β πΉ) = ( I βΎ (BaseβπΎ))) |
42 | 40, 41 | syl 17 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (β‘πΉ β πΉ) = ( I βΎ (BaseβπΎ))) |
43 | 42 | coeq2d 5823 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊ β (β‘πΉ β πΉ)) = (πΊ β ( I βΎ (BaseβπΎ)))) |
44 | 26, 4, 5 | ltrn1o 38616 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β πΊ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
45 | 1, 2, 44 | syl2anc 585 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΊ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
46 | | f1of 6789 |
. . . . . . . . . 10
β’ (πΊ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ) β πΊ:(BaseβπΎ)βΆ(BaseβπΎ)) |
47 | | fcoi1 6721 |
. . . . . . . . . 10
β’ (πΊ:(BaseβπΎ)βΆ(BaseβπΎ) β (πΊ β ( I βΎ (BaseβπΎ))) = πΊ) |
48 | 45, 46, 47 | 3syl 18 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊ β ( I βΎ (BaseβπΎ))) = πΊ) |
49 | 43, 48 | eqtrd 2777 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊ β (β‘πΉ β πΉ)) = πΊ) |
50 | 38, 49 | eqtrid 2789 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊ β β‘πΉ) β πΉ) = πΊ) |
51 | 50 | fveq1d 6849 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΊ β β‘πΉ) β πΉ)βπ) = (πΊβπ)) |
52 | 37, 51 | eqtr3d 2779 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊ β β‘πΉ)β(πΉβπ)) = (πΊβπ)) |
53 | 52 | oveq2d 7378 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ))) = ((πΉβπ) β¨ (πΊβπ))) |
54 | | eqid 2737 |
. . . . . 6
β’
(1.βπΎ) =
(1.βπΎ) |
55 | 10, 14, 54, 11, 4 | lhpjat2 38513 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) β ((πΉβπ) β¨ π) = (1.βπΎ)) |
56 | 1, 13, 55 | syl2anc 585 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β¨ π) = (1.βπΎ)) |
57 | 53, 56 | oveq12d 7380 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ)))(meetβπΎ)((πΉβπ) β¨ π)) = (((πΉβπ) β¨ (πΊβπ))(meetβπΎ)(1.βπΎ))) |
58 | | hlol 37852 |
. . . . 5
β’ (πΎ β HL β πΎ β OL) |
59 | 20, 58 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΎ β OL) |
60 | 10, 11, 4, 5 | ltrnat 38632 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ π β π΄) β (πΊβπ) β π΄) |
61 | 1, 2, 21, 60 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΊβπ) β π΄) |
62 | 26, 14, 11 | hlatjcl 37858 |
. . . . 5
β’ ((πΎ β HL β§ (πΉβπ) β π΄ β§ (πΊβπ) β π΄) β ((πΉβπ) β¨ (πΊβπ)) β (BaseβπΎ)) |
63 | 20, 23, 61, 62 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β¨ (πΊβπ)) β (BaseβπΎ)) |
64 | 26, 15, 54 | olm11 37718 |
. . . 4
β’ ((πΎ β OL β§ ((πΉβπ) β¨ (πΊβπ)) β (BaseβπΎ)) β (((πΉβπ) β¨ (πΊβπ))(meetβπΎ)(1.βπΎ)) = ((πΉβπ) β¨ (πΊβπ))) |
65 | 59, 63, 64 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΉβπ) β¨ (πΊβπ))(meetβπΎ)(1.βπΎ)) = ((πΉβπ) β¨ (πΊβπ))) |
66 | 57, 65 | eqtrd 2777 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΉβπ) β¨ ((πΊ β β‘πΉ)β(πΉβπ)))(meetβπΎ)((πΉβπ) β¨ π)) = ((πΉβπ) β¨ (πΊβπ))) |
67 | 19, 35, 66 | 3eqtrd 2781 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β¨ (π
β(πΊ β β‘πΉ))) = ((πΉβπ) β¨ (πΊβπ))) |