Step | Hyp | Ref
| Expression |
1 | | tendoset.e |
. 2
β’ πΈ = ((TEndoβπΎ)βπ) |
2 | | tendoset.l |
. . . . 5
β’ β€ =
(leβπΎ) |
3 | | tendoset.h |
. . . . 5
β’ π» = (LHypβπΎ) |
4 | 2, 3 | tendofset 39224 |
. . . 4
β’ (πΎ β π β (TEndoβπΎ) = (π€ β π» β¦ {π β£ (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))})) |
5 | 4 | fveq1d 6845 |
. . 3
β’ (πΎ β π β ((TEndoβπΎ)βπ) = ((π€ β π» β¦ {π β£ (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))})βπ)) |
6 | | fveq2 6843 |
. . . . . . . 8
β’ (π€ = π β ((LTrnβπΎ)βπ€) = ((LTrnβπΎ)βπ)) |
7 | 6, 6 | feq23d 6664 |
. . . . . . 7
β’ (π€ = π β (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ))) |
8 | 6 | raleqdv 3314 |
. . . . . . . 8
β’ (π€ = π β (βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β βπ β ((LTrnβπΎ)βπ)(π β(π β π)) = ((π βπ) β (π βπ)))) |
9 | 6, 8 | raleqbidv 3320 |
. . . . . . 7
β’ (π€ = π β (βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β βπ β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)(π β(π β π)) = ((π βπ) β (π βπ)))) |
10 | | fveq2 6843 |
. . . . . . . . . . 11
β’ (π€ = π β ((trLβπΎ)βπ€) = ((trLβπΎ)βπ)) |
11 | | tendoset.r |
. . . . . . . . . . 11
β’ π
= ((trLβπΎ)βπ) |
12 | 10, 11 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π€ = π β ((trLβπΎ)βπ€) = π
) |
13 | 12 | fveq1d 6845 |
. . . . . . . . 9
β’ (π€ = π β (((trLβπΎ)βπ€)β(π βπ)) = (π
β(π βπ))) |
14 | 12 | fveq1d 6845 |
. . . . . . . . 9
β’ (π€ = π β (((trLβπΎ)βπ€)βπ) = (π
βπ)) |
15 | 13, 14 | breq12d 5119 |
. . . . . . . 8
β’ (π€ = π β ((((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ) β (π
β(π βπ)) β€ (π
βπ))) |
16 | 6, 15 | raleqbidv 3320 |
. . . . . . 7
β’ (π€ = π β (βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ) β βπ β ((LTrnβπΎ)βπ)(π
β(π βπ)) β€ (π
βπ))) |
17 | 7, 9, 16 | 3anbi123d 1437 |
. . . . . 6
β’ (π€ = π β ((π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ)) β (π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ) β§ βπ β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ)(π
β(π βπ)) β€ (π
βπ)))) |
18 | 17 | abbidv 2806 |
. . . . 5
β’ (π€ = π β {π β£ (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))} = {π β£ (π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ) β§ βπ β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ)(π
β(π βπ)) β€ (π
βπ))}) |
19 | | eqid 2737 |
. . . . 5
β’ (π€ β π» β¦ {π β£ (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))}) = (π€ β π» β¦ {π β£ (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))}) |
20 | | fvex 6856 |
. . . . . . . 8
β’
((LTrnβπΎ)βπ) β V |
21 | 20, 20 | mapval 8778 |
. . . . . . 7
β’
(((LTrnβπΎ)βπ) βm ((LTrnβπΎ)βπ)) = {π β£ π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)} |
22 | | ovex 7391 |
. . . . . . 7
β’
(((LTrnβπΎ)βπ) βm ((LTrnβπΎ)βπ)) β V |
23 | 21, 22 | eqeltrri 2835 |
. . . . . 6
β’ {π β£ π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)} β V |
24 | | simp1 1137 |
. . . . . . 7
β’ ((π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ) β§ βπ β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ)(π
β(π βπ)) β€ (π
βπ)) β π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
25 | 24 | ss2abi 4024 |
. . . . . 6
β’ {π β£ (π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ) β§ βπ β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ)(π
β(π βπ)) β€ (π
βπ))} β {π β£ π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)} |
26 | 23, 25 | ssexi 5280 |
. . . . 5
β’ {π β£ (π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ) β§ βπ β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ)(π
β(π βπ)) β€ (π
βπ))} β V |
27 | 18, 19, 26 | fvmpt 6949 |
. . . 4
β’ (π β π» β ((π€ β π» β¦ {π β£ (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))})βπ) = {π β£ (π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ) β§ βπ β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ)(π
β(π βπ)) β€ (π
βπ))}) |
28 | | tendoset.t |
. . . . . . 7
β’ π = ((LTrnβπΎ)βπ) |
29 | 28, 28 | feq23i 6663 |
. . . . . 6
β’ (π :πβΆπ β π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ)) |
30 | 28 | raleqi 3312 |
. . . . . . 7
β’
(βπ β
π (π β(π β π)) = ((π βπ) β (π βπ)) β βπ β ((LTrnβπΎ)βπ)(π β(π β π)) = ((π βπ) β (π βπ))) |
31 | 28, 30 | raleqbii 3316 |
. . . . . 6
β’
(βπ β
π βπ β π (π β(π β π)) = ((π βπ) β (π βπ)) β βπ β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)(π β(π β π)) = ((π βπ) β (π βπ))) |
32 | 28 | raleqi 3312 |
. . . . . 6
β’
(βπ β
π (π
β(π βπ)) β€ (π
βπ) β βπ β ((LTrnβπΎ)βπ)(π
β(π βπ)) β€ (π
βπ)) |
33 | 29, 31, 32 | 3anbi123i 1156 |
. . . . 5
β’ ((π :πβΆπ β§ βπ β π βπ β π (π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β π (π
β(π βπ)) β€ (π
βπ)) β (π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ) β§ βπ β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ)(π
β(π βπ)) β€ (π
βπ))) |
34 | 33 | abbii 2807 |
. . . 4
β’ {π β£ (π :πβΆπ β§ βπ β π βπ β π (π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β π (π
β(π βπ)) β€ (π
βπ))} = {π β£ (π :((LTrnβπΎ)βπ)βΆ((LTrnβπΎ)βπ) β§ βπ β ((LTrnβπΎ)βπ)βπ β ((LTrnβπΎ)βπ)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ)(π
β(π βπ)) β€ (π
βπ))} |
35 | 27, 34 | eqtr4di 2795 |
. . 3
β’ (π β π» β ((π€ β π» β¦ {π β£ (π :((LTrnβπΎ)βπ€)βΆ((LTrnβπΎ)βπ€) β§ βπ β ((LTrnβπΎ)βπ€)βπ β ((LTrnβπΎ)βπ€)(π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β ((LTrnβπΎ)βπ€)(((trLβπΎ)βπ€)β(π βπ)) β€ (((trLβπΎ)βπ€)βπ))})βπ) = {π β£ (π :πβΆπ β§ βπ β π βπ β π (π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β π (π
β(π βπ)) β€ (π
βπ))}) |
36 | 5, 35 | sylan9eq 2797 |
. 2
β’ ((πΎ β π β§ π β π») β ((TEndoβπΎ)βπ) = {π β£ (π :πβΆπ β§ βπ β π βπ β π (π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β π (π
β(π βπ)) β€ (π
βπ))}) |
37 | 1, 36 | eqtrid 2789 |
1
β’ ((πΎ β π β§ π β π») β πΈ = {π β£ (π :πβΆπ β§ βπ β π βπ β π (π β(π β π)) = ((π βπ) β (π βπ)) β§ βπ β π (π
β(π βπ)) β€ (π
βπ))}) |