Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β π β (AtomsβπΎ)) |
2 | | simpll1 1213 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β πΎ β HL) |
3 | | lhprelat3.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
4 | | eqid 2733 |
. . . . . . . 8
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
5 | 3, 4 | atbase 37801 |
. . . . . . 7
β’ (π β (AtomsβπΎ) β π β π΅) |
6 | 5 | adantl 483 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β π β π΅) |
7 | | eqid 2733 |
. . . . . . 7
β’
(ocβπΎ) =
(ocβπΎ) |
8 | | lhprelat3.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
9 | 3, 7, 4, 8 | lhpoc2N 38528 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΅) β (π β (AtomsβπΎ) β ((ocβπΎ)βπ) β π»)) |
10 | 2, 6, 9 | syl2anc 585 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β (π β (AtomsβπΎ) β ((ocβπΎ)βπ) β π»)) |
11 | 1, 10 | mpbid 231 |
. . . 4
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β ((ocβπΎ)βπ) β π») |
12 | 11 | adantr 482 |
. . 3
β’
(((((πΎ β HL
β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β§ (((ocβπΎ)βπ)πΆ(((ocβπΎ)βπ)(joinβπΎ)π) β§ (((ocβπΎ)βπ)(joinβπΎ)π) β€ ((ocβπΎ)βπ))) β ((ocβπΎ)βπ) β π») |
13 | | hlop 37874 |
. . . . . . . . 9
β’ (πΎ β HL β πΎ β OP) |
14 | 2, 13 | syl 17 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β πΎ β OP) |
15 | 2 | hllatd 37876 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β πΎ β Lat) |
16 | | simpll3 1215 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β π β π΅) |
17 | 3, 7 | opoccl 37706 |
. . . . . . . . . 10
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
18 | 14, 6, 17 | syl2anc 585 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β ((ocβπΎ)βπ) β π΅) |
19 | | lhprelat3.m |
. . . . . . . . . 10
β’ β§ =
(meetβπΎ) |
20 | 3, 19 | latmcl 18337 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β π΅ β§ ((ocβπΎ)βπ) β π΅) β (π β§ ((ocβπΎ)βπ)) β π΅) |
21 | 15, 16, 18, 20 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β (π β§ ((ocβπΎ)βπ)) β π΅) |
22 | | lhprelat3.c |
. . . . . . . . 9
β’ πΆ = ( β βπΎ) |
23 | 3, 7, 22 | cvrcon3b 37789 |
. . . . . . . 8
β’ ((πΎ β OP β§ (π β§ ((ocβπΎ)βπ)) β π΅ β§ π β π΅) β ((π β§ ((ocβπΎ)βπ))πΆπ β ((ocβπΎ)βπ)πΆ((ocβπΎ)β(π β§ ((ocβπΎ)βπ))))) |
24 | 14, 21, 16, 23 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β ((π β§ ((ocβπΎ)βπ))πΆπ β ((ocβπΎ)βπ)πΆ((ocβπΎ)β(π β§ ((ocβπΎ)βπ))))) |
25 | | hlol 37873 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β OL) |
26 | 2, 25 | syl 17 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β πΎ β OL) |
27 | | eqid 2733 |
. . . . . . . . . 10
β’
(joinβπΎ) =
(joinβπΎ) |
28 | 3, 27, 19, 7 | oldmm3N 37731 |
. . . . . . . . 9
β’ ((πΎ β OL β§ π β π΅ β§ π β π΅) β ((ocβπΎ)β(π β§ ((ocβπΎ)βπ))) = (((ocβπΎ)βπ)(joinβπΎ)π)) |
29 | 26, 16, 6, 28 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β ((ocβπΎ)β(π β§ ((ocβπΎ)βπ))) = (((ocβπΎ)βπ)(joinβπΎ)π)) |
30 | 29 | breq2d 5121 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β (((ocβπΎ)βπ)πΆ((ocβπΎ)β(π β§ ((ocβπΎ)βπ))) β ((ocβπΎ)βπ)πΆ(((ocβπΎ)βπ)(joinβπΎ)π))) |
31 | 24, 30 | bitr2d 280 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β (((ocβπΎ)βπ)πΆ(((ocβπΎ)βπ)(joinβπΎ)π) β (π β§ ((ocβπΎ)βπ))πΆπ)) |
32 | | simpll2 1214 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β π β π΅) |
33 | | lhprelat3.l |
. . . . . . . . 9
β’ β€ =
(leβπΎ) |
34 | 3, 33, 7 | oplecon3b 37712 |
. . . . . . . 8
β’ ((πΎ β OP β§ π β π΅ β§ (π β§ ((ocβπΎ)βπ)) β π΅) β (π β€ (π β§ ((ocβπΎ)βπ)) β ((ocβπΎ)β(π β§ ((ocβπΎ)βπ))) β€ ((ocβπΎ)βπ))) |
35 | 14, 32, 21, 34 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β (π β€ (π β§ ((ocβπΎ)βπ)) β ((ocβπΎ)β(π β§ ((ocβπΎ)βπ))) β€ ((ocβπΎ)βπ))) |
36 | 29 | breq1d 5119 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β (((ocβπΎ)β(π β§ ((ocβπΎ)βπ))) β€ ((ocβπΎ)βπ) β (((ocβπΎ)βπ)(joinβπΎ)π) β€ ((ocβπΎ)βπ))) |
37 | 35, 36 | bitr2d 280 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β ((((ocβπΎ)βπ)(joinβπΎ)π) β€ ((ocβπΎ)βπ) β π β€ (π β§ ((ocβπΎ)βπ)))) |
38 | 31, 37 | anbi12d 632 |
. . . . 5
β’ ((((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β ((((ocβπΎ)βπ)πΆ(((ocβπΎ)βπ)(joinβπΎ)π) β§ (((ocβπΎ)βπ)(joinβπΎ)π) β€ ((ocβπΎ)βπ)) β ((π β§ ((ocβπΎ)βπ))πΆπ β§ π β€ (π β§ ((ocβπΎ)βπ))))) |
39 | 38 | biimpa 478 |
. . . 4
β’
(((((πΎ β HL
β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β§ (((ocβπΎ)βπ)πΆ(((ocβπΎ)βπ)(joinβπΎ)π) β§ (((ocβπΎ)βπ)(joinβπΎ)π) β€ ((ocβπΎ)βπ))) β ((π β§ ((ocβπΎ)βπ))πΆπ β§ π β€ (π β§ ((ocβπΎ)βπ)))) |
40 | 39 | ancomd 463 |
. . 3
β’
(((((πΎ β HL
β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β§ (((ocβπΎ)βπ)πΆ(((ocβπΎ)βπ)(joinβπΎ)π) β§ (((ocβπΎ)βπ)(joinβπΎ)π) β€ ((ocβπΎ)βπ))) β (π β€ (π β§ ((ocβπΎ)βπ)) β§ (π β§ ((ocβπΎ)βπ))πΆπ)) |
41 | | oveq2 7369 |
. . . . . 6
β’ (π€ = ((ocβπΎ)βπ) β (π β§ π€) = (π β§ ((ocβπΎ)βπ))) |
42 | 41 | breq2d 5121 |
. . . . 5
β’ (π€ = ((ocβπΎ)βπ) β (π β€ (π β§ π€) β π β€ (π β§ ((ocβπΎ)βπ)))) |
43 | 41 | breq1d 5119 |
. . . . 5
β’ (π€ = ((ocβπΎ)βπ) β ((π β§ π€)πΆπ β (π β§ ((ocβπΎ)βπ))πΆπ)) |
44 | 42, 43 | anbi12d 632 |
. . . 4
β’ (π€ = ((ocβπΎ)βπ) β ((π β€ (π β§ π€) β§ (π β§ π€)πΆπ) β (π β€ (π β§ ((ocβπΎ)βπ)) β§ (π β§ ((ocβπΎ)βπ))πΆπ))) |
45 | 44 | rspcev 3583 |
. . 3
β’
((((ocβπΎ)βπ) β π» β§ (π β€ (π β§ ((ocβπΎ)βπ)) β§ (π β§ ((ocβπΎ)βπ))πΆπ)) β βπ€ β π» (π β€ (π β§ π€) β§ (π β§ π€)πΆπ)) |
46 | 12, 40, 45 | syl2anc 585 |
. 2
β’
(((((πΎ β HL
β§ π β π΅ β§ π β π΅) β§ π < π) β§ π β (AtomsβπΎ)) β§ (((ocβπΎ)βπ)πΆ(((ocβπΎ)βπ)(joinβπΎ)π) β§ (((ocβπΎ)βπ)(joinβπΎ)π) β€ ((ocβπΎ)βπ))) β βπ€ β π» (π β€ (π β§ π€) β§ (π β§ π€)πΆπ)) |
47 | | simpl1 1192 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β πΎ β HL) |
48 | 47, 13 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β πΎ β OP) |
49 | | simpl3 1194 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β π β π΅) |
50 | 3, 7 | opoccl 37706 |
. . . 4
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
51 | 48, 49, 50 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β ((ocβπΎ)βπ) β π΅) |
52 | | simpl2 1193 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β π β π΅) |
53 | 3, 7 | opoccl 37706 |
. . . 4
β’ ((πΎ β OP β§ π β π΅) β ((ocβπΎ)βπ) β π΅) |
54 | 48, 52, 53 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β ((ocβπΎ)βπ) β π΅) |
55 | | simpr 486 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β π < π) |
56 | | lhprelat3.s |
. . . . . 6
β’ < =
(ltβπΎ) |
57 | 3, 56, 7 | opltcon3b 37716 |
. . . . 5
β’ ((πΎ β OP β§ π β π΅ β§ π β π΅) β (π < π β ((ocβπΎ)βπ) < ((ocβπΎ)βπ))) |
58 | 48, 52, 49, 57 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β (π < π β ((ocβπΎ)βπ) < ((ocβπΎ)βπ))) |
59 | 55, 58 | mpbid 231 |
. . 3
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β ((ocβπΎ)βπ) < ((ocβπΎ)βπ)) |
60 | 3, 33, 56, 27, 22, 4 | hlrelat3 37925 |
. . 3
β’ (((πΎ β HL β§
((ocβπΎ)βπ) β π΅ β§ ((ocβπΎ)βπ) β π΅) β§ ((ocβπΎ)βπ) < ((ocβπΎ)βπ)) β βπ β (AtomsβπΎ)(((ocβπΎ)βπ)πΆ(((ocβπΎ)βπ)(joinβπΎ)π) β§ (((ocβπΎ)βπ)(joinβπΎ)π) β€ ((ocβπΎ)βπ))) |
61 | 47, 51, 54, 59, 60 | syl31anc 1374 |
. 2
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β βπ β (AtomsβπΎ)(((ocβπΎ)βπ)πΆ(((ocβπΎ)βπ)(joinβπΎ)π) β§ (((ocβπΎ)βπ)(joinβπΎ)π) β€ ((ocβπΎ)βπ))) |
62 | 46, 61 | r19.29a 3156 |
1
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β βπ€ β π» (π β€ (π β§ π€) β§ (π β§ π€)πΆπ)) |