Step | Hyp | Ref
| Expression |
1 | | simp11 1204 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β πΎ β HL) |
2 | 1 | hllatd 37872 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β πΎ β Lat) |
3 | | simp12 1205 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β π β π΅) |
4 | | simp13 1206 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β π β π΅) |
5 | | pl42lem.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
6 | | pl42lem.j |
. . . . . . . 8
β’ β¨ =
(joinβπΎ) |
7 | 5, 6 | latjcl 18333 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
8 | 2, 3, 4, 7 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β (π β¨ π) β π΅) |
9 | | simp21 1207 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β π β π΅) |
10 | | pl42lem.m |
. . . . . . 7
β’ β§ =
(meetβπΎ) |
11 | 5, 10 | latmcl 18334 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β¨ π) β π΅ β§ π β π΅) β ((π β¨ π) β§ π) β π΅) |
12 | 2, 8, 9, 11 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β ((π β¨ π) β§ π) β π΅) |
13 | | simp22 1208 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β π β π΅) |
14 | 5, 6 | latjcl 18333 |
. . . . 5
β’ ((πΎ β Lat β§ ((π β¨ π) β§ π) β π΅ β§ π β π΅) β (((π β¨ π) β§ π) β¨ π) β π΅) |
15 | 2, 12, 13, 14 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β (((π β¨ π) β§ π) β¨ π) β π΅) |
16 | | simp23 1209 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β π β π΅) |
17 | | eqid 2733 |
. . . . 5
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
18 | | pl42lem.f |
. . . . 5
β’ πΉ = (pmapβπΎ) |
19 | 5, 10, 17, 18 | pmapmeet 38282 |
. . . 4
β’ ((πΎ β HL β§ (((π β¨ π) β§ π) β¨ π) β π΅ β§ π β π΅) β (πΉβ((((π β¨ π) β§ π) β¨ π) β§ π)) = ((πΉβ(((π β¨ π) β§ π) β¨ π)) β© (πΉβπ))) |
20 | 1, 15, 16, 19 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β (πΉβ((((π β¨ π) β§ π) β¨ π) β§ π)) = ((πΉβ(((π β¨ π) β§ π) β¨ π)) β© (πΉβπ))) |
21 | | pl42lem.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
22 | | hlop 37870 |
. . . . . . . . 9
β’ (πΎ β HL β πΎ β OP) |
23 | 1, 22 | syl 17 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β πΎ β OP) |
24 | | pl42lem.o |
. . . . . . . . 9
β’ β₯ =
(ocβπΎ) |
25 | 5, 24 | opoccl 37702 |
. . . . . . . 8
β’ ((πΎ β OP β§ π β π΅) β ( β₯ βπ) β π΅) |
26 | 23, 13, 25 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β ( β₯ βπ) β π΅) |
27 | 5, 21, 10 | latmle2 18359 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β¨ π) β π΅ β§ π β π΅) β ((π β¨ π) β§ π) β€ π) |
28 | 2, 8, 9, 27 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β ((π β¨ π) β§ π) β€ π) |
29 | | simp3r 1203 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β π β€ ( β₯ βπ)) |
30 | 5, 21, 2, 12, 9, 26, 28, 29 | lattrd 18340 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β ((π β¨ π) β§ π) β€ ( β₯ βπ)) |
31 | | pl42lem.p |
. . . . . . 7
β’ + =
(+πβπΎ) |
32 | 5, 21, 6, 18, 24, 31 | pmapojoinN 38477 |
. . . . . 6
β’ (((πΎ β HL β§ ((π β¨ π) β§ π) β π΅ β§ π β π΅) β§ ((π β¨ π) β§ π) β€ ( β₯ βπ)) β (πΉβ(((π β¨ π) β§ π) β¨ π)) = ((πΉβ((π β¨ π) β§ π)) + (πΉβπ))) |
33 | 1, 12, 13, 30, 32 | syl31anc 1374 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β (πΉβ(((π β¨ π) β§ π) β¨ π)) = ((πΉβ((π β¨ π) β§ π)) + (πΉβπ))) |
34 | 5, 10, 17, 18 | pmapmeet 38282 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β¨ π) β π΅ β§ π β π΅) β (πΉβ((π β¨ π) β§ π)) = ((πΉβ(π β¨ π)) β© (πΉβπ))) |
35 | 1, 8, 9, 34 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β (πΉβ((π β¨ π) β§ π)) = ((πΉβ(π β¨ π)) β© (πΉβπ))) |
36 | | simp3l 1202 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β π β€ ( β₯ βπ)) |
37 | 5, 21, 6, 18, 24, 31 | pmapojoinN 38477 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π β€ ( β₯ βπ)) β (πΉβ(π β¨ π)) = ((πΉβπ) + (πΉβπ))) |
38 | 1, 3, 4, 36, 37 | syl31anc 1374 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β (πΉβ(π β¨ π)) = ((πΉβπ) + (πΉβπ))) |
39 | 38 | ineq1d 4172 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β ((πΉβ(π β¨ π)) β© (πΉβπ)) = (((πΉβπ) + (πΉβπ)) β© (πΉβπ))) |
40 | 35, 39 | eqtrd 2773 |
. . . . . 6
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β (πΉβ((π β¨ π) β§ π)) = (((πΉβπ) + (πΉβπ)) β© (πΉβπ))) |
41 | 40 | oveq1d 7373 |
. . . . 5
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β ((πΉβ((π β¨ π) β§ π)) + (πΉβπ)) = ((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) + (πΉβπ))) |
42 | 33, 41 | eqtrd 2773 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β (πΉβ(((π β¨ π) β§ π) β¨ π)) = ((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) + (πΉβπ))) |
43 | 42 | ineq1d 4172 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β ((πΉβ(((π β¨ π) β§ π) β¨ π)) β© (πΉβπ)) = (((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) + (πΉβπ)) β© (πΉβπ))) |
44 | 20, 43 | eqtrd 2773 |
. 2
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ))) β (πΉβ((((π β¨ π) β§ π) β¨ π) β§ π)) = (((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) + (πΉβπ)) β© (πΉβπ))) |
45 | 44 | 3expia 1122 |
1
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ)) β (πΉβ((((π β¨ π) β§ π) β¨ π) β§ π)) = (((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) + (πΉβπ)) β© (πΉβπ)))) |