Step | Hyp | Ref
| Expression |
1 | | nnuz 12814 |
. . 3
β’ β =
(β€β₯β1) |
2 | | 1zzd 12542 |
. . 3
β’ (π β 1 β
β€) |
3 | | itg1climres.4 |
. . . . 5
β’ (π β πΉ β dom
β«1) |
4 | | i1frn 25064 |
. . . . 5
β’ (πΉ β dom β«1
β ran πΉ β
Fin) |
5 | 3, 4 | syl 17 |
. . . 4
β’ (π β ran πΉ β Fin) |
6 | | difss 4095 |
. . . 4
β’ (ran
πΉ β {0}) β ran
πΉ |
7 | | ssfi 9123 |
. . . 4
β’ ((ran
πΉ β Fin β§ (ran
πΉ β {0}) β ran
πΉ) β (ran πΉ β {0}) β
Fin) |
8 | 5, 6, 7 | sylancl 587 |
. . 3
β’ (π β (ran πΉ β {0}) β Fin) |
9 | | 1zzd 12542 |
. . . 4
β’ ((π β§ π β (ran πΉ β {0})) β 1 β
β€) |
10 | | i1fima 25065 |
. . . . . . . . . . . 12
β’ (πΉ β dom β«1
β (β‘πΉ β {π}) β dom vol) |
11 | 3, 10 | syl 17 |
. . . . . . . . . . 11
β’ (π β (β‘πΉ β {π}) β dom vol) |
12 | 11 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (β‘πΉ β {π}) β dom vol) |
13 | | itg1climres.1 |
. . . . . . . . . . . 12
β’ (π β π΄:ββΆdom vol) |
14 | 13 | ffvelcdmda 7039 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π΄βπ) β dom vol) |
15 | 14 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (π΄βπ) β dom vol) |
16 | | inmbl 24929 |
. . . . . . . . . 10
β’ (((β‘πΉ β {π}) β dom vol β§ (π΄βπ) β dom vol) β ((β‘πΉ β {π}) β© (π΄βπ)) β dom vol) |
17 | 12, 15, 16 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β ((β‘πΉ β {π}) β© (π΄βπ)) β dom vol) |
18 | | mblvol 24917 |
. . . . . . . . 9
β’ (((β‘πΉ β {π}) β© (π΄βπ)) β dom vol β (volβ((β‘πΉ β {π}) β© (π΄βπ))) = (vol*β((β‘πΉ β {π}) β© (π΄βπ)))) |
19 | 17, 18 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (volβ((β‘πΉ β {π}) β© (π΄βπ))) = (vol*β((β‘πΉ β {π}) β© (π΄βπ)))) |
20 | | inss1 4192 |
. . . . . . . . . 10
β’ ((β‘πΉ β {π}) β© (π΄βπ)) β (β‘πΉ β {π}) |
21 | 20 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β ((β‘πΉ β {π}) β© (π΄βπ)) β (β‘πΉ β {π})) |
22 | | mblss 24918 |
. . . . . . . . . 10
β’ ((β‘πΉ β {π}) β dom vol β (β‘πΉ β {π}) β β) |
23 | 12, 22 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (β‘πΉ β {π}) β β) |
24 | | mblvol 24917 |
. . . . . . . . . . 11
β’ ((β‘πΉ β {π}) β dom vol β (volβ(β‘πΉ β {π})) = (vol*β(β‘πΉ β {π}))) |
25 | 12, 24 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (volβ(β‘πΉ β {π})) = (vol*β(β‘πΉ β {π}))) |
26 | | i1fima2sn 25067 |
. . . . . . . . . . . 12
β’ ((πΉ β dom β«1
β§ π β (ran πΉ β {0})) β
(volβ(β‘πΉ β {π})) β β) |
27 | 3, 26 | sylan 581 |
. . . . . . . . . . 11
β’ ((π β§ π β (ran πΉ β {0})) β (volβ(β‘πΉ β {π})) β β) |
28 | 27 | adantr 482 |
. . . . . . . . . 10
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (volβ(β‘πΉ β {π})) β β) |
29 | 25, 28 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (vol*β(β‘πΉ β {π})) β β) |
30 | | ovolsscl 24873 |
. . . . . . . . 9
β’ ((((β‘πΉ β {π}) β© (π΄βπ)) β (β‘πΉ β {π}) β§ (β‘πΉ β {π}) β β β§ (vol*β(β‘πΉ β {π})) β β) β
(vol*β((β‘πΉ β {π}) β© (π΄βπ))) β β) |
31 | 21, 23, 29, 30 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (vol*β((β‘πΉ β {π}) β© (π΄βπ))) β β) |
32 | 19, 31 | eqeltrd 2834 |
. . . . . . 7
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β β) |
33 | 32 | fmpttd 7067 |
. . . . . 6
β’ ((π β§ π β (ran πΉ β {0})) β (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ)))):ββΆβ) |
34 | | itg1climres.2 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (π΄βπ) β (π΄β(π + 1))) |
35 | 34 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (π΄βπ) β (π΄β(π + 1))) |
36 | | sslin 4198 |
. . . . . . . . . . . 12
β’ ((π΄βπ) β (π΄β(π + 1)) β ((β‘πΉ β {π}) β© (π΄βπ)) β ((β‘πΉ β {π}) β© (π΄β(π + 1)))) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β ((β‘πΉ β {π}) β© (π΄βπ)) β ((β‘πΉ β {π}) β© (π΄β(π + 1)))) |
38 | 13 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (ran πΉ β {0})) β π΄:ββΆdom vol) |
39 | | peano2nn 12173 |
. . . . . . . . . . . . . 14
β’ (π β β β (π + 1) β
β) |
40 | | ffvelcdm 7036 |
. . . . . . . . . . . . . 14
β’ ((π΄:ββΆdom vol β§
(π + 1) β β)
β (π΄β(π + 1)) β dom
vol) |
41 | 38, 39, 40 | syl2an 597 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (π΄β(π + 1)) β dom vol) |
42 | | inmbl 24929 |
. . . . . . . . . . . . 13
β’ (((β‘πΉ β {π}) β dom vol β§ (π΄β(π + 1)) β dom vol) β ((β‘πΉ β {π}) β© (π΄β(π + 1))) β dom vol) |
43 | 12, 41, 42 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β ((β‘πΉ β {π}) β© (π΄β(π + 1))) β dom vol) |
44 | | mblss 24918 |
. . . . . . . . . . . 12
β’ (((β‘πΉ β {π}) β© (π΄β(π + 1))) β dom vol β ((β‘πΉ β {π}) β© (π΄β(π + 1))) β β) |
45 | 43, 44 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β ((β‘πΉ β {π}) β© (π΄β(π + 1))) β β) |
46 | | ovolss 24872 |
. . . . . . . . . . 11
β’ ((((β‘πΉ β {π}) β© (π΄βπ)) β ((β‘πΉ β {π}) β© (π΄β(π + 1))) β§ ((β‘πΉ β {π}) β© (π΄β(π + 1))) β β) β
(vol*β((β‘πΉ β {π}) β© (π΄βπ))) β€ (vol*β((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
47 | 37, 45, 46 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (vol*β((β‘πΉ β {π}) β© (π΄βπ))) β€ (vol*β((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
48 | | mblvol 24917 |
. . . . . . . . . . 11
β’ (((β‘πΉ β {π}) β© (π΄β(π + 1))) β dom vol β
(volβ((β‘πΉ β {π}) β© (π΄β(π + 1)))) = (vol*β((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
49 | 43, 48 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (volβ((β‘πΉ β {π}) β© (π΄β(π + 1)))) = (vol*β((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
50 | 47, 19, 49 | 3brtr4d 5141 |
. . . . . . . . 9
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
51 | 50 | ralrimiva 3140 |
. . . . . . . 8
β’ ((π β§ π β (ran πΉ β {0})) β βπ β β
(volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
52 | | fveq2 6846 |
. . . . . . . . . . . . . 14
β’ (π = π β (π΄βπ) = (π΄βπ)) |
53 | 52 | ineq2d 4176 |
. . . . . . . . . . . . 13
β’ (π = π β ((β‘πΉ β {π}) β© (π΄βπ)) = ((β‘πΉ β {π}) β© (π΄βπ))) |
54 | 53 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ (π = π β (volβ((β‘πΉ β {π}) β© (π΄βπ))) = (volβ((β‘πΉ β {π}) β© (π΄βπ)))) |
55 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))) = (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ)))) |
56 | | fvex 6859 |
. . . . . . . . . . . 12
β’
(volβ((β‘πΉ β {π}) β© (π΄βπ))) β V |
57 | 54, 55, 56 | fvmpt 6952 |
. . . . . . . . . . 11
β’ (π β β β ((π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) = (volβ((β‘πΉ β {π}) β© (π΄βπ)))) |
58 | | peano2nn 12173 |
. . . . . . . . . . . 12
β’ (π β β β (π + 1) β
β) |
59 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π = (π + 1) β (π΄βπ) = (π΄β(π + 1))) |
60 | 59 | ineq2d 4176 |
. . . . . . . . . . . . . 14
β’ (π = (π + 1) β ((β‘πΉ β {π}) β© (π΄βπ)) = ((β‘πΉ β {π}) β© (π΄β(π + 1)))) |
61 | 60 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ (π = (π + 1) β (volβ((β‘πΉ β {π}) β© (π΄βπ))) = (volβ((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
62 | | fvex 6859 |
. . . . . . . . . . . . 13
β’
(volβ((β‘πΉ β {π}) β© (π΄β(π + 1)))) β V |
63 | 61, 55, 62 | fvmpt 6952 |
. . . . . . . . . . . 12
β’ ((π + 1) β β β
((π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ))))β(π + 1)) = (volβ((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
64 | 58, 63 | syl 17 |
. . . . . . . . . . 11
β’ (π β β β ((π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ))))β(π + 1)) = (volβ((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
65 | 57, 64 | breq12d 5122 |
. . . . . . . . . 10
β’ (π β β β (((π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))β(π + 1)) β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ((β‘πΉ β {π}) β© (π΄β(π + 1)))))) |
66 | 65 | ralbiia 3091 |
. . . . . . . . 9
β’
(βπ β
β ((π β β
β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))β(π + 1)) β βπ β β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
67 | | fvoveq1 7384 |
. . . . . . . . . . . . 13
β’ (π = π β (π΄β(π + 1)) = (π΄β(π + 1))) |
68 | 67 | ineq2d 4176 |
. . . . . . . . . . . 12
β’ (π = π β ((β‘πΉ β {π}) β© (π΄β(π + 1))) = ((β‘πΉ β {π}) β© (π΄β(π + 1)))) |
69 | 68 | fveq2d 6850 |
. . . . . . . . . . 11
β’ (π = π β (volβ((β‘πΉ β {π}) β© (π΄β(π + 1)))) = (volβ((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
70 | 54, 69 | breq12d 5122 |
. . . . . . . . . 10
β’ (π = π β ((volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ((β‘πΉ β {π}) β© (π΄β(π + 1)))) β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ((β‘πΉ β {π}) β© (π΄β(π + 1)))))) |
71 | 70 | cbvralvw 3224 |
. . . . . . . . 9
β’
(βπ β
β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ((β‘πΉ β {π}) β© (π΄β(π + 1)))) β βπ β β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
72 | 66, 71 | bitr4i 278 |
. . . . . . . 8
β’
(βπ β
β ((π β β
β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))β(π + 1)) β βπ β β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
73 | 51, 72 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π β (ran πΉ β {0})) β βπ β β ((π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))β(π + 1))) |
74 | 73 | r19.21bi 3233 |
. . . . . 6
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))β(π + 1))) |
75 | | ovolss 24872 |
. . . . . . . . . . 11
β’ ((((β‘πΉ β {π}) β© (π΄βπ)) β (β‘πΉ β {π}) β§ (β‘πΉ β {π}) β β) β
(vol*β((β‘πΉ β {π}) β© (π΄βπ))) β€ (vol*β(β‘πΉ β {π}))) |
76 | 20, 23, 75 | sylancr 588 |
. . . . . . . . . 10
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (vol*β((β‘πΉ β {π}) β© (π΄βπ))) β€ (vol*β(β‘πΉ β {π}))) |
77 | 76, 19, 25 | 3brtr4d 5141 |
. . . . . . . . 9
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ(β‘πΉ β {π}))) |
78 | 77 | ralrimiva 3140 |
. . . . . . . 8
β’ ((π β§ π β (ran πΉ β {0})) β βπ β β
(volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ(β‘πΉ β {π}))) |
79 | 57 | breq1d 5119 |
. . . . . . . . . 10
β’ (π β β β (((π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ (volβ(β‘πΉ β {π})) β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ(β‘πΉ β {π})))) |
80 | 79 | ralbiia 3091 |
. . . . . . . . 9
β’
(βπ β
β ((π β β
β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ (volβ(β‘πΉ β {π})) β βπ β β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ(β‘πΉ β {π}))) |
81 | 54 | breq1d 5119 |
. . . . . . . . . 10
β’ (π = π β ((volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ(β‘πΉ β {π})) β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ(β‘πΉ β {π})))) |
82 | 81 | cbvralvw 3224 |
. . . . . . . . 9
β’
(βπ β
β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ(β‘πΉ β {π})) β βπ β β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ(β‘πΉ β {π}))) |
83 | 80, 82 | bitr4i 278 |
. . . . . . . 8
β’
(βπ β
β ((π β β
β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ (volβ(β‘πΉ β {π})) β βπ β β (volβ((β‘πΉ β {π}) β© (π΄βπ))) β€ (volβ(β‘πΉ β {π}))) |
84 | 78, 83 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π β (ran πΉ β {0})) β βπ β β ((π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ (volβ(β‘πΉ β {π}))) |
85 | | brralrspcev 5169 |
. . . . . . 7
β’
(((volβ(β‘πΉ β {π})) β β β§ βπ β β ((π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ (volβ(β‘πΉ β {π}))) β βπ₯ β β βπ β β ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ π₯) |
86 | 27, 84, 85 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β (ran πΉ β {0})) β βπ₯ β β βπ β β ((π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ π₯) |
87 | 1, 9, 33, 74, 86 | climsup 15563 |
. . . . 5
β’ ((π β§ π β (ran πΉ β {0})) β (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ)))) β sup(ran (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ)))), β, < )) |
88 | 17 | fmpttd 7067 |
. . . . . . 7
β’ ((π β§ π β (ran πΉ β {0})) β (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ))):ββΆdom vol) |
89 | 37 | ralrimiva 3140 |
. . . . . . . 8
β’ ((π β§ π β (ran πΉ β {0})) β βπ β β ((β‘πΉ β {π}) β© (π΄βπ)) β ((β‘πΉ β {π}) β© (π΄β(π + 1)))) |
90 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ))) = (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ))) |
91 | | fvex 6859 |
. . . . . . . . . . . . 13
β’ (π΄βπ) β V |
92 | 91 | inex2 5279 |
. . . . . . . . . . . 12
β’ ((β‘πΉ β {π}) β© (π΄βπ)) β V |
93 | 53, 90, 92 | fvmpt 6952 |
. . . . . . . . . . 11
β’ (π β β β ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))βπ) = ((β‘πΉ β {π}) β© (π΄βπ))) |
94 | | fvex 6859 |
. . . . . . . . . . . . . 14
β’ (π΄β(π + 1)) β V |
95 | 94 | inex2 5279 |
. . . . . . . . . . . . 13
β’ ((β‘πΉ β {π}) β© (π΄β(π + 1))) β V |
96 | 60, 90, 95 | fvmpt 6952 |
. . . . . . . . . . . 12
β’ ((π + 1) β β β
((π β β β¦
((β‘πΉ β {π}) β© (π΄βπ)))β(π + 1)) = ((β‘πΉ β {π}) β© (π΄β(π + 1)))) |
97 | 58, 96 | syl 17 |
. . . . . . . . . . 11
β’ (π β β β ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))β(π + 1)) = ((β‘πΉ β {π}) β© (π΄β(π + 1)))) |
98 | 93, 97 | sseq12d 3981 |
. . . . . . . . . 10
β’ (π β β β (((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))βπ) β ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))β(π + 1)) β ((β‘πΉ β {π}) β© (π΄βπ)) β ((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
99 | 98 | ralbiia 3091 |
. . . . . . . . 9
β’
(βπ β
β ((π β β
β¦ ((β‘πΉ β {π}) β© (π΄βπ)))βπ) β ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))β(π + 1)) β βπ β β ((β‘πΉ β {π}) β© (π΄βπ)) β ((β‘πΉ β {π}) β© (π΄β(π + 1)))) |
100 | 53, 68 | sseq12d 3981 |
. . . . . . . . . 10
β’ (π = π β (((β‘πΉ β {π}) β© (π΄βπ)) β ((β‘πΉ β {π}) β© (π΄β(π + 1))) β ((β‘πΉ β {π}) β© (π΄βπ)) β ((β‘πΉ β {π}) β© (π΄β(π + 1))))) |
101 | 100 | cbvralvw 3224 |
. . . . . . . . 9
β’
(βπ β
β ((β‘πΉ β {π}) β© (π΄βπ)) β ((β‘πΉ β {π}) β© (π΄β(π + 1))) β βπ β β ((β‘πΉ β {π}) β© (π΄βπ)) β ((β‘πΉ β {π}) β© (π΄β(π + 1)))) |
102 | 99, 101 | bitr4i 278 |
. . . . . . . 8
β’
(βπ β
β ((π β β
β¦ ((β‘πΉ β {π}) β© (π΄βπ)))βπ) β ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))β(π + 1)) β βπ β β ((β‘πΉ β {π}) β© (π΄βπ)) β ((β‘πΉ β {π}) β© (π΄β(π + 1)))) |
103 | 89, 102 | sylibr 233 |
. . . . . . 7
β’ ((π β§ π β (ran πΉ β {0})) β βπ β β ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))βπ) β ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))β(π + 1))) |
104 | | volsup 24943 |
. . . . . . 7
β’ (((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ))):ββΆdom vol β§
βπ β β
((π β β β¦
((β‘πΉ β {π}) β© (π΄βπ)))βπ) β ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))β(π + 1))) β (volββͺ ran (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))) = sup((vol β ran (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))), β*, <
)) |
105 | 88, 103, 104 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β (ran πΉ β {0})) β (volββͺ ran (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))) = sup((vol β ran (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))), β*, <
)) |
106 | 93 | iuneq2i 4979 |
. . . . . . . . . 10
β’ βͺ π β β ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))βπ) = βͺ π β β ((β‘πΉ β {π}) β© (π΄βπ)) |
107 | 53 | cbviunv 5004 |
. . . . . . . . . 10
β’ βͺ π β β ((β‘πΉ β {π}) β© (π΄βπ)) = βͺ
π β β ((β‘πΉ β {π}) β© (π΄βπ)) |
108 | | iunin2 5035 |
. . . . . . . . . 10
β’ βͺ π β β ((β‘πΉ β {π}) β© (π΄βπ)) = ((β‘πΉ β {π}) β© βͺ
π β β (π΄βπ)) |
109 | 106, 107,
108 | 3eqtr2i 2767 |
. . . . . . . . 9
β’ βͺ π β β ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))βπ) = ((β‘πΉ β {π}) β© βͺ
π β β (π΄βπ)) |
110 | | ffn 6672 |
. . . . . . . . . . . . . 14
β’ (π΄:ββΆdom vol β
π΄ Fn
β) |
111 | | fniunfv 7198 |
. . . . . . . . . . . . . 14
β’ (π΄ Fn β β βͺ π β β (π΄βπ) = βͺ ran π΄) |
112 | 13, 110, 111 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β βͺ π β β (π΄βπ) = βͺ ran π΄) |
113 | | itg1climres.3 |
. . . . . . . . . . . . 13
β’ (π β βͺ ran π΄ = β) |
114 | 112, 113 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β βͺ π β β (π΄βπ) = β) |
115 | 114 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (ran πΉ β {0})) β βͺ π β β (π΄βπ) = β) |
116 | 115 | ineq2d 4176 |
. . . . . . . . . 10
β’ ((π β§ π β (ran πΉ β {0})) β ((β‘πΉ β {π}) β© βͺ
π β β (π΄βπ)) = ((β‘πΉ β {π}) β© β)) |
117 | 11 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (ran πΉ β {0})) β (β‘πΉ β {π}) β dom vol) |
118 | 117, 22 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (ran πΉ β {0})) β (β‘πΉ β {π}) β β) |
119 | | df-ss 3931 |
. . . . . . . . . . 11
β’ ((β‘πΉ β {π}) β β β ((β‘πΉ β {π}) β© β) = (β‘πΉ β {π})) |
120 | 118, 119 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π β (ran πΉ β {0})) β ((β‘πΉ β {π}) β© β) = (β‘πΉ β {π})) |
121 | 116, 120 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ π β (ran πΉ β {0})) β ((β‘πΉ β {π}) β© βͺ
π β β (π΄βπ)) = (β‘πΉ β {π})) |
122 | 109, 121 | eqtrid 2785 |
. . . . . . . 8
β’ ((π β§ π β (ran πΉ β {0})) β βͺ π β β ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))βπ) = (β‘πΉ β {π})) |
123 | | ffn 6672 |
. . . . . . . . 9
β’ ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ))):ββΆdom vol β (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ))) Fn β) |
124 | | fniunfv 7198 |
. . . . . . . . 9
β’ ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ))) Fn β β βͺ π β β ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))βπ) = βͺ ran (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))) |
125 | 88, 123, 124 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ π β (ran πΉ β {0})) β βͺ π β β ((π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))βπ) = βͺ ran (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))) |
126 | 122, 125 | eqtr3d 2775 |
. . . . . . 7
β’ ((π β§ π β (ran πΉ β {0})) β (β‘πΉ β {π}) = βͺ ran (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))) |
127 | 126 | fveq2d 6850 |
. . . . . 6
β’ ((π β§ π β (ran πΉ β {0})) β (volβ(β‘πΉ β {π})) = (volββͺ
ran (π β β
β¦ ((β‘πΉ β {π}) β© (π΄βπ))))) |
128 | 33 | frnd 6680 |
. . . . . . . 8
β’ ((π β§ π β (ran πΉ β {0})) β ran (π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))) β β) |
129 | 33 | fdmd 6683 |
. . . . . . . . . 10
β’ ((π β§ π β (ran πΉ β {0})) β dom (π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))) = β) |
130 | | 1nn 12172 |
. . . . . . . . . . 11
β’ 1 β
β |
131 | | ne0i 4298 |
. . . . . . . . . . 11
β’ (1 β
β β β β β
) |
132 | 130, 131 | mp1i 13 |
. . . . . . . . . 10
β’ ((π β§ π β (ran πΉ β {0})) β β β
β
) |
133 | 129, 132 | eqnetrd 3008 |
. . . . . . . . 9
β’ ((π β§ π β (ran πΉ β {0})) β dom (π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))) β β
) |
134 | | dm0rn0 5884 |
. . . . . . . . . 10
β’ (dom
(π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))) = β
β ran (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ)))) = β
) |
135 | 134 | necon3bii 2993 |
. . . . . . . . 9
β’ (dom
(π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))) β β
β ran (π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))) β β
) |
136 | 133, 135 | sylib 217 |
. . . . . . . 8
β’ ((π β§ π β (ran πΉ β {0})) β ran (π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))) β β
) |
137 | | ffn 6672 |
. . . . . . . . . . 11
β’ ((π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))):ββΆβ β (π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))) Fn β) |
138 | | breq1 5112 |
. . . . . . . . . . . 12
β’ (π§ = ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β (π§ β€ π₯ β ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ π₯)) |
139 | 138 | ralrn 7042 |
. . . . . . . . . . 11
β’ ((π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))) Fn β β (βπ§ β ran (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))π§ β€ π₯ β βπ β β ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ π₯)) |
140 | 33, 137, 139 | 3syl 18 |
. . . . . . . . . 10
β’ ((π β§ π β (ran πΉ β {0})) β (βπ§ β ran (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))π§ β€ π₯ β βπ β β ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ π₯)) |
141 | 140 | rexbidv 3172 |
. . . . . . . . 9
β’ ((π β§ π β (ran πΉ β {0})) β (βπ₯ β β βπ§ β ran (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))π§ β€ π₯ β βπ₯ β β βπ β β ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β€ π₯)) |
142 | 86, 141 | mpbird 257 |
. . . . . . . 8
β’ ((π β§ π β (ran πΉ β {0})) β βπ₯ β β βπ§ β ran (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))π§ β€ π₯) |
143 | | supxrre 13255 |
. . . . . . . 8
β’ ((ran
(π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))) β β β§ ran (π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))) β β
β§ βπ₯ β β βπ§ β ran (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))π§ β€ π₯) β sup(ran (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ)))), β*, < ) = sup(ran
(π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))), β, < )) |
144 | 128, 136,
142, 143 | syl3anc 1372 |
. . . . . . 7
β’ ((π β§ π β (ran πΉ β {0})) β sup(ran (π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))), β*, < ) = sup(ran
(π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))), β, < )) |
145 | | volf 24916 |
. . . . . . . . . . . 12
β’ vol:dom
volβΆ(0[,]+β) |
146 | 145 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ π β (ran πΉ β {0})) β vol:dom
volβΆ(0[,]+β)) |
147 | 146, 17 | cofmpt 7082 |
. . . . . . . . . 10
β’ ((π β§ π β (ran πΉ β {0})) β (vol β (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))) = (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))) |
148 | 147 | rneqd 5897 |
. . . . . . . . 9
β’ ((π β§ π β (ran πΉ β {0})) β ran (vol β
(π β β β¦
((β‘πΉ β {π}) β© (π΄βπ)))) = ran (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))) |
149 | | rnco2 6209 |
. . . . . . . . 9
β’ ran (vol
β (π β β
β¦ ((β‘πΉ β {π}) β© (π΄βπ)))) = (vol β ran (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))) |
150 | 148, 149 | eqtr3di 2788 |
. . . . . . . 8
β’ ((π β§ π β (ran πΉ β {0})) β ran (π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))) = (vol β ran (π β β β¦ ((β‘πΉ β {π}) β© (π΄βπ))))) |
151 | 150 | supeq1d 9390 |
. . . . . . 7
β’ ((π β§ π β (ran πΉ β {0})) β sup(ran (π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))), β*, < ) = sup((vol
β ran (π β
β β¦ ((β‘πΉ β {π}) β© (π΄βπ)))), β*, <
)) |
152 | 144, 151 | eqtr3d 2775 |
. . . . . 6
β’ ((π β§ π β (ran πΉ β {0})) β sup(ran (π β β β¦
(volβ((β‘πΉ β {π}) β© (π΄βπ)))), β, < ) = sup((vol β ran
(π β β β¦
((β‘πΉ β {π}) β© (π΄βπ)))), β*, <
)) |
153 | 105, 127,
152 | 3eqtr4d 2783 |
. . . . 5
β’ ((π β§ π β (ran πΉ β {0})) β (volβ(β‘πΉ β {π})) = sup(ran (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ)))), β, < )) |
154 | 87, 153 | breqtrrd 5137 |
. . . 4
β’ ((π β§ π β (ran πΉ β {0})) β (π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ)))) β (volβ(β‘πΉ β {π}))) |
155 | | i1ff 25063 |
. . . . . . . 8
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
156 | | frn 6679 |
. . . . . . . 8
β’ (πΉ:ββΆβ β
ran πΉ β
β) |
157 | 3, 155, 156 | 3syl 18 |
. . . . . . 7
β’ (π β ran πΉ β β) |
158 | 157 | ssdifssd 4106 |
. . . . . 6
β’ (π β (ran πΉ β {0}) β
β) |
159 | 158 | sselda 3948 |
. . . . 5
β’ ((π β§ π β (ran πΉ β {0})) β π β β) |
160 | 159 | recnd 11191 |
. . . 4
β’ ((π β§ π β (ran πΉ β {0})) β π β β) |
161 | | nnex 12167 |
. . . . . 6
β’ β
β V |
162 | 161 | mptex 7177 |
. . . . 5
β’ (π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) β V |
163 | 162 | a1i 11 |
. . . 4
β’ ((π β§ π β (ran πΉ β {0})) β (π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) β V) |
164 | 33 | ffvelcdmda 7039 |
. . . . 5
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β β) |
165 | 164 | recnd 11191 |
. . . 4
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ) β β) |
166 | 54 | oveq2d 7377 |
. . . . . . 7
β’ (π = π β (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))) = (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) |
167 | | eqid 2733 |
. . . . . . 7
β’ (π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) = (π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) |
168 | | ovex 7394 |
. . . . . . 7
β’ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))) β V |
169 | 166, 167,
168 | fvmpt 6952 |
. . . . . 6
β’ (π β β β ((π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))))βπ) = (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) |
170 | 57 | oveq2d 7377 |
. . . . . 6
β’ (π β β β (π Β· ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ)) = (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) |
171 | 169, 170 | eqtr4d 2776 |
. . . . 5
β’ (π β β β ((π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))))βπ) = (π Β· ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ))) |
172 | 171 | adantl 483 |
. . . 4
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β ((π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))))βπ) = (π Β· ((π β β β¦ (volβ((β‘πΉ β {π}) β© (π΄βπ))))βπ))) |
173 | 1, 9, 154, 160, 163, 165, 172 | climmulc2 15528 |
. . 3
β’ ((π β§ π β (ran πΉ β {0})) β (π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) β (π Β· (volβ(β‘πΉ β {π})))) |
174 | 161 | mptex 7177 |
. . . 4
β’ (π β β β¦
(β«1βπΊ)) β V |
175 | 174 | a1i 11 |
. . 3
β’ (π β (π β β β¦
(β«1βπΊ)) β V) |
176 | 159 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β π β β) |
177 | 176, 32 | remulcld 11193 |
. . . . . . 7
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))) β β) |
178 | 177 | fmpttd 7067 |
. . . . . 6
β’ ((π β§ π β (ran πΉ β {0})) β (π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))):ββΆβ) |
179 | 178 | ffvelcdmda 7039 |
. . . . 5
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β ((π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))))βπ) β β) |
180 | 179 | recnd 11191 |
. . . 4
β’ (((π β§ π β (ran πΉ β {0})) β§ π β β) β ((π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))))βπ) β β) |
181 | 180 | anasss 468 |
. . 3
β’ ((π β§ (π β (ran πΉ β {0}) β§ π β β)) β ((π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))))βπ) β β) |
182 | 3 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β πΉ β dom
β«1) |
183 | | itg1climres.5 |
. . . . . . . . . 10
β’ πΊ = (π₯ β β β¦ if(π₯ β (π΄βπ), (πΉβπ₯), 0)) |
184 | 183 | i1fres 25093 |
. . . . . . . . 9
β’ ((πΉ β dom β«1
β§ (π΄βπ) β dom vol) β πΊ β dom
β«1) |
185 | 182, 14, 184 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β β) β πΊ β dom
β«1) |
186 | 8 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β (ran πΉ β {0}) β
Fin) |
187 | | ffn 6672 |
. . . . . . . . . . . . . 14
β’ (πΉ:ββΆβ β
πΉ Fn
β) |
188 | 3, 155, 187 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β πΉ Fn β) |
189 | 188 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β πΉ Fn β) |
190 | | fnfvelrn 7035 |
. . . . . . . . . . . 12
β’ ((πΉ Fn β β§ π₯ β β) β (πΉβπ₯) β ran πΉ) |
191 | 189, 190 | sylan 581 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β (πΉβπ₯) β ran πΉ) |
192 | | i1f0rn 25069 |
. . . . . . . . . . . . 13
β’ (πΉ β dom β«1
β 0 β ran πΉ) |
193 | 3, 192 | syl 17 |
. . . . . . . . . . . 12
β’ (π β 0 β ran πΉ) |
194 | 193 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π₯ β β) β 0 β ran πΉ) |
195 | 191, 194 | ifcld 4536 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π₯ β β) β if(π₯ β (π΄βπ), (πΉβπ₯), 0) β ran πΉ) |
196 | 195, 183 | fmptd 7066 |
. . . . . . . . 9
β’ ((π β§ π β β) β πΊ:ββΆran πΉ) |
197 | | frn 6679 |
. . . . . . . . 9
β’ (πΊ:ββΆran πΉ β ran πΊ β ran πΉ) |
198 | | ssdif 4103 |
. . . . . . . . 9
β’ (ran
πΊ β ran πΉ β (ran πΊ β {0}) β (ran πΉ β {0})) |
199 | 196, 197,
198 | 3syl 18 |
. . . . . . . 8
β’ ((π β§ π β β) β (ran πΊ β {0}) β (ran πΉ β {0})) |
200 | 157 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β ran πΉ β β) |
201 | 200 | ssdifd 4104 |
. . . . . . . 8
β’ ((π β§ π β β) β (ran πΉ β {0}) β (β
β {0})) |
202 | | itg1val2 25071 |
. . . . . . . 8
β’ ((πΊ β dom β«1
β§ ((ran πΉ β {0})
β Fin β§ (ran πΊ
β {0}) β (ran πΉ
β {0}) β§ (ran πΉ
β {0}) β (β β {0}))) β
(β«1βπΊ)
= Ξ£π β (ran
πΉ β {0})(π Β· (volβ(β‘πΊ β {π})))) |
203 | 185, 186,
199, 201, 202 | syl13anc 1373 |
. . . . . . 7
β’ ((π β§ π β β) β
(β«1βπΊ)
= Ξ£π β (ran
πΉ β {0})(π Β· (volβ(β‘πΊ β {π})))) |
204 | | fvex 6859 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πΉβπ₯) β V |
205 | | c0ex 11157 |
. . . . . . . . . . . . . . . . . . . . 21
β’ 0 β
V |
206 | 204, 205 | ifex 4540 |
. . . . . . . . . . . . . . . . . . . 20
β’ if(π₯ β (π΄βπ), (πΉβπ₯), 0) β V |
207 | 183 | fvmpt2 6963 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π₯ β β β§ if(π₯ β (π΄βπ), (πΉβπ₯), 0) β V) β (πΊβπ₯) = if(π₯ β (π΄βπ), (πΉβπ₯), 0)) |
208 | 206, 207 | mpan2 690 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β β β (πΊβπ₯) = if(π₯ β (π΄βπ), (πΉβπ₯), 0)) |
209 | 208 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β) β§ π β (ran πΉ β {0})) β§ π₯ β β) β (πΊβπ₯) = if(π₯ β (π΄βπ), (πΉβπ₯), 0)) |
210 | 209 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β) β§ π β (ran πΉ β {0})) β§ π₯ β β) β ((πΊβπ₯) = π β if(π₯ β (π΄βπ), (πΉβπ₯), 0) = π)) |
211 | | eldifsni 4754 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (ran πΉ β {0}) β π β 0) |
212 | 211 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ π β β) β§ π β (ran πΉ β {0})) β§ π₯ β β) β π β 0) |
213 | | neeq1 3003 |
. . . . . . . . . . . . . . . . . . . 20
β’ (if(π₯ β (π΄βπ), (πΉβπ₯), 0) = π β (if(π₯ β (π΄βπ), (πΉβπ₯), 0) β 0 β π β 0)) |
214 | 212, 213 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ π β β) β§ π β (ran πΉ β {0})) β§ π₯ β β) β (if(π₯ β (π΄βπ), (πΉβπ₯), 0) = π β if(π₯ β (π΄βπ), (πΉβπ₯), 0) β 0)) |
215 | | iffalse 4499 |
. . . . . . . . . . . . . . . . . . . 20
β’ (Β¬
π₯ β (π΄βπ) β if(π₯ β (π΄βπ), (πΉβπ₯), 0) = 0) |
216 | 215 | necon1ai 2968 |
. . . . . . . . . . . . . . . . . . 19
β’ (if(π₯ β (π΄βπ), (πΉβπ₯), 0) β 0 β π₯ β (π΄βπ)) |
217 | 214, 216 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ π β β) β§ π β (ran πΉ β {0})) β§ π₯ β β) β (if(π₯ β (π΄βπ), (πΉβπ₯), 0) = π β π₯ β (π΄βπ))) |
218 | 217 | pm4.71rd 564 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β) β§ π β (ran πΉ β {0})) β§ π₯ β β) β (if(π₯ β (π΄βπ), (πΉβπ₯), 0) = π β (π₯ β (π΄βπ) β§ if(π₯ β (π΄βπ), (πΉβπ₯), 0) = π))) |
219 | 210, 218 | bitrd 279 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β) β§ π β (ran πΉ β {0})) β§ π₯ β β) β ((πΊβπ₯) = π β (π₯ β (π΄βπ) β§ if(π₯ β (π΄βπ), (πΉβπ₯), 0) = π))) |
220 | | iftrue 4496 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β (π΄βπ) β if(π₯ β (π΄βπ), (πΉβπ₯), 0) = (πΉβπ₯)) |
221 | 220 | eqeq1d 2735 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β (π΄βπ) β (if(π₯ β (π΄βπ), (πΉβπ₯), 0) = π β (πΉβπ₯) = π)) |
222 | 221 | pm5.32i 576 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β (π΄βπ) β§ if(π₯ β (π΄βπ), (πΉβπ₯), 0) = π) β (π₯ β (π΄βπ) β§ (πΉβπ₯) = π)) |
223 | 222 | biancomi 464 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β (π΄βπ) β§ if(π₯ β (π΄βπ), (πΉβπ₯), 0) = π) β ((πΉβπ₯) = π β§ π₯ β (π΄βπ))) |
224 | 219, 223 | bitrdi 287 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β) β§ π β (ran πΉ β {0})) β§ π₯ β β) β ((πΊβπ₯) = π β ((πΉβπ₯) = π β§ π₯ β (π΄βπ)))) |
225 | 224 | pm5.32da 580 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (ran πΉ β {0})) β ((π₯ β β β§ (πΊβπ₯) = π) β (π₯ β β β§ ((πΉβπ₯) = π β§ π₯ β (π΄βπ))))) |
226 | | anass 470 |
. . . . . . . . . . . . . 14
β’ (((π₯ β β β§ (πΉβπ₯) = π) β§ π₯ β (π΄βπ)) β (π₯ β β β§ ((πΉβπ₯) = π β§ π₯ β (π΄βπ)))) |
227 | 225, 226 | bitr4di 289 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (ran πΉ β {0})) β ((π₯ β β β§ (πΊβπ₯) = π) β ((π₯ β β β§ (πΉβπ₯) = π) β§ π₯ β (π΄βπ)))) |
228 | | i1ff 25063 |
. . . . . . . . . . . . . . . 16
β’ (πΊ β dom β«1
β πΊ:ββΆβ) |
229 | | ffn 6672 |
. . . . . . . . . . . . . . . 16
β’ (πΊ:ββΆβ β
πΊ Fn
β) |
230 | 185, 228,
229 | 3syl 18 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β πΊ Fn β) |
231 | 230 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (ran πΉ β {0})) β πΊ Fn β) |
232 | | fniniseg 7014 |
. . . . . . . . . . . . . 14
β’ (πΊ Fn β β (π₯ β (β‘πΊ β {π}) β (π₯ β β β§ (πΊβπ₯) = π))) |
233 | 231, 232 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (ran πΉ β {0})) β (π₯ β (β‘πΊ β {π}) β (π₯ β β β§ (πΊβπ₯) = π))) |
234 | | elin 3930 |
. . . . . . . . . . . . . 14
β’ (π₯ β ((β‘πΉ β {π}) β© (π΄βπ)) β (π₯ β (β‘πΉ β {π}) β§ π₯ β (π΄βπ))) |
235 | 189 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β (ran πΉ β {0})) β πΉ Fn β) |
236 | | fniniseg 7014 |
. . . . . . . . . . . . . . . 16
β’ (πΉ Fn β β (π₯ β (β‘πΉ β {π}) β (π₯ β β β§ (πΉβπ₯) = π))) |
237 | 235, 236 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ π β (ran πΉ β {0})) β (π₯ β (β‘πΉ β {π}) β (π₯ β β β§ (πΉβπ₯) = π))) |
238 | 237 | anbi1d 631 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ π β (ran πΉ β {0})) β ((π₯ β (β‘πΉ β {π}) β§ π₯ β (π΄βπ)) β ((π₯ β β β§ (πΉβπ₯) = π) β§ π₯ β (π΄βπ)))) |
239 | 234, 238 | bitrid 283 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ π β (ran πΉ β {0})) β (π₯ β ((β‘πΉ β {π}) β© (π΄βπ)) β ((π₯ β β β§ (πΉβπ₯) = π) β§ π₯ β (π΄βπ)))) |
240 | 227, 233,
239 | 3bitr4d 311 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ π β (ran πΉ β {0})) β (π₯ β (β‘πΊ β {π}) β π₯ β ((β‘πΉ β {π}) β© (π΄βπ)))) |
241 | 240 | alrimiv 1931 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ π β (ran πΉ β {0})) β βπ₯(π₯ β (β‘πΊ β {π}) β π₯ β ((β‘πΉ β {π}) β© (π΄βπ)))) |
242 | | nfmpt1 5217 |
. . . . . . . . . . . . . . 15
β’
β²π₯(π₯ β β β¦ if(π₯ β (π΄βπ), (πΉβπ₯), 0)) |
243 | 183, 242 | nfcxfr 2902 |
. . . . . . . . . . . . . 14
β’
β²π₯πΊ |
244 | 243 | nfcnv 5838 |
. . . . . . . . . . . . 13
β’
β²π₯β‘πΊ |
245 | | nfcv 2904 |
. . . . . . . . . . . . 13
β’
β²π₯{π} |
246 | 244, 245 | nfima 6025 |
. . . . . . . . . . . 12
β’
β²π₯(β‘πΊ β {π}) |
247 | | nfcv 2904 |
. . . . . . . . . . . 12
β’
β²π₯((β‘πΉ β {π}) β© (π΄βπ)) |
248 | 246, 247 | cleqf 2935 |
. . . . . . . . . . 11
β’ ((β‘πΊ β {π}) = ((β‘πΉ β {π}) β© (π΄βπ)) β βπ₯(π₯ β (β‘πΊ β {π}) β π₯ β ((β‘πΉ β {π}) β© (π΄βπ)))) |
249 | 241, 248 | sylibr 233 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ π β (ran πΉ β {0})) β (β‘πΊ β {π}) = ((β‘πΉ β {π}) β© (π΄βπ))) |
250 | 249 | fveq2d 6850 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ π β (ran πΉ β {0})) β (volβ(β‘πΊ β {π})) = (volβ((β‘πΉ β {π}) β© (π΄βπ)))) |
251 | 250 | oveq2d 7377 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π β (ran πΉ β {0})) β (π Β· (volβ(β‘πΊ β {π}))) = (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) |
252 | 251 | sumeq2dv 15596 |
. . . . . . 7
β’ ((π β§ π β β) β Ξ£π β (ran πΉ β {0})(π Β· (volβ(β‘πΊ β {π}))) = Ξ£π β (ran πΉ β {0})(π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) |
253 | 203, 252 | eqtrd 2773 |
. . . . . 6
β’ ((π β§ π β β) β
(β«1βπΊ)
= Ξ£π β (ran
πΉ β {0})(π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) |
254 | 253 | mpteq2dva 5209 |
. . . . 5
β’ (π β (π β β β¦
(β«1βπΊ)) = (π β β β¦ Ξ£π β (ran πΉ β {0})(π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))))) |
255 | 254 | fveq1d 6848 |
. . . 4
β’ (π β ((π β β β¦
(β«1βπΊ))βπ) = ((π β β β¦ Ξ£π β (ran πΉ β {0})(π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))))βπ)) |
256 | 166 | sumeq2sdv 15597 |
. . . . . 6
β’ (π = π β Ξ£π β (ran πΉ β {0})(π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))) = Ξ£π β (ran πΉ β {0})(π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) |
257 | | eqid 2733 |
. . . . . 6
β’ (π β β β¦
Ξ£π β (ran πΉ β {0})(π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) = (π β β β¦ Ξ£π β (ran πΉ β {0})(π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) |
258 | | sumex 15581 |
. . . . . 6
β’
Ξ£π β (ran
πΉ β {0})(π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))) β V |
259 | 256, 257,
258 | fvmpt 6952 |
. . . . 5
β’ (π β β β ((π β β β¦
Ξ£π β (ran πΉ β {0})(π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))))βπ) = Ξ£π β (ran πΉ β {0})(π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) |
260 | 169 | sumeq2sdv 15597 |
. . . . 5
β’ (π β β β
Ξ£π β (ran πΉ β {0})((π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))))βπ) = Ξ£π β (ran πΉ β {0})(π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ))))) |
261 | 259, 260 | eqtr4d 2776 |
. . . 4
β’ (π β β β ((π β β β¦
Ξ£π β (ran πΉ β {0})(π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))))βπ) = Ξ£π β (ran πΉ β {0})((π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))))βπ)) |
262 | 255, 261 | sylan9eq 2793 |
. . 3
β’ ((π β§ π β β) β ((π β β β¦
(β«1βπΊ))βπ) = Ξ£π β (ran πΉ β {0})((π β β β¦ (π Β· (volβ((β‘πΉ β {π}) β© (π΄βπ)))))βπ)) |
263 | 1, 2, 8, 173, 175, 181, 262 | climfsum 15713 |
. 2
β’ (π β (π β β β¦
(β«1βπΊ)) β Ξ£π β (ran πΉ β {0})(π Β· (volβ(β‘πΉ β {π})))) |
264 | | itg1val 25070 |
. . 3
β’ (πΉ β dom β«1
β (β«1βπΉ) = Ξ£π β (ran πΉ β {0})(π Β· (volβ(β‘πΉ β {π})))) |
265 | 3, 264 | syl 17 |
. 2
β’ (π β
(β«1βπΉ)
= Ξ£π β (ran
πΉ β {0})(π Β· (volβ(β‘πΉ β {π})))) |
266 | 263, 265 | breqtrrd 5137 |
1
β’ (π β (π β β β¦
(β«1βπΊ)) β (β«1βπΉ)) |