Step | Hyp | Ref
| Expression |
1 | | simpl1 1192 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β§ π = 0 ) β (πΎ β HL β§ π β π»)) |
2 | | cdleml1.b |
. . . . 5
β’ π΅ = (BaseβπΎ) |
3 | | cdleml1.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | | cdleml1.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
5 | | cdleml1.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
6 | | cdleml3.o |
. . . . 5
β’ 0 = (π β π β¦ ( I βΎ π΅)) |
7 | 2, 3, 4, 5, 6 | tendo0cl 39303 |
. . . 4
β’ ((πΎ β HL β§ π β π») β 0 β πΈ) |
8 | 1, 7 | syl 17 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β§ π = 0 ) β 0 β πΈ) |
9 | | simpl2l 1227 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β§ π = 0 ) β π β πΈ) |
10 | 2, 3, 4, 5, 6 | tendo0mul 39339 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β ( 0 β π) = 0 ) |
11 | 1, 9, 10 | syl2anc 585 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β§ π = 0 ) β ( 0 β π) = 0 ) |
12 | | simpr 486 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β§ π = 0 ) β π = 0 ) |
13 | 11, 12 | eqtr4d 2776 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β§ π = 0 ) β ( 0 β π) = π) |
14 | | coeq1 5817 |
. . . . 5
β’ (π = 0 β (π β π) = ( 0 β π)) |
15 | 14 | eqeq1d 2735 |
. . . 4
β’ (π = 0 β ((π β π) = π β ( 0 β π) = π)) |
16 | 15 | rspcev 3583 |
. . 3
β’ (( 0 β πΈ β§ ( 0 β π) = π) β βπ β πΈ (π β π) = π) |
17 | 8, 13, 16 | syl2anc 585 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β§ π = 0 ) β βπ β πΈ (π β π) = π) |
18 | | simpl1 1192 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β§ π β 0 ) β (πΎ β HL β§ π β π»)) |
19 | | simpl2 1193 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β§ π β 0 ) β (π β πΈ β§ π β πΈ)) |
20 | | simpl3 1194 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β§ π β 0 ) β π β 0 ) |
21 | | simpr 486 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β§ π β 0 ) β π β 0 ) |
22 | | cdleml1.r |
. . . 4
β’ π
= ((trLβπΎ)βπ) |
23 | 2, 3, 4, 22, 5, 6 | cdleml4N 39492 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (π β 0 β§ π β 0 )) β βπ β πΈ (π β π) = π) |
24 | 18, 19, 20, 21, 23 | syl112anc 1375 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β§ π β 0 ) β βπ β πΈ (π β π) = π) |
25 | 17, 24 | pm2.61dane 3029 |
1
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β βπ β πΈ (π β π) = π) |