Step | Hyp | Ref
| Expression |
1 | | dva1dim.h |
. . . . . . . . . 10
β’ π» = (LHypβπΎ) |
2 | | dva1dim.t |
. . . . . . . . . 10
β’ π = ((LTrnβπΎ)βπ) |
3 | | dva1dim.e |
. . . . . . . . . 10
β’ πΈ = ((TEndoβπΎ)βπ) |
4 | 1, 2, 3 | tendocl 39280 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (π βπΉ) β π) |
5 | | dva1dim.l |
. . . . . . . . . 10
β’ β€ =
(leβπΎ) |
6 | | dva1dim.r |
. . . . . . . . . 10
β’ π
= ((trLβπΎ)βπ) |
7 | 5, 1, 2, 6, 3 | tendotp 39274 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (π
β(π βπΉ)) β€ (π
βπΉ)) |
8 | 4, 7 | jca 513 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β ((π βπΉ) β π β§ (π
β(π βπΉ)) β€ (π
βπΉ))) |
9 | 8 | 3expb 1121 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΉ β π)) β ((π βπΉ) β π β§ (π
β(π βπΉ)) β€ (π
βπΉ))) |
10 | 9 | anass1rs 654 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β πΈ) β ((π βπΉ) β π β§ (π
β(π βπΉ)) β€ (π
βπΉ))) |
11 | | eleq1 2822 |
. . . . . . 7
β’ (π = (π βπΉ) β (π β π β (π βπΉ) β π)) |
12 | | fveq2 6846 |
. . . . . . . 8
β’ (π = (π βπΉ) β (π
βπ) = (π
β(π βπΉ))) |
13 | 12 | breq1d 5119 |
. . . . . . 7
β’ (π = (π βπΉ) β ((π
βπ) β€ (π
βπΉ) β (π
β(π βπΉ)) β€ (π
βπΉ))) |
14 | 11, 13 | anbi12d 632 |
. . . . . 6
β’ (π = (π βπΉ) β ((π β π β§ (π
βπ) β€ (π
βπΉ)) β ((π βπΉ) β π β§ (π
β(π βπΉ)) β€ (π
βπΉ)))) |
15 | 10, 14 | syl5ibrcom 247 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β πΈ) β (π = (π βπΉ) β (π β π β§ (π
βπ) β€ (π
βπΉ)))) |
16 | 15 | rexlimdva 3149 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (βπ β πΈ π = (π βπΉ) β (π β π β§ (π
βπ) β€ (π
βπΉ)))) |
17 | | simpll 766 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π β§ (π
βπ) β€ (π
βπΉ))) β (πΎ β HL β§ π β π»)) |
18 | | simplr 768 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π β§ (π
βπ) β€ (π
βπΉ))) β πΉ β π) |
19 | | simprl 770 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π β§ (π
βπ) β€ (π
βπΉ))) β π β π) |
20 | | simprr 772 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π β§ (π
βπ) β€ (π
βπΉ))) β (π
βπ) β€ (π
βπΉ)) |
21 | 5, 1, 2, 6, 3 | tendoex 39488 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π
βπ) β€ (π
βπΉ)) β βπ β πΈ (π βπΉ) = π) |
22 | 17, 18, 19, 20, 21 | syl121anc 1376 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π β§ (π
βπ) β€ (π
βπΉ))) β βπ β πΈ (π βπΉ) = π) |
23 | | eqcom 2740 |
. . . . . . 7
β’ ((π βπΉ) = π β π = (π βπΉ)) |
24 | 23 | rexbii 3094 |
. . . . . 6
β’
(βπ β
πΈ (π βπΉ) = π β βπ β πΈ π = (π βπΉ)) |
25 | 22, 24 | sylib 217 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π β§ (π
βπ) β€ (π
βπΉ))) β βπ β πΈ π = (π βπΉ)) |
26 | 25 | ex 414 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β ((π β π β§ (π
βπ) β€ (π
βπΉ)) β βπ β πΈ π = (π βπΉ))) |
27 | 16, 26 | impbid 211 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (βπ β πΈ π = (π βπΉ) β (π β π β§ (π
βπ) β€ (π
βπΉ)))) |
28 | 27 | abbidv 2802 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β {π β£ βπ β πΈ π = (π βπΉ)} = {π β£ (π β π β§ (π
βπ) β€ (π
βπΉ))}) |
29 | | df-rab 3407 |
. 2
β’ {π β π β£ (π
βπ) β€ (π
βπΉ)} = {π β£ (π β π β§ (π
βπ) β€ (π
βπΉ))} |
30 | 28, 29 | eqtr4di 2791 |
1
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β {π β£ βπ β πΈ π = (π βπΉ)} = {π β π β£ (π
βπ) β€ (π
βπΉ)}) |