Step | Hyp | Ref
| Expression |
1 | | simp1l 1194 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β πΎ β HL) |
2 | | simp1r 1195 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β π β π») |
3 | | eqid 2726 |
. . . . 5
β’
(ocβπΎ) =
(ocβπΎ) |
4 | | eqid 2726 |
. . . . 5
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
5 | | lhpmod.h |
. . . . 5
β’ π» = (LHypβπΎ) |
6 | 3, 4, 5 | lhpocat 39401 |
. . . 4
β’ ((πΎ β HL β§ π β π») β ((ocβπΎ)βπ) β (AtomsβπΎ)) |
7 | 1, 2, 6 | syl2anc 583 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((ocβπΎ)βπ) β (AtomsβπΎ)) |
8 | | hlop 38745 |
. . . . 5
β’ (πΎ β HL β πΎ β OP) |
9 | 1, 8 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β πΎ β OP) |
10 | | simp2l 1196 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β π β π΅) |
11 | | lhpmod.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
12 | 11, 3 | opoccl 38577 |
. . . 4
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
13 | 9, 10, 12 | syl2anc 583 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((ocβπΎ)βπ) β π΅) |
14 | | simp2r 1197 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β π β π΅) |
15 | 11, 3 | opoccl 38577 |
. . . 4
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
16 | 9, 14, 15 | syl2anc 583 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((ocβπΎ)βπ) β π΅) |
17 | | simp3 1135 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β π β€ π) |
18 | 11, 5 | lhpbase 39382 |
. . . . . 6
β’ (π β π» β π β π΅) |
19 | 2, 18 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β π β π΅) |
20 | | lhpmod.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
21 | 11, 20, 3 | oplecon3b 38583 |
. . . . 5
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π β€ π β ((ocβπΎ)βπ) β€ ((ocβπΎ)βπ))) |
22 | 9, 10, 19, 21 | syl3anc 1368 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β (π β€ π β ((ocβπΎ)βπ) β€ ((ocβπΎ)βπ))) |
23 | 17, 22 | mpbid 231 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((ocβπΎ)βπ) β€ ((ocβπΎ)βπ)) |
24 | | lhpmod.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
25 | | lhpmod.m |
. . . 4
β’ β§ =
(meetβπΎ) |
26 | 11, 20, 24, 25, 4 | atmod2i1 39245 |
. . 3
β’ ((πΎ β HL β§
(((ocβπΎ)βπ) β (AtomsβπΎ) β§ ((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β§ ((ocβπΎ)βπ) β€ ((ocβπΎ)βπ)) β ((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ ((ocβπΎ)βπ)) = (((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) |
27 | 1, 7, 13, 16, 23, 26 | syl131anc 1380 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ ((ocβπΎ)βπ)) = (((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) |
28 | 1 | hllatd 38747 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β πΎ β Lat) |
29 | 11, 25 | latmcl 18405 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
30 | 28, 14, 19, 29 | syl3anc 1368 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β (π β§ π) β π΅) |
31 | 11, 24 | latjcl 18404 |
. . . . 5
β’ ((πΎ β Lat β§ π β π΅ β§ (π β§ π) β π΅) β (π β¨ (π β§ π)) β π΅) |
32 | 28, 10, 30, 31 | syl3anc 1368 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β (π β¨ (π β§ π)) β π΅) |
33 | 11, 24 | latjcl 18404 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
34 | 28, 10, 14, 33 | syl3anc 1368 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β (π β¨ π) β π΅) |
35 | 11, 25 | latmcl 18405 |
. . . . 5
β’ ((πΎ β Lat β§ (π β¨ π) β π΅ β§ π β π΅) β ((π β¨ π) β§ π) β π΅) |
36 | 28, 34, 19, 35 | syl3anc 1368 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((π β¨ π) β§ π) β π΅) |
37 | 11, 3 | opcon3b 38579 |
. . . 4
β’ ((πΎ β OP β§ (π β¨ (π β§ π)) β π΅ β§ ((π β¨ π) β§ π) β π΅) β ((π β¨ (π β§ π)) = ((π β¨ π) β§ π) β ((ocβπΎ)β((π β¨ π) β§ π)) = ((ocβπΎ)β(π β¨ (π β§ π))))) |
38 | 9, 32, 36, 37 | syl3anc 1368 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((π β¨ (π β§ π)) = ((π β¨ π) β§ π) β ((ocβπΎ)β((π β¨ π) β§ π)) = ((ocβπΎ)β(π β¨ (π β§ π))))) |
39 | | hlol 38744 |
. . . . . . 7
β’ (πΎ β HL β πΎ β OL) |
40 | 1, 39 | syl 17 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β πΎ β OL) |
41 | 11, 24, 25, 3 | oldmm1 38600 |
. . . . . 6
β’ ((πΎ β OL β§ (π β¨ π) β π΅ β§ π β π΅) β ((ocβπΎ)β((π β¨ π) β§ π)) = (((ocβπΎ)β(π β¨ π)) β¨ ((ocβπΎ)βπ))) |
42 | 40, 34, 19, 41 | syl3anc 1368 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((ocβπΎ)β((π β¨ π) β§ π)) = (((ocβπΎ)β(π β¨ π)) β¨ ((ocβπΎ)βπ))) |
43 | 11, 24, 25, 3 | oldmj1 38604 |
. . . . . . 7
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(π β¨ π)) = (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) |
44 | 40, 10, 14, 43 | syl3anc 1368 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((ocβπΎ)β(π β¨ π)) = (((ocβπΎ)βπ) β§ ((ocβπΎ)βπ))) |
45 | 44 | oveq1d 7420 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β (((ocβπΎ)β(π β¨ π)) β¨ ((ocβπΎ)βπ)) = ((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ ((ocβπΎ)βπ))) |
46 | 42, 45 | eqtrd 2766 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((ocβπΎ)β((π β¨ π) β§ π)) = ((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ ((ocβπΎ)βπ))) |
47 | 11, 24, 25, 3 | oldmj1 38604 |
. . . . . 6
β’ ((πΎ β OL β§ π β π΅ β§ (π β§ π) β π΅) β ((ocβπΎ)β(π β¨ (π β§ π))) = (((ocβπΎ)βπ) β§ ((ocβπΎ)β(π β§ π)))) |
48 | 40, 10, 30, 47 | syl3anc 1368 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((ocβπΎ)β(π β¨ (π β§ π))) = (((ocβπΎ)βπ) β§ ((ocβπΎ)β(π β§ π)))) |
49 | 11, 24, 25, 3 | oldmm1 38600 |
. . . . . . 7
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(π β§ π)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
50 | 40, 14, 19, 49 | syl3anc 1368 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((ocβπΎ)β(π β§ π)) = (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))) |
51 | 50 | oveq2d 7421 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β (((ocβπΎ)βπ) β§ ((ocβπΎ)β(π β§ π))) = (((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) |
52 | 48, 51 | eqtrd 2766 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((ocβπΎ)β(π β¨ (π β§ π))) = (((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ)))) |
53 | 46, 52 | eqeq12d 2742 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β (((ocβπΎ)β((π β¨ π) β§ π)) = ((ocβπΎ)β(π β¨ (π β§ π))) β ((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ ((ocβπΎ)βπ)) = (((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))))) |
54 | 38, 53 | bitrd 279 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((π β¨ (π β§ π)) = ((π β¨ π) β§ π) β ((((ocβπΎ)βπ) β§ ((ocβπΎ)βπ)) β¨ ((ocβπΎ)βπ)) = (((ocβπΎ)βπ) β§ (((ocβπΎ)βπ) β¨ ((ocβπΎ)βπ))))) |
55 | 27, 54 | mpbird 257 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β (π β¨ (π β§ π)) = ((π β¨ π) β§ π)) |