Step | Hyp | Ref
| Expression |
1 | | eqop 7967 |
. . . . 5
β’ (π β (π Γ πΈ) β (π = β¨(π βπΉ), 0 β© β
((1st βπ)
= (π βπΉ) β§ (2nd
βπ) = 0
))) |
2 | 1 | adantl 483 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β (π Γ πΈ)) β (π = β¨(π βπΉ), 0 β© β
((1st βπ)
= (π βπΉ) β§ (2nd
βπ) = 0
))) |
3 | 2 | rexbidv 3172 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β (π Γ πΈ)) β (βπ β πΈ π = β¨(π βπΉ), 0 β© β βπ β πΈ ((1st βπ) = (π βπΉ) β§ (2nd βπ) = 0 ))) |
4 | | r19.41v 3182 |
. . . 4
β’
(βπ β
πΈ ((1st
βπ) = (π βπΉ) β§ (2nd βπ) = 0 ) β (βπ β πΈ (1st βπ) = (π βπΉ) β§ (2nd βπ) = 0 )) |
5 | | fvex 6859 |
. . . . . . . 8
β’
(1st βπ) β V |
6 | | eqeq1 2737 |
. . . . . . . . 9
β’ (π = (1st βπ) β (π = (π βπΉ) β (1st βπ) = (π βπΉ))) |
7 | 6 | rexbidv 3172 |
. . . . . . . 8
β’ (π = (1st βπ) β (βπ β πΈ π = (π βπΉ) β βπ β πΈ (1st βπ) = (π βπΉ))) |
8 | 5, 7 | elab 3634 |
. . . . . . 7
β’
((1st βπ) β {π β£ βπ β πΈ π = (π βπΉ)} β βπ β πΈ (1st βπ) = (π βπΉ)) |
9 | | dvhb1dim.l |
. . . . . . . . . 10
β’ β€ =
(leβπΎ) |
10 | | dvhb1dim.h |
. . . . . . . . . 10
β’ π» = (LHypβπΎ) |
11 | | dvhb1dim.t |
. . . . . . . . . 10
β’ π = ((LTrnβπΎ)βπ) |
12 | | dvhb1dim.r |
. . . . . . . . . 10
β’ π
= ((trLβπΎ)βπ) |
13 | | dvhb1dim.e |
. . . . . . . . . 10
β’ πΈ = ((TEndoβπΎ)βπ) |
14 | 9, 10, 11, 12, 13 | dva1dim 39498 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β {π β£ βπ β πΈ π = (π βπΉ)} = {π β π β£ (π
βπ) β€ (π
βπΉ)}) |
15 | 14 | adantr 482 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β (π Γ πΈ)) β {π β£ βπ β πΈ π = (π βπΉ)} = {π β π β£ (π
βπ) β€ (π
βπΉ)}) |
16 | 15 | eleq2d 2820 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β (π Γ πΈ)) β ((1st βπ) β {π β£ βπ β πΈ π = (π βπΉ)} β (1st βπ) β {π β π β£ (π
βπ) β€ (π
βπΉ)})) |
17 | 8, 16 | bitr3id 285 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β (π Γ πΈ)) β (βπ β πΈ (1st βπ) = (π βπΉ) β (1st βπ) β {π β π β£ (π
βπ) β€ (π
βπΉ)})) |
18 | | xp1st 7957 |
. . . . . . . 8
β’ (π β (π Γ πΈ) β (1st βπ) β π) |
19 | 18 | adantl 483 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β (π Γ πΈ)) β (1st βπ) β π) |
20 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = (1st βπ) β (π
βπ) = (π
β(1st βπ))) |
21 | 20 | breq1d 5119 |
. . . . . . . 8
β’ (π = (1st βπ) β ((π
βπ) β€ (π
βπΉ) β (π
β(1st βπ)) β€ (π
βπΉ))) |
22 | 21 | elrab3 3650 |
. . . . . . 7
β’
((1st βπ) β π β ((1st βπ) β {π β π β£ (π
βπ) β€ (π
βπΉ)} β (π
β(1st βπ)) β€ (π
βπΉ))) |
23 | 19, 22 | syl 17 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β (π Γ πΈ)) β ((1st βπ) β {π β π β£ (π
βπ) β€ (π
βπΉ)} β (π
β(1st βπ)) β€ (π
βπΉ))) |
24 | 17, 23 | bitrd 279 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β (π Γ πΈ)) β (βπ β πΈ (1st βπ) = (π βπΉ) β (π
β(1st βπ)) β€ (π
βπΉ))) |
25 | 24 | anbi1d 631 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β (π Γ πΈ)) β ((βπ β πΈ (1st βπ) = (π βπΉ) β§ (2nd βπ) = 0 ) β ((π
β(1st
βπ)) β€ (π
βπΉ) β§ (2nd βπ) = 0 ))) |
26 | 4, 25 | bitrid 283 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β (π Γ πΈ)) β (βπ β πΈ ((1st βπ) = (π βπΉ) β§ (2nd βπ) = 0 ) β ((π
β(1st
βπ)) β€ (π
βπΉ) β§ (2nd βπ) = 0 ))) |
27 | 3, 26 | bitrd 279 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π) β§ π β (π Γ πΈ)) β (βπ β πΈ π = β¨(π βπΉ), 0 β© β ((π
β(1st
βπ)) β€ (π
βπΉ) β§ (2nd βπ) = 0 ))) |
28 | 27 | rabbidva 3413 |
1
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β {π β (π Γ πΈ) β£ βπ β πΈ π = β¨(π βπΉ), 0 β©} = {π β (π Γ πΈ) β£ ((π
β(1st βπ)) β€ (π
βπΉ) β§ (2nd βπ) = 0 )}) |