Step | Hyp | Ref
| Expression |
1 | | elex 3464 |
. 2
β’ (πΎ β π β πΎ β V) |
2 | | fveq2 6843 |
. . . . 5
β’ (π = πΎ β (LHypβπ) = (LHypβπΎ)) |
3 | | tendoset.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | eqtr4di 2795 |
. . . 4
β’ (π = πΎ β (LHypβπ) = π») |
5 | | fveq2 6843 |
. . . . . . . 8
β’ (π = πΎ β (LTrnβπ) = (LTrnβπΎ)) |
6 | 5 | fveq1d 6845 |
. . . . . . 7
β’ (π = πΎ β ((LTrnβπ)βπ€) = ((LTrnβπΎ)βπ€)) |
7 | 6, 6 | feq23d 6664 |
. . . . . 6
β’ (π = πΎ β (π :((LTrnβπ)βπ€)βΆ((LTrnβπ)βπ€) β π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€))) |
8 | 6 | raleqdv 3314 |
. . . . . . 7
β’ (π = πΎ β (βπ β ((LTrnβπ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)))) |
9 | 6, 8 | raleqbidv 3320 |
. . . . . 6
β’ (π = πΎ β (βπ β ((LTrnβπ)βπ€)βπ β ((LTrnβπ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)))) |
10 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = πΎ β (trLβπ) = (trLβπΎ)) |
11 | 10 | fveq1d 6845 |
. . . . . . . . 9
β’ (π = πΎ β ((trLβπ)βπ€) = ((trLβπΎ)βπ€)) |
12 | 11 | fveq1d 6845 |
. . . . . . . 8
β’ (π = πΎ β (((trLβπ)βπ€)β(π βπ)) = (((trLβπΎ)βπ€)β(π βπ))) |
13 | | fveq2 6843 |
. . . . . . . . 9
β’ (π = πΎ β (leβπ) = (leβπΎ)) |
14 | | tendoset.l |
. . . . . . . . 9
β’ β€ =
(leβπΎ) |
15 | 13, 14 | eqtr4di 2795 |
. . . . . . . 8
β’ (π = πΎ β (leβπ) = β€ ) |
16 | 11 | fveq1d 6845 |
. . . . . . . 8
β’ (π = πΎ β (((trLβπ)βπ€)βπ) = (((trLβπΎ)βπ€)βπ)) |
17 | 12, 15, 16 | breq123d 5120 |
. . . . . . 7
β’ (π = πΎ β ((((trLβπ)βπ€)β(π βπ))(leβπ)(((trLβπ)βπ€)βπ) β (((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))) |
18 | 6, 17 | raleqbidv 3320 |
. . . . . 6
β’ (π = πΎ β (βπ β ((LTrnβπ)βπ€)(((trLβπ)βπ€)β(π βπ))(leβπ)(((trLβπ)βπ€)βπ) β βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))) |
19 | 7, 9, 18 | 3anbi123d 1437 |
. . . . 5
β’ (π = πΎ β ((π :((LTrnβπ)βπ€)βΆ((LTrnβπ)βπ€) β§ βπ β ((LTrnβπ)βπ€)βπ β ((LTrnβπ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπ)βπ€)(((trLβπ)βπ€)β(π βπ))(leβπ)(((trLβπ)βπ€)βπ)) β (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ)))) |
20 | 19 | abbidv 2806 |
. . . 4
β’ (π = πΎ β {π β£ (π :((LTrnβπ)βπ€)βΆ((LTrnβπ)βπ€) β§ βπ β ((LTrnβπ)βπ€)βπ β ((LTrnβπ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπ)βπ€)(((trLβπ)βπ€)β(π βπ))(leβπ)(((trLβπ)βπ€)βπ))} = {π β£ (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))}) |
21 | 4, 20 | mpteq12dv 5197 |
. . 3
β’ (π = πΎ β (π€ β (LHypβπ) β¦ {π β£ (π :((LTrnβπ)βπ€)βΆ((LTrnβπ)βπ€) β§ βπ β ((LTrnβπ)βπ€)βπ β ((LTrnβπ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπ)βπ€)(((trLβπ)βπ€)β(π βπ))(leβπ)(((trLβπ)βπ€)βπ))}) = (π€ β π» β¦ {π β£ (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))})) |
22 | | df-tendo 39221 |
. . 3
β’ TEndo =
(π β V β¦ (π€ β (LHypβπ) β¦ {π β£ (π :((LTrnβπ)βπ€)βΆ((LTrnβπ)βπ€) β§ βπ β ((LTrnβπ)βπ€)βπ β ((LTrnβπ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπ)βπ€)(((trLβπ)βπ€)β(π βπ))(leβπ)(((trLβπ)βπ€)βπ))})) |
23 | 21, 22, 3 | mptfvmpt 7179 |
. 2
β’ (πΎ β V β
(TEndoβπΎ) = (π€ β π» β¦ {π β£ (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))})) |
24 | 1, 23 | syl 17 |
1
β’ (πΎ β π β (TEndoβπΎ) = (π€ β π» β¦ {π β£ (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))})) |