Step | Hyp | Ref
| Expression |
1 | | mblfinlem4 36523 |
. 2
β’ (((π΄ β β β§
(vol*βπ΄) β
β) β§ π΄ β dom
vol) β (vol*βπ΄)
= sup({π¦ β£
βπ β
(Clsdβ(topGenβran (,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) |
2 | | elpwi 4609 |
. . . . 5
β’ (π€ β π« β β
π€ β
β) |
3 | | elmapi 8842 |
. . . . . . . . . . . 12
β’ (π β (( β€ β© (β
Γ β)) βm β) β π:ββΆ( β€ β© (β Γ
β))) |
4 | | inss1 4228 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ β© π΄) β π€ |
5 | | ovolsscl 25002 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π€ β© π΄) β π€ β§ π€ β β β§ (vol*βπ€) β β) β
(vol*β(π€ β© π΄)) β
β) |
6 | 4, 5 | mp3an1 1448 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π€ β β β§
(vol*βπ€) β
β) β (vol*β(π€ β© π΄)) β β) |
7 | | difss 4131 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π€ β π΄) β π€ |
8 | | ovolsscl 25002 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π€ β π΄) β π€ β§ π€ β β β§ (vol*βπ€) β β) β
(vol*β(π€ β
π΄)) β
β) |
9 | 7, 8 | mp3an1 1448 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π€ β β β§
(vol*βπ€) β
β) β (vol*β(π€ β π΄)) β β) |
10 | 6, 9 | readdcld 11242 |
. . . . . . . . . . . . . . . . . 18
β’ ((π€ β β β§
(vol*βπ€) β
β) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β β) |
11 | 10 | rexrd 11263 |
. . . . . . . . . . . . . . . . 17
β’ ((π€ β β β§
(vol*βπ€) β
β) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β
β*) |
12 | 11 | ad3antlr 729 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π:ββΆ( β€ β© (β Γ
β))) β§ π€ β
βͺ ran ((,) β π)) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β
β*) |
13 | | rncoss 5971 |
. . . . . . . . . . . . . . . . . . 19
β’ ran ((,)
β π) β ran
(,) |
14 | 13 | unissi 4917 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ ran ((,) β π) β βͺ ran
(,) |
15 | | unirnioo 13425 |
. . . . . . . . . . . . . . . . . 18
β’ β =
βͺ ran (,) |
16 | 14, 15 | sseqtrri 4019 |
. . . . . . . . . . . . . . . . 17
β’ βͺ ran ((,) β π) β β |
17 | | ovolcl 24994 |
. . . . . . . . . . . . . . . . 17
β’ (βͺ ran ((,) β π) β β β (vol*ββͺ ran ((,) β π)) β
β*) |
18 | 16, 17 | mp1i 13 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π:ββΆ( β€ β© (β Γ
β))) β§ π€ β
βͺ ran ((,) β π)) β (vol*ββͺ ran ((,) β π)) β
β*) |
19 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . 19
β’ ((abs
β β ) β π) = ((abs β β ) β π) |
20 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . 19
β’ seq1( + ,
((abs β β ) β π)) = seq1( + , ((abs β β )
β π)) |
21 | 19, 20 | ovolsf 24988 |
. . . . . . . . . . . . . . . . . 18
β’ (π:ββΆ( β€ β©
(β Γ β)) β seq1( + , ((abs β β ) β
π)):ββΆ(0[,)+β)) |
22 | | frn 6724 |
. . . . . . . . . . . . . . . . . . 19
β’ (seq1( +
, ((abs β β ) β π)):ββΆ(0[,)+β) β ran
seq1( + , ((abs β β ) β π)) β (0[,)+β)) |
23 | | icossxr 13408 |
. . . . . . . . . . . . . . . . . . 19
β’
(0[,)+β) β β* |
24 | 22, 23 | sstrdi 3994 |
. . . . . . . . . . . . . . . . . 18
β’ (seq1( +
, ((abs β β ) β π)):ββΆ(0[,)+β) β ran
seq1( + , ((abs β β ) β π)) β
β*) |
25 | | supxrcl 13293 |
. . . . . . . . . . . . . . . . . 18
β’ (ran
seq1( + , ((abs β β ) β π)) β β* β sup(ran
seq1( + , ((abs β β ) β π)), β*, < ) β
β*) |
26 | 21, 24, 25 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
β’ (π:ββΆ( β€ β©
(β Γ β)) β sup(ran seq1( + , ((abs β β )
β π)),
β*, < ) β β*) |
27 | 26 | ad2antlr 725 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π:ββΆ( β€ β© (β Γ
β))) β§ π€ β
βͺ ran ((,) β π)) β sup(ran seq1( + , ((abs β
β ) β π)),
β*, < ) β β*) |
28 | | pnfge 13109 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((vol*β(π€
β© π΄)) +
(vol*β(π€ β
π΄))) β
β* β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ +β) |
29 | 11, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π€ β β β§
(vol*βπ€) β
β) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ +β) |
30 | 29 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π€ β β β§
(vol*βπ€) β
β) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) = +β) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ +β) |
31 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π€ β β β§
(vol*βπ€) β
β) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) = +β) β (vol*ββͺ ran ((,) β π)) = +β) |
32 | 30, 31 | breqtrrd 5176 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π€ β β β§
(vol*βπ€) β
β) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) = +β) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (vol*ββͺ ran ((,) β π))) |
33 | 32 | adantlll 716 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) = +β) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (vol*ββͺ ran ((,) β π))) |
34 | 16, 17 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(vol*ββͺ ran ((,) β π)) β
β* |
35 | | nltpnft 13142 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((vol*ββͺ ran ((,) β π)) β β*
β ((vol*ββͺ ran ((,) β π)) = +β β Β¬
(vol*ββͺ ran ((,) β π)) < +β)) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((vol*ββͺ ran ((,) β π)) = +β β Β¬
(vol*ββͺ ran ((,) β π)) < +β) |
37 | 36 | necon2abii 2991 |
. . . . . . . . . . . . . . . . . . . 20
β’
((vol*ββͺ ran ((,) β π)) < +β β
(vol*ββͺ ran ((,) β π)) β +β) |
38 | | ovolge0 24997 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (βͺ ran ((,) β π) β β β 0 β€
(vol*ββͺ ran ((,) β π))) |
39 | 16, 38 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 β€
(vol*ββͺ ran ((,) β π)) |
40 | | 0re 11215 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 0 β
β |
41 | | xrre3 13149 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((((vol*ββͺ ran ((,) β π)) β β*
β§ 0 β β) β§ (0 β€ (vol*ββͺ
ran ((,) β π)) β§
(vol*ββͺ ran ((,) β π)) < +β)) β (vol*ββͺ ran ((,) β π)) β β) |
42 | 34, 40, 41 | mpanl12 700 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((0 β€
(vol*ββͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) < +β) β (vol*ββͺ ran ((,) β π)) β β) |
43 | 39, 42 | mpan 688 |
. . . . . . . . . . . . . . . . . . . 20
β’
((vol*ββͺ ran ((,) β π)) < +β β
(vol*ββͺ ran ((,) β π)) β β) |
44 | 37, 43 | sylbir 234 |
. . . . . . . . . . . . . . . . . . 19
β’
((vol*ββͺ ran ((,) β π)) β +β β
(vol*ββͺ ran ((,) β π)) β β) |
45 | 10 | ad3antlr 729 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β β) |
46 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ)) β π§ = (volβπ)) |
47 | | eleq1w 2816 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β (π β dom vol β π β dom vol)) |
48 | | uniretop 24278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ β =
βͺ (topGenβran (,)) |
49 | 48 | cldss 22532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β
(Clsdβ(topGenβran (,))) β π β β) |
50 | | dfss4 4258 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β β β (β
β (β β π)) = π) |
51 | 49, 50 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β
(Clsdβ(topGenβran (,))) β (β β (β β
π)) = π) |
52 | | rembl 25056 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ β
β dom vol |
53 | 48 | cldopn 22534 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β
(Clsdβ(topGenβran (,))) β (β β π) β (topGenβran
(,))) |
54 | | opnmbl 25118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((β
β π) β
(topGenβran (,)) β (β β π) β dom vol) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π β
(Clsdβ(topGenβran (,))) β (β β π) β dom vol) |
56 | | difmbl 25059 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((β
β dom vol β§ (β β π) β dom vol) β (β β
(β β π)) β
dom vol) |
57 | 52, 55, 56 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π β
(Clsdβ(topGenβran (,))) β (β β (β β
π)) β dom
vol) |
58 | 51, 57 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π β
(Clsdβ(topGenβran (,))) β π β dom vol) |
59 | 47, 58 | vtoclga 3565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β
(Clsdβ(topGenβran (,))) β π β dom vol) |
60 | | mblvol 25046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β dom vol β
(volβπ) =
(vol*βπ)) |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β
(Clsdβ(topGenβran (,))) β (volβπ) = (vol*βπ)) |
62 | 46, 61 | sylan9eqr 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))) β π§ = (vol*βπ)) |
63 | 62 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ)))) β π§ = (vol*βπ)) |
64 | | inss1 4228 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (βͺ ran ((,) β π) β© π΄) β βͺ ran
((,) β π) |
65 | | sstr 3990 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β (βͺ ran ((,) β π) β© π΄) β§ (βͺ ran
((,) β π) β© π΄) β βͺ ran ((,) β π)) β π β βͺ ran
((,) β π)) |
66 | 64, 65 | mpan2 689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (βͺ ran ((,) β π) β© π΄) β π β βͺ ran
((,) β π)) |
67 | 66 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))) β π β βͺ ran
((,) β π)) |
68 | | ovolsscl 25002 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β βͺ ran ((,) β π) β§ βͺ ran ((,)
β π) β β
β§ (vol*ββͺ ran ((,) β π)) β β) β
(vol*βπ) β
β) |
69 | 16, 68 | mp3an2 1449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β βͺ ran ((,) β π) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*βπ) β
β) |
70 | 69 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((vol*ββͺ ran ((,) β π)) β β β§ π β βͺ ran ((,) β π)) β (vol*βπ) β β) |
71 | 67, 70 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ)))) β (vol*βπ) β β) |
72 | 63, 71 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ)))) β π§ β β) |
73 | 72 | rexlimdvaa 3156 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((vol*ββͺ ran ((,) β π)) β β β
(βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ)) β π§ β β)) |
74 | 73 | abssdv 4065 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((vol*ββͺ ran ((,) β π)) β β β {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))} β β) |
75 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π§ = π¦ β (π§ = (volβπ) β π¦ = (volβπ))) |
76 | 75 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ = π¦ β ((π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ)) β (π β (βͺ ran
((,) β π) β© π΄) β§ π¦ = (volβπ)))) |
77 | 76 | rexbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ = π¦ β (βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π¦ = (volβπ)))) |
78 | 77 | ralab 3687 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ¦ β
{π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}π¦ β€ (vol*ββͺ ran ((,) β π)) β βπ¦(βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π¦ = (volβπ)) β π¦ β€ (vol*ββͺ ran ((,) β π)))) |
79 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β (βͺ ran ((,) β π) β© π΄) β§ π¦ = (volβπ)) β π¦ = (volβπ)) |
80 | 79, 61 | sylan9eqr 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β© π΄) β§ π¦ = (volβπ))) β π¦ = (vol*βπ)) |
81 | | ovolss 25001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β βͺ ran ((,) β π) β§ βͺ ran ((,)
β π) β β)
β (vol*βπ) β€
(vol*ββͺ ran ((,) β π))) |
82 | 66, 16, 81 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (βͺ ran ((,) β π) β© π΄) β (vol*βπ) β€ (vol*ββͺ ran ((,) β π))) |
83 | 82 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β© π΄) β§ π¦ = (volβπ))) β (vol*βπ) β€ (vol*ββͺ ran ((,) β π))) |
84 | 80, 83 | eqbrtrd 5170 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β© π΄) β§ π¦ = (volβπ))) β π¦ β€ (vol*ββͺ ran ((,) β π))) |
85 | 84 | rexlimiva 3147 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π¦ = (volβπ)) β π¦ β€ (vol*ββͺ ran ((,) β π))) |
86 | 78, 85 | mpgbir 1801 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
βπ¦ β
{π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}π¦ β€ (vol*ββͺ ran ((,) β π)) |
87 | | brralrspcev 5208 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((vol*ββͺ ran ((,) β π)) β β β§
βπ¦ β {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}π¦ β€ (vol*ββͺ ran ((,) β π))) β βπ₯ β β βπ¦ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}π¦ β€ π₯) |
88 | 86, 87 | mpan2 689 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((vol*ββͺ ran ((,) β π)) β β β
βπ₯ β β
βπ¦ β {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}π¦ β€ π₯) |
89 | | retop 24277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(topGenβran (,)) β Top |
90 | | 0cld 22541 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((topGenβran (,)) β Top β β
β
(Clsdβ(topGenβran (,)))) |
91 | 89, 90 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ β
β (Clsdβ(topGenβran (,))) |
92 | | 0ss 4396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ β
β (βͺ ran ((,) β π) β© π΄) |
93 | | 0mbl 25055 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ β
β dom vol |
94 | | mblvol 25046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (β
β dom vol β (volββ
) =
(vol*ββ
)) |
95 | 93, 94 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(volββ
) = (vol*ββ
) |
96 | | ovol0 25009 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(vol*ββ
) = 0 |
97 | 95, 96 | eqtr2i 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ 0 =
(volββ
) |
98 | 92, 97 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (β
β (βͺ ran ((,) β π) β© π΄) β§ 0 =
(volββ
)) |
99 | | sseq1 4007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = β
β (π β (βͺ ran ((,) β π) β© π΄) β β
β (βͺ ran ((,) β π) β© π΄))) |
100 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = β
β
(volβπ) =
(volββ
)) |
101 | 100 | eqeq2d 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = β
β (0 =
(volβπ) β 0 =
(volββ
))) |
102 | 99, 101 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = β
β ((π β (βͺ ran ((,) β π) β© π΄) β§ 0 = (volβπ)) β (β
β (βͺ ran ((,) β π) β© π΄) β§ 0 =
(volββ
)))) |
103 | 102 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((β
β (Clsdβ(topGenβran (,))) β§ (β
β (βͺ ran ((,) β π) β© π΄) β§ 0 = (volββ
))) β
βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ 0 = (volβπ))) |
104 | 91, 98, 103 | mp2an 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ 0 = (volβπ)) |
105 | | c0ex 11207 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ 0 β
V |
106 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π§ = 0 β (π§ = (volβπ) β 0 = (volβπ))) |
107 | 106 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π§ = 0 β ((π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ)) β (π β (βͺ ran
((,) β π) β© π΄) β§ 0 = (volβπ)))) |
108 | 107 | rexbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ = 0 β (βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ 0 = (volβπ)))) |
109 | 105, 108 | elab 3668 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (0 β
{π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))} β βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ 0 = (volβπ))) |
110 | 104, 109 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 0 β
{π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))} |
111 | 110 | ne0ii 4337 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))} β β
|
112 | | suprcl 12173 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))} β β β§ {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))} β β
β§ βπ₯ β β βπ¦ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}π¦ β€ π₯) β sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}, β, < ) β
β) |
113 | 111, 112 | mp3an2 1449 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))} β β β§ βπ₯ β β βπ¦ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}π¦ β€ π₯) β sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}, β, < ) β
β) |
114 | 74, 88, 113 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((vol*ββͺ ran ((,) β π)) β β β
sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}, β, < ) β
β) |
115 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ)) β π§ = (volβπ)) |
116 | | eleq1w 2816 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β (π β dom vol β π β dom vol)) |
117 | 116, 58 | vtoclga 3565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β
(Clsdβ(topGenβran (,))) β π β dom vol) |
118 | | mblvol 25046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π β dom vol β
(volβπ) =
(vol*βπ)) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β
(Clsdβ(topGenβran (,))) β (volβπ) = (vol*βπ)) |
120 | 115, 119 | sylan9eqr 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))) β π§ = (vol*βπ)) |
121 | 120 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ)))) β π§ = (vol*βπ)) |
122 | | difss2 4133 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (βͺ ran ((,) β π) β π΄) β π β βͺ ran
((,) β π)) |
123 | 122 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))) β π β βͺ ran
((,) β π)) |
124 | | ovolsscl 25002 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β βͺ ran ((,) β π) β§ βͺ ran ((,)
β π) β β
β§ (vol*ββͺ ran ((,) β π)) β β) β
(vol*βπ) β
β) |
125 | 16, 124 | mp3an2 1449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β βͺ ran ((,) β π) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*βπ) β
β) |
126 | 125 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((vol*ββͺ ran ((,) β π)) β β β§ π β βͺ ran ((,) β π)) β (vol*βπ) β β) |
127 | 123, 126 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ)))) β (vol*βπ) β β) |
128 | 121, 127 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ)))) β π§ β β) |
129 | 128 | rexlimdvaa 3156 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((vol*ββͺ ran ((,) β π)) β β β
(βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ)) β π§ β β)) |
130 | 129 | abssdv 4065 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((vol*ββͺ ran ((,) β π)) β β β {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))} β β) |
131 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π§ = π¦ β (π§ = (volβπ) β π¦ = (volβπ))) |
132 | 131 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ = π¦ β ((π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ)) β (π β (βͺ ran
((,) β π) β
π΄) β§ π¦ = (volβπ)))) |
133 | 132 | rexbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π§ = π¦ β (βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π¦ = (volβπ)))) |
134 | 133 | ralab 3687 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ¦ β
{π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}π¦ β€ (vol*ββͺ ran ((,) β π)) β βπ¦(βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π¦ = (volβπ)) β π¦ β€ (vol*ββͺ ran ((,) β π)))) |
135 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π β (βͺ ran ((,) β π) β π΄) β§ π¦ = (volβπ)) β π¦ = (volβπ)) |
136 | 135, 119 | sylan9eqr 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β
π΄) β§ π¦ = (volβπ))) β π¦ = (vol*βπ)) |
137 | | ovolss 25001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((π β βͺ ran ((,) β π) β§ βͺ ran ((,)
β π) β β)
β (vol*βπ) β€
(vol*ββͺ ran ((,) β π))) |
138 | 122, 16, 137 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (βͺ ran ((,) β π) β π΄) β (vol*βπ) β€ (vol*ββͺ ran ((,) β π))) |
139 | 138 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β
π΄) β§ π¦ = (volβπ))) β (vol*βπ) β€ (vol*ββͺ ran ((,) β π))) |
140 | 136, 139 | eqbrtrd 5170 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β (βͺ ran
((,) β π) β
π΄) β§ π¦ = (volβπ))) β π¦ β€ (vol*ββͺ ran ((,) β π))) |
141 | 140 | rexlimiva 3147 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π¦ = (volβπ)) β π¦ β€ (vol*ββͺ ran ((,) β π))) |
142 | 134, 141 | mpgbir 1801 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
βπ¦ β
{π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}π¦ β€ (vol*ββͺ ran ((,) β π)) |
143 | | brralrspcev 5208 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(((vol*ββͺ ran ((,) β π)) β β β§
βπ¦ β {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}π¦ β€ (vol*ββͺ ran ((,) β π))) β βπ₯ β β βπ¦ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π¦ β€ π₯) |
144 | 142, 143 | mpan2 689 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((vol*ββͺ ran ((,) β π)) β β β
βπ₯ β β
βπ¦ β {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}π¦ β€ π₯) |
145 | | 0ss 4396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ β
β (βͺ ran ((,) β π) β π΄) |
146 | 145, 97 | pm3.2i 471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (β
β (βͺ ran ((,) β π) β π΄) β§ 0 =
(volββ
)) |
147 | | sseq1 4007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = β
β (π β (βͺ ran ((,) β π) β π΄) β β
β (βͺ ran ((,) β π) β π΄))) |
148 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = β
β
(volβπ) =
(volββ
)) |
149 | 148 | eqeq2d 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = β
β (0 =
(volβπ) β 0 =
(volββ
))) |
150 | 147, 149 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π = β
β ((π β (βͺ ran ((,) β π) β π΄) β§ 0 = (volβπ)) β (β
β (βͺ ran ((,) β π) β π΄) β§ 0 =
(volββ
)))) |
151 | 150 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((β
β (Clsdβ(topGenβran (,))) β§ (β
β (βͺ ran ((,) β π) β π΄) β§ 0 = (volββ
))) β
βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ 0 =
(volβπ))) |
152 | 91, 146, 151 | mp2an 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ 0 =
(volβπ)) |
153 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π§ = 0 β (π§ = (volβπ) β 0 = (volβπ))) |
154 | 153 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π§ = 0 β ((π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ)) β (π β (βͺ ran
((,) β π) β
π΄) β§ 0 =
(volβπ)))) |
155 | 154 | rexbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π§ = 0 β (βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ 0 = (volβπ)))) |
156 | 105, 155 | elab 3668 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (0 β
{π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))} β βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ 0 = (volβπ))) |
157 | 152, 156 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ 0 β
{π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))} |
158 | 157 | ne0ii 4337 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))} β β
|
159 | | suprcl 12173 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))} β β β§ {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))} β β
β§ βπ₯ β β βπ¦ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π¦ β€ π₯) β sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}, β, < ) β
β) |
160 | 158, 159 | mp3an2 1449 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))} β β β§ βπ₯ β β βπ¦ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π¦ β€ π₯) β sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}, β, < ) β
β) |
161 | 130, 144,
160 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((vol*ββͺ ran ((,) β π)) β β β
sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}, β, < ) β
β) |
162 | 114, 161 | readdcld 11242 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((vol*ββͺ ran ((,) β π)) β β β
(sup({π§ β£
βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}, β, < ) + sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}, β, < )) β
β) |
163 | 162 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β (sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}, β, < ) + sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}, β, < )) β
β) |
164 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*ββͺ ran ((,) β π)) β β) |
165 | 6 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π€ β β β§
(vol*βπ€) β
β) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*β(π€ β© π΄)) β β) |
166 | 9 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π€ β β β§
(vol*βπ€) β
β) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*β(π€ β π΄)) β β) |
167 | | ovolsscl 25002 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((βͺ ran ((,) β π) β© π΄) β βͺ ran
((,) β π) β§ βͺ ran ((,) β π) β β β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*β(βͺ ran ((,) β π) β© π΄)) β β) |
168 | 64, 16, 167 | mp3an12 1451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((vol*ββͺ ran ((,) β π)) β β β
(vol*β(βͺ ran ((,) β π) β© π΄)) β β) |
169 | 168 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π€ β β β§
(vol*βπ€) β
β) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*β(βͺ ran ((,) β π) β© π΄)) β β) |
170 | | difss 4131 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (βͺ ran ((,) β π) β π΄) β βͺ ran
((,) β π) |
171 | | ovolsscl 25002 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((βͺ ran ((,) β π) β π΄) β βͺ ran
((,) β π) β§ βͺ ran ((,) β π) β β β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*β(βͺ ran ((,) β π) β π΄)) β β) |
172 | 170, 16, 171 | mp3an12 1451 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((vol*ββͺ ran ((,) β π)) β β β
(vol*β(βͺ ran ((,) β π) β π΄)) β β) |
173 | 172 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π€ β β β§
(vol*βπ€) β
β) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*β(βͺ ran ((,) β π) β π΄)) β β) |
174 | | ssrin 4233 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π€ β βͺ ran ((,) β π) β (π€ β© π΄) β (βͺ ran
((,) β π) β© π΄)) |
175 | 64, 16 | sstri 3991 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (βͺ ran ((,) β π) β© π΄) β β |
176 | | ovolss 25001 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π€ β© π΄) β (βͺ ran
((,) β π) β© π΄) β§ (βͺ ran ((,) β π) β© π΄) β β) β (vol*β(π€ β© π΄)) β€ (vol*β(βͺ ran ((,) β π) β© π΄))) |
177 | 174, 175,
176 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π€ β βͺ ran ((,) β π) β (vol*β(π€ β© π΄)) β€ (vol*β(βͺ ran ((,) β π) β© π΄))) |
178 | 177 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π€ β β β§
(vol*βπ€) β
β) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*β(π€ β© π΄)) β€ (vol*β(βͺ ran ((,) β π) β© π΄))) |
179 | | ssdif 4139 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π€ β βͺ ran ((,) β π) β (π€ β π΄) β (βͺ ran
((,) β π) β
π΄)) |
180 | 170, 16 | sstri 3991 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (βͺ ran ((,) β π) β π΄) β β |
181 | | ovolss 25001 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((π€ β π΄) β (βͺ ran
((,) β π) β
π΄) β§ (βͺ ran ((,) β π) β π΄) β β) β (vol*β(π€ β π΄)) β€ (vol*β(βͺ ran ((,) β π) β π΄))) |
182 | 179, 180,
181 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π€ β βͺ ran ((,) β π) β (vol*β(π€ β π΄)) β€ (vol*β(βͺ ran ((,) β π) β π΄))) |
183 | 182 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π€ β β β§
(vol*βπ€) β
β) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*β(π€ β π΄)) β€ (vol*β(βͺ ran ((,) β π) β π΄))) |
184 | 165, 166,
169, 173, 178, 183 | le2addd 11832 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π€ β β β§
(vol*βπ€) β
β) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ ((vol*β(βͺ ran ((,) β π) β© π΄)) + (vol*β(βͺ ran ((,) β π) β π΄)))) |
185 | | dfin4 4267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (βͺ ran ((,) β π) β© π΄) = (βͺ ran ((,)
β π) β (βͺ ran ((,) β π) β π΄)) |
186 | 185 | fveq2i 6894 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(vol*β(βͺ ran ((,) β π) β© π΄)) = (vol*β(βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄))) |
187 | 186 | oveq1i 7418 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((vol*β(βͺ ran ((,) β π) β© π΄)) + (vol*β(βͺ ran ((,) β π) β π΄))) = ((vol*β(βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄))) + (vol*β(βͺ ran ((,) β π) β π΄))) |
188 | 184, 187 | breqtrdi 5189 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π€ β β β§
(vol*βπ€) β
β) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ ((vol*β(βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄))) + (vol*β(βͺ ran ((,) β π) β π΄)))) |
189 | 188 | adantlll 716 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ ((vol*β(βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄))) + (vol*β(βͺ ran ((,) β π) β π΄)))) |
190 | | simpll 765 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
(((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π€ β
βͺ ran ((,) β π)) β ((π΄ β β β§ (vol*βπ΄) β β) β§
(vol*βπ΄) = sup({π¦ β£ βπ β
(Clsdβ(topGenβran (,)))(π β π΄ β§ π¦ = (volβπ))}, β, < ))) |
191 | 185 | sseq2i 4011 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β (βͺ ran ((,) β π) β© π΄) β π β (βͺ ran
((,) β π) β
(βͺ ran ((,) β π) β π΄))) |
192 | 191 | anbi1i 624 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ)) β (π β (βͺ ran
((,) β π) β
(βͺ ran ((,) β π) β π΄)) β§ π§ = (volβπ))) |
193 | 192 | rexbii 3094 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄)) β§ π§ = (volβπ))) |
194 | 193 | abbii 2802 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))} = {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄)) β§ π§ = (volβπ))} |
195 | 194 | supeq1i 9441 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
sup({π§ β£
βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}, β, < ) = sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
(βͺ ran ((,) β π) β π΄)) β§ π§ = (volβπ))}, β, < ) |
196 | 16 | jctl 524 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((vol*ββͺ ran ((,) β π)) β β β (βͺ ran ((,) β π) β β β§ (vol*ββͺ ran ((,) β π)) β β)) |
197 | 196 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (vol*ββͺ ran ((,) β π)) β β) β (βͺ ran ((,) β π) β β β§ (vol*ββͺ ran ((,) β π)) β β)) |
198 | 172, 180 | jctil 520 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((vol*ββͺ ran ((,) β π)) β β β ((βͺ ran ((,) β π) β π΄) β β β§ (vol*β(βͺ ran ((,) β π) β π΄)) β β)) |
199 | 198 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (vol*ββͺ ran ((,) β π)) β β) β ((βͺ ran ((,) β π) β π΄) β β β§ (vol*β(βͺ ran ((,) β π) β π΄)) β β)) |
200 | | ltso 11293 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ < Or
β |
201 | 200 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((vol*ββͺ ran ((,) β π)) β β β < Or
β) |
202 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((vol*ββͺ ran ((,) β π)) β β β
(vol*ββͺ ran ((,) β π)) β β) |
203 | | vex 3478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ π₯ β V |
204 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π§ = π₯ β (π§ = (volβπ) β π₯ = (volβπ))) |
205 | 204 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π§ = π₯ β ((π β βͺ ran
((,) β π) β§ π§ = (volβπ)) β (π β βͺ ran
((,) β π) β§ π₯ = (volβπ)))) |
206 | 205 | rexbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π§ = π₯ β (βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π₯ = (volβπ)))) |
207 | 203, 206 | elab 3668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π₯ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ))} β βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π₯ = (volβπ))) |
208 | 16, 137 | mpan2 689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β βͺ ran ((,) β π) β (vol*βπ) β€ (vol*ββͺ ran ((,) β π))) |
209 | 208 | ad2antrl 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β βͺ ran
((,) β π) β§ π₯ = (volβπ))) β (vol*βπ) β€ (vol*ββͺ ran ((,) β π))) |
210 | 48 | cldss 22532 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β
(Clsdβ(topGenβran (,))) β π β β) |
211 | | ovolcl 24994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β β β
(vol*βπ) β
β*) |
212 | 210, 211 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π β
(Clsdβ(topGenβran (,))) β (vol*βπ) β
β*) |
213 | | xrlenlt 11278 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(((vol*βπ)
β β* β§ (vol*ββͺ ran
((,) β π)) β
β*) β ((vol*βπ) β€ (vol*ββͺ ran ((,) β π)) β Β¬ (vol*ββͺ ran ((,) β π)) < (vol*βπ))) |
214 | 212, 34, 213 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β
(Clsdβ(topGenβran (,))) β ((vol*βπ) β€ (vol*ββͺ ran ((,) β π)) β Β¬ (vol*ββͺ ran ((,) β π)) < (vol*βπ))) |
215 | 214 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β βͺ ran
((,) β π) β§ π₯ = (volβπ))) β ((vol*βπ) β€ (vol*ββͺ ran ((,) β π)) β Β¬ (vol*ββͺ ran ((,) β π)) < (vol*βπ))) |
216 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π₯ = (volβπ) β π₯ = (volβπ)) |
217 | 216, 119 | sylan9eqr 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β
(Clsdβ(topGenβran (,))) β§ π₯ = (volβπ)) β π₯ = (vol*βπ)) |
218 | | breq2 5152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π₯ = (vol*βπ) β ((vol*ββͺ ran ((,) β π)) < π₯ β (vol*ββͺ ran ((,) β π)) < (vol*βπ))) |
219 | 218 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π₯ = (vol*βπ) β (Β¬
(vol*ββͺ ran ((,) β π)) < π₯ β Β¬ (vol*ββͺ ran ((,) β π)) < (vol*βπ))) |
220 | 217, 219 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β
(Clsdβ(topGenβran (,))) β§ π₯ = (volβπ)) β (Β¬ (vol*ββͺ ran ((,) β π)) < π₯ β Β¬ (vol*ββͺ ran ((,) β π)) < (vol*βπ))) |
221 | 220 | adantrl 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β βͺ ran
((,) β π) β§ π₯ = (volβπ))) β (Β¬ (vol*ββͺ ran ((,) β π)) < π₯ β Β¬ (vol*ββͺ ran ((,) β π)) < (vol*βπ))) |
222 | 215, 221 | bitr4d 281 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β βͺ ran
((,) β π) β§ π₯ = (volβπ))) β ((vol*βπ) β€ (vol*ββͺ ran ((,) β π)) β Β¬ (vol*ββͺ ran ((,) β π)) < π₯)) |
223 | 209, 222 | mpbid 231 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π β
(Clsdβ(topGenβran (,))) β§ (π β βͺ ran
((,) β π) β§ π₯ = (volβπ))) β Β¬ (vol*ββͺ ran ((,) β π)) < π₯) |
224 | 223 | rexlimiva 3147 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(βπ β
(Clsdβ(topGenβran (,)))(π β βͺ ran
((,) β π) β§ π₯ = (volβπ)) β Β¬ (vol*ββͺ ran ((,) β π)) < π₯) |
225 | 207, 224 | sylbi 216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π₯ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ))} β Β¬ (vol*ββͺ ran ((,) β π)) < π₯) |
226 | 225 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((vol*ββͺ ran ((,) β π)) β β β§ π₯ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ))}) β Β¬ (vol*ββͺ ran ((,) β π)) < π₯) |
227 | | retopbas 24276 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ran (,)
β TopBases |
228 | | bastg 22468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (ran (,)
β TopBases β ran (,) β (topGenβran (,))) |
229 | 227, 228 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ran (,)
β (topGenβran (,)) |
230 | 13, 229 | sstri 3991 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ran ((,)
β π) β
(topGenβran (,)) |
231 | | uniopn 22398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
(((topGenβran (,)) β Top β§ ran ((,) β π) β (topGenβran
(,))) β βͺ ran ((,) β π) β (topGenβran
(,))) |
232 | 89, 230, 231 | mp2an 690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ βͺ ran ((,) β π) β (topGenβran
(,)) |
233 | | mblfinlem2 36521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((βͺ ran ((,) β π) β (topGenβran (,)) β§ π₯ β β β§ π₯ < (vol*ββͺ ran ((,) β π))) β βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π₯ < (vol*βπ))) |
234 | 232, 233 | mp3an1 1448 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π₯ β β β§ π₯ < (vol*ββͺ ran ((,) β π))) β βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π₯ < (vol*βπ))) |
235 | 119 | eqcomd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π β
(Clsdβ(topGenβran (,))) β (vol*βπ) = (volβπ)) |
236 | 235 | anim1i 615 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β
(Clsdβ(topGenβran (,))) β§ π₯ < (vol*βπ)) β ((vol*βπ) = (volβπ) β§ π₯ < (vol*βπ))) |
237 | 236 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π β
(Clsdβ(topGenβran (,))) β (π₯ < (vol*βπ) β ((vol*βπ) = (volβπ) β§ π₯ < (vol*βπ)))) |
238 | 237 | anim2d 612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π β
(Clsdβ(topGenβran (,))) β ((π β βͺ ran
((,) β π) β§ π₯ < (vol*βπ)) β (π β βͺ ran
((,) β π) β§
((vol*βπ) =
(volβπ) β§ π₯ < (vol*βπ))))) |
239 | | fvex 6904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
(vol*βπ)
β V |
240 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ (π¦ = (vol*βπ) β (π¦ = (volβπ) β (vol*βπ) = (volβπ))) |
241 | 240 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π¦ = (vol*βπ) β ((π β βͺ ran
((,) β π) β§ π¦ = (volβπ)) β (π β βͺ ran
((,) β π) β§
(vol*βπ) =
(volβπ)))) |
242 | | breq2 5152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ (π¦ = (vol*βπ) β (π₯ < π¦ β π₯ < (vol*βπ))) |
243 | 241, 242 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π¦ = (vol*βπ) β (((π β βͺ ran
((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦) β ((π β βͺ ran
((,) β π) β§
(vol*βπ) =
(volβπ)) β§ π₯ < (vol*βπ)))) |
244 | 239, 243 | spcev 3596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (((π β βͺ ran ((,) β π) β§ (vol*βπ) = (volβπ)) β§ π₯ < (vol*βπ)) β βπ¦((π β βͺ ran
((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦)) |
245 | 244 | anasss 467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β βͺ ran ((,) β π) β§ ((vol*βπ) = (volβπ) β§ π₯ < (vol*βπ))) β βπ¦((π β βͺ ran
((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦)) |
246 | 238, 245 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π β
(Clsdβ(topGenβran (,))) β ((π β βͺ ran
((,) β π) β§ π₯ < (vol*βπ)) β βπ¦((π β βͺ ran
((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦))) |
247 | 246 | reximia 3081 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(βπ β
(Clsdβ(topGenβran (,)))(π β βͺ ran
((,) β π) β§ π₯ < (vol*βπ)) β βπ β
(Clsdβ(topGenβran (,)))βπ¦((π β βͺ ran
((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦)) |
248 | 234, 247 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ ((π₯ β β β§ π₯ < (vol*ββͺ ran ((,) β π))) β βπ β (Clsdβ(topGenβran
(,)))βπ¦((π β βͺ ran ((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦)) |
249 | | r19.41v 3188 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(βπ β
(Clsdβ(topGenβran (,)))((π β βͺ ran
((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦) β (βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦)) |
250 | 249 | exbii 1850 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(βπ¦βπ β (Clsdβ(topGenβran
(,)))((π β βͺ ran ((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦) β βπ¦(βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦)) |
251 | | rexcom4 3285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(βπ β
(Clsdβ(topGenβran (,)))βπ¦((π β βͺ ran
((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦) β βπ¦βπ β (Clsdβ(topGenβran
(,)))((π β βͺ ran ((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦)) |
252 | 131 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π§ = π¦ β ((π β βͺ ran
((,) β π) β§ π§ = (volβπ)) β (π β βͺ ran
((,) β π) β§ π¦ = (volβπ)))) |
253 | 252 | rexbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π§ = π¦ β (βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π¦ = (volβπ)))) |
254 | 253 | rexab 3690 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(βπ¦ β
{π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β βͺ ran
((,) β π) β§ π§ = (volβπ))}π₯ < π¦ β βπ¦(βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦)) |
255 | 250, 251,
254 | 3bitr4i 302 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
(βπ β
(Clsdβ(topGenβran (,)))βπ¦((π β βͺ ran
((,) β π) β§ π¦ = (volβπ)) β§ π₯ < π¦) β βπ¦ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ))}π₯ < π¦) |
256 | 248, 255 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ ((π₯ β β β§ π₯ < (vol*ββͺ ran ((,) β π))) β βπ¦ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ))}π₯ < π¦) |
257 | 256 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((vol*ββͺ ran ((,) β π)) β β β§ (π₯ β β β§ π₯ < (vol*ββͺ ran ((,) β π)))) β βπ¦ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ))}π₯ < π¦) |
258 | 201, 202,
226, 257 | eqsupd 9451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((vol*ββͺ ran ((,) β π)) β β β
sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β βͺ ran
((,) β π) β§ π§ = (volβπ))}, β, < ) = (vol*ββͺ ran ((,) β π))) |
259 | 258 | eqcomd 2738 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((vol*ββͺ ran ((,) β π)) β β β
(vol*ββͺ ran ((,) β π)) = sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ))}, β, < )) |
260 | 259 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*ββͺ ran ((,) β π)) = sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ))}, β, < )) |
261 | | sseq1 4007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β (π β βͺ ran
((,) β π) β
π β βͺ ran ((,) β π))) |
262 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π = π β (volβπ) = (volβπ)) |
263 | 262 | eqeq2d 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β (π§ = (volβπ) β π§ = (volβπ))) |
264 | 261, 263 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π β ((π β βͺ ran
((,) β π) β§ π§ = (volβπ)) β (π β βͺ ran
((,) β π) β§ π§ = (volβπ)))) |
265 | 264 | cbvrexvw 3235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(βπ β
(Clsdβ(topGenβran (,)))(π β βͺ ran
((,) β π) β§ π§ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ))) |
266 | 265 | abbii 2802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β βͺ ran
((,) β π) β§ π§ = (volβπ))} = {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ))} |
267 | 266 | supeq1i 9441 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
sup({π§ β£
βπ β
(Clsdβ(topGenβran (,)))(π β βͺ ran
((,) β π) β§ π§ = (volβπ))}, β, < ) = sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β βͺ ran
((,) β π) β§ π§ = (volβπ))}, β, < ) |
268 | 260, 267 | eqtrdi 2788 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*ββͺ ran ((,) β π)) = sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ))}, β, < )) |
269 | | simpll 765 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (vol*ββͺ ran ((,) β π)) β β) β (π΄ β β β§ (vol*βπ΄) β
β)) |
270 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π¦ = π§ β (π¦ = (volβπ) β π§ = (volβπ))) |
271 | 270 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π¦ = π§ β ((π β π΄ β§ π¦ = (volβπ)) β (π β π΄ β§ π§ = (volβπ)))) |
272 | 271 | rexbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (π¦ = π§ β (βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π§ = (volβπ)))) |
273 | | sseq1 4007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π β (π β π΄ β π β π΄)) |
274 | | fveq2 6891 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (π = π β (volβπ) = (volβπ)) |
275 | 274 | eqeq2d 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ (π = π β (π§ = (volβπ) β π§ = (volβπ))) |
276 | 273, 275 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (π = π β ((π β π΄ β§ π§ = (volβπ)) β (π β π΄ β§ π§ = (volβπ)))) |
277 | 276 | cbvrexvw 3235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(βπ β
(Clsdβ(topGenβran (,)))(π β π΄ β§ π§ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π§ = (volβπ))) |
278 | 272, 277 | bitrdi 286 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π¦ = π§ β (βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π§ = (volβπ)))) |
279 | 278 | cbvabv 2805 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ {π¦ β£ βπ β
(Clsdβ(topGenβran (,)))(π β π΄ β§ π¦ = (volβπ))} = {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π§ = (volβπ))} |
280 | 279 | supeq1i 9441 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
sup({π¦ β£
βπ β
(Clsdβ(topGenβran (,)))(π β π΄ β§ π¦ = (volβπ))}, β, < ) = sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β π΄ β§ π§ = (volβπ))}, β, < ) |
281 | 280 | eqeq2i 2745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((vol*βπ΄) =
sup({π¦ β£ βπ β
(Clsdβ(topGenβran (,)))(π β π΄ β§ π¦ = (volβπ))}, β, < ) β (vol*βπ΄) = sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π§ = (volβπ))}, β, < )) |
282 | 281 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((vol*βπ΄) =
sup({π¦ β£ βπ β
(Clsdβ(topGenβran (,)))(π β π΄ β§ π¦ = (volβπ))}, β, < ) β (vol*βπ΄) = sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π§ = (volβπ))}, β, < )) |
283 | 282 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*βπ΄) = sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π§ = (volβπ))}, β, < )) |
284 | | mblfinlem3 36522 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((βͺ ran ((,) β π) β β β§ (vol*ββͺ ran ((,) β π)) β β) β§ (π΄ β β β§ (vol*βπ΄) β β) β§
((vol*ββͺ ran ((,) β π)) = sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ))}, β, < ) β§ (vol*βπ΄) = sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π§ = (volβπ))}, β, < ))) β sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}, β, < ) = (vol*β(βͺ ran ((,) β π) β π΄))) |
285 | 197, 269,
260, 283, 284 | syl112anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (vol*ββͺ ran ((,) β π)) β β) β sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}, β, < ) = (vol*β(βͺ ran ((,) β π) β π΄))) |
286 | | sseq1 4007 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π = π β (π β (βͺ ran
((,) β π) β
π΄) β π β (βͺ ran ((,) β π) β π΄))) |
287 | 286, 263 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π = π β ((π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ)) β (π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ)))) |
288 | 287 | cbvrexvw 3235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))) |
289 | 288 | abbii 2802 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))} = {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))} |
290 | 289 | supeq1i 9441 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
sup({π§ β£
βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}, β, < ) = sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}, β, < ) |
291 | 285, 290 | eqtr3di 2787 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*β(βͺ ran ((,) β π) β π΄)) = sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}, β, < )) |
292 | | mblfinlem3 36522 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((βͺ ran ((,) β π) β β β§ (vol*ββͺ ran ((,) β π)) β β) β§ ((βͺ ran ((,) β π) β π΄) β β β§ (vol*β(βͺ ran ((,) β π) β π΄)) β β) β§ ((vol*ββͺ ran ((,) β π)) = sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β βͺ ran ((,) β π) β§ π§ = (volβπ))}, β, < ) β§ (vol*β(βͺ ran ((,) β π) β π΄)) = sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}, β, < ))) β sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
(βͺ ran ((,) β π) β π΄)) β§ π§ = (volβπ))}, β, < ) = (vol*β(βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄)))) |
293 | 197, 199,
268, 291, 292 | syl112anc 1374 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (vol*ββͺ ran ((,) β π)) β β) β sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
(βͺ ran ((,) β π) β π΄)) β§ π§ = (volβπ))}, β, < ) = (vol*β(βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄)))) |
294 | 195, 293 | eqtrid 2784 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (vol*ββͺ ran ((,) β π)) β β) β sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}, β, < ) = (vol*β(βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄)))) |
295 | 294, 285 | oveq12d 7426 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (vol*ββͺ ran ((,) β π)) β β) β (sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}, β, < ) + sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}, β, < )) = ((vol*β(βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄))) + (vol*β(βͺ ran ((,) β π) β π΄)))) |
296 | 190, 295 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β (sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}, β, < ) + sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}, β, < )) = ((vol*β(βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄))) + (vol*β(βͺ ran ((,) β π) β π΄)))) |
297 | 189, 296 | breqtrrd 5176 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (sup({π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}, β, < ) + sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}, β, < ))) |
298 | | ne0i 4334 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (0 β
{π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))} β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))} β β
) |
299 | 110, 298 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((vol*ββͺ ran ((,) β π)) β β β {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))} β β
) |
300 | | ne0i 4334 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (0 β
{π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))} β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))} β β
) |
301 | 157, 300 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((vol*ββͺ ran ((,) β π)) β β β {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))} β β
) |
302 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)} = {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)} |
303 | 74, 299, 88, 130, 301, 144, 302 | supadd 12181 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((vol*ββͺ ran ((,) β π)) β β β
(sup({π§ β£
βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}, β, < ) + sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}, β, < )) = sup({π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)}, β, < )) |
304 | | reeanv 3226 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(βπ β
(Clsdβ(topGenβran (,)))βπ β (Clsdβ(topGenβran
(,)))((π β (βͺ ran ((,) β π) β© π΄) β§ π’ = (volβπ)) β§ (π β (βͺ ran
((,) β π) β
π΄) β§ π£ = (volβπ))) β (βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π’ = (volβπ)) β§ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π£ = (volβπ)))) |
305 | | vex 3478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ π’ β V |
306 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π§ = π’ β (π§ = (volβπ) β π’ = (volβπ))) |
307 | 306 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π§ = π’ β ((π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ)) β (π β (βͺ ran
((,) β π) β© π΄) β§ π’ = (volβπ)))) |
308 | 307 | rexbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π§ = π’ β (βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π’ = (volβπ)))) |
309 | 305, 308 | elab 3668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))} β βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π’ = (volβπ))) |
310 | | vex 3478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ π£ β V |
311 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ (π§ = π£ β (π§ = (volβπ) β π£ = (volβπ))) |
312 | 311 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’ (π§ = π£ β ((π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ)) β (π β (βͺ ran
((,) β π) β
π΄) β§ π£ = (volβπ)))) |
313 | 312 | rexbidv 3178 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π§ = π£ β (βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ)) β βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π£ = (volβπ)))) |
314 | 310, 313 | elab 3668 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))} β βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π£ = (volβπ))) |
315 | 309, 314 | anbi12i 627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ ((π’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))} β§ π£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}) β (βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π’ = (volβπ)) β§ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π£ = (volβπ)))) |
316 | 304, 315 | bitr4i 277 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(βπ β
(Clsdβ(topGenβran (,)))βπ β (Clsdβ(topGenβran
(,)))((π β (βͺ ran ((,) β π) β© π΄) β§ π’ = (volβπ)) β§ (π β (βͺ ran
((,) β π) β
π΄) β§ π£ = (volβπ))) β (π’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))} β§ π£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))})) |
317 | | an4 654 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (((π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄)) β§ (π’ = (volβπ) β§ π£ = (volβπ))) β ((π β (βͺ ran
((,) β π) β© π΄) β§ π’ = (volβπ)) β§ (π β (βͺ ran
((,) β π) β
π΄) β§ π£ = (volβπ)))) |
318 | | oveq12 7417 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π’ = (volβπ) β§ π£ = (volβπ)) β (π’ + π£) = ((volβπ) + (volβπ))) |
319 | 59 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,))))
β π β dom
vol) |
320 | 319 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β π β dom
vol) |
321 | 117 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,))))
β π β dom
vol) |
322 | 321 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β π β dom
vol) |
323 | | ss2in 4236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄)) β (π β© π) β ((βͺ ran
((,) β π) β© π΄) β© (βͺ ran ((,) β π) β π΄))) |
324 | 185 | ineq1i 4208 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((βͺ ran ((,) β π) β© π΄) β© (βͺ ran
((,) β π) β
π΄)) = ((βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄)) β© (βͺ ran ((,) β π) β π΄)) |
325 | | incom 4201 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄)) β© (βͺ ran ((,) β π) β π΄)) = ((βͺ ran ((,)
β π) β π΄) β© (βͺ ran ((,) β π) β (βͺ ran
((,) β π) β
π΄))) |
326 | | disjdif 4471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ ((βͺ ran ((,) β π) β π΄) β© (βͺ ran
((,) β π) β
(βͺ ran ((,) β π) β π΄))) = β
|
327 | 324, 325,
326 | 3eqtri 2764 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((βͺ ran ((,) β π) β© π΄) β© (βͺ ran
((,) β π) β
π΄)) =
β
|
328 | 323, 327 | sseqtrdi 4032 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄)) β (π β© π) β β
) |
329 | | ss0 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β© π) β β
β (π β© π) = β
) |
330 | 328, 329 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄)) β (π β© π) = β
) |
331 | 330 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β (π β© π) = β
) |
332 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,))))
β (volβπ) =
(vol*βπ)) |
333 | 332 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β
(volβπ) =
(vol*βπ)) |
334 | 66, 16 | jctir 521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π β (βͺ ran ((,) β π) β© π΄) β (π β βͺ ran
((,) β π) β§ βͺ ran ((,) β π) β β)) |
335 | 68 | 3expa 1118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (((π β βͺ ran ((,) β π) β§ βͺ ran ((,)
β π) β β)
β§ (vol*ββͺ ran ((,) β π)) β β) β
(vol*βπ) β
β) |
336 | 334, 335 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π β (βͺ ran ((,) β π) β© π΄) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*βπ) β
β) |
337 | 336 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((vol*ββͺ ran ((,) β π)) β β β§ π β (βͺ ran ((,) β π) β© π΄)) β (vol*βπ) β β) |
338 | 337 | ad2ant2r 745 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β
(vol*βπ) β
β) |
339 | 333, 338 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β
(volβπ) β
β) |
340 | 119 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,))))
β (volβπ) =
(vol*βπ)) |
341 | 340 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β
(volβπ) =
(vol*βπ)) |
342 | 122, 16 | jctir 521 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (π β (βͺ ran ((,) β π) β π΄) β (π β βͺ ran
((,) β π) β§ βͺ ran ((,) β π) β β)) |
343 | 124 | 3expa 1118 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
β’ (((π β βͺ ran ((,) β π) β§ βͺ ran ((,)
β π) β β)
β§ (vol*ββͺ ran ((,) β π)) β β) β
(vol*βπ) β
β) |
344 | 342, 343 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
β’ ((π β (βͺ ran ((,) β π) β π΄) β§ (vol*ββͺ ran ((,) β π)) β β) β (vol*βπ) β
β) |
345 | 344 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’
(((vol*ββͺ ran ((,) β π)) β β β§ π β (βͺ ran ((,) β π) β π΄)) β (vol*βπ) β β) |
346 | 345 | ad2ant2rl 747 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β
(vol*βπ) β
β) |
347 | 341, 346 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β
(volβπ) β
β) |
348 | | volun 25061 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ (((π β dom vol β§ π β dom vol β§ (π β© π) = β
) β§ ((volβπ) β β β§
(volβπ) β
β)) β (volβ(π βͺ π)) = ((volβπ) + (volβπ))) |
349 | 320, 322,
331, 339, 347, 348 | syl32anc 1378 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β
(volβ(π βͺ π)) = ((volβπ) + (volβπ))) |
350 | | unmbl 25053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
β’ ((π β dom vol β§ π β dom vol) β (π βͺ π) β dom vol) |
351 | 59, 117, 350 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,))))
β (π βͺ π) β dom
vol) |
352 | | mblvol 25046 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
β’ ((π βͺ π) β dom vol β (volβ(π βͺ π)) = (vol*β(π βͺ π))) |
353 | 351, 352 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
β’ ((π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,))))
β (volβ(π βͺ
π)) = (vol*β(π βͺ π))) |
354 | 353 | ad2antlr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β
(volβ(π βͺ π)) = (vol*β(π βͺ π))) |
355 | 349, 354 | eqtr3d 2774 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β
((volβπ) +
(volβπ)) =
(vol*β(π βͺ π))) |
356 | 318, 355 | sylan9eqr 2794 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’
(((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β§ (π’ = (volβπ) β§ π£ = (volβπ))) β (π’ + π£) = (vol*β(π βͺ π))) |
357 | | eqtr 2755 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π¦ = (π’ + π£) β§ (π’ + π£) = (vol*β(π βͺ π))) β π¦ = (vol*β(π βͺ π))) |
358 | 357 | ancoms 459 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ (((π’ + π£) = (vol*β(π βͺ π)) β§ π¦ = (π’ + π£)) β π¦ = (vol*β(π βͺ π))) |
359 | 356, 358 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β§ (π’ = (volβπ) β§ π£ = (volβπ))) β§ π¦ = (π’ + π£)) β π¦ = (vol*β(π βͺ π))) |
360 | 66, 122 | anim12i 613 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄)) β (π β βͺ ran ((,) β π) β§ π β βͺ ran
((,) β π))) |
361 | | unss 4184 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
β’ ((π β βͺ ran ((,) β π) β§ π β βͺ ran
((,) β π)) β
(π βͺ π) β βͺ ran
((,) β π)) |
362 | 360, 361 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ ((π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄)) β (π βͺ π) β βͺ ran
((,) β π)) |
363 | | ovolss 25001 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
β’ (((π βͺ π) β βͺ ran
((,) β π) β§ βͺ ran ((,) β π) β β) β (vol*β(π βͺ π)) β€ (vol*ββͺ ran ((,) β π))) |
364 | 362, 16, 363 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
β’ ((π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄)) β
(vol*β(π βͺ π)) β€ (vol*ββͺ ran ((,) β π))) |
365 | 364 | ad3antlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
((((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β§ (π’ = (volβπ) β§ π£ = (volβπ))) β§ π¦ = (π’ + π£)) β (vol*β(π βͺ π)) β€ (vol*ββͺ ran ((,) β π))) |
366 | 359, 365 | eqbrtrd 5170 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β§ (π’ = (volβπ) β§ π£ = (volβπ))) β§ π¦ = (π’ + π£)) β π¦ β€ (vol*ββͺ ran ((,) β π))) |
367 | 366 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β§ (π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄))) β§ (π’ = (volβπ) β§ π£ = (volβπ))) β (π¦ = (π’ + π£) β π¦ β€ (vol*ββͺ ran ((,) β π)))) |
368 | 367 | expl 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
(((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β (((π β (βͺ ran ((,) β π) β© π΄) β§ π β (βͺ ran
((,) β π) β
π΄)) β§ (π’ = (volβπ) β§ π£ = (volβπ))) β (π¦ = (π’ + π£) β π¦ β€ (vol*ββͺ ran ((,) β π))))) |
369 | 317, 368 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(((vol*ββͺ ran ((,) β π)) β β β§ (π β
(Clsdβ(topGenβran (,))) β§ π β (Clsdβ(topGenβran (,)))))
β (((π β (βͺ ran ((,) β π) β© π΄) β§ π’ = (volβπ)) β§ (π β (βͺ ran
((,) β π) β
π΄) β§ π£ = (volβπ))) β (π¦ = (π’ + π£) β π¦ β€ (vol*ββͺ ran ((,) β π))))) |
370 | 369 | rexlimdvva 3211 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
((vol*ββͺ ran ((,) β π)) β β β
(βπ β
(Clsdβ(topGenβran (,)))βπ β (Clsdβ(topGenβran
(,)))((π β (βͺ ran ((,) β π) β© π΄) β§ π’ = (volβπ)) β§ (π β (βͺ ran
((,) β π) β
π΄) β§ π£ = (volβπ))) β (π¦ = (π’ + π£) β π¦ β€ (vol*ββͺ ran ((,) β π))))) |
371 | 316, 370 | biimtrrid 242 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((vol*ββͺ ran ((,) β π)) β β β ((π’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))} β§ π£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}) β (π¦ = (π’ + π£) β π¦ β€ (vol*ββͺ ran ((,) β π))))) |
372 | 371 | rexlimdvv 3210 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((vol*ββͺ ran ((,) β π)) β β β
(βπ’ β {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π¦ = (π’ + π£) β π¦ β€ (vol*ββͺ ran ((,) β π)))) |
373 | 372 | alrimiv 1930 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((vol*ββͺ ran ((,) β π)) β β β
βπ¦(βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π¦ = (π’ + π£) β π¦ β€ (vol*ββͺ ran ((,) β π)))) |
374 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π‘ = π¦ β (π‘ = (π’ + π£) β π¦ = (π’ + π£))) |
375 | 374 | 2rexbidv 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π‘ = π¦ β (βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£) β βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π¦ = (π’ + π£))) |
376 | 375 | ralab 3687 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(βπ¦ β
{π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)}π¦ β€ (vol*ββͺ ran ((,) β π)) β βπ¦(βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π¦ = (π’ + π£) β π¦ β€ (vol*ββͺ ran ((,) β π)))) |
377 | 373, 376 | sylibr 233 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((vol*ββͺ ran ((,) β π)) β β β
βπ¦ β {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)}π¦ β€ (vol*ββͺ ran ((,) β π))) |
378 | | simpr 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))} β§ π£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))})) β§ π‘ = (π’ + π£)) β π‘ = (π’ + π£)) |
379 | 74 | sselda 3982 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((vol*ββͺ ran ((,) β π)) β β β§ π’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}) β π’ β β) |
380 | 130 | sselda 3982 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’
(((vol*ββͺ ran ((,) β π)) β β β§ π£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}) β π£ β β) |
381 | | readdcl 11192 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
β’ ((π’ β β β§ π£ β β) β (π’ + π£) β β) |
382 | 379, 380,
381 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
β’
((((vol*ββͺ ran ((,) β π)) β β β§ π’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}) β§ ((vol*ββͺ ran ((,) β π)) β β β§ π£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))})) β (π’ + π£) β β) |
383 | 382 | anandis 676 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’
(((vol*ββͺ ran ((,) β π)) β β β§ (π’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))} β§ π£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))})) β (π’ + π£) β β) |
384 | 383 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))} β§ π£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))})) β§ π‘ = (π’ + π£)) β (π’ + π£) β β) |
385 | 378, 384 | eqeltrd 2833 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((((vol*ββͺ ran ((,) β π)) β β β§ (π’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))} β§ π£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))})) β§ π‘ = (π’ + π£)) β π‘ β β) |
386 | 385 | ex 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(((vol*ββͺ ran ((,) β π)) β β β§ (π’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))} β§ π£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))})) β (π‘ = (π’ + π£) β π‘ β β)) |
387 | 386 | rexlimdvva 3211 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
((vol*ββͺ ran ((,) β π)) β β β
(βπ’ β {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£) β π‘ β β)) |
388 | 387 | abssdv 4065 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((vol*ββͺ ran ((,) β π)) β β β {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)} β β) |
389 | | 00id 11388 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (0 + 0) =
0 |
390 | 389 | eqcomi 2741 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ 0 = (0 +
0) |
391 | | rspceov 7455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ ((0
β {π§ β£
βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))} β§ 0 β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))} β§ 0 = (0 + 0)) β βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}0 = (π’ + π£)) |
392 | 110, 157,
390, 391 | mp3an 1461 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
βπ’ β
{π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}0 = (π’ + π£) |
393 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
β’ (π‘ = 0 β (π‘ = (π’ + π£) β 0 = (π’ + π£))) |
394 | 393 | 2rexbidv 3219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
β’ (π‘ = 0 β (βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£) β βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}0 = (π’ + π£))) |
395 | 105, 394 | spcev 3596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
(βπ’ β
{π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}0 = (π’ + π£) β βπ‘βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)) |
396 | 392, 395 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
βπ‘βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£) |
397 | | abn0 4380 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ ({π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)} β β
β βπ‘βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)) |
398 | 396, 397 | mpbir 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)} β β
|
399 | 398 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((vol*ββͺ ran ((,) β π)) β β β {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)} β β
) |
400 | | brralrspcev 5208 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’
(((vol*ββͺ ran ((,) β π)) β β β§
βπ¦ β {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)}π¦ β€ (vol*ββͺ ran ((,) β π))) β βπ₯ β β βπ¦ β {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)}π¦ β€ π₯) |
401 | 377, 400 | mpdan 685 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
((vol*ββͺ ran ((,) β π)) β β β
βπ₯ β β
βπ¦ β {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)}π¦ β€ π₯) |
402 | 388, 399,
401 | 3jca 1128 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((vol*ββͺ ran ((,) β π)) β β β ({π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)} β β β§ {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)} β β
β§ βπ₯ β β βπ¦ β {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)}π¦ β€ π₯)) |
403 | | suprleub 12179 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((({π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)} β β β§ {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)} β β
β§ βπ₯ β β βπ¦ β {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)}π¦ β€ π₯) β§ (vol*ββͺ ran ((,) β π)) β β) β (sup({π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)}, β, < ) β€ (vol*ββͺ ran ((,) β π)) β βπ¦ β {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)}π¦ β€ (vol*ββͺ ran ((,) β π)))) |
404 | 402, 403 | mpancom 686 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
((vol*ββͺ ran ((,) β π)) β β β
(sup({π‘ β£
βπ’ β {π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)}, β, < ) β€ (vol*ββͺ ran ((,) β π)) β βπ¦ β {π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)}π¦ β€ (vol*ββͺ ran ((,) β π)))) |
405 | 377, 404 | mpbird 256 |
. . . . . . . . . . . . . . . . . . . . . 22
β’
((vol*ββͺ ran ((,) β π)) β β β
sup({π‘ β£ βπ’ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β© π΄) β§ π§ = (volβπ))}βπ£ β {π§ β£ βπ β (Clsdβ(topGenβran
(,)))(π β (βͺ ran ((,) β π) β π΄) β§ π§ = (volβπ))}π‘ = (π’ + π£)}, β, < ) β€ (vol*ββͺ ran ((,) β π))) |
406 | 303, 405 | eqbrtrd 5170 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((vol*ββͺ ran ((,) β π)) β β β
(sup({π§ β£
βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}, β, < ) + sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}, β, < )) β€ (vol*ββͺ ran ((,) β π))) |
407 | 406 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β (sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β© π΄) β§ π§ = (volβπ))}, β, < ) + sup({π§ β£ βπ β
(Clsdβ(topGenβran (,)))(π β (βͺ ran
((,) β π) β
π΄) β§ π§ = (volβπ))}, β, < )) β€ (vol*ββͺ ran ((,) β π))) |
408 | 45, 163, 164, 297, 407 | letrd 11370 |
. . . . . . . . . . . . . . . . . . 19
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β β) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (vol*ββͺ ran ((,) β π))) |
409 | 44, 408 | sylan2 593 |
. . . . . . . . . . . . . . . . . 18
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π€ β
βͺ ran ((,) β π)) β§ (vol*ββͺ ran ((,) β π)) β +β) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (vol*ββͺ ran ((,) β π))) |
410 | 33, 409 | pm2.61dane 3029 |
. . . . . . . . . . . . . . . . 17
β’
(((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π€ β
βͺ ran ((,) β π)) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (vol*ββͺ ran ((,) β π))) |
411 | 410 | adantlr 713 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π:ββΆ( β€ β© (β Γ
β))) β§ π€ β
βͺ ran ((,) β π)) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (vol*ββͺ ran ((,) β π))) |
412 | | ssid 4004 |
. . . . . . . . . . . . . . . . . 18
β’ βͺ ran ((,) β π) β βͺ ran
((,) β π) |
413 | 20 | ovollb 24995 |
. . . . . . . . . . . . . . . . . 18
β’ ((π:ββΆ( β€ β©
(β Γ β)) β§ βͺ ran ((,) β
π) β βͺ ran ((,) β π)) β (vol*ββͺ ran ((,) β π)) β€ sup(ran seq1( + , ((abs β
β ) β π)),
β*, < )) |
414 | 412, 413 | mpan2 689 |
. . . . . . . . . . . . . . . . 17
β’ (π:ββΆ( β€ β©
(β Γ β)) β (vol*ββͺ ran
((,) β π)) β€
sup(ran seq1( + , ((abs β β ) β π)), β*, <
)) |
415 | 414 | ad2antlr 725 |
. . . . . . . . . . . . . . . 16
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π:ββΆ( β€ β© (β Γ
β))) β§ π€ β
βͺ ran ((,) β π)) β (vol*ββͺ ran ((,) β π)) β€ sup(ran seq1( + , ((abs β
β ) β π)),
β*, < )) |
416 | 12, 18, 27, 411, 415 | xrletrd 13140 |
. . . . . . . . . . . . . . 15
β’
((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π:ββΆ( β€ β© (β Γ
β))) β§ π€ β
βͺ ran ((,) β π)) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ sup(ran seq1( + , ((abs β
β ) β π)),
β*, < )) |
417 | 416 | adantr 481 |
. . . . . . . . . . . . . 14
β’
(((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π:ββΆ( β€ β© (β Γ
β))) β§ π€ β
βͺ ran ((,) β π)) β§ π’ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < )) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ sup(ran seq1( + , ((abs β
β ) β π)),
β*, < )) |
418 | | simpr 485 |
. . . . . . . . . . . . . 14
β’
(((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π:ββΆ( β€ β© (β Γ
β))) β§ π€ β
βͺ ran ((,) β π)) β§ π’ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < )) β π’ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < )) |
419 | 417, 418 | breqtrrd 5176 |
. . . . . . . . . . . . 13
β’
(((((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π:ββΆ( β€ β© (β Γ
β))) β§ π€ β
βͺ ran ((,) β π)) β§ π’ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < )) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ π’) |
420 | 419 | expl 458 |
. . . . . . . . . . . 12
β’
(((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π:ββΆ( β€ β© (β Γ
β))) β ((π€
β βͺ ran ((,) β π) β§ π’ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < )) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ π’)) |
421 | 3, 420 | sylan2 593 |
. . . . . . . . . . 11
β’
(((((π΄ β
β β§ (vol*βπ΄) β β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β§ π β ((
β€ β© (β Γ β)) βm β)) β
((π€ β βͺ ran ((,) β π) β§ π’ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < )) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ π’)) |
422 | 421 | rexlimdva 3155 |
. . . . . . . . . 10
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β (βπ
β (( β€ β© (β Γ β)) βm
β)(π€ β βͺ ran ((,) β π) β§ π’ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < )) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ π’)) |
423 | 422 | ralrimivw 3150 |
. . . . . . . . 9
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β βπ’
β β* (βπ β (( β€ β© (β Γ
β)) βm β)(π€ β βͺ ran
((,) β π) β§ π’ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < )) β
((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ π’)) |
424 | | eqeq1 2736 |
. . . . . . . . . . . 12
β’ (π£ = π’ β (π£ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < ) β π’ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < ))) |
425 | 424 | anbi2d 629 |
. . . . . . . . . . 11
β’ (π£ = π’ β ((π€ β βͺ ran
((,) β π) β§ π£ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < )) β
(π€ β βͺ ran ((,) β π) β§ π’ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < )))) |
426 | 425 | rexbidv 3178 |
. . . . . . . . . 10
β’ (π£ = π’ β (βπ β (( β€ β© (β Γ
β)) βm β)(π€ β βͺ ran
((,) β π) β§ π£ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < )) β
βπ β (( β€
β© (β Γ β)) βm β)(π€ β βͺ ran
((,) β π) β§ π’ = sup(ran seq1( + , ((abs
β β ) β π)), β*, <
)))) |
427 | 426 | ralrab 3689 |
. . . . . . . . 9
β’
(βπ’ β
{π£ β
β* β£ βπ β (( β€ β© (β Γ
β)) βm β)(π€ β βͺ ran
((,) β π) β§ π£ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ))}
((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ π’ β βπ’ β β* (βπ β (( β€ β© (β
Γ β)) βm β)(π€ β βͺ ran
((,) β π) β§ π’ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < )) β
((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ π’)) |
428 | 423, 427 | sylibr 233 |
. . . . . . . 8
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β βπ’
β {π£ β
β* β£ βπ β (( β€ β© (β Γ
β)) βm β)(π€ β βͺ ran
((,) β π) β§ π£ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ))}
((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ π’) |
429 | | ssrab2 4077 |
. . . . . . . . 9
β’ {π£ β β*
β£ βπ β ((
β€ β© (β Γ β)) βm β)(π€ β βͺ ran ((,) β π) β§ π£ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < ))} β β* |
430 | 11 | adantl 482 |
. . . . . . . . 9
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β
β*) |
431 | | infxrgelb 13313 |
. . . . . . . . 9
β’ (({π£ β β*
β£ βπ β ((
β€ β© (β Γ β)) βm β)(π€ β βͺ ran ((,) β π) β§ π£ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < ))} β β* β§
((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β β*) β
(((vol*β(π€ β©
π΄)) + (vol*β(π€ β π΄))) β€ inf({π£ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π€ β βͺ ran
((,) β π) β§ π£ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ))},
β*, < ) β βπ’ β {π£ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π€ β βͺ ran
((,) β π) β§ π£ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ))}
((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ π’)) |
432 | 429, 430,
431 | sylancr 587 |
. . . . . . . 8
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β (((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ inf({π£ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π€ β βͺ ran
((,) β π) β§ π£ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ))},
β*, < ) β βπ’ β {π£ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π€ β βͺ ran
((,) β π) β§ π£ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ))}
((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ π’)) |
433 | 428, 432 | mpbird 256 |
. . . . . . 7
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ inf({π£ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π€ β βͺ ran
((,) β π) β§ π£ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ))},
β*, < )) |
434 | | eqid 2732 |
. . . . . . . . 9
β’ {π£ β β*
β£ βπ β ((
β€ β© (β Γ β)) βm β)(π€ β βͺ ran ((,) β π) β§ π£ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < ))} = {π£ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π€ β βͺ ran
((,) β π) β§ π£ = sup(ran seq1( + , ((abs
β β ) β π)), β*, <
))} |
435 | 434 | ovolval 24989 |
. . . . . . . 8
β’ (π€ β β β
(vol*βπ€) = inf({π£ β β*
β£ βπ β ((
β€ β© (β Γ β)) βm β)(π€ β βͺ ran ((,) β π) β§ π£ = sup(ran seq1( + , ((abs β β )
β π)),
β*, < ))}, β*, < )) |
436 | 435 | ad2antrl 726 |
. . . . . . 7
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β (vol*βπ€) = inf({π£ β β* β£
βπ β (( β€
β© (β Γ β)) βm β)(π€ β βͺ ran
((,) β π) β§ π£ = sup(ran seq1( + , ((abs
β β ) β π)), β*, < ))},
β*, < )) |
437 | 433, 436 | breqtrrd 5176 |
. . . . . 6
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ (π€ β β β§
(vol*βπ€) β
β)) β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (vol*βπ€)) |
438 | 437 | expr 457 |
. . . . 5
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ π€ β β) β
((vol*βπ€) β
β β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (vol*βπ€))) |
439 | 2, 438 | sylan2 593 |
. . . 4
β’ ((((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β§ π€ β π« β)
β ((vol*βπ€)
β β β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (vol*βπ€))) |
440 | 439 | ralrimiva 3146 |
. . 3
β’ (((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β βπ€ β π«
β((vol*βπ€)
β β β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (vol*βπ€))) |
441 | | ismbl2 25043 |
. . . . 5
β’ (π΄ β dom vol β (π΄ β β β§
βπ€ β π«
β((vol*βπ€)
β β β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (vol*βπ€)))) |
442 | 441 | baibr 537 |
. . . 4
β’ (π΄ β β β
(βπ€ β π«
β((vol*βπ€)
β β β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (vol*βπ€)) β π΄ β dom vol)) |
443 | 442 | ad2antrr 724 |
. . 3
β’ (((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β (βπ€ β π«
β((vol*βπ€)
β β β ((vol*β(π€ β© π΄)) + (vol*β(π€ β π΄))) β€ (vol*βπ€)) β π΄ β dom vol)) |
444 | 440, 443 | mpbid 231 |
. 2
β’ (((π΄ β β β§
(vol*βπ΄) β
β) β§ (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < )) β π΄ β dom
vol) |
445 | 1, 444 | impbida 799 |
1
β’ ((π΄ β β β§
(vol*βπ΄) β
β) β (π΄ β
dom vol β (vol*βπ΄) = sup({π¦ β£ βπ β (Clsdβ(topGenβran
(,)))(π β π΄ β§ π¦ = (volβπ))}, β, < ))) |