Step | Hyp | Ref
| Expression |
1 | | omlfh1.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
2 | | eqid 2733 |
. . . . . . 7
β’
(ocβπΎ) =
(ocβπΎ) |
3 | | omlfh1.c |
. . . . . . 7
β’ πΆ = (cmβπΎ) |
4 | 1, 2, 3 | cmt4N 37760 |
. . . . . 6
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ))) |
5 | 4 | 3adant3r3 1185 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆπ β ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ))) |
6 | 1, 2, 3 | cmt4N 37760 |
. . . . . 6
β’ ((πΎ β OML β§ π β π΅ β§ π β π΅) β (ππΆπ β ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ))) |
7 | 6 | 3adant3r2 1184 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (ππΆπ β ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ))) |
8 | 5, 7 | anbi12d 632 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ππΆπ β§ ππΆπ) β (((ocβπΎ)βπ)πΆ((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ)))) |
9 | | simpl 484 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β OML) |
10 | | omlop 37749 |
. . . . . . . 8
β’ (πΎ β OML β πΎ β OP) |
11 | 10 | adantr 482 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β OP) |
12 | | simpr1 1195 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
13 | 1, 2 | opoccl 37702 |
. . . . . . 7
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
14 | 11, 12, 13 | syl2anc 585 |
. . . . . 6
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)βπ) β π΅) |
15 | | simpr2 1196 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
16 | 1, 2 | opoccl 37702 |
. . . . . . 7
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
17 | 11, 15, 16 | syl2anc 585 |
. . . . . 6
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)βπ) β π΅) |
18 | | simpr3 1197 |
. . . . . . 7
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
19 | 1, 2 | opoccl 37702 |
. . . . . . 7
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
20 | 11, 18, 19 | syl2anc 585 |
. . . . . 6
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)βπ) β π΅) |
21 | 14, 17, 20 | 3jca 1129 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅)) |
22 | | omlfh1.j |
. . . . . . . 8
β’ β¨ =
(joinβπΎ) |
23 | | omlfh1.m |
. . . . . . . 8
β’ β§ =
(meetβπΎ) |
24 | 1, 22, 23, 3 | omlfh1N 37766 |
. . . . . . 7
β’ ((πΎ β OML β§
(((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β§ (((ocβπΎ)βπ)πΆ((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ))) β (((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = ((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))) |
25 | 24 | fveq2d 6847 |
. . . . . 6
β’ ((πΎ β OML β§
(((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β§ (((ocβπΎ)βπ)πΆ((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ))) β ((ocβπΎ)β(((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = ((ocβπΎ)β((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))))) |
26 | 25 | 3exp 1120 |
. . . . 5
β’ (πΎ β OML β
((((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β ((((ocβπΎ)βπ)πΆ((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ)) β ((ocβπΎ)β(((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = ((ocβπΎ)β((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))))))) |
27 | 9, 21, 26 | sylc 65 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((((ocβπΎ)βπ)πΆ((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)πΆ((ocβπΎ)βπ)) β ((ocβπΎ)β(((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = ((ocβπΎ)β((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))))) |
28 | 8, 27 | sylbid 239 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ππΆπ β§ ππΆπ) β ((ocβπΎ)β(((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = ((ocβπΎ)β((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))))) |
29 | 28 | 3impia 1118 |
. 2
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β ((ocβπΎ)β(((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = ((ocβπΎ)β((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))))) |
30 | | omlol 37748 |
. . . . . 6
β’ (πΎ β OML β πΎ β OL) |
31 | 30 | adantr 482 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β OL) |
32 | | omllat 37750 |
. . . . . . 7
β’ (πΎ β OML β πΎ β Lat) |
33 | 32 | adantr 482 |
. . . . . 6
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β Lat) |
34 | 1, 22 | latjcl 18333 |
. . . . . 6
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β π΅) |
35 | 33, 17, 20, 34 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β π΅) |
36 | 1, 22, 23, 2 | oldmm2 37726 |
. . . . 5
β’ ((πΎ β OL β§ π β π΅ β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) β π΅) β ((ocβπΎ)β(((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = (π β¨ ((ocβπΎ)β(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))))) |
37 | 31, 12, 35, 36 | syl3anc 1372 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β(((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = (π β¨ ((ocβπΎ)β(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))))) |
38 | 1, 22, 23, 2 | oldmj4 37732 |
. . . . . 6
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ π)) |
39 | 31, 15, 18, 38 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) = (π β§ π)) |
40 | 39 | oveq2d 7374 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ ((ocβπΎ)β(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) = (π β¨ (π β§ π))) |
41 | 37, 40 | eqtr2d 2774 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β¨ (π β§ π)) = ((ocβπΎ)β(((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))))) |
42 | 41 | 3adant3 1133 |
. 2
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β¨ (π β§ π)) = ((ocβπΎ)β(((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))))) |
43 | 1, 23 | latmcl 18334 |
. . . . . 6
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β π΅) |
44 | 33, 14, 17, 43 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β π΅) |
45 | 1, 23 | latmcl 18334 |
. . . . . 6
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β π΅) |
46 | 33, 14, 20, 45 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β π΅) |
47 | 1, 22, 23, 2 | oldmj1 37729 |
. . . . 5
β’ ((πΎ β OL β§
(((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β π΅ β§ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β π΅) β ((ocβπΎ)β((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))) = (((ocβπΎ)β(((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) β§ ((ocβπΎ)β(((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))))) |
48 | 31, 44, 46, 47 | syl3anc 1372 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))) = (((ocβπΎ)β(((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) β§ ((ocβπΎ)β(((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))))) |
49 | 1, 22, 23, 2 | oldmm4 37728 |
. . . . . 6
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) = (π β¨ π)) |
50 | 31, 12, 15, 49 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β(((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) = (π β¨ π)) |
51 | 1, 22, 23, 2 | oldmm4 37728 |
. . . . . 6
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) = (π β¨ π)) |
52 | 31, 12, 18, 51 | syl3anc 1372 |
. . . . 5
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β(((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) = (π β¨ π)) |
53 | 50, 52 | oveq12d 7376 |
. . . 4
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((ocβπΎ)β(((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) β§ ((ocβπΎ)β(((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)))) = ((π β¨ π) β§ (π β¨ π))) |
54 | 48, 53 | eqtr2d 2774 |
. . 3
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β¨ π) β§ (π β¨ π)) = ((ocβπΎ)β((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))))) |
55 | 54 | 3adant3 1133 |
. 2
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β ((π β¨ π) β§ (π β¨ π)) = ((ocβπΎ)β((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))))) |
56 | 29, 42, 55 | 3eqtr4d 2783 |
1
β’ ((πΎ β OML β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (ππΆπ β§ ππΆπ)) β (π β¨ (π β§ π)) = ((π β¨ π) β§ (π β¨ π))) |