Step | Hyp | Ref
| Expression |
1 | | tendoid.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
2 | | tendoid.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
3 | | eqid 2737 |
. . . . . . 7
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
4 | 1, 2, 3 | idltrn 38616 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β ( I βΎ π΅) β ((LTrnβπΎ)βπ)) |
5 | 4 | adantr 482 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β ( I βΎ π΅) β ((LTrnβπΎ)βπ)) |
6 | | eqid 2737 |
. . . . . 6
β’
(leβπΎ) =
(leβπΎ) |
7 | | eqid 2737 |
. . . . . 6
β’
((trLβπΎ)βπ) = ((trLβπΎ)βπ) |
8 | | tendoid.e |
. . . . . 6
β’ πΈ = ((TEndoβπΎ)βπ) |
9 | 6, 2, 3, 7, 8 | tendotp 39227 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ ( I βΎ π΅) β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβ( I βΎ π΅)))(leβπΎ)(((trLβπΎ)βπ)β( I βΎ π΅))) |
10 | 5, 9 | mpd3an3 1463 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (((trLβπΎ)βπ)β(πβ( I βΎ π΅)))(leβπΎ)(((trLβπΎ)βπ)β( I βΎ π΅))) |
11 | | eqid 2737 |
. . . . . 6
β’
(0.βπΎ) =
(0.βπΎ) |
12 | 1, 11, 2, 7 | trlid0 38642 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (((trLβπΎ)βπ)β( I βΎ π΅)) = (0.βπΎ)) |
13 | 12 | adantr 482 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (((trLβπΎ)βπ)β( I βΎ π΅)) = (0.βπΎ)) |
14 | 10, 13 | breqtrd 5132 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (((trLβπΎ)βπ)β(πβ( I βΎ π΅)))(leβπΎ)(0.βπΎ)) |
15 | | hlop 37827 |
. . . . 5
β’ (πΎ β HL β πΎ β OP) |
16 | 15 | ad2antrr 725 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β πΎ β OP) |
17 | 2, 3, 8 | tendocl 39233 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ ( I βΎ π΅) β ((LTrnβπΎ)βπ)) β (πβ( I βΎ π΅)) β ((LTrnβπΎ)βπ)) |
18 | 5, 17 | mpd3an3 1463 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πβ( I βΎ π΅)) β ((LTrnβπΎ)βπ)) |
19 | 1, 2, 3, 7 | trlcl 38630 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πβ( I βΎ π΅)) β ((LTrnβπΎ)βπ)) β (((trLβπΎ)βπ)β(πβ( I βΎ π΅))) β π΅) |
20 | 18, 19 | syldan 592 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (((trLβπΎ)βπ)β(πβ( I βΎ π΅))) β π΅) |
21 | 1, 6, 11 | ople0 37652 |
. . . 4
β’ ((πΎ β OP β§
(((trLβπΎ)βπ)β(πβ( I βΎ π΅))) β π΅) β ((((trLβπΎ)βπ)β(πβ( I βΎ π΅)))(leβπΎ)(0.βπΎ) β (((trLβπΎ)βπ)β(πβ( I βΎ π΅))) = (0.βπΎ))) |
22 | 16, 20, 21 | syl2anc 585 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β ((((trLβπΎ)βπ)β(πβ( I βΎ π΅)))(leβπΎ)(0.βπΎ) β (((trLβπΎ)βπ)β(πβ( I βΎ π΅))) = (0.βπΎ))) |
23 | 14, 22 | mpbid 231 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (((trLβπΎ)βπ)β(πβ( I βΎ π΅))) = (0.βπΎ)) |
24 | 1, 11, 2, 3, 7 | trlid0b 38644 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πβ( I βΎ π΅)) β ((LTrnβπΎ)βπ)) β ((πβ( I βΎ π΅)) = ( I βΎ π΅) β (((trLβπΎ)βπ)β(πβ( I βΎ π΅))) = (0.βπΎ))) |
25 | 18, 24 | syldan 592 |
. 2
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β ((πβ( I βΎ π΅)) = ( I βΎ π΅) β (((trLβπΎ)βπ)β(πβ( I βΎ π΅))) = (0.βπΎ))) |
26 | 23, 25 | mpbird 257 |
1
β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πβ( I βΎ π΅)) = ( I βΎ π΅)) |