Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (πΎ β HL β§ π β π»)) |
2 | | simp21 1207 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β π β πΈ) |
3 | | simp23 1209 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β π β π) |
4 | | cdleml1.h |
. . . 4
β’ π» = (LHypβπΎ) |
5 | | cdleml1.t |
. . . 4
β’ π = ((LTrnβπΎ)βπ) |
6 | | cdleml1.e |
. . . 4
β’ πΈ = ((TEndoβπΎ)βπ) |
7 | 4, 5, 6 | tendocl 39280 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (πβπ) β π) |
8 | 1, 2, 3, 7 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (πβπ) β π) |
9 | | simp22 1208 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β π β πΈ) |
10 | 4, 5, 6 | tendocl 39280 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (πβπ) β π) |
11 | 1, 9, 3, 10 | syl3anc 1372 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (πβπ) β π) |
12 | | cdleml1.b |
. . 3
β’ π΅ = (BaseβπΎ) |
13 | | cdleml1.r |
. . 3
β’ π
= ((trLβπΎ)βπ) |
14 | 12, 4, 5, 13, 6 | cdleml1N 39489 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (π
β(πβπ)) = (π
β(πβπ))) |
15 | 4, 5, 13, 6 | cdlemk 39487 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((πβπ) β π β§ (πβπ) β π) β§ (π
β(πβπ)) = (π
β(πβπ))) β βπ β πΈ (π β(πβπ)) = (πβπ)) |
16 | 1, 8, 11, 14, 15 | syl121anc 1376 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β βπ β πΈ (π β(πβπ)) = (πβπ)) |