Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. 2
β’ π = π |
2 | | oveq2 7366 |
. . . . . . 7
β’ (πΊ = π β (π β¨ πΊ) = (π β¨ π)) |
3 | | simp1l 1198 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΎ β HL) |
4 | | simp22l 1293 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π΄) |
5 | | cdleme18.j |
. . . . . . . . 9
β’ β¨ =
(joinβπΎ) |
6 | | cdleme18.a |
. . . . . . . . 9
β’ π΄ = (AtomsβπΎ) |
7 | 5, 6 | hlatjidm 37877 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄) β (π β¨ π) = π) |
8 | 3, 4, 7 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β¨ π) = π) |
9 | 2, 8 | sylan9eqr 2795 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β§ πΊ = π) β (π β¨ πΊ) = π) |
10 | | simp1 1137 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (πΎ β HL β§ π β π»)) |
11 | | simp21l 1291 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π΄) |
12 | | simp22 1208 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
13 | | simp23 1209 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
14 | | cdleme18.l |
. . . . . . . . . 10
β’ β€ =
(leβπΎ) |
15 | 14, 5, 6 | hlatlej2 37884 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
16 | 3, 11, 4, 15 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β€ (π β¨ π)) |
17 | | cdleme18.m |
. . . . . . . . 9
β’ β§ =
(meetβπΎ) |
18 | | cdleme18.h |
. . . . . . . . 9
β’ π» = (LHypβπΎ) |
19 | | cdleme18.u |
. . . . . . . . 9
β’ π = ((π β¨ π) β§ π) |
20 | | cdleme18.f |
. . . . . . . . 9
β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) |
21 | | cdleme18.g |
. . . . . . . . 9
β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) |
22 | 14, 5, 17, 6, 18, 19, 20, 21 | cdleme5 38749 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β (π β¨ πΊ) = (π β¨ π)) |
23 | 10, 11, 4, 12, 13, 16, 22 | syl132anc 1389 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β¨ πΊ) = (π β¨ π)) |
24 | 23 | adantr 482 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β§ πΊ = π) β (π β¨ πΊ) = (π β¨ π)) |
25 | 9, 24 | eqtr3d 2775 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β§ πΊ = π) β π = (π β¨ π)) |
26 | | simp3l 1202 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π) |
27 | 5, 6 | 2atneat 38024 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β Β¬ (π β¨ π) β π΄) |
28 | 3, 11, 4, 26, 27 | syl13anc 1373 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ (π β¨ π) β π΄) |
29 | | nelne2 3039 |
. . . . . . . 8
β’ ((π β π΄ β§ Β¬ (π β¨ π) β π΄) β π β (π β¨ π)) |
30 | 29 | necomd 2996 |
. . . . . . 7
β’ ((π β π΄ β§ Β¬ (π β¨ π) β π΄) β (π β¨ π) β π) |
31 | 4, 28, 30 | syl2anc 585 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β¨ π) β π) |
32 | 31 | adantr 482 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β§ πΊ = π) β (π β¨ π) β π) |
33 | 25, 32 | eqnetrd 3008 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β§ πΊ = π) β π β π) |
34 | 33 | ex 414 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (πΊ = π β π β π)) |
35 | 34 | necon2d 2963 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π = π β πΊ β π)) |
36 | 1, 35 | mpi 20 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΊ β π) |