Step | Hyp | Ref
| Expression |
1 | | nnuz 12663 |
. . 3
β’ β =
(β€β₯β1) |
2 | | eqid 2736 |
. . 3
β’ seq1( + ,
((abs β β ) β (πΎ β π»))) = seq1( + , ((abs β β )
β (πΎ β π»))) |
3 | | 1zzd 12393 |
. . 3
β’ ((π β§ π½ β β) β 1 β
β€) |
4 | | eqidd 2737 |
. . 3
β’ (((π β§ π½ β β) β§ π β β) β (((abs β
β ) β (πΎ
β π»))βπ) = (((abs β β )
β (πΎ β π»))βπ)) |
5 | | uniioombl.1 |
. . . . . . . . . 10
β’ (π β πΉ:ββΆ( β€ β© (β
Γ β))) |
6 | | uniioombl.2 |
. . . . . . . . . 10
β’ (π β Disj π₯ β β
((,)β(πΉβπ₯))) |
7 | | uniioombl.3 |
. . . . . . . . . 10
β’ π = seq1( + , ((abs β
β ) β πΉ)) |
8 | | uniioombl.a |
. . . . . . . . . 10
β’ π΄ = βͺ
ran ((,) β πΉ) |
9 | | uniioombl.e |
. . . . . . . . . 10
β’ (π β (vol*βπΈ) β
β) |
10 | | uniioombl.c |
. . . . . . . . . 10
β’ (π β πΆ β
β+) |
11 | | uniioombl.g |
. . . . . . . . . 10
β’ (π β πΊ:ββΆ( β€ β© (β
Γ β))) |
12 | | uniioombl.s |
. . . . . . . . . 10
β’ (π β πΈ β βͺ ran
((,) β πΊ)) |
13 | | uniioombl.t |
. . . . . . . . . 10
β’ π = seq1( + , ((abs β
β ) β πΊ)) |
14 | | uniioombl.v |
. . . . . . . . . 10
β’ (π β sup(ran π, β*, < ) β€
((vol*βπΈ) + πΆ)) |
15 | 5, 6, 7, 8, 9, 10,
11, 12, 13, 14 | uniioombllem2a 24787 |
. . . . . . . . 9
β’ (((π β§ π½ β β) β§ π§ β β) β (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) β ran (,)) |
16 | | uniioombllem2.h |
. . . . . . . . . 10
β’ π» = (π§ β β β¦ (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) |
17 | 16 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π½ β β) β π» = (π§ β β β¦ (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))))) |
18 | | uniioombllem2.k |
. . . . . . . . . . . 12
β’ πΎ = (π₯ β ran (,) β¦ if(π₯ = β
, β¨0, 0β©, β¨inf(π₯, β*, < ),
sup(π₯, β*,
< )β©)) |
19 | 18 | ioorf 24778 |
. . . . . . . . . . 11
β’ πΎ:ran (,)βΆ( β€ β©
(β* Γ β*)) |
20 | 19 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ π½ β β) β πΎ:ran (,)βΆ( β€ β©
(β* Γ β*))) |
21 | 20 | feqmptd 6865 |
. . . . . . . . 9
β’ ((π β§ π½ β β) β πΎ = (π¦ β ran (,) β¦ (πΎβπ¦))) |
22 | | fveq2 6800 |
. . . . . . . . 9
β’ (π¦ = (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) β (πΎβπ¦) = (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))))) |
23 | 15, 17, 21, 22 | fmptco 7029 |
. . . . . . . 8
β’ ((π β§ π½ β β) β (πΎ β π») = (π§ β β β¦ (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))))) |
24 | | inss2 4169 |
. . . . . . . . . . 11
β’
(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) β ((,)β(πΊβπ½)) |
25 | | inss2 4169 |
. . . . . . . . . . . . . . . 16
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
26 | 11 | ffvelcdmda 6989 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π½ β β) β (πΊβπ½) β ( β€ β© (β Γ
β))) |
27 | 25, 26 | sselid 3924 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π½ β β) β (πΊβπ½) β (β Γ
β)) |
28 | | 1st2nd2 7898 |
. . . . . . . . . . . . . . 15
β’ ((πΊβπ½) β (β Γ β) β
(πΊβπ½) = β¨(1st β(πΊβπ½)), (2nd β(πΊβπ½))β©) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π½ β β) β (πΊβπ½) = β¨(1st β(πΊβπ½)), (2nd β(πΊβπ½))β©) |
30 | 29 | fveq2d 6804 |
. . . . . . . . . . . . 13
β’ ((π β§ π½ β β) β ((,)β(πΊβπ½)) = ((,)ββ¨(1st
β(πΊβπ½)), (2nd
β(πΊβπ½))β©)) |
31 | | df-ov 7306 |
. . . . . . . . . . . . 13
β’
((1st β(πΊβπ½))(,)(2nd β(πΊβπ½))) = ((,)ββ¨(1st
β(πΊβπ½)), (2nd
β(πΊβπ½))β©) |
32 | 30, 31 | eqtr4di 2794 |
. . . . . . . . . . . 12
β’ ((π β§ π½ β β) β ((,)β(πΊβπ½)) = ((1st β(πΊβπ½))(,)(2nd β(πΊβπ½)))) |
33 | | ioossre 13182 |
. . . . . . . . . . . 12
β’
((1st β(πΊβπ½))(,)(2nd β(πΊβπ½))) β β |
34 | 32, 33 | eqsstrdi 3980 |
. . . . . . . . . . 11
β’ ((π β§ π½ β β) β ((,)β(πΊβπ½)) β β) |
35 | 32 | fveq2d 6804 |
. . . . . . . . . . . . 13
β’ ((π β§ π½ β β) β
(vol*β((,)β(πΊβπ½))) = (vol*β((1st
β(πΊβπ½))(,)(2nd
β(πΊβπ½))))) |
36 | | ovolfcl 24671 |
. . . . . . . . . . . . . . 15
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ π½ β β) β ((1st
β(πΊβπ½)) β β β§
(2nd β(πΊβπ½)) β β β§ (1st
β(πΊβπ½)) β€ (2nd
β(πΊβπ½)))) |
37 | 11, 36 | sylan 581 |
. . . . . . . . . . . . . 14
β’ ((π β§ π½ β β) β ((1st
β(πΊβπ½)) β β β§
(2nd β(πΊβπ½)) β β β§ (1st
β(πΊβπ½)) β€ (2nd
β(πΊβπ½)))) |
38 | | ovolioo 24773 |
. . . . . . . . . . . . . 14
β’
(((1st β(πΊβπ½)) β β β§ (2nd
β(πΊβπ½)) β β β§
(1st β(πΊβπ½)) β€ (2nd β(πΊβπ½))) β (vol*β((1st
β(πΊβπ½))(,)(2nd
β(πΊβπ½)))) = ((2nd
β(πΊβπ½)) β (1st
β(πΊβπ½)))) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π½ β β) β
(vol*β((1st β(πΊβπ½))(,)(2nd β(πΊβπ½)))) = ((2nd β(πΊβπ½)) β (1st β(πΊβπ½)))) |
40 | 35, 39 | eqtrd 2776 |
. . . . . . . . . . . 12
β’ ((π β§ π½ β β) β
(vol*β((,)β(πΊβπ½))) = ((2nd β(πΊβπ½)) β (1st β(πΊβπ½)))) |
41 | 37 | simp2d 1143 |
. . . . . . . . . . . . 13
β’ ((π β§ π½ β β) β (2nd
β(πΊβπ½)) β
β) |
42 | 37 | simp1d 1142 |
. . . . . . . . . . . . 13
β’ ((π β§ π½ β β) β (1st
β(πΊβπ½)) β
β) |
43 | 41, 42 | resubcld 11445 |
. . . . . . . . . . . 12
β’ ((π β§ π½ β β) β ((2nd
β(πΊβπ½)) β (1st
β(πΊβπ½))) β
β) |
44 | 40, 43 | eqeltrd 2837 |
. . . . . . . . . . 11
β’ ((π β§ π½ β β) β
(vol*β((,)β(πΊβπ½))) β β) |
45 | | ovolsscl 24691 |
. . . . . . . . . . 11
β’
(((((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) β ((,)β(πΊβπ½)) β§ ((,)β(πΊβπ½)) β β β§
(vol*β((,)β(πΊβπ½))) β β) β
(vol*β(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) β β) |
46 | 24, 34, 44, 45 | mp3an2i 1466 |
. . . . . . . . . 10
β’ ((π β§ π½ β β) β
(vol*β(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) β β) |
47 | 46 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π½ β β) β§ π§ β β) β
(vol*β(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) β β) |
48 | 18 | ioorcl 24782 |
. . . . . . . . 9
β’
(((((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) β ran (,) β§
(vol*β(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) β β) β (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) β ( β€ β© (β Γ
β))) |
49 | 15, 47, 48 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π½ β β) β§ π§ β β) β (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) β ( β€ β© (β Γ
β))) |
50 | 23, 49 | fmpt3d 7018 |
. . . . . . 7
β’ ((π β§ π½ β β) β (πΎ β π»):ββΆ( β€ β© (β
Γ β))) |
51 | | eqid 2736 |
. . . . . . . 8
β’ ((abs
β β ) β (πΎ β π»)) = ((abs β β ) β (πΎ β π»)) |
52 | 51 | ovolfsf 24676 |
. . . . . . 7
β’ ((πΎ β π»):ββΆ( β€ β© (β
Γ β)) β ((abs β β ) β (πΎ β π»)):ββΆ(0[,)+β)) |
53 | 50, 52 | syl 17 |
. . . . . 6
β’ ((π β§ π½ β β) β ((abs β
β ) β (πΎ
β π»)):ββΆ(0[,)+β)) |
54 | 53 | ffvelcdmda 6989 |
. . . . 5
β’ (((π β§ π½ β β) β§ π β β) β (((abs β
β ) β (πΎ
β π»))βπ) β
(0[,)+β)) |
55 | | elrege0 13228 |
. . . . 5
β’ ((((abs
β β ) β (πΎ β π»))βπ) β (0[,)+β) β ((((abs
β β ) β (πΎ β π»))βπ) β β β§ 0 β€ (((abs β
β ) β (πΎ
β π»))βπ))) |
56 | 54, 55 | sylib 217 |
. . . 4
β’ (((π β§ π½ β β) β§ π β β) β ((((abs β
β ) β (πΎ
β π»))βπ) β β β§ 0 β€
(((abs β β ) β (πΎ β π»))βπ))) |
57 | 56 | simpld 496 |
. . 3
β’ (((π β§ π½ β β) β§ π β β) β (((abs β
β ) β (πΎ
β π»))βπ) β
β) |
58 | 56 | simprd 497 |
. . 3
β’ (((π β§ π½ β β) β§ π β β) β 0 β€ (((abs β
β ) β (πΎ
β π»))βπ)) |
59 | 23 | fveq1d 6802 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π½ β β) β ((πΎ β π»)βπ§) = ((π§ β β β¦ (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))))βπ§)) |
60 | | fvex 6813 |
. . . . . . . . . . . . . . . 16
β’ (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) β V |
61 | | eqid 2736 |
. . . . . . . . . . . . . . . . 17
β’ (π§ β β β¦ (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))))) = (π§ β β β¦ (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))))) |
62 | 61 | fvmpt2 6914 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β β β§ (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) β V) β ((π§ β β β¦ (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))))βπ§) = (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))))) |
63 | 60, 62 | mpan2 689 |
. . . . . . . . . . . . . . 15
β’ (π§ β β β ((π§ β β β¦ (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))))βπ§) = (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))))) |
64 | 59, 63 | sylan9eq 2796 |
. . . . . . . . . . . . . 14
β’ (((π β§ π½ β β) β§ π§ β β) β ((πΎ β π»)βπ§) = (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))))) |
65 | 64 | fveq2d 6804 |
. . . . . . . . . . . . 13
β’ (((π β§ π½ β β) β§ π§ β β) β ((,)β((πΎ β π»)βπ§)) = ((,)β(πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))))) |
66 | 18 | ioorinv 24781 |
. . . . . . . . . . . . . 14
β’
((((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) β ran (,) β ((,)β(πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))))) = (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) |
67 | 15, 66 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π½ β β) β§ π§ β β) β ((,)β(πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))))) = (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) |
68 | 65, 67 | eqtrd 2776 |
. . . . . . . . . . . 12
β’ (((π β§ π½ β β) β§ π§ β β) β ((,)β((πΎ β π»)βπ§)) = (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) |
69 | 68 | ralrimiva 3140 |
. . . . . . . . . . 11
β’ ((π β§ π½ β β) β βπ§ β β
((,)β((πΎ β
π»)βπ§)) = (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) |
70 | | 2fveq3 6805 |
. . . . . . . . . . . . 13
β’ (π§ = π₯ β ((,)β((πΎ β π»)βπ§)) = ((,)β((πΎ β π»)βπ₯))) |
71 | | 2fveq3 6805 |
. . . . . . . . . . . . . 14
β’ (π§ = π₯ β ((,)β(πΉβπ§)) = ((,)β(πΉβπ₯))) |
72 | 71 | ineq1d 4151 |
. . . . . . . . . . . . 13
β’ (π§ = π₯ β (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) = (((,)β(πΉβπ₯)) β© ((,)β(πΊβπ½)))) |
73 | 70, 72 | eqeq12d 2752 |
. . . . . . . . . . . 12
β’ (π§ = π₯ β (((,)β((πΎ β π»)βπ§)) = (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) β ((,)β((πΎ β π»)βπ₯)) = (((,)β(πΉβπ₯)) β© ((,)β(πΊβπ½))))) |
74 | 73 | rspccva 3565 |
. . . . . . . . . . 11
β’
((βπ§ β
β ((,)β((πΎ
β π»)βπ§)) = (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) β§ π₯ β β) β ((,)β((πΎ β π»)βπ₯)) = (((,)β(πΉβπ₯)) β© ((,)β(πΊβπ½)))) |
75 | 69, 74 | sylan 581 |
. . . . . . . . . 10
β’ (((π β§ π½ β β) β§ π₯ β β) β ((,)β((πΎ β π»)βπ₯)) = (((,)β(πΉβπ₯)) β© ((,)β(πΊβπ½)))) |
76 | | inss1 4168 |
. . . . . . . . . 10
β’
(((,)β(πΉβπ₯)) β© ((,)β(πΊβπ½))) β ((,)β(πΉβπ₯)) |
77 | 75, 76 | eqsstrdi 3980 |
. . . . . . . . 9
β’ (((π β§ π½ β β) β§ π₯ β β) β ((,)β((πΎ β π»)βπ₯)) β ((,)β(πΉβπ₯))) |
78 | 77 | ralrimiva 3140 |
. . . . . . . 8
β’ ((π β§ π½ β β) β βπ₯ β β
((,)β((πΎ β
π»)βπ₯)) β ((,)β(πΉβπ₯))) |
79 | 6 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π½ β β) β Disj π₯ β β
((,)β(πΉβπ₯))) |
80 | | disjss2 5049 |
. . . . . . . 8
β’
(βπ₯ β
β ((,)β((πΎ
β π»)βπ₯)) β ((,)β(πΉβπ₯)) β (Disj π₯ β β ((,)β(πΉβπ₯)) β Disj π₯ β β ((,)β((πΎ β π»)βπ₯)))) |
81 | 78, 79, 80 | sylc 65 |
. . . . . . 7
β’ ((π β§ π½ β β) β Disj π₯ β β
((,)β((πΎ β
π»)βπ₯))) |
82 | 50, 81, 2 | uniioovol 24784 |
. . . . . 6
β’ ((π β§ π½ β β) β (vol*ββͺ ran ((,) β (πΎ β π»))) = sup(ran seq1( + , ((abs β
β ) β (πΎ
β π»))),
β*, < )) |
83 | 67 | mpteq2dva 5181 |
. . . . . . . . . . 11
β’ ((π β§ π½ β β) β (π§ β β β¦ ((,)β(πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))))) = (π§ β β β¦ (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))))) |
84 | | rexpssxrxp 11062 |
. . . . . . . . . . . . . 14
β’ (β
Γ β) β (β* Γ
β*) |
85 | 25, 84 | sstri 3935 |
. . . . . . . . . . . . 13
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
86 | 85, 49 | sselid 3924 |
. . . . . . . . . . . 12
β’ (((π β§ π½ β β) β§ π§ β β) β (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) β (β* Γ
β*)) |
87 | | ioof 13221 |
. . . . . . . . . . . . . 14
β’
(,):(β* Γ β*)βΆπ«
β |
88 | 87 | a1i 11 |
. . . . . . . . . . . . 13
β’ ((π β§ π½ β β) β
(,):(β* Γ β*)βΆπ«
β) |
89 | 88 | feqmptd 6865 |
. . . . . . . . . . . 12
β’ ((π β§ π½ β β) β (,) = (π¦ β (β*
Γ β*) β¦ ((,)βπ¦))) |
90 | | fveq2 6800 |
. . . . . . . . . . . 12
β’ (π¦ = (πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) β ((,)βπ¦) = ((,)β(πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))))) |
91 | 86, 23, 89, 90 | fmptco 7029 |
. . . . . . . . . . 11
β’ ((π β§ π½ β β) β ((,) β (πΎ β π»)) = (π§ β β β¦ ((,)β(πΎβ(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))))))) |
92 | 83, 91, 17 | 3eqtr4d 2786 |
. . . . . . . . . 10
β’ ((π β§ π½ β β) β ((,) β (πΎ β π»)) = π») |
93 | 92 | rneqd 5855 |
. . . . . . . . 9
β’ ((π β§ π½ β β) β ran ((,) β
(πΎ β π»)) = ran π») |
94 | 93 | unieqd 4858 |
. . . . . . . 8
β’ ((π β§ π½ β β) β βͺ ran ((,) β (πΎ β π»)) = βͺ ran π») |
95 | | fvex 6813 |
. . . . . . . . . . . . . 14
β’
((,)β(πΉβπ§)) β V |
96 | 95 | inex1 5250 |
. . . . . . . . . . . . 13
β’
(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) β V |
97 | 16 | fvmpt2 6914 |
. . . . . . . . . . . . 13
β’ ((π§ β β β§
(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) β V) β (π»βπ§) = (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) |
98 | 96, 97 | mpan2 689 |
. . . . . . . . . . . 12
β’ (π§ β β β (π»βπ§) = (((,)β(πΉβπ§)) β© ((,)β(πΊβπ½)))) |
99 | | incom 4141 |
. . . . . . . . . . . 12
β’
(((,)β(πΉβπ§)) β© ((,)β(πΊβπ½))) = (((,)β(πΊβπ½)) β© ((,)β(πΉβπ§))) |
100 | 98, 99 | eqtrdi 2792 |
. . . . . . . . . . 11
β’ (π§ β β β (π»βπ§) = (((,)β(πΊβπ½)) β© ((,)β(πΉβπ§)))) |
101 | 100 | iuneq2i 4952 |
. . . . . . . . . 10
β’ βͺ π§ β β (π»βπ§) = βͺ π§ β β
(((,)β(πΊβπ½)) β© ((,)β(πΉβπ§))) |
102 | | iunin2 5007 |
. . . . . . . . . 10
β’ βͺ π§ β β (((,)β(πΊβπ½)) β© ((,)β(πΉβπ§))) = (((,)β(πΊβπ½)) β© βͺ
π§ β β
((,)β(πΉβπ§))) |
103 | 101, 102 | eqtri 2764 |
. . . . . . . . 9
β’ βͺ π§ β β (π»βπ§) = (((,)β(πΊβπ½)) β© βͺ
π§ β β
((,)β(πΉβπ§))) |
104 | 15, 16 | fmptd 7016 |
. . . . . . . . . . 11
β’ ((π β§ π½ β β) β π»:ββΆran (,)) |
105 | 104 | ffnd 6627 |
. . . . . . . . . 10
β’ ((π β§ π½ β β) β π» Fn β) |
106 | | fniunfv 7148 |
. . . . . . . . . 10
β’ (π» Fn β β βͺ π§ β β (π»βπ§) = βͺ ran π») |
107 | 105, 106 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π½ β β) β βͺ π§ β β (π»βπ§) = βͺ ran π») |
108 | 103, 107 | eqtr3id 2790 |
. . . . . . . 8
β’ ((π β§ π½ β β) β (((,)β(πΊβπ½)) β© βͺ
π§ β β
((,)β(πΉβπ§))) = βͺ ran π») |
109 | 5 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π½ β β) β πΉ:ββΆ( β€ β© (β
Γ β))) |
110 | | fvco3 6895 |
. . . . . . . . . . . 12
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π§ β β) β (((,) β πΉ)βπ§) = ((,)β(πΉβπ§))) |
111 | 109, 110 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β§ π½ β β) β§ π§ β β) β (((,) β πΉ)βπ§) = ((,)β(πΉβπ§))) |
112 | 111 | iuneq2dv 4955 |
. . . . . . . . . 10
β’ ((π β§ π½ β β) β βͺ π§ β β (((,) β πΉ)βπ§) = βͺ π§ β β
((,)β(πΉβπ§))) |
113 | | ffn 6626 |
. . . . . . . . . . . . . 14
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
114 | 87, 113 | ax-mp 5 |
. . . . . . . . . . . . 13
β’ (,) Fn
(β* Γ β*) |
115 | | fss 6643 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β* Γ β*)) β πΉ:ββΆ(β* Γ
β*)) |
116 | 109, 85, 115 | sylancl 587 |
. . . . . . . . . . . . 13
β’ ((π β§ π½ β β) β πΉ:ββΆ(β* Γ
β*)) |
117 | | fnfco 6665 |
. . . . . . . . . . . . 13
β’ (((,) Fn
(β* Γ β*) β§ πΉ:ββΆ(β* Γ
β*)) β ((,) β πΉ) Fn β) |
118 | 114, 116,
117 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ π½ β β) β ((,) β πΉ) Fn β) |
119 | | fniunfv 7148 |
. . . . . . . . . . . 12
β’ (((,)
β πΉ) Fn β
β βͺ π§ β β (((,) β πΉ)βπ§) = βͺ ran ((,)
β πΉ)) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π½ β β) β βͺ π§ β β (((,) β πΉ)βπ§) = βͺ ran ((,)
β πΉ)) |
121 | 120, 8 | eqtr4di 2794 |
. . . . . . . . . 10
β’ ((π β§ π½ β β) β βͺ π§ β β (((,) β πΉ)βπ§) = π΄) |
122 | 112, 121 | eqtr3d 2778 |
. . . . . . . . 9
β’ ((π β§ π½ β β) β βͺ π§ β β ((,)β(πΉβπ§)) = π΄) |
123 | 122 | ineq2d 4152 |
. . . . . . . 8
β’ ((π β§ π½ β β) β (((,)β(πΊβπ½)) β© βͺ
π§ β β
((,)β(πΉβπ§))) = (((,)β(πΊβπ½)) β© π΄)) |
124 | 94, 108, 123 | 3eqtr2d 2782 |
. . . . . . 7
β’ ((π β§ π½ β β) β βͺ ran ((,) β (πΎ β π»)) = (((,)β(πΊβπ½)) β© π΄)) |
125 | 124 | fveq2d 6804 |
. . . . . 6
β’ ((π β§ π½ β β) β (vol*ββͺ ran ((,) β (πΎ β π»))) = (vol*β(((,)β(πΊβπ½)) β© π΄))) |
126 | 82, 125 | eqtr3d 2778 |
. . . . 5
β’ ((π β§ π½ β β) β sup(ran seq1( + ,
((abs β β ) β (πΎ β π»))), β*, < ) =
(vol*β(((,)β(πΊβπ½)) β© π΄))) |
127 | | inss1 4168 |
. . . . . 6
β’
(((,)β(πΊβπ½)) β© π΄) β ((,)β(πΊβπ½)) |
128 | | ovolsscl 24691 |
. . . . . 6
β’
(((((,)β(πΊβπ½)) β© π΄) β ((,)β(πΊβπ½)) β§ ((,)β(πΊβπ½)) β β β§
(vol*β((,)β(πΊβπ½))) β β) β
(vol*β(((,)β(πΊβπ½)) β© π΄)) β β) |
129 | 127, 34, 44, 128 | mp3an2i 1466 |
. . . . 5
β’ ((π β§ π½ β β) β
(vol*β(((,)β(πΊβπ½)) β© π΄)) β β) |
130 | 126, 129 | eqeltrd 2837 |
. . . 4
β’ ((π β§ π½ β β) β sup(ran seq1( + ,
((abs β β ) β (πΎ β π»))), β*, < ) β
β) |
131 | 51, 2 | ovolsf 24677 |
. . . . . . . . 9
β’ ((πΎ β π»):ββΆ( β€ β© (β
Γ β)) β seq1( + , ((abs β β ) β (πΎ β π»))):ββΆ(0[,)+β)) |
132 | 50, 131 | syl 17 |
. . . . . . . 8
β’ ((π β§ π½ β β) β seq1( + , ((abs
β β ) β (πΎ β π»))):ββΆ(0[,)+β)) |
133 | 132 | frnd 6634 |
. . . . . . 7
β’ ((π β§ π½ β β) β ran seq1( + , ((abs
β β ) β (πΎ β π»))) β (0[,)+β)) |
134 | | icossxr 13206 |
. . . . . . 7
β’
(0[,)+β) β β* |
135 | 133, 134 | sstrdi 3938 |
. . . . . 6
β’ ((π β§ π½ β β) β ran seq1( + , ((abs
β β ) β (πΎ β π»))) β
β*) |
136 | 132 | ffnd 6627 |
. . . . . . 7
β’ ((π β§ π½ β β) β seq1( + , ((abs
β β ) β (πΎ β π»))) Fn β) |
137 | | fnfvelrn 6986 |
. . . . . . 7
β’ ((seq1( +
, ((abs β β ) β (πΎ β π»))) Fn β β§ π¦ β β) β (seq1( + , ((abs
β β ) β (πΎ β π»)))βπ¦) β ran seq1( + , ((abs β β
) β (πΎ β π»)))) |
138 | 136, 137 | sylan 581 |
. . . . . 6
β’ (((π β§ π½ β β) β§ π¦ β β) β (seq1( + , ((abs
β β ) β (πΎ β π»)))βπ¦) β ran seq1( + , ((abs β β
) β (πΎ β π»)))) |
139 | | supxrub 13100 |
. . . . . 6
β’ ((ran
seq1( + , ((abs β β ) β (πΎ β π»))) β β* β§ (seq1(
+ , ((abs β β ) β (πΎ β π»)))βπ¦) β ran seq1( + , ((abs β β
) β (πΎ β π»)))) β (seq1( + , ((abs
β β ) β (πΎ β π»)))βπ¦) β€ sup(ran seq1( + , ((abs β
β ) β (πΎ
β π»))),
β*, < )) |
140 | 135, 138,
139 | syl2an2r 683 |
. . . . 5
β’ (((π β§ π½ β β) β§ π¦ β β) β (seq1( + , ((abs
β β ) β (πΎ β π»)))βπ¦) β€ sup(ran seq1( + , ((abs β
β ) β (πΎ
β π»))),
β*, < )) |
141 | 140 | ralrimiva 3140 |
. . . 4
β’ ((π β§ π½ β β) β βπ¦ β β (seq1( + , ((abs
β β ) β (πΎ β π»)))βπ¦) β€ sup(ran seq1( + , ((abs β
β ) β (πΎ
β π»))),
β*, < )) |
142 | | brralrspcev 5141 |
. . . 4
β’ ((sup(ran
seq1( + , ((abs β β ) β (πΎ β π»))), β*, < ) β
β β§ βπ¦
β β (seq1( + , ((abs β β ) β (πΎ β π»)))βπ¦) β€ sup(ran seq1( + , ((abs β
β ) β (πΎ
β π»))),
β*, < )) β βπ₯ β β βπ¦ β β (seq1( + , ((abs β
β ) β (πΎ
β π»)))βπ¦) β€ π₯) |
143 | 130, 141,
142 | syl2anc 585 |
. . 3
β’ ((π β§ π½ β β) β βπ₯ β β βπ¦ β β (seq1( + , ((abs
β β ) β (πΎ β π»)))βπ¦) β€ π₯) |
144 | 1, 2, 3, 4, 57, 58, 143 | isumsup2 15599 |
. 2
β’ ((π β§ π½ β β) β seq1( + , ((abs
β β ) β (πΎ β π»))) β sup(ran seq1( + , ((abs β
β ) β (πΎ
β π»))), β, <
)) |
145 | 51 | ovolfs2 24776 |
. . . . 5
β’ ((πΎ β π»):ββΆ( β€ β© (β
Γ β)) β ((abs β β ) β (πΎ β π»)) = ((vol* β (,)) β (πΎ β π»))) |
146 | 50, 145 | syl 17 |
. . . 4
β’ ((π β§ π½ β β) β ((abs β
β ) β (πΎ
β π»)) = ((vol*
β (,)) β (πΎ
β π»))) |
147 | | coass 6179 |
. . . . 5
β’ ((vol*
β (,)) β (πΎ
β π»)) = (vol* β
((,) β (πΎ β
π»))) |
148 | 92 | coeq2d 5780 |
. . . . 5
β’ ((π β§ π½ β β) β (vol* β ((,)
β (πΎ β π»))) = (vol* β π»)) |
149 | 147, 148 | eqtrid 2788 |
. . . 4
β’ ((π β§ π½ β β) β ((vol* β (,))
β (πΎ β π»)) = (vol* β π»)) |
150 | 146, 149 | eqtrd 2776 |
. . 3
β’ ((π β§ π½ β β) β ((abs β
β ) β (πΎ
β π»)) = (vol* β
π»)) |
151 | 150 | seqeq3d 13771 |
. 2
β’ ((π β§ π½ β β) β seq1( + , ((abs
β β ) β (πΎ β π»))) = seq1( + , (vol* β π»))) |
152 | | rge0ssre 13230 |
. . . . 5
β’
(0[,)+β) β β |
153 | 133, 152 | sstrdi 3938 |
. . . 4
β’ ((π β§ π½ β β) β ran seq1( + , ((abs
β β ) β (πΎ β π»))) β β) |
154 | | 1nn 12026 |
. . . . . . 7
β’ 1 β
β |
155 | 132 | fdmd 6637 |
. . . . . . 7
β’ ((π β§ π½ β β) β dom seq1( + , ((abs
β β ) β (πΎ β π»))) = β) |
156 | 154, 155 | eleqtrrid 2844 |
. . . . . 6
β’ ((π β§ π½ β β) β 1 β dom seq1( +
, ((abs β β ) β (πΎ β π»)))) |
157 | 156 | ne0d 4275 |
. . . . 5
β’ ((π β§ π½ β β) β dom seq1( + , ((abs
β β ) β (πΎ β π»))) β β
) |
158 | | dm0rn0 5842 |
. . . . . 6
β’ (dom
seq1( + , ((abs β β ) β (πΎ β π»))) = β
β ran seq1( + , ((abs
β β ) β (πΎ β π»))) = β
) |
159 | 158 | necon3bii 2994 |
. . . . 5
β’ (dom
seq1( + , ((abs β β ) β (πΎ β π»))) β β
β ran seq1( + , ((abs
β β ) β (πΎ β π»))) β β
) |
160 | 157, 159 | sylib 217 |
. . . 4
β’ ((π β§ π½ β β) β ran seq1( + , ((abs
β β ) β (πΎ β π»))) β β
) |
161 | | breq1 5084 |
. . . . . . . 8
β’ (π§ = (seq1( + , ((abs β
β ) β (πΎ
β π»)))βπ¦) β (π§ β€ π₯ β (seq1( + , ((abs β β )
β (πΎ β π»)))βπ¦) β€ π₯)) |
162 | 161 | ralrn 6992 |
. . . . . . 7
β’ (seq1( +
, ((abs β β ) β (πΎ β π»))) Fn β β (βπ§ β ran seq1( + , ((abs
β β ) β (πΎ β π»)))π§ β€ π₯ β βπ¦ β β (seq1( + , ((abs β
β ) β (πΎ
β π»)))βπ¦) β€ π₯)) |
163 | 136, 162 | syl 17 |
. . . . . 6
β’ ((π β§ π½ β β) β (βπ§ β ran seq1( + , ((abs
β β ) β (πΎ β π»)))π§ β€ π₯ β βπ¦ β β (seq1( + , ((abs β
β ) β (πΎ
β π»)))βπ¦) β€ π₯)) |
164 | 163 | rexbidv 3172 |
. . . . 5
β’ ((π β§ π½ β β) β (βπ₯ β β βπ§ β ran seq1( + , ((abs
β β ) β (πΎ β π»)))π§ β€ π₯ β βπ₯ β β βπ¦ β β (seq1( + , ((abs β
β ) β (πΎ
β π»)))βπ¦) β€ π₯)) |
165 | 143, 164 | mpbird 258 |
. . . 4
β’ ((π β§ π½ β β) β βπ₯ β β βπ§ β ran seq1( + , ((abs
β β ) β (πΎ β π»)))π§ β€ π₯) |
166 | | supxrre 13103 |
. . . 4
β’ ((ran
seq1( + , ((abs β β ) β (πΎ β π»))) β β β§ ran seq1( + ,
((abs β β ) β (πΎ β π»))) β β
β§ βπ₯ β β βπ§ β ran seq1( + , ((abs
β β ) β (πΎ β π»)))π§ β€ π₯) β sup(ran seq1( + , ((abs β
β ) β (πΎ
β π»))),
β*, < ) = sup(ran seq1( + , ((abs β β ) β
(πΎ β π»))), β, <
)) |
167 | 153, 160,
165, 166 | syl3anc 1371 |
. . 3
β’ ((π β§ π½ β β) β sup(ran seq1( + ,
((abs β β ) β (πΎ β π»))), β*, < ) = sup(ran
seq1( + , ((abs β β ) β (πΎ β π»))), β, < )) |
168 | 167, 126 | eqtr3d 2778 |
. 2
β’ ((π β§ π½ β β) β sup(ran seq1( + ,
((abs β β ) β (πΎ β π»))), β, < ) =
(vol*β(((,)β(πΊβπ½)) β© π΄))) |
169 | 144, 151,
168 | 3brtr3d 5112 |
1
β’ ((π β§ π½ β β) β seq1( + , (vol*
β π»)) β
(vol*β(((,)β(πΊβπ½)) β© π΄))) |