Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. . . 4
β’
(leβπΎ) =
(leβπΎ) |
2 | | eqid 2737 |
. . . 4
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
3 | | trlcnv.h |
. . . 4
β’ π» = (LHypβπΎ) |
4 | 1, 2, 3 | lhpexnle 38472 |
. . 3
β’ ((πΎ β HL β§ π β π») β βπ β (AtomsβπΎ) Β¬ π(leβπΎ)π) |
5 | 4 | adantr 482 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β βπ β (AtomsβπΎ) Β¬ π(leβπΎ)π) |
6 | | eqid 2737 |
. . . . . . . . . 10
β’
(BaseβπΎ) =
(BaseβπΎ) |
7 | | trlcnv.t |
. . . . . . . . . 10
β’ π = ((LTrnβπΎ)βπ) |
8 | 6, 3, 7 | ltrn1o 38590 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
9 | 8 | 3adant3 1133 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ)) |
10 | | simp3l 1202 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β π β (AtomsβπΎ)) |
11 | 6, 2 | atbase 37754 |
. . . . . . . . 9
β’ (π β (AtomsβπΎ) β π β (BaseβπΎ)) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β π β (BaseβπΎ)) |
13 | | f1ocnvfv1 7223 |
. . . . . . . 8
β’ ((πΉ:(BaseβπΎ)β1-1-ontoβ(BaseβπΎ) β§ π β (BaseβπΎ)) β (β‘πΉβ(πΉβπ)) = π) |
14 | 9, 12, 13 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (β‘πΉβ(πΉβπ)) = π) |
15 | 14 | oveq2d 7374 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β ((πΉβπ)(joinβπΎ)(β‘πΉβ(πΉβπ))) = ((πΉβπ)(joinβπΎ)π)) |
16 | | simp1l 1198 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β πΎ β HL) |
17 | 1, 2, 3, 7 | ltrnat 38606 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β (AtomsβπΎ)) β (πΉβπ) β (AtomsβπΎ)) |
18 | 17 | 3adant3r 1182 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (πΉβπ) β (AtomsβπΎ)) |
19 | | eqid 2737 |
. . . . . . . 8
β’
(joinβπΎ) =
(joinβπΎ) |
20 | 19, 2 | hlatjcom 37833 |
. . . . . . 7
β’ ((πΎ β HL β§ (πΉβπ) β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β ((πΉβπ)(joinβπΎ)π) = (π(joinβπΎ)(πΉβπ))) |
21 | 16, 18, 10, 20 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β ((πΉβπ)(joinβπΎ)π) = (π(joinβπΎ)(πΉβπ))) |
22 | 15, 21 | eqtrd 2777 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β ((πΉβπ)(joinβπΎ)(β‘πΉβ(πΉβπ))) = (π(joinβπΎ)(πΉβπ))) |
23 | 22 | oveq1d 7373 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (((πΉβπ)(joinβπΎ)(β‘πΉβ(πΉβπ)))(meetβπΎ)π) = ((π(joinβπΎ)(πΉβπ))(meetβπΎ)π)) |
24 | | simp1 1137 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (πΎ β HL β§ π β π»)) |
25 | 3, 7 | ltrncnv 38612 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β β‘πΉ β π) |
26 | 25 | 3adant3 1133 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β β‘πΉ β π) |
27 | 1, 2, 3, 7 | ltrnel 38605 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β ((πΉβπ) β (AtomsβπΎ) β§ Β¬ (πΉβπ)(leβπΎ)π)) |
28 | | eqid 2737 |
. . . . . 6
β’
(meetβπΎ) =
(meetβπΎ) |
29 | | trlcnv.r |
. . . . . 6
β’ π
= ((trLβπΎ)βπ) |
30 | 1, 19, 28, 2, 3, 7,
29 | trlval2 38629 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ β‘πΉ β π β§ ((πΉβπ) β (AtomsβπΎ) β§ Β¬ (πΉβπ)(leβπΎ)π)) β (π
ββ‘πΉ) = (((πΉβπ)(joinβπΎ)(β‘πΉβ(πΉβπ)))(meetβπΎ)π)) |
31 | 24, 26, 27, 30 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (π
ββ‘πΉ) = (((πΉβπ)(joinβπΎ)(β‘πΉβ(πΉβπ)))(meetβπΎ)π)) |
32 | 1, 19, 28, 2, 3, 7,
29 | trlval2 38629 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (π
βπΉ) = ((π(joinβπΎ)(πΉβπ))(meetβπΎ)π)) |
33 | 23, 31, 32 | 3eqtr4d 2787 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (π
ββ‘πΉ) = (π
βπΉ)) |
34 | 33 | 3expa 1119 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β (AtomsβπΎ) β§ Β¬ π(leβπΎ)π)) β (π
ββ‘πΉ) = (π
βπΉ)) |
35 | 5, 34 | rexlimddv 3159 |
1
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
ββ‘πΉ) = (π
βπΉ)) |