Step | Hyp | Ref
| Expression |
1 | | hllat 37828 |
. . . . . 6
β’ (πΎ β HL β πΎ β Lat) |
2 | 1 | ad2antrr 725 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β πΎ β Lat) |
3 | | hlop 37827 |
. . . . . . . . 9
β’ (πΎ β HL β πΎ β OP) |
4 | 3 | ad2antrr 725 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β πΎ β OP) |
5 | | eqid 2737 |
. . . . . . . . . 10
β’
(BaseβπΎ) =
(BaseβπΎ) |
6 | | djaj.h |
. . . . . . . . . 10
β’ π» = (LHypβπΎ) |
7 | | djaj.i |
. . . . . . . . . 10
β’ πΌ = ((DIsoAβπΎ)βπ) |
8 | 5, 6, 7 | diadmclN 39503 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β π β (BaseβπΎ)) |
9 | 8 | adantrr 716 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β π β (BaseβπΎ)) |
10 | | eqid 2737 |
. . . . . . . . 9
β’
(ocβπΎ) =
(ocβπΎ) |
11 | 5, 10 | opoccl 37659 |
. . . . . . . 8
β’ ((πΎ β OP β§ π β (BaseβπΎ)) β ((ocβπΎ)βπ) β (BaseβπΎ)) |
12 | 4, 9, 11 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((ocβπΎ)βπ) β (BaseβπΎ)) |
13 | 5, 6 | lhpbase 38464 |
. . . . . . . . 9
β’ (π β π» β π β (BaseβπΎ)) |
14 | 13 | ad2antlr 726 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β π β (BaseβπΎ)) |
15 | 5, 10 | opoccl 37659 |
. . . . . . . 8
β’ ((πΎ β OP β§ π β (BaseβπΎ)) β ((ocβπΎ)βπ) β (BaseβπΎ)) |
16 | 4, 14, 15 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((ocβπΎ)βπ) β (BaseβπΎ)) |
17 | | djaj.k |
. . . . . . . 8
β’ β¨ =
(joinβπΎ) |
18 | 5, 17 | latjcl 18329 |
. . . . . . 7
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β (BaseβπΎ) β§ ((ocβπΎ)βπ) β (BaseβπΎ)) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β (BaseβπΎ)) |
19 | 2, 12, 16, 18 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β (BaseβπΎ)) |
20 | | eqid 2737 |
. . . . . . 7
β’
(meetβπΎ) =
(meetβπΎ) |
21 | 5, 20 | latmcl 18330 |
. . . . . 6
β’ ((πΎ β Lat β§
(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ)) |
22 | 2, 19, 14, 21 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ)) |
23 | 5, 6, 7 | diadmclN 39503 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β π β (BaseβπΎ)) |
24 | 23 | adantrl 715 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β π β (BaseβπΎ)) |
25 | 5, 10 | opoccl 37659 |
. . . . . . . 8
β’ ((πΎ β OP β§ π β (BaseβπΎ)) β ((ocβπΎ)βπ) β (BaseβπΎ)) |
26 | 4, 24, 25 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((ocβπΎ)βπ) β (BaseβπΎ)) |
27 | 5, 17 | latjcl 18329 |
. . . . . . 7
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β (BaseβπΎ) β§ ((ocβπΎ)βπ) β (BaseβπΎ)) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β (BaseβπΎ)) |
28 | 2, 26, 16, 27 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β (BaseβπΎ)) |
29 | 5, 20 | latmcl 18330 |
. . . . . 6
β’ ((πΎ β Lat β§
(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ)) |
30 | 2, 28, 14, 29 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ)) |
31 | 5, 20 | latmcl 18330 |
. . . . 5
β’ ((πΎ β Lat β§
((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ) β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ)) β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) β (BaseβπΎ)) |
32 | 2, 22, 30, 31 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) β (BaseβπΎ)) |
33 | | eqid 2737 |
. . . . 5
β’
(leβπΎ) =
(leβπΎ) |
34 | 5, 33, 20 | latmle2 18355 |
. . . . . 6
β’ ((πΎ β Lat β§
((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ) β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ)) β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))(leβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) |
35 | 2, 22, 30, 34 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))(leβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) |
36 | 5, 33, 20 | latmle2 18355 |
. . . . . 6
β’ ((πΎ β Lat β§
(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(leβπΎ)π) |
37 | 2, 28, 14, 36 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(leβπΎ)π) |
38 | 5, 33, 2, 32, 30, 14, 35, 37 | lattrd 18336 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))(leβπΎ)π) |
39 | 5, 33, 6, 7 | diaeldm 39502 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β ((((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) β dom πΌ β ((((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) β (BaseβπΎ) β§ (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))(leβπΎ)π))) |
40 | 39 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) β dom πΌ β ((((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) β (BaseβπΎ) β§ (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))(leβπΎ)π))) |
41 | 32, 38, 40 | mpbir2and 712 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) β dom πΌ) |
42 | | eqid 2737 |
. . . 4
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
43 | | eqid 2737 |
. . . 4
β’
((ocAβπΎ)βπ) = ((ocAβπΎ)βπ) |
44 | 17, 20, 10, 6, 42, 7, 43 | diaocN 39591 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) β dom πΌ) β (πΌβ((((ocβπΎ)β(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) = (((ocAβπΎ)βπ)β(πΌβ(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))))) |
45 | 41, 44 | syldan 592 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβ((((ocβπΎ)β(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) = (((ocAβπΎ)βπ)β(πΌβ(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))))) |
46 | | hloml 37822 |
. . . . . 6
β’ (πΎ β HL β πΎ β OML) |
47 | 46 | ad2antrr 725 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β πΎ β OML) |
48 | 5, 17 | latjcl 18329 |
. . . . . 6
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π β¨ π) β (BaseβπΎ)) |
49 | 2, 9, 24, 48 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (π β¨ π) β (BaseβπΎ)) |
50 | 33, 6, 7 | diadmleN 39504 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β π(leβπΎ)π) |
51 | 50 | adantrr 716 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β π(leβπΎ)π) |
52 | 33, 6, 7 | diadmleN 39504 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β π(leβπΎ)π) |
53 | 52 | adantrl 715 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β π(leβπΎ)π) |
54 | 5, 33, 17 | latjle12 18340 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ π β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((π(leβπΎ)π β§ π(leβπΎ)π) β (π β¨ π)(leβπΎ)π)) |
55 | 2, 9, 24, 14, 54 | syl13anc 1373 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((π(leβπΎ)π β§ π(leβπΎ)π) β (π β¨ π)(leβπΎ)π)) |
56 | 51, 53, 55 | mpbi2and 711 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (π β¨ π)(leβπΎ)π) |
57 | 5, 33, 17, 20, 10 | omlspjN 37726 |
. . . . 5
β’ ((πΎ β OML β§ ((π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ (π β¨ π)(leβπΎ)π) β (((π β¨ π) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) = (π β¨ π)) |
58 | 47, 49, 14, 56, 57 | syl121anc 1376 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((π β¨ π) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) = (π β¨ π)) |
59 | 5, 17 | latjidm 18352 |
. . . . . . . 8
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β (BaseβπΎ)) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)) |
60 | 2, 16, 59 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) = ((ocβπΎ)βπ)) |
61 | 60 | oveq2d 7374 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((π β¨ π) β¨ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = ((π β¨ π) β¨ ((ocβπΎ)βπ))) |
62 | 5, 17 | latjass 18373 |
. . . . . . . 8
β’ ((πΎ β Lat β§ ((π β¨ π) β (BaseβπΎ) β§ ((ocβπΎ)βπ) β (BaseβπΎ) β§ ((ocβπΎ)βπ) β (BaseβπΎ))) β (((π β¨ π) β¨ ((ocβπΎ)βπ)) β¨ ((ocβπΎ)βπ)) = ((π β¨ π) β¨ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) |
63 | 2, 49, 16, 16, 62 | syl13anc 1373 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((π β¨ π) β¨ ((ocβπΎ)βπ)) β¨ ((ocβπΎ)βπ)) = ((π β¨ π) β¨ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) |
64 | | hlol 37826 |
. . . . . . . . . . 11
β’ (πΎ β HL β πΎ β OL) |
65 | 64 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β πΎ β OL) |
66 | 5, 17, 20, 10 | oldmm2 37683 |
. . . . . . . . . 10
β’ ((πΎ β OL β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((ocβπΎ)β(((ocβπΎ)β(π β¨ π))(meetβπΎ)π)) = ((π β¨ π) β¨ ((ocβπΎ)βπ))) |
67 | 65, 49, 14, 66 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((ocβπΎ)β(((ocβπΎ)β(π β¨ π))(meetβπΎ)π)) = ((π β¨ π) β¨ ((ocβπΎ)βπ))) |
68 | 5, 17, 20, 10 | oldmj1 37686 |
. . . . . . . . . . . . . 14
β’ ((πΎ β OL β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((ocβπΎ)β(π β¨ π)) = (((ocβπΎ)βπ)(meetβπΎ)((ocβπΎ)βπ))) |
69 | 65, 9, 24, 68 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((ocβπΎ)β(π β¨ π)) = (((ocβπΎ)βπ)(meetβπΎ)((ocβπΎ)βπ))) |
70 | 5, 33, 20 | latleeqm1 18357 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π(leβπΎ)π β (π(meetβπΎ)π) = π)) |
71 | 2, 9, 14, 70 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (π(leβπΎ)π β (π(meetβπΎ)π) = π)) |
72 | 51, 71 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (π(meetβπΎ)π) = π) |
73 | 72 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((ocβπΎ)β(π(meetβπΎ)π)) = ((ocβπΎ)βπ)) |
74 | 5, 17, 20, 10 | oldmm1 37682 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β OL β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((ocβπΎ)β(π(meetβπΎ)π)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
75 | 65, 9, 14, 74 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((ocβπΎ)β(π(meetβπΎ)π)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
76 | 73, 75 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((ocβπΎ)βπ) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
77 | 5, 33, 20 | latleeqm1 18357 |
. . . . . . . . . . . . . . . . . 18
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β (π(leβπΎ)π β (π(meetβπΎ)π) = π)) |
78 | 2, 24, 14, 77 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (π(leβπΎ)π β (π(meetβπΎ)π) = π)) |
79 | 53, 78 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (π(meetβπΎ)π) = π) |
80 | 79 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((ocβπΎ)β(π(meetβπΎ)π)) = ((ocβπΎ)βπ)) |
81 | 5, 17, 20, 10 | oldmm1 37682 |
. . . . . . . . . . . . . . . 16
β’ ((πΎ β OL β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((ocβπΎ)β(π(meetβπΎ)π)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
82 | 65, 24, 14, 81 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((ocβπΎ)β(π(meetβπΎ)π)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
83 | 80, 82 | eqtr3d 2779 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((ocβπΎ)βπ) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
84 | 76, 83 | oveq12d 7376 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((ocβπΎ)βπ)(meetβπΎ)((ocβπΎ)βπ)) = ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) |
85 | 69, 84 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((ocβπΎ)β(π β¨ π)) = ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) |
86 | 85 | oveq1d 7373 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((ocβπΎ)β(π β¨ π))(meetβπΎ)π) = (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))(meetβπΎ)π)) |
87 | 5, 20 | latmmdir 37700 |
. . . . . . . . . . . 12
β’ ((πΎ β OL β§
((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β (BaseβπΎ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))(meetβπΎ)π) = (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) |
88 | 65, 19, 28, 14, 87 | syl13anc 1373 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))(meetβπΎ)π) = (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) |
89 | 86, 88 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((ocβπΎ)β(π β¨ π))(meetβπΎ)π) = (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) |
90 | 89 | fveq2d 6847 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((ocβπΎ)β(((ocβπΎ)β(π β¨ π))(meetβπΎ)π)) = ((ocβπΎ)β(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)))) |
91 | 67, 90 | eqtr3d 2779 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((π β¨ π) β¨ ((ocβπΎ)βπ)) = ((ocβπΎ)β(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)))) |
92 | 91 | oveq1d 7373 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((π β¨ π) β¨ ((ocβπΎ)βπ)) β¨ ((ocβπΎ)βπ)) = (((ocβπΎ)β(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) β¨ ((ocβπΎ)βπ))) |
93 | 63, 92 | eqtr3d 2779 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((π β¨ π) β¨ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (((ocβπΎ)β(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) β¨ ((ocβπΎ)βπ))) |
94 | 61, 93 | eqtr3d 2779 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((π β¨ π) β¨ ((ocβπΎ)βπ)) = (((ocβπΎ)β(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) β¨ ((ocβπΎ)βπ))) |
95 | 94 | oveq1d 7373 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((π β¨ π) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) = ((((ocβπΎ)β(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) |
96 | 58, 95 | eqtr3d 2779 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (π β¨ π) = ((((ocβπΎ)β(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) |
97 | 96 | fveq2d 6847 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβ(π β¨ π)) = (πΌβ((((ocβπΎ)β(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) |
98 | | simpl 484 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΎ β HL β§ π β π»)) |
99 | 6, 7 | diaclN 39516 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (πΌβπ) β ran πΌ) |
100 | 99 | adantrr 716 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβπ) β ran πΌ) |
101 | 6, 42, 7 | diaelrnN 39511 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΌβπ) β ran πΌ) β (πΌβπ) β ((LTrnβπΎ)βπ)) |
102 | 100, 101 | syldan 592 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβπ) β ((LTrnβπΎ)βπ)) |
103 | 6, 7 | diaclN 39516 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (πΌβπ) β ran πΌ) |
104 | 103 | adantrl 715 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβπ) β ran πΌ) |
105 | 6, 42, 7 | diaelrnN 39511 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΌβπ) β ran πΌ) β (πΌβπ) β ((LTrnβπΎ)βπ)) |
106 | 104, 105 | syldan 592 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβπ) β ((LTrnβπΎ)βπ)) |
107 | | djaj.j |
. . . . 5
β’ π½ = ((vAβπΎ)βπ) |
108 | 6, 42, 7, 43, 107 | djavalN 39601 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((πΌβπ) β ((LTrnβπΎ)βπ) β§ (πΌβπ) β ((LTrnβπΎ)βπ))) β ((πΌβπ)π½(πΌβπ)) = (((ocAβπΎ)βπ)β((((ocAβπΎ)βπ)β(πΌβπ)) β© (((ocAβπΎ)βπ)β(πΌβπ))))) |
109 | 98, 102, 106, 108 | syl12anc 836 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((πΌβπ)π½(πΌβπ)) = (((ocAβπΎ)βπ)β((((ocAβπΎ)βπ)β(πΌβπ)) β© (((ocAβπΎ)βπ)β(πΌβπ))))) |
110 | 5, 33, 20 | latmle2 18355 |
. . . . . . . 8
β’ ((πΎ β Lat β§
(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(leβπΎ)π) |
111 | 2, 19, 14, 110 | syl3anc 1372 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(leβπΎ)π) |
112 | 5, 33, 6, 7 | diaeldm 39502 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β dom πΌ β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ) β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(leβπΎ)π))) |
113 | 112 | adantr 482 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β dom πΌ β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ) β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(leβπΎ)π))) |
114 | 22, 111, 113 | mpbir2and 712 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β dom πΌ) |
115 | 5, 33, 6, 7 | diaeldm 39502 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β dom πΌ β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ) β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(leβπΎ)π))) |
116 | 115 | adantr 482 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β dom πΌ β (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β (BaseβπΎ) β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(leβπΎ)π))) |
117 | 30, 37, 116 | mpbir2and 712 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β dom πΌ) |
118 | 20, 6, 7 | diameetN 39522 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β dom πΌ β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π) β dom πΌ)) β (πΌβ(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) = ((πΌβ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) β© (πΌβ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)))) |
119 | 98, 114, 117, 118 | syl12anc 836 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβ(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) = ((πΌβ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) β© (πΌβ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)))) |
120 | 17, 20, 10, 6, 42, 7, 43 | diaocN 39591 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (πΌβ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) = (((ocAβπΎ)βπ)β(πΌβπ))) |
121 | 120 | adantrr 716 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) = (((ocAβπΎ)βπ)β(πΌβπ))) |
122 | 17, 20, 10, 6, 42, 7, 43 | diaocN 39591 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (πΌβ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) = (((ocAβπΎ)βπ)β(πΌβπ))) |
123 | 122 | adantrl 715 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) = (((ocAβπΎ)βπ)β(πΌβπ))) |
124 | 121, 123 | ineq12d 4174 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((πΌβ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)) β© (πΌβ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) = ((((ocAβπΎ)βπ)β(πΌβπ)) β© (((ocAβπΎ)βπ)β(πΌβπ)))) |
125 | 119, 124 | eqtrd 2777 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβ(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))) = ((((ocAβπΎ)βπ)β(πΌβπ)) β© (((ocAβπΎ)βπ)β(πΌβπ)))) |
126 | 125 | fveq2d 6847 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (((ocAβπΎ)βπ)β(πΌβ(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)))) = (((ocAβπΎ)βπ)β((((ocAβπΎ)βπ)β(πΌβπ)) β© (((ocAβπΎ)βπ)β(πΌβπ))))) |
127 | 109, 126 | eqtr4d 2780 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β ((πΌβπ)π½(πΌβπ)) = (((ocAβπΎ)βπ)β(πΌβ(((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π)(meetβπΎ)((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))(meetβπΎ)π))))) |
128 | 45, 97, 127 | 3eqtr4d 2787 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβ(π β¨ π)) = ((πΌβπ)π½(πΌβπ))) |