Step | Hyp | Ref
| Expression |
1 | | simpl11 1249 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β§ π β π΄) β (πΎ β HL β§ π β π»)) |
2 | | simpl12 1250 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β§ π β π΄) β πΉ β π) |
3 | | simpl13 1251 |
. . . . 5
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β§ π β π΄) β πΊ β π) |
4 | 2, 3 | jca 513 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β§ π β π΄) β (πΉ β π β§ πΊ β π)) |
5 | | simpr 486 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β§ π β π΄) β π β π΄) |
6 | | simpl2 1193 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β§ π β π΄) β (π β π΄ β§ Β¬ π β€ π)) |
7 | | simpl3 1194 |
. . . 4
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β§ π β π΄) β (πΉβπ) = (πΊβπ)) |
8 | | cdlemd.l |
. . . . 5
β’ β€ =
(leβπΎ) |
9 | | eqid 2737 |
. . . . 5
β’
(joinβπΎ) =
(joinβπΎ) |
10 | | cdlemd.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
11 | | cdlemd.h |
. . . . 5
β’ π» = (LHypβπΎ) |
12 | | cdlemd.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
13 | 8, 9, 10, 11, 12 | cdlemd9 38672 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β (πΉβπ) = (πΊβπ)) |
14 | 1, 4, 5, 6, 7, 13 | syl311anc 1385 |
. . 3
β’
(((((πΎ β HL
β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β§ π β π΄) β (πΉβπ) = (πΊβπ)) |
15 | 14 | ralrimiva 3144 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β βπ β π΄ (πΉβπ) = (πΊβπ)) |
16 | 10, 11, 12 | ltrneq2 38614 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (βπ β π΄ (πΉβπ) = (πΊβπ) β πΉ = πΊ)) |
17 | 16 | 3ad2ant1 1134 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β (βπ β π΄ (πΉβπ) = (πΊβπ) β πΉ = πΊ)) |
18 | 15, 17 | mpbid 231 |
1
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β πΉ = πΊ) |