Step | Hyp | Ref
| Expression |
1 | | ovolval2.a |
. . 3
β’ (π β π΄ β β) |
2 | | eqid 2732 |
. . . 4
β’ {π¦ β β*
β£ βπ β ((
β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < ))} = {π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ = sup(ran seq1( + , ((abs
β β ) β π)), β*, <
))} |
3 | 2 | ovolval 24981 |
. . 3
β’ (π΄ β β β
(vol*βπ΄) = inf({π¦ β β*
β£ βπ β ((
β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < ))}, β*, < )) |
4 | 1, 3 | syl 17 |
. 2
β’ (π β (vol*βπ΄) = inf({π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ))},
β*, < )) |
5 | 2 | a1i 11 |
. . . 4
β’ (π β {π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ))} = {π¦ β β*
β£ βπ β ((
β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < ))}) |
6 | | reex 11197 |
. . . . . . . . . . . . . . 15
β’ β
β V |
7 | 6, 6 | xpex 7736 |
. . . . . . . . . . . . . 14
β’ (β
Γ β) β V |
8 | | inss2 4228 |
. . . . . . . . . . . . . 14
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
9 | | mapss 8879 |
. . . . . . . . . . . . . 14
β’
(((β Γ β) β V β§ ( β€ β© (β Γ
β)) β (β Γ β)) β (( β€ β© (β
Γ β)) βm β) β ((β Γ
β) βm β)) |
10 | 7, 8, 9 | mp2an 690 |
. . . . . . . . . . . . 13
β’ (( β€
β© (β Γ β)) βm β) β ((β
Γ β) βm β) |
11 | 10 | sseli 3977 |
. . . . . . . . . . . 12
β’ (π β (( β€ β© (β
Γ β)) βm β) β π β ((β Γ β)
βm β)) |
12 | | 1zzd 12589 |
. . . . . . . . . . . 12
β’ (π β ((β Γ
β) βm β) β 1 β β€) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
β’ (π β (( β€ β© (β
Γ β)) βm β) β 1 β
β€) |
14 | 13 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β 1 β
β€) |
15 | | nnuz 12861 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
16 | | absfico 43902 |
. . . . . . . . . . . . . 14
β’
abs:ββΆ(0[,)+β) |
17 | | subf 11458 |
. . . . . . . . . . . . . 14
β’ β
:(β Γ β)βΆβ |
18 | | fco 6738 |
. . . . . . . . . . . . . 14
β’
((abs:ββΆ(0[,)+β) β§ β :(β Γ
β)βΆβ) β (abs β β ):(β Γ
β)βΆ(0[,)+β)) |
19 | 16, 17, 18 | mp2an 690 |
. . . . . . . . . . . . 13
β’ (abs
β β ):(β Γ
β)βΆ(0[,)+β) |
20 | 19 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (( β€ β© (β
Γ β)) βm β) β (abs β β
):(β Γ β)βΆ(0[,)+β)) |
21 | | rr2sscn2 44062 |
. . . . . . . . . . . . 13
β’ (β
Γ β) β (β Γ β) |
22 | 21 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β (( β€ β© (β
Γ β)) βm β) β (β Γ β)
β (β Γ β)) |
23 | | elmapi 8839 |
. . . . . . . . . . . . 13
β’ (π β ((β Γ
β) βm β) β π:ββΆ(β Γ
β)) |
24 | 11, 23 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (( β€ β© (β
Γ β)) βm β) β π:ββΆ(β Γ
β)) |
25 | 20, 22, 24 | fcoss 43894 |
. . . . . . . . . . 11
β’ (π β (( β€ β© (β
Γ β)) βm β) β ((abs β β )
β π):ββΆ(0[,)+β)) |
26 | 25 | adantl 482 |
. . . . . . . . . 10
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β ((abs β β ) β
π):ββΆ(0[,)+β)) |
27 | | eqid 2732 |
. . . . . . . . . 10
β’ seq1( + ,
((abs β β ) β π)) = seq1( + , ((abs β β )
β π)) |
28 | 14, 15, 26, 27 | sge0seq 45148 |
. . . . . . . . 9
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β
(Ξ£^β((abs β β ) β π)) = sup(ran seq1( + , ((abs
β β ) β π)), β*, <
)) |
29 | 28 | eqcomd 2738 |
. . . . . . . 8
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β sup(ran seq1( + , ((abs β
β ) β π)),
β*, < ) = (Ξ£^β((abs
β β ) β π))) |
30 | 29 | eqeq2d 2743 |
. . . . . . 7
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β (π¦ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < ) β π¦ =
(Ξ£^β((abs β β ) β π)))) |
31 | 30 | anbi2d 629 |
. . . . . 6
β’ ((π β§ π β (( β€ β© (β Γ
β)) βm β)) β ((π΄ β βͺ ran
((,) β π) β§ π¦ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < )) β
(π΄ β βͺ ran ((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π))))) |
32 | 31 | rexbidva 3176 |
. . . . 5
β’ (π β (βπ β (( β€ β© (β Γ
β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < )) β
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π))))) |
33 | 32 | rabbidv 3440 |
. . . 4
β’ (π β {π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ))} = {π¦ β β*
β£ βπ β ((
β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π)))}) |
34 | | ovolval2.m |
. . . . . 6
β’ π = {π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π)))} |
35 | 34 | eqcomi 2741 |
. . . . 5
β’ {π¦ β β*
β£ βπ β ((
β€ β© (β Γ β)) βm β)(π΄ β βͺ ran ((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π)))} = π |
36 | 35 | a1i 11 |
. . . 4
β’ (π β {π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ =
(Ξ£^β((abs β β ) β π)))} = π) |
37 | 5, 33, 36 | 3eqtrd 2776 |
. . 3
β’ (π β {π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ))} = π) |
38 | 37 | infeq1d 9468 |
. 2
β’ (π β inf({π¦ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π΄ β βͺ ran
((,) β π) β§ π¦ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ))},
β*, < ) = inf(π, β*, <
)) |
39 | 4, 38 | eqtrd 2772 |
1
β’ (π β (vol*βπ΄) = inf(π, β*, <
)) |