Step | Hyp | Ref
| Expression |
1 | | uniioombl.1 |
. . . 4
β’ (π β πΉ:ββΆ( β€ β© (β
Γ β))) |
2 | | ovolficcss 24856 |
. . . 4
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β βͺ ran ([,] β
πΉ) β
β) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β βͺ ran ([,] β πΉ) β β) |
4 | | ovolcl 24865 |
. . 3
β’ (βͺ ran ([,] β πΉ) β β β (vol*ββͺ ran ([,] β πΉ)) β
β*) |
5 | 3, 4 | syl 17 |
. 2
β’ (π β (vol*ββͺ ran ([,] β πΉ)) β
β*) |
6 | | eqid 2733 |
. . . . . . 7
β’ ((abs
β β ) β πΉ) = ((abs β β ) β πΉ) |
7 | | uniioombl.3 |
. . . . . . 7
β’ π = seq1( + , ((abs β
β ) β πΉ)) |
8 | 6, 7 | ovolsf 24859 |
. . . . . 6
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β π:ββΆ(0[,)+β)) |
9 | 1, 8 | syl 17 |
. . . . 5
β’ (π β π:ββΆ(0[,)+β)) |
10 | 9 | frnd 6680 |
. . . 4
β’ (π β ran π β (0[,)+β)) |
11 | | icossxr 13358 |
. . . 4
β’
(0[,)+β) β β* |
12 | 10, 11 | sstrdi 3960 |
. . 3
β’ (π β ran π β
β*) |
13 | | supxrcl 13243 |
. . 3
β’ (ran
π β
β* β sup(ran π, β*, < ) β
β*) |
14 | 12, 13 | syl 17 |
. 2
β’ (π β sup(ran π, β*, < ) β
β*) |
15 | | ssid 3970 |
. . 3
β’ βͺ ran ([,] β πΉ) β βͺ ran
([,] β πΉ) |
16 | 7 | ovollb2 24876 |
. . 3
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ βͺ ran ([,] β
πΉ) β βͺ ran ([,] β πΉ)) β (vol*ββͺ ran ([,] β πΉ)) β€ sup(ran π, β*, <
)) |
17 | 1, 15, 16 | sylancl 587 |
. 2
β’ (π β (vol*ββͺ ran ([,] β πΉ)) β€ sup(ran π, β*, <
)) |
18 | | uniioombl.2 |
. . . 4
β’ (π β Disj π₯ β β
((,)β(πΉβπ₯))) |
19 | 1, 18, 7 | uniioovol 24966 |
. . 3
β’ (π β (vol*ββͺ ran ((,) β πΉ)) = sup(ran π, β*, <
)) |
20 | | ioossicc 13359 |
. . . . . . . . . . . 12
β’
((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯))) β ((1st β(πΉβπ₯))[,](2nd β(πΉβπ₯))) |
21 | | df-ov 7364 |
. . . . . . . . . . . 12
β’
((1st β(πΉβπ₯))(,)(2nd β(πΉβπ₯))) = ((,)ββ¨(1st
β(πΉβπ₯)), (2nd
β(πΉβπ₯))β©) |
22 | | df-ov 7364 |
. . . . . . . . . . . 12
β’
((1st β(πΉβπ₯))[,](2nd β(πΉβπ₯))) = ([,]ββ¨(1st
β(πΉβπ₯)), (2nd
β(πΉβπ₯))β©) |
23 | 20, 21, 22 | 3sstr3i 3990 |
. . . . . . . . . . 11
β’
((,)ββ¨(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))β©) β
([,]ββ¨(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))β©) |
24 | 23 | a1i 11 |
. . . . . . . . . 10
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β
((,)ββ¨(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))β©) β
([,]ββ¨(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))β©)) |
25 | | ffvelcdm 7036 |
. . . . . . . . . . . . 13
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (πΉβπ₯) β ( β€ β© (β Γ
β))) |
26 | 25 | elin2d 4163 |
. . . . . . . . . . . 12
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (πΉβπ₯) β (β Γ
β)) |
27 | | 1st2nd2 7964 |
. . . . . . . . . . . 12
β’ ((πΉβπ₯) β (β Γ β) β
(πΉβπ₯) = β¨(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))β©) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . 11
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (πΉβπ₯) = β¨(1st β(πΉβπ₯)), (2nd β(πΉβπ₯))β©) |
29 | 28 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β ((,)β(πΉβπ₯)) = ((,)ββ¨(1st
β(πΉβπ₯)), (2nd
β(πΉβπ₯))β©)) |
30 | 28 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β ([,]β(πΉβπ₯)) = ([,]ββ¨(1st
β(πΉβπ₯)), (2nd
β(πΉβπ₯))β©)) |
31 | 24, 29, 30 | 3sstr4d 3995 |
. . . . . . . . 9
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β ((,)β(πΉβπ₯)) β ([,]β(πΉβπ₯))) |
32 | | fvco3 6944 |
. . . . . . . . 9
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (((,) β πΉ)βπ₯) = ((,)β(πΉβπ₯))) |
33 | | fvco3 6944 |
. . . . . . . . 9
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (([,] β πΉ)βπ₯) = ([,]β(πΉβπ₯))) |
34 | 31, 32, 33 | 3sstr4d 3995 |
. . . . . . . 8
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π₯ β β) β (((,) β πΉ)βπ₯) β (([,] β πΉ)βπ₯)) |
35 | 1, 34 | sylan 581 |
. . . . . . 7
β’ ((π β§ π₯ β β) β (((,) β πΉ)βπ₯) β (([,] β πΉ)βπ₯)) |
36 | 35 | ralrimiva 3140 |
. . . . . 6
β’ (π β βπ₯ β β (((,) β πΉ)βπ₯) β (([,] β πΉ)βπ₯)) |
37 | | ss2iun 4976 |
. . . . . 6
β’
(βπ₯ β
β (((,) β πΉ)βπ₯) β (([,] β πΉ)βπ₯) β βͺ
π₯ β β (((,)
β πΉ)βπ₯) β βͺ π₯ β β (([,] β πΉ)βπ₯)) |
38 | 36, 37 | syl 17 |
. . . . 5
β’ (π β βͺ π₯ β β (((,) β πΉ)βπ₯) β βͺ
π₯ β β (([,]
β πΉ)βπ₯)) |
39 | | ioof 13373 |
. . . . . . . 8
β’
(,):(β* Γ β*)βΆπ«
β |
40 | | ffn 6672 |
. . . . . . . 8
β’
((,):(β* Γ β*)βΆπ«
β β (,) Fn (β* Γ
β*)) |
41 | 39, 40 | ax-mp 5 |
. . . . . . 7
β’ (,) Fn
(β* Γ β*) |
42 | | inss2 4193 |
. . . . . . . . 9
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
43 | | rexpssxrxp 11208 |
. . . . . . . . 9
β’ (β
Γ β) β (β* Γ
β*) |
44 | 42, 43 | sstri 3957 |
. . . . . . . 8
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
45 | | fss 6689 |
. . . . . . . 8
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β* Γ β*)) β πΉ:ββΆ(β* Γ
β*)) |
46 | 1, 44, 45 | sylancl 587 |
. . . . . . 7
β’ (π β πΉ:ββΆ(β* Γ
β*)) |
47 | | fnfco 6711 |
. . . . . . 7
β’ (((,) Fn
(β* Γ β*) β§ πΉ:ββΆ(β* Γ
β*)) β ((,) β πΉ) Fn β) |
48 | 41, 46, 47 | sylancr 588 |
. . . . . 6
β’ (π β ((,) β πΉ) Fn β) |
49 | | fniunfv 7198 |
. . . . . 6
β’ (((,)
β πΉ) Fn β
β βͺ π₯ β β (((,) β πΉ)βπ₯) = βͺ ran ((,)
β πΉ)) |
50 | 48, 49 | syl 17 |
. . . . 5
β’ (π β βͺ π₯ β β (((,) β πΉ)βπ₯) = βͺ ran ((,)
β πΉ)) |
51 | | iccf 13374 |
. . . . . . . 8
β’
[,]:(β* Γ β*)βΆπ«
β* |
52 | | ffn 6672 |
. . . . . . . 8
β’
([,]:(β* Γ β*)βΆπ«
β* β [,] Fn (β* Γ
β*)) |
53 | 51, 52 | ax-mp 5 |
. . . . . . 7
β’ [,] Fn
(β* Γ β*) |
54 | | fnfco 6711 |
. . . . . . 7
β’ (([,] Fn
(β* Γ β*) β§ πΉ:ββΆ(β* Γ
β*)) β ([,] β πΉ) Fn β) |
55 | 53, 46, 54 | sylancr 588 |
. . . . . 6
β’ (π β ([,] β πΉ) Fn β) |
56 | | fniunfv 7198 |
. . . . . 6
β’ (([,]
β πΉ) Fn β
β βͺ π₯ β β (([,] β πΉ)βπ₯) = βͺ ran ([,]
β πΉ)) |
57 | 55, 56 | syl 17 |
. . . . 5
β’ (π β βͺ π₯ β β (([,] β πΉ)βπ₯) = βͺ ran ([,]
β πΉ)) |
58 | 38, 50, 57 | 3sstr3d 3994 |
. . . 4
β’ (π β βͺ ran ((,) β πΉ) β βͺ ran
([,] β πΉ)) |
59 | | ovolss 24872 |
. . . 4
β’ ((βͺ ran ((,) β πΉ) β βͺ ran
([,] β πΉ) β§ βͺ ran ([,] β πΉ) β β) β (vol*ββͺ ran ((,) β πΉ)) β€ (vol*ββͺ ran ([,] β πΉ))) |
60 | 58, 3, 59 | syl2anc 585 |
. . 3
β’ (π β (vol*ββͺ ran ((,) β πΉ)) β€ (vol*ββͺ ran ([,] β πΉ))) |
61 | 19, 60 | eqbrtrrd 5133 |
. 2
β’ (π β sup(ran π, β*, < ) β€
(vol*ββͺ ran ([,] β πΉ))) |
62 | 5, 14, 17, 61 | xrletrid 13083 |
1
β’ (π β (vol*ββͺ ran ([,] β πΉ)) = sup(ran π, β*, <
)) |