Step | Hyp | Ref
| Expression |
1 | | simp1 1133 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) |
2 | | simp21 1203 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π£ β π΄ β§ π£ β€ π)) |
3 | | simp23l 1291 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β πΉ β π) |
4 | | simp3 1135 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) |
5 | | cdlemg12.l |
. . . 4
β’ β€ =
(leβπΎ) |
6 | | cdlemg12.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
7 | | cdlemg12.m |
. . . 4
β’ β§ =
(meetβπΎ) |
8 | | cdlemg12.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
9 | | cdlemg12.h |
. . . 4
β’ π» = (LHypβπΎ) |
10 | | cdlemg12.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
11 | | cdlemg12b.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
12 | | cdlemg31.n |
. . . 4
β’ π = ((π β¨ π£) β§ (π β¨ (π
βπΉ))) |
13 | 5, 6, 7, 8, 9, 10,
11, 12 | cdlemg33c0 40086 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ πΉ β π) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ π§ β€ (π β¨ π£))) |
14 | 1, 2, 3, 4, 13 | syl121anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ π§ β€ (π β¨ π£))) |
15 | | simp11l 1281 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β πΎ β HL) |
16 | | hlatl 38743 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β AtLat) |
17 | 15, 16 | syl 17 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β πΎ β AtLat) |
18 | | eqid 2726 |
. . . . . . . . . 10
β’
(0.βπΎ) =
(0.βπΎ) |
19 | 18, 8 | atn0 38691 |
. . . . . . . . 9
β’ ((πΎ β AtLat β§ π§ β π΄) β π§ β (0.βπΎ)) |
20 | 17, 19 | sylan 579 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π§ β π΄) β π§ β (0.βπΎ)) |
21 | | simp22l 1289 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π = (0.βπΎ)) |
22 | 21 | adantr 480 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π§ β π΄) β π = (0.βπΎ)) |
23 | 20, 22 | neeqtrrd 3009 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π§ β π΄) β π§ β π) |
24 | | simp22r 1290 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π = (0.βπΎ)) |
25 | 24 | adantr 480 |
. . . . . . . 8
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π§ β π΄) β π = (0.βπΎ)) |
26 | 20, 25 | neeqtrrd 3009 |
. . . . . . 7
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π§ β π΄) β π§ β π) |
27 | 23, 26 | jca 511 |
. . . . . 6
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π§ β π΄) β (π§ β π β§ π§ β π)) |
28 | 27 | biantrurd 532 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π§ β π΄) β (π§ β€ (π β¨ π£) β ((π§ β π β§ π§ β π) β§ π§ β€ (π β¨ π£)))) |
29 | | df-3an 1086 |
. . . . 5
β’ ((π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)) β ((π§ β π β§ π§ β π) β§ π§ β€ (π β¨ π£))) |
30 | 28, 29 | bitr4di 289 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π§ β π΄) β (π§ β€ (π β¨ π£) β (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) |
31 | 30 | anbi2d 628 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β§ π§ β π΄) β ((Β¬ π§ β€ π β§ π§ β€ (π β¨ π£)) β (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£))))) |
32 | 31 | rexbidva 3170 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (βπ§ β π΄ (Β¬ π§ β€ π β§ π§ β€ (π β¨ π£)) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£))))) |
33 | 14, 32 | mpbid 231 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π£ β π΄ β§ π£ β€ π) β§ (π = (0.βπΎ) β§ π = (0.βπΎ)) β§ (πΉ β π β§ πΊ β π)) β§ (π β π β§ π£ β (π
βπΉ) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π§ β π β§ π§ β π β§ π§ β€ (π β¨ π£)))) |