Step | Hyp | Ref
| Expression |
1 | | simp1l 1198 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β πΎ β HL) |
2 | | simp2ll 1241 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β π β π΄) |
3 | | simp2rl 1243 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β π β π΄) |
4 | | simp1r 1199 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β π β π») |
5 | | eqid 2738 |
. . . 4
β’
(BaseβπΎ) =
(BaseβπΎ) |
6 | | cdlemb2.h |
. . . 4
β’ π» = (LHypβπΎ) |
7 | 5, 6 | lhpbase 38347 |
. . 3
β’ (π β π» β π β (BaseβπΎ)) |
8 | 4, 7 | syl 17 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β π β (BaseβπΎ)) |
9 | | simp3 1139 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β π β π) |
10 | | eqid 2738 |
. . . 4
β’
(1.βπΎ) =
(1.βπΎ) |
11 | | eqid 2738 |
. . . 4
β’ ( β
βπΎ) = ( β
βπΎ) |
12 | 10, 11, 6 | lhp1cvr 38348 |
. . 3
β’ ((πΎ β HL β§ π β π») β π( β βπΎ)(1.βπΎ)) |
13 | 12 | 3ad2ant1 1134 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β π( β βπΎ)(1.βπΎ)) |
14 | | simp2lr 1242 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β Β¬ π β€ π) |
15 | | simp2rr 1244 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β Β¬ π β€ π) |
16 | | cdlemb2.l |
. . 3
β’ β€ =
(leβπΎ) |
17 | | cdlemb2.j |
. . 3
β’ β¨ =
(joinβπΎ) |
18 | | cdlemb2.a |
. . 3
β’ π΄ = (AtomsβπΎ) |
19 | 5, 16, 17, 10, 11, 18 | cdlemb 38143 |
. 2
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β (BaseβπΎ) β§ π β π) β§ (π( β βπΎ)(1.βπΎ) β§ Β¬ π β€ π β§ Β¬ π β€ π)) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ (π β¨ π))) |
20 | 1, 2, 3, 8, 9, 13,
14, 15, 19 | syl323anc 1401 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ (π β¨ π))) |