Step | Hyp | Ref
| Expression |
1 | | cvrexch.b |
. . 3
β’ π΅ = (BaseβπΎ) |
2 | | cvrexch.j |
. . 3
β’ β¨ =
(joinβπΎ) |
3 | | cvrexch.m |
. . 3
β’ β§ =
(meetβπΎ) |
4 | | cvrexch.c |
. . 3
β’ πΆ = ( β βπΎ) |
5 | 1, 2, 3, 4 | cvrexchlem 38290 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β ππΆ(π β¨ π))) |
6 | | simp1 1137 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β πΎ β HL) |
7 | | hlop 38232 |
. . . . . . 7
β’ (πΎ β HL β πΎ β OP) |
8 | 7 | 3ad2ant1 1134 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β πΎ β OP) |
9 | | simp3 1139 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β π β π΅) |
10 | | eqid 2733 |
. . . . . . 7
β’
(ocβπΎ) =
(ocβπΎ) |
11 | 1, 10 | opoccl 38064 |
. . . . . 6
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
12 | 8, 9, 11 | syl2anc 585 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
13 | | simp2 1138 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β π β π΅) |
14 | 1, 10 | opoccl 38064 |
. . . . . 6
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
15 | 8, 13, 14 | syl2anc 585 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
16 | 1, 2, 3, 4 | cvrexchlem 38290 |
. . . . 5
β’ ((πΎ β HL β§
((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β ((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))πΆ((ocβπΎ)βπ) β ((ocβπΎ)βπ)πΆ(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) |
17 | 6, 12, 15, 16 | syl3anc 1372 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))πΆ((ocβπΎ)βπ) β ((ocβπΎ)βπ)πΆ(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) |
18 | | hlol 38231 |
. . . . . . 7
β’ (πΎ β HL β πΎ β OL) |
19 | 1, 2, 3, 10 | oldmj1 38091 |
. . . . . . 7
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(π β¨ π)) = (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) |
20 | 18, 19 | syl3an1 1164 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(π β¨ π)) = (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) |
21 | | hllat 38233 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β Lat) |
22 | 21 | 3ad2ant1 1134 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β πΎ β Lat) |
23 | 1, 3 | latmcom 18416 |
. . . . . . 7
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) = (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) |
24 | 22, 15, 12, 23 | syl3anc 1372 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) = (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) |
25 | 20, 24 | eqtrd 2773 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(π β¨ π)) = (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) |
26 | 25 | breq1d 5159 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (((ocβπΎ)β(π β¨ π))πΆ((ocβπΎ)βπ) β (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))πΆ((ocβπΎ)βπ))) |
27 | 1, 2, 3, 10 | oldmm1 38087 |
. . . . . . 7
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(π β§ π)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
28 | 18, 27 | syl3an1 1164 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(π β§ π)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
29 | 1, 2 | latjcom 18400 |
. . . . . . 7
β’ ((πΎ β Lat β§
((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
30 | 22, 15, 12, 29 | syl3anc 1372 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
31 | 28, 30 | eqtrd 2773 |
. . . . 5
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(π β§ π)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
32 | 31 | breq2d 5161 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (((ocβπΎ)βπ)πΆ((ocβπΎ)β(π β§ π)) β ((ocβπΎ)βπ)πΆ(((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) |
33 | 17, 26, 32 | 3imtr4d 294 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (((ocβπΎ)β(π β¨ π))πΆ((ocβπΎ)βπ) β ((ocβπΎ)βπ)πΆ((ocβπΎ)β(π β§ π)))) |
34 | 1, 2 | latjcl 18392 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
35 | 21, 34 | syl3an1 1164 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
36 | 1, 10, 4 | cvrcon3b 38147 |
. . . 4
β’ ((πΎ β OP β§ π β π΅ β§ (π β¨ π) β π΅) β (ππΆ(π β¨ π) β ((ocβπΎ)β(π β¨ π))πΆ((ocβπΎ)βπ))) |
37 | 8, 13, 35, 36 | syl3anc 1372 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (ππΆ(π β¨ π) β ((ocβπΎ)β(π β¨ π))πΆ((ocβπΎ)βπ))) |
38 | 1, 3 | latmcl 18393 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
39 | 21, 38 | syl3an1 1164 |
. . . 4
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
40 | 1, 10, 4 | cvrcon3b 38147 |
. . . 4
β’ ((πΎ β OP β§ (π β§ π) β π΅ β§ π β π΅) β ((π β§ π)πΆπ β ((ocβπΎ)βπ)πΆ((ocβπΎ)β(π β§ π)))) |
41 | 8, 39, 9, 40 | syl3anc 1372 |
. . 3
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β ((ocβπΎ)βπ)πΆ((ocβπΎ)β(π β§ π)))) |
42 | 33, 37, 41 | 3imtr4d 294 |
. 2
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (ππΆ(π β¨ π) β (π β§ π)πΆπ)) |
43 | 5, 42 | impbid 211 |
1
β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β ππΆ(π β¨ π))) |