Step | Hyp | Ref
| Expression |
1 | | ioof 13373 |
. . . . . 6
β’
(,):(β* Γ β*)βΆπ«
β |
2 | | uniioombl.1 |
. . . . . . 7
β’ (π β πΉ:ββΆ( β€ β© (β
Γ β))) |
3 | | inss2 4193 |
. . . . . . . 8
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
4 | | rexpssxrxp 11208 |
. . . . . . . 8
β’ (β
Γ β) β (β* Γ
β*) |
5 | 3, 4 | sstri 3957 |
. . . . . . 7
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
6 | | fss 6689 |
. . . . . . 7
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β* Γ β*)) β πΉ:ββΆ(β* Γ
β*)) |
7 | 2, 5, 6 | sylancl 587 |
. . . . . 6
β’ (π β πΉ:ββΆ(β* Γ
β*)) |
8 | | fco 6696 |
. . . . . 6
β’
(((,):(β* Γ β*)βΆπ«
β β§ πΉ:ββΆ(β* Γ
β*)) β ((,) β πΉ):ββΆπ«
β) |
9 | 1, 7, 8 | sylancr 588 |
. . . . 5
β’ (π β ((,) β πΉ):ββΆπ«
β) |
10 | 9 | frnd 6680 |
. . . 4
β’ (π β ran ((,) β πΉ) β π«
β) |
11 | | sspwuni 5064 |
. . . 4
β’ (ran ((,)
β πΉ) β
π« β β βͺ ran ((,) β πΉ) β
β) |
12 | 10, 11 | sylib 217 |
. . 3
β’ (π β βͺ ran ((,) β πΉ) β β) |
13 | | ovolcl 24865 |
. . 3
β’ (βͺ ran ((,) β πΉ) β β β (vol*ββͺ ran ((,) β πΉ)) β
β*) |
14 | 12, 13 | syl 17 |
. 2
β’ (π β (vol*ββͺ ran ((,) β πΉ)) β
β*) |
15 | | eqid 2733 |
. . . . . 6
β’ ((abs
β β ) β πΉ) = ((abs β β ) β πΉ) |
16 | | uniioombl.3 |
. . . . . 6
β’ π = seq1( + , ((abs β
β ) β πΉ)) |
17 | 15, 16 | ovolsf 24859 |
. . . . 5
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β π:ββΆ(0[,)+β)) |
18 | | frn 6679 |
. . . . 5
β’ (π:ββΆ(0[,)+β)
β ran π β
(0[,)+β)) |
19 | 2, 17, 18 | 3syl 18 |
. . . 4
β’ (π β ran π β (0[,)+β)) |
20 | | icossxr 13358 |
. . . 4
β’
(0[,)+β) β β* |
21 | 19, 20 | sstrdi 3960 |
. . 3
β’ (π β ran π β
β*) |
22 | | supxrcl 13243 |
. . 3
β’ (ran
π β
β* β sup(ran π, β*, < ) β
β*) |
23 | 21, 22 | syl 17 |
. 2
β’ (π β sup(ran π, β*, < ) β
β*) |
24 | | ssid 3970 |
. . 3
β’ βͺ ran ((,) β πΉ) β βͺ ran
((,) β πΉ) |
25 | 16 | ovollb 24866 |
. . 3
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ βͺ ran ((,) β
πΉ) β βͺ ran ((,) β πΉ)) β (vol*ββͺ ran ((,) β πΉ)) β€ sup(ran π, β*, <
)) |
26 | 2, 24, 25 | sylancl 587 |
. 2
β’ (π β (vol*ββͺ ran ((,) β πΉ)) β€ sup(ran π, β*, <
)) |
27 | 16 | fveq1i 6847 |
. . . . . . . 8
β’ (πβπ) = (seq1( + , ((abs β β )
β πΉ))βπ) |
28 | 2 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β πΉ:ββΆ( β€ β© (β
Γ β))) |
29 | | elfznn 13479 |
. . . . . . . . . . 11
β’ (π₯ β (1...π) β π₯ β β) |
30 | 15 | ovolfsval 24857 |
. . . . . . . . . . 11
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (((abs β
β ) β πΉ)βπ₯) = ((2nd β(πΉβπ₯)) β (1st β(πΉβπ₯)))) |
31 | 28, 29, 30 | syl2an 597 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (((abs β β ) β
πΉ)βπ₯) = ((2nd β(πΉβπ₯)) β (1st β(πΉβπ₯)))) |
32 | | fvco3 6944 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (((,) β πΉ)βπ₯) = ((,)β(πΉβπ₯))) |
33 | 28, 29, 32 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (((,) β πΉ)βπ₯) = ((,)β(πΉβπ₯))) |
34 | | ffvelcdm 7036 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (πΉβπ₯) β ( β€ β© (β Γ
β))) |
35 | 28, 29, 34 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (πΉβπ₯) β ( β€ β© (β Γ
β))) |
36 | 35 | elin2d 4163 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (πΉβπ₯) β (β Γ
β)) |
37 | | 1st2nd2 7964 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβπ₯) β (β Γ β) β
(πΉβπ₯) = β¨(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))β©) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (πΉβπ₯) = β¨(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))β©) |
39 | 38 | fveq2d 6850 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π₯ β (1...π)) β ((,)β(πΉβπ₯)) = ((,)ββ¨(1st
β(πΉβπ₯)), (2nd
β(πΉβπ₯))β©)) |
40 | | df-ov 7364 |
. . . . . . . . . . . . . . 15
β’
((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯))) = ((,)ββ¨(1st
β(πΉβπ₯)), (2nd
β(πΉβπ₯))β©) |
41 | 39, 40 | eqtr4di 2791 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π₯ β (1...π)) β ((,)β(πΉβπ₯)) = ((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯)))) |
42 | 33, 41 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (((,) β πΉ)βπ₯) = ((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯)))) |
43 | | ioombl 24952 |
. . . . . . . . . . . . 13
β’
((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯))) β dom vol |
44 | 42, 43 | eqeltrdi 2842 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (((,) β πΉ)βπ₯) β dom vol) |
45 | | mblvol 24917 |
. . . . . . . . . . . 12
β’ ((((,)
β πΉ)βπ₯) β dom vol β
(volβ(((,) β πΉ)βπ₯)) = (vol*β(((,) β πΉ)βπ₯))) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (volβ(((,) β πΉ)βπ₯)) = (vol*β(((,) β πΉ)βπ₯))) |
47 | 42 | fveq2d 6850 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (vol*β(((,) β πΉ)βπ₯)) = (vol*β((1st
β(πΉβπ₯))(,)(2nd
β(πΉβπ₯))))) |
48 | | ovolfcl 24853 |
. . . . . . . . . . . . 13
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β ((1st
β(πΉβπ₯)) β β β§
(2nd β(πΉβπ₯)) β β β§ (1st
β(πΉβπ₯)) β€ (2nd
β(πΉβπ₯)))) |
49 | 28, 29, 48 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β (1...π)) β ((1st β(πΉβπ₯)) β β β§ (2nd
β(πΉβπ₯)) β β β§
(1st β(πΉβπ₯)) β€ (2nd β(πΉβπ₯)))) |
50 | | ovolioo 24955 |
. . . . . . . . . . . 12
β’
(((1st β(πΉβπ₯)) β β β§ (2nd
β(πΉβπ₯)) β β β§
(1st β(πΉβπ₯)) β€ (2nd β(πΉβπ₯))) β (vol*β((1st
β(πΉβπ₯))(,)(2nd
β(πΉβπ₯)))) = ((2nd
β(πΉβπ₯)) β (1st
β(πΉβπ₯)))) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (vol*β((1st
β(πΉβπ₯))(,)(2nd
β(πΉβπ₯)))) = ((2nd
β(πΉβπ₯)) β (1st
β(πΉβπ₯)))) |
52 | 46, 47, 51 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (volβ(((,) β πΉ)βπ₯)) = ((2nd β(πΉβπ₯)) β (1st β(πΉβπ₯)))) |
53 | 31, 52 | eqtr4d 2776 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (((abs β β ) β
πΉ)βπ₯) = (volβ(((,) β πΉ)βπ₯))) |
54 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π β β) |
55 | | nnuz 12814 |
. . . . . . . . . 10
β’ β =
(β€β₯β1) |
56 | 54, 55 | eleqtrdi 2844 |
. . . . . . . . 9
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
57 | 49 | simp2d 1144 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (2nd β(πΉβπ₯)) β β) |
58 | 49 | simp1d 1143 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (1st β(πΉβπ₯)) β β) |
59 | 57, 58 | resubcld 11591 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β (1...π)) β ((2nd β(πΉβπ₯)) β (1st β(πΉβπ₯))) β β) |
60 | 52, 59 | eqeltrd 2834 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (volβ(((,) β πΉ)βπ₯)) β β) |
61 | 60 | recnd 11191 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β (1...π)) β (volβ(((,) β πΉ)βπ₯)) β β) |
62 | 53, 56, 61 | fsumser 15623 |
. . . . . . . 8
β’ ((π β§ π β β) β Ξ£π₯ β (1...π)(volβ(((,) β πΉ)βπ₯)) = (seq1( + , ((abs β β )
β πΉ))βπ)) |
63 | 27, 62 | eqtr4id 2792 |
. . . . . . 7
β’ ((π β§ π β β) β (πβπ) = Ξ£π₯ β (1...π)(volβ(((,) β πΉ)βπ₯))) |
64 | | fzfid 13887 |
. . . . . . . 8
β’ ((π β§ π β β) β (1...π) β Fin) |
65 | 44, 60 | jca 513 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π₯ β (1...π)) β ((((,) β πΉ)βπ₯) β dom vol β§ (volβ(((,)
β πΉ)βπ₯)) β
β)) |
66 | 65 | ralrimiva 3140 |
. . . . . . . 8
β’ ((π β§ π β β) β βπ₯ β (1...π)((((,) β πΉ)βπ₯) β dom vol β§ (volβ(((,)
β πΉ)βπ₯)) β
β)) |
67 | | fz1ssnn 13481 |
. . . . . . . . 9
β’
(1...π) β
β |
68 | | uniioombl.2 |
. . . . . . . . . . 11
β’ (π β Disj π₯ β β
((,)β(πΉβπ₯))) |
69 | 2, 32 | sylan 581 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β β) β (((,) β πΉ)βπ₯) = ((,)β(πΉβπ₯))) |
70 | 69 | disjeq2dv 5079 |
. . . . . . . . . . 11
β’ (π β (Disj π₯ β β (((,) β
πΉ)βπ₯) β Disj π₯ β β ((,)β(πΉβπ₯)))) |
71 | 68, 70 | mpbird 257 |
. . . . . . . . . 10
β’ (π β Disj π₯ β β (((,) β
πΉ)βπ₯)) |
72 | 71 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β Disj π₯ β β (((,) β
πΉ)βπ₯)) |
73 | | disjss1 5080 |
. . . . . . . . 9
β’
((1...π) β
β β (Disj π₯ β β (((,) β πΉ)βπ₯) β Disj π₯ β (1...π)(((,) β πΉ)βπ₯))) |
74 | 67, 72, 73 | mpsyl 68 |
. . . . . . . 8
β’ ((π β§ π β β) β Disj π₯ β (1...π)(((,) β πΉ)βπ₯)) |
75 | | volfiniun 24934 |
. . . . . . . 8
β’
(((1...π) β Fin
β§ βπ₯ β
(1...π)((((,) β πΉ)βπ₯) β dom vol β§ (volβ(((,)
β πΉ)βπ₯)) β β) β§
Disj π₯ β
(1...π)(((,) β πΉ)βπ₯)) β (volββͺ π₯ β (1...π)(((,) β πΉ)βπ₯)) = Ξ£π₯ β (1...π)(volβ(((,) β πΉ)βπ₯))) |
76 | 64, 66, 74, 75 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β β) β (volββͺ π₯ β (1...π)(((,) β πΉ)βπ₯)) = Ξ£π₯ β (1...π)(volβ(((,) β πΉ)βπ₯))) |
77 | 44 | ralrimiva 3140 |
. . . . . . . . 9
β’ ((π β§ π β β) β βπ₯ β (1...π)(((,) β πΉ)βπ₯) β dom vol) |
78 | | finiunmbl 24931 |
. . . . . . . . 9
β’
(((1...π) β Fin
β§ βπ₯ β
(1...π)(((,) β πΉ)βπ₯) β dom vol) β βͺ π₯ β (1...π)(((,) β πΉ)βπ₯) β dom vol) |
79 | 64, 77, 78 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β β) β βͺ π₯ β (1...π)(((,) β πΉ)βπ₯) β dom vol) |
80 | | mblvol 24917 |
. . . . . . . 8
β’ (βͺ π₯ β (1...π)(((,) β πΉ)βπ₯) β dom vol β (volββͺ π₯ β (1...π)(((,) β πΉ)βπ₯)) = (vol*ββͺ π₯ β (1...π)(((,) β πΉ)βπ₯))) |
81 | 79, 80 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β) β (volββͺ π₯ β (1...π)(((,) β πΉ)βπ₯)) = (vol*ββͺ π₯ β (1...π)(((,) β πΉ)βπ₯))) |
82 | 63, 76, 81 | 3eqtr2d 2779 |
. . . . . 6
β’ ((π β§ π β β) β (πβπ) = (vol*ββͺ π₯ β (1...π)(((,) β πΉ)βπ₯))) |
83 | | iunss1 4972 |
. . . . . . . . 9
β’
((1...π) β
β β βͺ π₯ β (1...π)(((,) β πΉ)βπ₯) β βͺ
π₯ β β (((,)
β πΉ)βπ₯)) |
84 | 67, 83 | mp1i 13 |
. . . . . . . 8
β’ ((π β§ π β β) β βͺ π₯ β (1...π)(((,) β πΉ)βπ₯) β βͺ
π₯ β β (((,)
β πΉ)βπ₯)) |
85 | 9 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β ((,) β πΉ):ββΆπ«
β) |
86 | | ffn 6672 |
. . . . . . . . 9
β’ (((,)
β πΉ):ββΆπ« β β
((,) β πΉ) Fn
β) |
87 | | fniunfv 7198 |
. . . . . . . . 9
β’ (((,)
β πΉ) Fn β
β βͺ π₯ β β (((,) β πΉ)βπ₯) = βͺ ran ((,)
β πΉ)) |
88 | 85, 86, 87 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ π β β) β βͺ π₯ β β (((,) β πΉ)βπ₯) = βͺ ran ((,)
β πΉ)) |
89 | 84, 88 | sseqtrd 3988 |
. . . . . . 7
β’ ((π β§ π β β) β βͺ π₯ β (1...π)(((,) β πΉ)βπ₯) β βͺ ran
((,) β πΉ)) |
90 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β βͺ ran ((,) β πΉ) β β) |
91 | | ovolss 24872 |
. . . . . . 7
β’
((βͺ π₯ β (1...π)(((,) β πΉ)βπ₯) β βͺ ran
((,) β πΉ) β§ βͺ ran ((,) β πΉ) β β) β
(vol*ββͺ π₯ β (1...π)(((,) β πΉ)βπ₯)) β€ (vol*ββͺ ran ((,) β πΉ))) |
92 | 89, 90, 91 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β β) β (vol*ββͺ π₯ β (1...π)(((,) β πΉ)βπ₯)) β€ (vol*ββͺ ran ((,) β πΉ))) |
93 | 82, 92 | eqbrtrd 5131 |
. . . . 5
β’ ((π β§ π β β) β (πβπ) β€ (vol*ββͺ ran ((,) β πΉ))) |
94 | 93 | ralrimiva 3140 |
. . . 4
β’ (π β βπ β β (πβπ) β€ (vol*ββͺ ran ((,) β πΉ))) |
95 | 2, 17 | syl 17 |
. . . . 5
β’ (π β π:ββΆ(0[,)+β)) |
96 | | ffn 6672 |
. . . . 5
β’ (π:ββΆ(0[,)+β)
β π Fn
β) |
97 | | breq1 5112 |
. . . . . 6
β’ (π¦ = (πβπ) β (π¦ β€ (vol*ββͺ ran ((,) β πΉ)) β (πβπ) β€ (vol*ββͺ ran ((,) β πΉ)))) |
98 | 97 | ralrn 7042 |
. . . . 5
β’ (π Fn β β
(βπ¦ β ran π π¦ β€ (vol*ββͺ ran ((,) β πΉ)) β βπ β β (πβπ) β€ (vol*ββͺ ran ((,) β πΉ)))) |
99 | 95, 96, 98 | 3syl 18 |
. . . 4
β’ (π β (βπ¦ β ran π π¦ β€ (vol*ββͺ ran ((,) β πΉ)) β βπ β β (πβπ) β€ (vol*ββͺ ran ((,) β πΉ)))) |
100 | 94, 99 | mpbird 257 |
. . 3
β’ (π β βπ¦ β ran π π¦ β€ (vol*ββͺ ran ((,) β πΉ))) |
101 | | supxrleub 13254 |
. . . 4
β’ ((ran
π β
β* β§ (vol*ββͺ ran ((,)
β πΉ)) β
β*) β (sup(ran π, β*, < ) β€
(vol*ββͺ ran ((,) β πΉ)) β βπ¦ β ran π π¦ β€ (vol*ββͺ ran ((,) β πΉ)))) |
102 | 21, 14, 101 | syl2anc 585 |
. . 3
β’ (π β (sup(ran π, β*, < ) β€
(vol*ββͺ ran ((,) β πΉ)) β βπ¦ β ran π π¦ β€ (vol*ββͺ ran ((,) β πΉ)))) |
103 | 100, 102 | mpbird 257 |
. 2
β’ (π β sup(ran π, β*, < ) β€
(vol*ββͺ ran ((,) β πΉ))) |
104 | 14, 23, 26, 103 | xrletrid 13083 |
1
β’ (π β (vol*ββͺ ran ((,) β πΉ)) = sup(ran π, β*, <
)) |