Step | Hyp | Ref
| Expression |
1 | | eqid 2737 |
. 2
β’
(BaseβπΎ) =
(BaseβπΎ) |
2 | | cdlemg8.l |
. 2
β’ β€ =
(leβπΎ) |
3 | | simp11l 1285 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β πΎ β HL) |
4 | 3 | hllatd 37855 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β πΎ β Lat) |
5 | | simp12l 1287 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β π β π΄) |
6 | | simp11 1204 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β (πΎ β HL β§ π β π»)) |
7 | | simp21 1207 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β πΉ β π) |
8 | | simp22 1208 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β πΊ β π) |
9 | | cdlemg8.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
10 | | cdlemg8.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
11 | | cdlemg8.t |
. . . . . . 7
β’ π = ((LTrnβπΎ)βπ) |
12 | 2, 9, 10, 11 | ltrnat 38632 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ π β π΄) β (πΊβπ) β π΄) |
13 | 6, 8, 5, 12 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β (πΊβπ) β π΄) |
14 | 2, 9, 10, 11 | ltrnat 38632 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (πΊβπ) β π΄) β (πΉβ(πΊβπ)) β π΄) |
15 | 6, 7, 13, 14 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β (πΉβ(πΊβπ)) β π΄) |
16 | | cdlemg8.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
17 | 1, 16, 9 | hlatjcl 37858 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ (πΉβ(πΊβπ)) β π΄) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
18 | 3, 5, 15, 17 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
19 | | simp13l 1289 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β π β π΄) |
20 | 2, 9, 10, 11 | ltrnat 38632 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ π β π΄) β (πΊβπ) β π΄) |
21 | 6, 8, 19, 20 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β (πΊβπ) β π΄) |
22 | 2, 9, 10, 11 | ltrnat 38632 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (πΊβπ) β π΄) β (πΉβ(πΊβπ)) β π΄) |
23 | 6, 7, 21, 22 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β (πΉβ(πΊβπ)) β π΄) |
24 | 1, 16, 9 | hlatjcl 37858 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ (πΉβ(πΊβπ)) β π΄) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
25 | 3, 19, 23, 24 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
26 | | cdlemg8.m |
. . . 4
β’ β§ =
(meetβπΎ) |
27 | 1, 26 | latmcl 18336 |
. . 3
β’ ((πΎ β Lat β§ (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ) β§ (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β (BaseβπΎ)) |
28 | 4, 18, 25, 27 | syl3anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β (BaseβπΎ)) |
29 | | cdlemg10.r |
. . . . 5
β’ π
= ((trLβπΎ)βπ) |
30 | 1, 10, 11, 29 | trlcl 38656 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
βπΉ) β (BaseβπΎ)) |
31 | 6, 7, 30 | syl2anc 585 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β (π
βπΉ) β (BaseβπΎ)) |
32 | 1, 10, 11, 29 | trlcl 38656 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
βπΊ) β (BaseβπΎ)) |
33 | 6, 8, 32 | syl2anc 585 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β (π
βπΊ) β (BaseβπΎ)) |
34 | 1, 16 | latjcl 18335 |
. . 3
β’ ((πΎ β Lat β§ (π
βπΉ) β (BaseβπΎ) β§ (π
βπΊ) β (BaseβπΎ)) β ((π
βπΉ) β¨ (π
βπΊ)) β (BaseβπΎ)) |
35 | 4, 31, 33, 34 | syl3anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β ((π
βπΉ) β¨ (π
βπΊ)) β (BaseβπΎ)) |
36 | | simp11r 1286 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β π β π») |
37 | 1, 10 | lhpbase 38490 |
. . 3
β’ (π β π» β π β (BaseβπΎ)) |
38 | 36, 37 | syl 17 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β π β (BaseβπΎ)) |
39 | 2, 16, 26, 9, 10, 11, 29 | cdlemg10a 39132 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β€ ((π
βπΉ) β¨ (π
βπΊ))) |
40 | 2, 10, 11, 29 | trlle 38676 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π
βπΉ) β€ π) |
41 | 6, 7, 40 | syl2anc 585 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β (π
βπΉ) β€ π) |
42 | 2, 10, 11, 29 | trlle 38676 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
βπΊ) β€ π) |
43 | 6, 8, 42 | syl2anc 585 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β (π
βπΊ) β€ π) |
44 | 1, 2, 16 | latjle12 18346 |
. . . 4
β’ ((πΎ β Lat β§ ((π
βπΉ) β (BaseβπΎ) β§ (π
βπΊ) β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((π
βπΉ) β€ π β§ (π
βπΊ) β€ π) β ((π
βπΉ) β¨ (π
βπΊ)) β€ π)) |
45 | 4, 31, 33, 38, 44 | syl13anc 1373 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β (((π
βπΉ) β€ π β§ (π
βπΊ) β€ π) β ((π
βπΉ) β¨ (π
βπΊ)) β€ π)) |
46 | 41, 43, 45 | mpbi2and 711 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β ((π
βπΉ) β¨ (π
βπΊ)) β€ π) |
47 | 1, 2, 4, 28, 35, 38, 39, 46 | lattrd 18342 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ (π
βπΉ) β€ (π β¨ π) β§ Β¬ (π
βπΊ) β€ (π β¨ π))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) β€ π) |