Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ π β€ π)) β (πΎ β HL β§ π β π»)) |
2 | | simpl2 1193 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ π β€ π)) β π β π΅) |
3 | | simprl 770 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ π β€ π)) β π β€ π) |
4 | | simpl3 1194 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ π β€ π)) β π β π΅) |
5 | | simprr 772 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ π β€ π)) β π β€ π) |
6 | | dihord.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
7 | | dihord.l |
. . . 4
β’ β€ =
(leβπΎ) |
8 | | dihord.h |
. . . 4
β’ π» = (LHypβπΎ) |
9 | | dihord.i |
. . . 4
β’ πΌ = ((DIsoHβπΎ)βπ) |
10 | 6, 7, 8, 9 | dihord3 39770 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ π β€ π)) β ((πΌβπ) β (πΌβπ) β π β€ π)) |
11 | 1, 2, 3, 4, 5, 10 | syl122anc 1380 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ π β€ π)) β ((πΌβπ) β (πΌβπ) β π β€ π)) |
12 | | simpl1 1192 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ Β¬ π β€ π)) β (πΎ β HL β§ π β π»)) |
13 | | simpl2 1193 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ Β¬ π β€ π)) β π β π΅) |
14 | | simprl 770 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ Β¬ π β€ π)) β π β€ π) |
15 | | simpl3 1194 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ Β¬ π β€ π)) β π β π΅) |
16 | | simprr 772 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ Β¬ π β€ π)) β Β¬ π β€ π) |
17 | 6, 7, 8, 9 | dihord5a 39776 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β§ (πΌβπ) β (πΌβπ)) β π β€ π) |
18 | 6, 7, 8, 9 | dihord5b 39772 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β§ π β€ π) β (πΌβπ) β (πΌβπ)) |
19 | 17, 18 | impbida 800 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β ((πΌβπ) β (πΌβπ) β π β€ π)) |
20 | 12, 13, 14, 15, 16, 19 | syl122anc 1380 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β€ π β§ Β¬ π β€ π)) β ((πΌβπ) β (πΌβπ) β π β€ π)) |
21 | | simpl1 1192 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ π β€ π)) β (πΎ β HL β§ π β π»)) |
22 | | simpl2 1193 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ π β€ π)) β π β π΅) |
23 | | simprl 770 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ π β€ π)) β Β¬ π β€ π) |
24 | | simpl3 1194 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ π β€ π)) β π β π΅) |
25 | | simprr 772 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ π β€ π)) β π β€ π) |
26 | 6, 7, 8, 9 | dihord6a 39774 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (πΌβπ) β (πΌβπ)) β π β€ π) |
27 | 6, 7, 8, 9 | dihord6b 39773 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ π β€ π) β (πΌβπ) β (πΌβπ)) |
28 | 26, 27 | impbida 800 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β ((πΌβπ) β (πΌβπ) β π β€ π)) |
29 | 21, 22, 23, 24, 25, 28 | syl122anc 1380 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ π β€ π)) β ((πΌβπ) β (πΌβπ) β π β€ π)) |
30 | | simpl1 1192 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ Β¬ π β€ π)) β (πΎ β HL β§ π β π»)) |
31 | | simpl2 1193 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ Β¬ π β€ π)) β π β π΅) |
32 | | simprl 770 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ Β¬ π β€ π)) β Β¬ π β€ π) |
33 | | simpl3 1194 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ Β¬ π β€ π)) β π β π΅) |
34 | | simprr 772 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ Β¬ π β€ π)) β Β¬ π β€ π) |
35 | 6, 7, 8, 9 | dihord4 39771 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β ((πΌβπ) β (πΌβπ) β π β€ π)) |
36 | 30, 31, 32, 33, 34, 35 | syl122anc 1380 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ Β¬ π β€ π)) β ((πΌβπ) β (πΌβπ) β π β€ π)) |
37 | 11, 20, 29, 36 | 4casesdan 1041 |
1
β’ (((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β ((πΌβπ) β (πΌβπ) β π β€ π)) |