Step | Hyp | Ref
| Expression |
1 | | ioorf.1 |
. . . . . 6
β’ πΉ = (π₯ β ran (,) β¦ if(π₯ = β
, β¨0, 0β©, β¨inf(π₯, β*, < ),
sup(π₯, β*,
< )β©)) |
2 | 1 | ioorf 24960 |
. . . . 5
β’ πΉ:ran (,)βΆ( β€ β©
(β* Γ β*)) |
3 | 2 | ffvelcdmi 7038 |
. . . 4
β’ (π΄ β ran (,) β (πΉβπ΄) β ( β€ β© (β*
Γ β*))) |
4 | 3 | adantr 482 |
. . 3
β’ ((π΄ β ran (,) β§
(vol*βπ΄) β
β) β (πΉβπ΄) β ( β€ β© (β*
Γ β*))) |
5 | 4 | elin1d 4162 |
. 2
β’ ((π΄ β ran (,) β§
(vol*βπ΄) β
β) β (πΉβπ΄) β β€ ) |
6 | 1 | ioorval 24961 |
. . . . . 6
β’ (π΄ β ran (,) β (πΉβπ΄) = if(π΄ = β
, β¨0, 0β©,
β¨inf(π΄,
β*, < ), sup(π΄, β*, <
)β©)) |
7 | 6 | adantr 482 |
. . . . 5
β’ ((π΄ β ran (,) β§
(vol*βπ΄) β
β) β (πΉβπ΄) = if(π΄ = β
, β¨0, 0β©,
β¨inf(π΄,
β*, < ), sup(π΄, β*, <
)β©)) |
8 | | iftrue 4496 |
. . . . 5
β’ (π΄ = β
β if(π΄ = β
, β¨0, 0β©,
β¨inf(π΄,
β*, < ), sup(π΄, β*, < )β©) =
β¨0, 0β©) |
9 | 7, 8 | sylan9eq 2793 |
. . . 4
β’ (((π΄ β ran (,) β§
(vol*βπ΄) β
β) β§ π΄ = β
)
β (πΉβπ΄) = β¨0,
0β©) |
10 | | 0re 11165 |
. . . . 5
β’ 0 β
β |
11 | | opelxpi 5674 |
. . . . 5
β’ ((0
β β β§ 0 β β) β β¨0, 0β© β (β
Γ β)) |
12 | 10, 10, 11 | mp2an 691 |
. . . 4
β’ β¨0,
0β© β (β Γ β) |
13 | 9, 12 | eqeltrdi 2842 |
. . 3
β’ (((π΄ β ran (,) β§
(vol*βπ΄) β
β) β§ π΄ = β
)
β (πΉβπ΄) β (β Γ
β)) |
14 | | ioof 13373 |
. . . . . 6
β’
(,):(β* Γ β*)βΆπ«
β |
15 | | ffn 6672 |
. . . . . 6
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
16 | | ovelrn 7534 |
. . . . . 6
β’ ((,) Fn
(β* Γ β*) β (π΄ β ran (,) β βπ β β*
βπ β
β* π΄ =
(π(,)π))) |
17 | 14, 15, 16 | mp2b 10 |
. . . . 5
β’ (π΄ β ran (,) β
βπ β
β* βπ β β* π΄ = (π(,)π)) |
18 | 1 | ioorinv2 24962 |
. . . . . . . . . 10
β’ ((π(,)π) β β
β (πΉβ(π(,)π)) = β¨π, πβ©) |
19 | 18 | adantl 483 |
. . . . . . . . 9
β’
(((vol*β(π(,)π)) β β β§ (π(,)π) β β
) β (πΉβ(π(,)π)) = β¨π, πβ©) |
20 | | ioorcl2 24959 |
. . . . . . . . . . 11
β’ (((π(,)π) β β
β§ (vol*β(π(,)π)) β β) β (π β β β§ π β β)) |
21 | 20 | ancoms 460 |
. . . . . . . . . 10
β’
(((vol*β(π(,)π)) β β β§ (π(,)π) β β
) β (π β β β§ π β β)) |
22 | | opelxpi 5674 |
. . . . . . . . . 10
β’ ((π β β β§ π β β) β
β¨π, πβ© β (β Γ
β)) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
β’
(((vol*β(π(,)π)) β β β§ (π(,)π) β β
) β β¨π, πβ© β (β Γ
β)) |
24 | 19, 23 | eqeltrd 2834 |
. . . . . . . 8
β’
(((vol*β(π(,)π)) β β β§ (π(,)π) β β
) β (πΉβ(π(,)π)) β (β Γ
β)) |
25 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π΄ = (π(,)π) β (vol*βπ΄) = (vol*β(π(,)π))) |
26 | 25 | eleq1d 2819 |
. . . . . . . . . 10
β’ (π΄ = (π(,)π) β ((vol*βπ΄) β β β (vol*β(π(,)π)) β β)) |
27 | | neeq1 3003 |
. . . . . . . . . 10
β’ (π΄ = (π(,)π) β (π΄ β β
β (π(,)π) β β
)) |
28 | 26, 27 | anbi12d 632 |
. . . . . . . . 9
β’ (π΄ = (π(,)π) β (((vol*βπ΄) β β β§ π΄ β β
) β ((vol*β(π(,)π)) β β β§ (π(,)π) β β
))) |
29 | | fveq2 6846 |
. . . . . . . . . 10
β’ (π΄ = (π(,)π) β (πΉβπ΄) = (πΉβ(π(,)π))) |
30 | 29 | eleq1d 2819 |
. . . . . . . . 9
β’ (π΄ = (π(,)π) β ((πΉβπ΄) β (β Γ β) β
(πΉβ(π(,)π)) β (β Γ
β))) |
31 | 28, 30 | imbi12d 345 |
. . . . . . . 8
β’ (π΄ = (π(,)π) β ((((vol*βπ΄) β β β§ π΄ β β
) β (πΉβπ΄) β (β Γ β)) β
(((vol*β(π(,)π)) β β β§ (π(,)π) β β
) β (πΉβ(π(,)π)) β (β Γ
β)))) |
32 | 24, 31 | mpbiri 258 |
. . . . . . 7
β’ (π΄ = (π(,)π) β (((vol*βπ΄) β β β§ π΄ β β
) β (πΉβπ΄) β (β Γ
β))) |
33 | 32 | a1i 11 |
. . . . . 6
β’ ((π β β*
β§ π β
β*) β (π΄ = (π(,)π) β (((vol*βπ΄) β β β§ π΄ β β
) β (πΉβπ΄) β (β Γ
β)))) |
34 | 33 | rexlimivv 3193 |
. . . . 5
β’
(βπ β
β* βπ β β* π΄ = (π(,)π) β (((vol*βπ΄) β β β§ π΄ β β
) β (πΉβπ΄) β (β Γ
β))) |
35 | 17, 34 | sylbi 216 |
. . . 4
β’ (π΄ β ran (,) β
(((vol*βπ΄) β
β β§ π΄ β
β
) β (πΉβπ΄) β (β Γ
β))) |
36 | 35 | impl 457 |
. . 3
β’ (((π΄ β ran (,) β§
(vol*βπ΄) β
β) β§ π΄ β
β
) β (πΉβπ΄) β (β Γ
β)) |
37 | 13, 36 | pm2.61dane 3029 |
. 2
β’ ((π΄ β ran (,) β§
(vol*βπ΄) β
β) β (πΉβπ΄) β (β Γ
β)) |
38 | 5, 37 | elind 4158 |
1
β’ ((π΄ β ran (,) β§
(vol*βπ΄) β
β) β (πΉβπ΄) β ( β€ β© (β Γ
β))) |