Step | Hyp | Ref
| Expression |
1 | | simpl 484 |
. . . 4
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β OL) |
2 | | ollat 37678 |
. . . . . 6
β’ (πΎ β OL β πΎ β Lat) |
3 | 2 | adantr 482 |
. . . . 5
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β Lat) |
4 | | olop 37679 |
. . . . . . 7
β’ (πΎ β OL β πΎ β OP) |
5 | 4 | adantr 482 |
. . . . . 6
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β πΎ β OP) |
6 | | simpr1 1195 |
. . . . . 6
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
7 | | olmass.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
8 | | eqid 2737 |
. . . . . . 7
β’
(ocβπΎ) =
(ocβπΎ) |
9 | 7, 8 | opoccl 37659 |
. . . . . 6
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
10 | 5, 6, 9 | syl2anc 585 |
. . . . 5
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)βπ) β π΅) |
11 | | simpr2 1196 |
. . . . . 6
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
12 | 7, 8 | opoccl 37659 |
. . . . . 6
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
13 | 5, 11, 12 | syl2anc 585 |
. . . . 5
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)βπ) β π΅) |
14 | | eqid 2737 |
. . . . . 6
β’
(joinβπΎ) =
(joinβπΎ) |
15 | 7, 14 | latjcl 18329 |
. . . . 5
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β (((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ)) β π΅) |
16 | 3, 10, 13, 15 | syl3anc 1372 |
. . . 4
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ)) β π΅) |
17 | | simpr3 1197 |
. . . 4
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β π β π΅) |
18 | | olmass.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
19 | 7, 14, 18, 8 | oldmj3 37688 |
. . . 4
β’ ((πΎ β OL β§
(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ)) β π΅ β§ π β π΅) β ((ocβπΎ)β((((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))(joinβπΎ)((ocβπΎ)βπ))) = (((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))) β§ π)) |
20 | 1, 16, 17, 19 | syl3anc 1372 |
. . 3
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β((((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))(joinβπΎ)((ocβπΎ)βπ))) = (((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))) β§ π)) |
21 | 7, 8 | opoccl 37659 |
. . . . . 6
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
22 | 5, 17, 21 | syl2anc 585 |
. . . . 5
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)βπ) β π΅) |
23 | 7, 14 | latjass 18373 |
. . . . 5
β’ ((πΎ β Lat β§
(((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅)) β ((((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))(joinβπΎ)((ocβπΎ)βπ)) = (((ocβπΎ)βπ)(joinβπΎ)(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ)))) |
24 | 3, 10, 13, 22, 23 | syl13anc 1373 |
. . . 4
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))(joinβπΎ)((ocβπΎ)βπ)) = (((ocβπΎ)βπ)(joinβπΎ)(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ)))) |
25 | 24 | fveq2d 6847 |
. . 3
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β((((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))(joinβπΎ)((ocβπΎ)βπ))) = ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))))) |
26 | 7, 14, 18, 8 | oldmj4 37689 |
. . . . 5
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))) = (π β§ π)) |
27 | 26 | 3adant3r3 1185 |
. . . 4
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))) = (π β§ π)) |
28 | 27 | oveq1d 7373 |
. . 3
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))) β§ π) = ((π β§ π) β§ π)) |
29 | 20, 25, 28 | 3eqtr3rd 2786 |
. 2
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β§ π) = ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))))) |
30 | 7, 14 | latjcl 18329 |
. . . 4
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β (((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ)) β π΅) |
31 | 3, 13, 22, 30 | syl3anc 1372 |
. . 3
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ)) β π΅) |
32 | 7, 14, 18, 8 | oldmj2 37687 |
. . 3
β’ ((πΎ β OL β§ π β π΅ β§ (((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ)) β π΅) β ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ)))) = (π β§ ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))))) |
33 | 1, 6, 31, 32 | syl3anc 1372 |
. 2
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ)))) = (π β§ ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))))) |
34 | 7, 14, 18, 8 | oldmj4 37689 |
. . . 4
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))) = (π β§ π)) |
35 | 34 | 3adant3r1 1183 |
. . 3
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ))) = (π β§ π)) |
36 | 35 | oveq2d 7374 |
. 2
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (π β§ ((ocβπΎ)β(((ocβπΎ)βπ)(joinβπΎ)((ocβπΎ)βπ)))) = (π β§ (π β§ π))) |
37 | 29, 33, 36 | 3eqtrd 2781 |
1
β’ ((πΎ β OL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β§ π) β§ π) = (π β§ (π β§ π))) |