Step | Hyp | Ref
| Expression |
1 | | omllat 37750 |
. . . . 5
β’ (πΎ β OML β πΎ β Lat) |
2 | | omlfh1.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
3 | | eqid 2733 |
. . . . . 6
β’
(leβπΎ) =
(leβπΎ) |
4 | | omlfh1.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
5 | | omlfh1.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
6 | 2, 3, 4, 5 | latledi 18371 |
. . . . 5
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β¨ (π β§ π))(leβπΎ)(π β§ (π β¨ π))) |
7 | 1, 6 | sylan 581 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β¨ (π β§ π))(leβπΎ)(π β§ (π β¨ π))) |
8 | 7 | 3adant3 1133 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β ((π β§ π) β¨ (π β§ π))(leβπΎ)(π β§ (π β¨ π))) |
9 | 1 | adantr 482 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β Lat) |
10 | | simpr1 1195 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
11 | | simpr2 1196 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
12 | | simpr3 1197 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
13 | 2, 4 | latjcl 18333 |
. . . . . . . 8
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
14 | 9, 11, 12, 13 | syl3anc 1372 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ π) β π΅) |
15 | 2, 5 | latmcom 18357 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β π΅ β§ (π β¨ π) β π΅) β (π β§ (π β¨ π)) = ((π β¨ π) β§ π)) |
16 | 9, 10, 14, 15 | syl3anc 1372 |
. . . . . 6
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ (π β¨ π)) = ((π β¨ π) β§ π)) |
17 | | omlol 37748 |
. . . . . . . . 9
β’ (πΎ β OML β πΎ β OL) |
18 | 17 | adantr 482 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β OL) |
19 | 2, 5 | latmcl 18334 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
20 | 9, 10, 11, 19 | syl3anc 1372 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ π) β π΅) |
21 | 2, 5 | latmcl 18334 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
22 | 9, 10, 12, 21 | syl3anc 1372 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ π) β π΅) |
23 | | eqid 2733 |
. . . . . . . . 9
β’
(ocβπΎ) =
(ocβπΎ) |
24 | 2, 4, 5, 23 | oldmj1 37729 |
. . . . . . . 8
β’ ((πΎ β OL β§ (π β§ π) β π΅ β§ (π β§ π) β π΅) β ((ocβπΎ)β((π β§ π) β¨ (π β§ π))) = (((ocβπΎ)β(π β§ π)) β§ ((ocβπΎ)β(π β§ π)))) |
25 | 18, 20, 22, 24 | syl3anc 1372 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β((π β§ π) β¨ (π β§ π))) = (((ocβπΎ)β(π β§ π)) β§ ((ocβπΎ)β(π β§ π)))) |
26 | 2, 4, 5, 23 | oldmm1 37725 |
. . . . . . . . 9
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(π β§ π)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
27 | 18, 10, 11, 26 | syl3anc 1372 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β(π β§ π)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
28 | 2, 4, 5, 23 | oldmm1 37725 |
. . . . . . . . 9
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(π β§ π)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
29 | 18, 10, 12, 28 | syl3anc 1372 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β(π β§ π)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
30 | 27, 29 | oveq12d 7376 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((ocβπΎ)β(π β§ π)) β§ ((ocβπΎ)β(π β§ π))) = ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) |
31 | 25, 30 | eqtrd 2773 |
. . . . . 6
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β((π β§ π) β¨ (π β§ π))) = ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) |
32 | 16, 31 | oveq12d 7376 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ (π β¨ π)) β§ ((ocβπΎ)β((π β§ π) β¨ (π β§ π)))) = (((π β¨ π) β§ π) β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))))) |
33 | 32 | 3adant3 1133 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β ((π β§ (π β¨ π)) β§ ((ocβπΎ)β((π β§ π) β¨ (π β§ π)))) = (((π β¨ π) β§ π) β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))))) |
34 | | omlop 37749 |
. . . . . . . . . . 11
β’ (πΎ β OML β πΎ β OP) |
35 | 34 | adantr 482 |
. . . . . . . . . 10
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β OP) |
36 | 2, 23 | opoccl 37702 |
. . . . . . . . . 10
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
37 | 35, 10, 36 | syl2anc 585 |
. . . . . . . . 9
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)βπ) β π΅) |
38 | 2, 23 | opoccl 37702 |
. . . . . . . . . 10
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
39 | 35, 11, 38 | syl2anc 585 |
. . . . . . . . 9
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)βπ) β π΅) |
40 | 2, 4 | latjcl 18333 |
. . . . . . . . 9
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β π΅) |
41 | 9, 37, 39, 40 | syl3anc 1372 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β π΅) |
42 | 2, 23 | opoccl 37702 |
. . . . . . . . . 10
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
43 | 35, 12, 42 | syl2anc 585 |
. . . . . . . . 9
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)βπ) β π΅) |
44 | 2, 4 | latjcl 18333 |
. . . . . . . . 9
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β π΅) |
45 | 9, 37, 43, 44 | syl3anc 1372 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β π΅) |
46 | 2, 5 | latmcl 18334 |
. . . . . . . 8
β’ ((πΎ β Lat β§
(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β π΅ β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β π΅) β ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) β π΅) |
47 | 9, 41, 45, 46 | syl3anc 1372 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) β π΅) |
48 | 2, 5 | latmassOLD 37737 |
. . . . . . 7
β’ ((πΎ β OL β§ ((π β¨ π) β π΅ β§ π β π΅ β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) β π΅)) β (((π β¨ π) β§ π) β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = ((π β¨ π) β§ (π β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))))) |
49 | 18, 14, 10, 47, 48 | syl13anc 1373 |
. . . . . 6
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((π β¨ π) β§ π) β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = ((π β¨ π) β§ (π β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))))) |
50 | 49 | 3adant3 1133 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (((π β¨ π) β§ π) β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = ((π β¨ π) β§ (π β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))))) |
51 | | omlfh1.c |
. . . . . . . . . . . . . 14
β’ πΆ = (cmβπΎ) |
52 | 2, 23, 51 | cmt2N 37758 |
. . . . . . . . . . . . 13
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ππΆ((ocβπΎ)βπ))) |
53 | 52 | 3adant3r3 1185 |
. . . . . . . . . . . 12
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆπ β ππΆ((ocβπΎ)βπ))) |
54 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β OML) |
55 | 2, 4, 5, 23, 51 | cmtbr3N 37762 |
. . . . . . . . . . . . 13
β’ ((πΎ β OML β§ π β π΅ β§ ((ocβπΎ)βπ) β π΅) β (ππΆ((ocβπΎ)βπ) β (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ ((ocβπΎ)βπ)))) |
56 | 54, 10, 39, 55 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆ((ocβπΎ)βπ) β (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ ((ocβπΎ)βπ)))) |
57 | 53, 56 | bitrd 279 |
. . . . . . . . . . 11
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆπ β (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ ((ocβπΎ)βπ)))) |
58 | 57 | biimpa 478 |
. . . . . . . . . 10
β’ (((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β§ ππΆπ) β (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ ((ocβπΎ)βπ))) |
59 | 58 | adantrr 716 |
. . . . . . . . 9
β’ (((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β§ (ππΆπ β§ ππΆπ)) β (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ ((ocβπΎ)βπ))) |
60 | 59 | 3impa 1111 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ ((ocβπΎ)βπ))) |
61 | 2, 23, 51 | cmt2N 37758 |
. . . . . . . . . . . . 13
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ππΆ((ocβπΎ)βπ))) |
62 | 61 | 3adant3r2 1184 |
. . . . . . . . . . . 12
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆπ β ππΆ((ocβπΎ)βπ))) |
63 | 2, 4, 5, 23, 51 | cmtbr3N 37762 |
. . . . . . . . . . . . 13
β’ ((πΎ β OML β§ π β π΅ β§ ((ocβπΎ)βπ) β π΅) β (ππΆ((ocβπΎ)βπ) β (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ ((ocβπΎ)βπ)))) |
64 | 54, 10, 43, 63 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆ((ocβπΎ)βπ) β (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ ((ocβπΎ)βπ)))) |
65 | 62, 64 | bitrd 279 |
. . . . . . . . . . 11
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆπ β (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ ((ocβπΎ)βπ)))) |
66 | 65 | biimpa 478 |
. . . . . . . . . 10
β’ (((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β§ ππΆπ) β (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ ((ocβπΎ)βπ))) |
67 | 66 | adantrl 715 |
. . . . . . . . 9
β’ (((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β§ (ππΆπ β§ ππΆπ)) β (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ ((ocβπΎ)βπ))) |
68 | 67 | 3impa 1111 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ ((ocβπΎ)βπ))) |
69 | 60, 68 | oveq12d 7376 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β ((π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) β§ (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = ((π β§ ((ocβπΎ)βπ)) β§ (π β§ ((ocβπΎ)βπ)))) |
70 | 2, 5 | latmmdiN 37742 |
. . . . . . . . 9
β’ ((πΎ β OL β§ (π β π΅ β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β π΅ β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β π΅)) β (π β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = ((π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) β§ (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))))) |
71 | 18, 10, 41, 45, 70 | syl13anc 1373 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = ((π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) β§ (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))))) |
72 | 71 | 3adant3 1133 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = ((π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) β§ (π β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))))) |
73 | 2, 5 | latmmdiN 37742 |
. . . . . . . . 9
β’ ((πΎ β OL β§ (π β π΅ β§ ((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅)) β (π β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) = ((π β§ ((ocβπΎ)βπ)) β§ (π β§ ((ocβπΎ)βπ)))) |
74 | 18, 10, 39, 43, 73 | syl13anc 1373 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) = ((π β§ ((ocβπΎ)βπ)) β§ (π β§ ((ocβπΎ)βπ)))) |
75 | 74 | 3adant3 1133 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) = ((π β§ ((ocβπΎ)βπ)) β§ (π β§ ((ocβπΎ)βπ)))) |
76 | 69, 72, 75 | 3eqtr4d 2783 |
. . . . . 6
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = (π β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))) |
77 | 76 | oveq2d 7374 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β ((π β¨ π) β§ (π β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))))) = ((π β¨ π) β§ (π β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))))) |
78 | 2, 5 | latmcl 18334 |
. . . . . . . 8
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β π΅) |
79 | 9, 39, 43, 78 | syl3anc 1372 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β π΅) |
80 | 2, 5 | latm12 37738 |
. . . . . . 7
β’ ((πΎ β OL β§ ((π β¨ π) β π΅ β§ π β π΅ β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β π΅)) β ((π β¨ π) β§ (π β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))) = (π β§ ((π β¨ π) β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))))) |
81 | 18, 14, 10, 79, 80 | syl13anc 1373 |
. . . . . 6
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β§ (π β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))) = (π β§ ((π β¨ π) β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))))) |
82 | 81 | 3adant3 1133 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β ((π β¨ π) β§ (π β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))) = (π β§ ((π β¨ π) β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))))) |
83 | 50, 77, 82 | 3eqtrd 2777 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (((π β¨ π) β§ π) β§ ((((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = (π β§ ((π β¨ π) β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))))) |
84 | 2, 4, 5, 23 | oldmj1 37729 |
. . . . . . . . . 10
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(π β¨ π)) = (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) |
85 | 18, 11, 12, 84 | syl3anc 1372 |
. . . . . . . . 9
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β(π β¨ π)) = (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) |
86 | 85 | oveq2d 7374 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β§ ((ocβπΎ)β(π β¨ π))) = ((π β¨ π) β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))) |
87 | | eqid 2733 |
. . . . . . . . . 10
β’
(0.βπΎ) =
(0.βπΎ) |
88 | 2, 23, 5, 87 | opnoncon 37716 |
. . . . . . . . 9
β’ ((πΎ β OP β§ (π β¨ π) β π΅) β ((π β¨ π) β§ ((ocβπΎ)β(π β¨ π))) = (0.βπΎ)) |
89 | 35, 14, 88 | syl2anc 585 |
. . . . . . . 8
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β§ ((ocβπΎ)β(π β¨ π))) = (0.βπΎ)) |
90 | 86, 89 | eqtr3d 2775 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) = (0.βπΎ)) |
91 | 90 | oveq2d 7374 |
. . . . . 6
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ ((π β¨ π) β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))) = (π β§ (0.βπΎ))) |
92 | 2, 5, 87 | olm01 37744 |
. . . . . . 7
β’ ((πΎ β OL β§ π β π΅) β (π β§ (0.βπΎ)) = (0.βπΎ)) |
93 | 18, 10, 92 | syl2anc 585 |
. . . . . 6
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ (0.βπΎ)) = (0.βπΎ)) |
94 | 91, 93 | eqtrd 2773 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ ((π β¨ π) β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))) = (0.βπΎ)) |
95 | 94 | 3adant3 1133 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β§ ((π β¨ π) β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))) = (0.βπΎ)) |
96 | 33, 83, 95 | 3eqtrd 2777 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β ((π β§ (π β¨ π)) β§ ((ocβπΎ)β((π β§ π) β¨ (π β§ π)))) = (0.βπΎ)) |
97 | 2, 4 | latjcl 18333 |
. . . . . 6
β’ ((πΎ β Lat β§ (π β§ π) β π΅ β§ (π β§ π) β π΅) β ((π β§ π) β¨ (π β§ π)) β π΅) |
98 | 9, 20, 22, 97 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β¨ (π β§ π)) β π΅) |
99 | 2, 5 | latmcl 18334 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ (π β¨ π) β π΅) β (π β§ (π β¨ π)) β π΅) |
100 | 9, 10, 14, 99 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ (π β¨ π)) β π΅) |
101 | 2, 3, 5, 23, 87 | omllaw3 37753 |
. . . . 5
β’ ((πΎ β OML β§ ((π β§ π) β¨ (π β§ π)) β π΅ β§ (π β§ (π β¨ π)) β π΅) β ((((π β§ π) β¨ (π β§ π))(leβπΎ)(π β§ (π β¨ π)) β§ ((π β§ (π β¨ π)) β§ ((ocβπΎ)β((π β§ π) β¨ (π β§ π)))) = (0.βπΎ)) β ((π β§ π) β¨ (π β§ π)) = (π β§ (π β¨ π)))) |
102 | 54, 98, 100, 101 | syl3anc 1372 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((((π β§ π) β¨ (π β§ π))(leβπΎ)(π β§ (π β¨ π)) β§ ((π β§ (π β¨ π)) β§ ((ocβπΎ)β((π β§ π) β¨ (π β§ π)))) = (0.βπΎ)) β ((π β§ π) β¨ (π β§ π)) = (π β§ (π β¨ π)))) |
103 | 102 | 3adant3 1133 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β ((((π β§ π) β¨ (π β§ π))(leβπΎ)(π β§ (π β¨ π)) β§ ((π β§ (π β¨ π)) β§ ((ocβπΎ)β((π β§ π) β¨ (π β§ π)))) = (0.βπΎ)) β ((π β§ π) β¨ (π β§ π)) = (π β§ (π β¨ π)))) |
104 | 8, 96, 103 | mp2and 698 |
. 2
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β ((π β§ π) β¨ (π β§ π)) = (π β§ (π β¨ π))) |
105 | 104 | eqcomd 2739 |
1
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ (π β§ π))) |