Step | Hyp | Ref
| Expression |
1 | | dva1dim.h |
. . . . . . . . . 10
β’ π» = (LHypβπΎ) |
2 | | dva1dim.t |
. . . . . . . . . 10
β’ π = ((LTrnβπΎ)βπ) |
3 | | dva1dim.e |
. . . . . . . . . 10
β’ πΈ = ((TEndoβπΎ)βπ) |
4 | 1, 2, 3 | tendocl 40149 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (π βπΉ) β π) |
5 | | dva1dim.l |
. . . . . . . . . 10
β’ β€ =
(leβπΎ) |
6 | | dva1dim.r |
. . . . . . . . . 10
β’ π
= ((trLβπΎ)βπ) |
7 | 5, 1, 2, 6, 3 | tendotp 40143 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (π
β(π βπΉ)) β€ (π
βπΉ)) |
8 | 4, 7 | jca 511 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β ((π βπΉ) β π β§ (π
β(π βπΉ)) β€ (π
βπΉ))) |
9 | 8 | 3expb 1117 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΉ β π)) β ((π βπΉ) β π β§ (π
β(π βπΉ)) β€ (π
βπΉ))) |
10 | 9 | anass1rs 652 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β πΈ) β ((π βπΉ) β π β§ (π
β(π βπΉ)) β€ (π
βπΉ))) |
11 | | eleq1 2815 |
. . . . . . 7
β’ (π = (π βπΉ) β (π β π β (π βπΉ) β π)) |
12 | | fveq2 6884 |
. . . . . . . 8
β’ (π = (π βπΉ) β (π
βπ) = (π
β(π βπΉ))) |
13 | 12 | breq1d 5151 |
. . . . . . 7
β’ (π = (π βπΉ) β ((π
βπ) β€ (π
βπΉ) β (π
β(π βπΉ)) β€ (π
βπΉ))) |
14 | 11, 13 | anbi12d 630 |
. . . . . 6
β’ (π = (π βπΉ) β ((π β π β§ (π
βπ) β€ (π
βπΉ)) β ((π βπΉ) β π β§ (π
β(π βπΉ)) β€ (π
βπΉ)))) |
15 | 10, 14 | syl5ibrcom 246 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β πΈ) β (π = (π βπΉ) β (π β π β§ (π
βπ) β€ (π
βπΉ)))) |
16 | 15 | rexlimdva 3149 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (βπ β πΈ π = (π βπΉ) β (π β π β§ (π
βπ) β€ (π
βπΉ)))) |
17 | | simpll 764 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π β§ (π
βπ) β€ (π
βπΉ))) β (πΎ β HL β§ π β π»)) |
18 | | simplr 766 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π β§ (π
βπ) β€ (π
βπΉ))) β πΉ β π) |
19 | | simprl 768 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π β§ (π
βπ) β€ (π
βπΉ))) β π β π) |
20 | | simprr 770 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π β§ (π
βπ) β€ (π
βπΉ))) β (π
βπ) β€ (π
βπΉ)) |
21 | 5, 1, 2, 6, 3 | tendoex 40357 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π
βπ) β€ (π
βπΉ)) β βπ β πΈ (π βπΉ) = π) |
22 | 17, 18, 19, 20, 21 | syl121anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π β§ (π
βπ) β€ (π
βπΉ))) β βπ β πΈ (π βπΉ) = π) |
23 | | eqcom 2733 |
. . . . . . 7
β’ ((π βπΉ) = π β π = (π βπΉ)) |
24 | 23 | rexbii 3088 |
. . . . . 6
β’
(βπ β
πΈ (π βπΉ) = π β βπ β πΈ π = (π βπΉ)) |
25 | 22, 24 | sylib 217 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ (π β π β§ (π
βπ) β€ (π
βπΉ))) β βπ β πΈ π = (π βπΉ)) |
26 | 25 | ex 412 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β ((π β π β§ (π
βπ) β€ (π
βπΉ)) β βπ β πΈ π = (π βπΉ))) |
27 | 16, 26 | impbid 211 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (βπ β πΈ π = (π βπΉ) β (π β π β§ (π
βπ) β€ (π
βπΉ)))) |
28 | 27 | abbidv 2795 |
. 2
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β {π β£ βπ β πΈ π = (π βπΉ)} = {π β£ (π β π β§ (π
βπ) β€ (π
βπΉ))}) |
29 | | df-rab 3427 |
. 2
β’ {π β π β£ (π
βπ) β€ (π
βπΉ)} = {π β£ (π β π β§ (π
βπ) β€ (π
βπΉ))} |
30 | 28, 29 | eqtr4di 2784 |
1
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β {π β£ βπ β πΈ π = (π βπΉ)} = {π β π β£ (π
βπ) β€ (π
βπΉ)}) |