Step | Hyp | Ref
| Expression |
1 | | i1fadd.1 |
. . . 4
β’ (π β πΉ β dom
β«1) |
2 | | i1frn 25057 |
. . . 4
β’ (πΉ β dom β«1
β ran πΉ β
Fin) |
3 | 1, 2 | syl 17 |
. . 3
β’ (π β ran πΉ β Fin) |
4 | | i1fadd.2 |
. . . . . 6
β’ (π β πΊ β dom
β«1) |
5 | | i1frn 25057 |
. . . . . 6
β’ (πΊ β dom β«1
β ran πΊ β
Fin) |
6 | 4, 5 | syl 17 |
. . . . 5
β’ (π β ran πΊ β Fin) |
7 | 6 | adantr 482 |
. . . 4
β’ ((π β§ π¦ β ran πΉ) β ran πΊ β Fin) |
8 | | i1ff 25056 |
. . . . . . . . . 10
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
9 | 1, 8 | syl 17 |
. . . . . . . . 9
β’ (π β πΉ:ββΆβ) |
10 | 9 | frnd 6681 |
. . . . . . . 8
β’ (π β ran πΉ β β) |
11 | 10 | sselda 3949 |
. . . . . . 7
β’ ((π β§ π¦ β ran πΉ) β π¦ β β) |
12 | 11 | adantr 482 |
. . . . . 6
β’ (((π β§ π¦ β ran πΉ) β§ π§ β ran πΊ) β π¦ β β) |
13 | 12 | recnd 11190 |
. . . . 5
β’ (((π β§ π¦ β ran πΉ) β§ π§ β ran πΊ) β π¦ β β) |
14 | | itg1add.3 |
. . . . . . . . 9
β’ πΌ = (π β β, π β β β¦ if((π = 0 β§ π = 0), 0, (volβ((β‘πΉ β {π}) β© (β‘πΊ β {π}))))) |
15 | 1, 4, 14 | itg1addlem2 25077 |
. . . . . . . 8
β’ (π β πΌ:(β Γ
β)βΆβ) |
16 | 15 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β ran πΉ) β§ π§ β ran πΊ) β πΌ:(β Γ
β)βΆβ) |
17 | | i1ff 25056 |
. . . . . . . . . . 11
β’ (πΊ β dom β«1
β πΊ:ββΆβ) |
18 | 4, 17 | syl 17 |
. . . . . . . . . 10
β’ (π β πΊ:ββΆβ) |
19 | 18 | frnd 6681 |
. . . . . . . . 9
β’ (π β ran πΊ β β) |
20 | 19 | sselda 3949 |
. . . . . . . 8
β’ ((π β§ π§ β ran πΊ) β π§ β β) |
21 | 20 | adantlr 714 |
. . . . . . 7
β’ (((π β§ π¦ β ran πΉ) β§ π§ β ran πΊ) β π§ β β) |
22 | 16, 12, 21 | fovcdmd 7531 |
. . . . . 6
β’ (((π β§ π¦ β ran πΉ) β§ π§ β ran πΊ) β (π¦πΌπ§) β β) |
23 | 22 | recnd 11190 |
. . . . 5
β’ (((π β§ π¦ β ran πΉ) β§ π§ β ran πΊ) β (π¦πΌπ§) β β) |
24 | 13, 23 | mulcld 11182 |
. . . 4
β’ (((π β§ π¦ β ran πΉ) β§ π§ β ran πΊ) β (π¦ Β· (π¦πΌπ§)) β β) |
25 | 7, 24 | fsumcl 15625 |
. . 3
β’ ((π β§ π¦ β ran πΉ) β Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§)) β β) |
26 | 21 | recnd 11190 |
. . . . 5
β’ (((π β§ π¦ β ran πΉ) β§ π§ β ran πΊ) β π§ β β) |
27 | 26, 23 | mulcld 11182 |
. . . 4
β’ (((π β§ π¦ β ran πΉ) β§ π§ β ran πΊ) β (π§ Β· (π¦πΌπ§)) β β) |
28 | 7, 27 | fsumcl 15625 |
. . 3
β’ ((π β§ π¦ β ran πΉ) β Ξ£π§ β ran πΊ(π§ Β· (π¦πΌπ§)) β β) |
29 | 3, 25, 28 | fsumadd 15632 |
. 2
β’ (π β Ξ£π¦ β ran πΉ(Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§)) + Ξ£π§ β ran πΊ(π§ Β· (π¦πΌπ§))) = (Ξ£π¦ β ran πΉΞ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§)) + Ξ£π¦ β ran πΉΞ£π§ β ran πΊ(π§ Β· (π¦πΌπ§)))) |
30 | | itg1add.4 |
. . . 4
β’ π = ( + βΎ (ran πΉ Γ ran πΊ)) |
31 | 1, 4, 14, 30 | itg1addlem4 25079 |
. . 3
β’ (π β
(β«1β(πΉ
βf + πΊ)) =
Ξ£π¦ β ran πΉΞ£π§ β ran πΊ((π¦ + π§) Β· (π¦πΌπ§))) |
32 | 13, 26, 23 | adddird 11187 |
. . . . . 6
β’ (((π β§ π¦ β ran πΉ) β§ π§ β ran πΊ) β ((π¦ + π§) Β· (π¦πΌπ§)) = ((π¦ Β· (π¦πΌπ§)) + (π§ Β· (π¦πΌπ§)))) |
33 | 32 | sumeq2dv 15595 |
. . . . 5
β’ ((π β§ π¦ β ran πΉ) β Ξ£π§ β ran πΊ((π¦ + π§) Β· (π¦πΌπ§)) = Ξ£π§ β ran πΊ((π¦ Β· (π¦πΌπ§)) + (π§ Β· (π¦πΌπ§)))) |
34 | 7, 24, 27 | fsumadd 15632 |
. . . . 5
β’ ((π β§ π¦ β ran πΉ) β Ξ£π§ β ran πΊ((π¦ Β· (π¦πΌπ§)) + (π§ Β· (π¦πΌπ§))) = (Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§)) + Ξ£π§ β ran πΊ(π§ Β· (π¦πΌπ§)))) |
35 | 33, 34 | eqtrd 2777 |
. . . 4
β’ ((π β§ π¦ β ran πΉ) β Ξ£π§ β ran πΊ((π¦ + π§) Β· (π¦πΌπ§)) = (Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§)) + Ξ£π§ β ran πΊ(π§ Β· (π¦πΌπ§)))) |
36 | 35 | sumeq2dv 15595 |
. . 3
β’ (π β Ξ£π¦ β ran πΉΞ£π§ β ran πΊ((π¦ + π§) Β· (π¦πΌπ§)) = Ξ£π¦ β ran πΉ(Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§)) + Ξ£π§ β ran πΊ(π§ Β· (π¦πΌπ§)))) |
37 | 31, 36 | eqtrd 2777 |
. 2
β’ (π β
(β«1β(πΉ
βf + πΊ)) =
Ξ£π¦ β ran πΉ(Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§)) + Ξ£π§ β ran πΊ(π§ Β· (π¦πΌπ§)))) |
38 | | itg1val 25063 |
. . . . 5
β’ (πΉ β dom β«1
β (β«1βπΉ) = Ξ£π¦ β (ran πΉ β {0})(π¦ Β· (volβ(β‘πΉ β {π¦})))) |
39 | 1, 38 | syl 17 |
. . . 4
β’ (π β
(β«1βπΉ)
= Ξ£π¦ β (ran
πΉ β {0})(π¦ Β· (volβ(β‘πΉ β {π¦})))) |
40 | 18 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β (ran πΉ β {0})) β πΊ:ββΆβ) |
41 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β (ran πΉ β {0})) β ran πΊ β Fin) |
42 | | inss2 4194 |
. . . . . . . . . 10
β’ ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) β (β‘πΊ β {π§}) |
43 | 42 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) β (β‘πΊ β {π§})) |
44 | | i1fima 25058 |
. . . . . . . . . . . 12
β’ (πΉ β dom β«1
β (β‘πΉ β {π¦}) β dom vol) |
45 | 1, 44 | syl 17 |
. . . . . . . . . . 11
β’ (π β (β‘πΉ β {π¦}) β dom vol) |
46 | 45 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β (β‘πΉ β {π¦}) β dom vol) |
47 | | i1fima 25058 |
. . . . . . . . . . . 12
β’ (πΊ β dom β«1
β (β‘πΊ β {π§}) β dom vol) |
48 | 4, 47 | syl 17 |
. . . . . . . . . . 11
β’ (π β (β‘πΊ β {π§}) β dom vol) |
49 | 48 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β (β‘πΊ β {π§}) β dom vol) |
50 | | inmbl 24922 |
. . . . . . . . . 10
β’ (((β‘πΉ β {π¦}) β dom vol β§ (β‘πΊ β {π§}) β dom vol) β ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) β dom vol) |
51 | 46, 49, 50 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) β dom vol) |
52 | 10 | ssdifssd 4107 |
. . . . . . . . . . . . 13
β’ (π β (ran πΉ β {0}) β
β) |
53 | 52 | sselda 3949 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (ran πΉ β {0})) β π¦ β β) |
54 | 53 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β π¦ β β) |
55 | 19 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (ran πΉ β {0})) β ran πΊ β β) |
56 | 55 | sselda 3949 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β π§ β β) |
57 | | eldifsni 4755 |
. . . . . . . . . . . . 13
β’ (π¦ β (ran πΉ β {0}) β π¦ β 0) |
58 | 57 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β π¦ β 0) |
59 | | simpl 484 |
. . . . . . . . . . . . 13
β’ ((π¦ = 0 β§ π§ = 0) β π¦ = 0) |
60 | 59 | necon3ai 2969 |
. . . . . . . . . . . 12
β’ (π¦ β 0 β Β¬ (π¦ = 0 β§ π§ = 0)) |
61 | 58, 60 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β Β¬ (π¦ = 0 β§ π§ = 0)) |
62 | 1, 4, 14 | itg1addlem3 25078 |
. . . . . . . . . . 11
β’ (((π¦ β β β§ π§ β β) β§ Β¬
(π¦ = 0 β§ π§ = 0)) β (π¦πΌπ§) = (volβ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})))) |
63 | 54, 56, 61, 62 | syl21anc 837 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β (π¦πΌπ§) = (volβ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})))) |
64 | 15 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β πΌ:(β Γ
β)βΆβ) |
65 | 64, 54, 56 | fovcdmd 7531 |
. . . . . . . . . 10
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β (π¦πΌπ§) β β) |
66 | 63, 65 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β (volβ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§}))) β β) |
67 | 40, 41, 43, 51, 66 | itg1addlem1 25072 |
. . . . . . . 8
β’ ((π β§ π¦ β (ran πΉ β {0})) β (volββͺ π§ β ran πΊ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§}))) = Ξ£π§ β ran πΊ(volβ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})))) |
68 | | iunin2 5036 |
. . . . . . . . . 10
β’ βͺ π§ β ran πΊ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) = ((β‘πΉ β {π¦}) β© βͺ
π§ β ran πΊ(β‘πΊ β {π§})) |
69 | 1 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π¦ β (ran πΉ β {0})) β πΉ β dom
β«1) |
70 | 69, 44 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (ran πΉ β {0})) β (β‘πΉ β {π¦}) β dom vol) |
71 | | mblss 24911 |
. . . . . . . . . . . . 13
β’ ((β‘πΉ β {π¦}) β dom vol β (β‘πΉ β {π¦}) β β) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (ran πΉ β {0})) β (β‘πΉ β {π¦}) β β) |
73 | | iunid 5025 |
. . . . . . . . . . . . . . 15
β’ βͺ π§ β ran πΊ{π§} = ran πΊ |
74 | 73 | imaeq2i 6016 |
. . . . . . . . . . . . . 14
β’ (β‘πΊ β βͺ
π§ β ran πΊ{π§}) = (β‘πΊ β ran πΊ) |
75 | | imaiun 7197 |
. . . . . . . . . . . . . 14
β’ (β‘πΊ β βͺ
π§ β ran πΊ{π§}) = βͺ
π§ β ran πΊ(β‘πΊ β {π§}) |
76 | | cnvimarndm 6039 |
. . . . . . . . . . . . . 14
β’ (β‘πΊ β ran πΊ) = dom πΊ |
77 | 74, 75, 76 | 3eqtr3i 2773 |
. . . . . . . . . . . . 13
β’ βͺ π§ β ran πΊ(β‘πΊ β {π§}) = dom πΊ |
78 | 40 | fdmd 6684 |
. . . . . . . . . . . . 13
β’ ((π β§ π¦ β (ran πΉ β {0})) β dom πΊ = β) |
79 | 77, 78 | eqtrid 2789 |
. . . . . . . . . . . 12
β’ ((π β§ π¦ β (ran πΉ β {0})) β βͺ π§ β ran πΊ(β‘πΊ β {π§}) = β) |
80 | 72, 79 | sseqtrrd 3990 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β (ran πΉ β {0})) β (β‘πΉ β {π¦}) β βͺ π§ β ran πΊ(β‘πΊ β {π§})) |
81 | | df-ss 3932 |
. . . . . . . . . . 11
β’ ((β‘πΉ β {π¦}) β βͺ π§ β ran πΊ(β‘πΊ β {π§}) β ((β‘πΉ β {π¦}) β© βͺ
π§ β ran πΊ(β‘πΊ β {π§})) = (β‘πΉ β {π¦})) |
82 | 80, 81 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π¦ β (ran πΉ β {0})) β ((β‘πΉ β {π¦}) β© βͺ
π§ β ran πΊ(β‘πΊ β {π§})) = (β‘πΉ β {π¦})) |
83 | 68, 82 | eqtr2id 2790 |
. . . . . . . . 9
β’ ((π β§ π¦ β (ran πΉ β {0})) β (β‘πΉ β {π¦}) = βͺ
π§ β ran πΊ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§}))) |
84 | 83 | fveq2d 6851 |
. . . . . . . 8
β’ ((π β§ π¦ β (ran πΉ β {0})) β (volβ(β‘πΉ β {π¦})) = (volββͺ π§ β ran πΊ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})))) |
85 | 63 | sumeq2dv 15595 |
. . . . . . . 8
β’ ((π β§ π¦ β (ran πΉ β {0})) β Ξ£π§ β ran πΊ(π¦πΌπ§) = Ξ£π§ β ran πΊ(volβ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})))) |
86 | 67, 84, 85 | 3eqtr4d 2787 |
. . . . . . 7
β’ ((π β§ π¦ β (ran πΉ β {0})) β (volβ(β‘πΉ β {π¦})) = Ξ£π§ β ran πΊ(π¦πΌπ§)) |
87 | 86 | oveq2d 7378 |
. . . . . 6
β’ ((π β§ π¦ β (ran πΉ β {0})) β (π¦ Β· (volβ(β‘πΉ β {π¦}))) = (π¦ Β· Ξ£π§ β ran πΊ(π¦πΌπ§))) |
88 | 53 | recnd 11190 |
. . . . . . 7
β’ ((π β§ π¦ β (ran πΉ β {0})) β π¦ β β) |
89 | 65 | recnd 11190 |
. . . . . . 7
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β (π¦πΌπ§) β β) |
90 | 41, 88, 89 | fsummulc2 15676 |
. . . . . 6
β’ ((π β§ π¦ β (ran πΉ β {0})) β (π¦ Β· Ξ£π§ β ran πΊ(π¦πΌπ§)) = Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§))) |
91 | 87, 90 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π¦ β (ran πΉ β {0})) β (π¦ Β· (volβ(β‘πΉ β {π¦}))) = Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§))) |
92 | 91 | sumeq2dv 15595 |
. . . 4
β’ (π β Ξ£π¦ β (ran πΉ β {0})(π¦ Β· (volβ(β‘πΉ β {π¦}))) = Ξ£π¦ β (ran πΉ β {0})Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§))) |
93 | | difssd 4097 |
. . . . 5
β’ (π β (ran πΉ β {0}) β ran πΉ) |
94 | 54 | recnd 11190 |
. . . . . . 7
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β π¦ β β) |
95 | 94, 89 | mulcld 11182 |
. . . . . 6
β’ (((π β§ π¦ β (ran πΉ β {0})) β§ π§ β ran πΊ) β (π¦ Β· (π¦πΌπ§)) β β) |
96 | 41, 95 | fsumcl 15625 |
. . . . 5
β’ ((π β§ π¦ β (ran πΉ β {0})) β Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§)) β β) |
97 | | dfin4 4232 |
. . . . . . . 8
β’ (ran
πΉ β© {0}) = (ran πΉ β (ran πΉ β {0})) |
98 | | inss2 4194 |
. . . . . . . 8
β’ (ran
πΉ β© {0}) β
{0} |
99 | 97, 98 | eqsstrri 3984 |
. . . . . . 7
β’ (ran
πΉ β (ran πΉ β {0})) β
{0} |
100 | 99 | sseli 3945 |
. . . . . 6
β’ (π¦ β (ran πΉ β (ran πΉ β {0})) β π¦ β {0}) |
101 | | elsni 4608 |
. . . . . . . . . . 11
β’ (π¦ β {0} β π¦ = 0) |
102 | 101 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π¦ β {0}) β§ π§ β ran πΊ) β π¦ = 0) |
103 | 102 | oveq1d 7377 |
. . . . . . . . 9
β’ (((π β§ π¦ β {0}) β§ π§ β ran πΊ) β (π¦ Β· (π¦πΌπ§)) = (0 Β· (π¦πΌπ§))) |
104 | 15 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β {0}) β§ π§ β ran πΊ) β πΌ:(β Γ
β)βΆβ) |
105 | | 0re 11164 |
. . . . . . . . . . . . 13
β’ 0 β
β |
106 | 102, 105 | eqeltrdi 2846 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β {0}) β§ π§ β ran πΊ) β π¦ β β) |
107 | 20 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β {0}) β§ π§ β ran πΊ) β π§ β β) |
108 | 104, 106,
107 | fovcdmd 7531 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β {0}) β§ π§ β ran πΊ) β (π¦πΌπ§) β β) |
109 | 108 | recnd 11190 |
. . . . . . . . . 10
β’ (((π β§ π¦ β {0}) β§ π§ β ran πΊ) β (π¦πΌπ§) β β) |
110 | 109 | mul02d 11360 |
. . . . . . . . 9
β’ (((π β§ π¦ β {0}) β§ π§ β ran πΊ) β (0 Β· (π¦πΌπ§)) = 0) |
111 | 103, 110 | eqtrd 2777 |
. . . . . . . 8
β’ (((π β§ π¦ β {0}) β§ π§ β ran πΊ) β (π¦ Β· (π¦πΌπ§)) = 0) |
112 | 111 | sumeq2dv 15595 |
. . . . . . 7
β’ ((π β§ π¦ β {0}) β Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§)) = Ξ£π§ β ran πΊ0) |
113 | 6 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β {0}) β ran πΊ β Fin) |
114 | 113 | olcd 873 |
. . . . . . . 8
β’ ((π β§ π¦ β {0}) β (ran πΊ β (β€β₯β0)
β¨ ran πΊ β
Fin)) |
115 | | sumz 15614 |
. . . . . . . 8
β’ ((ran
πΊ β
(β€β₯β0) β¨ ran πΊ β Fin) β Ξ£π§ β ran πΊ0 = 0) |
116 | 114, 115 | syl 17 |
. . . . . . 7
β’ ((π β§ π¦ β {0}) β Ξ£π§ β ran πΊ0 = 0) |
117 | 112, 116 | eqtrd 2777 |
. . . . . 6
β’ ((π β§ π¦ β {0}) β Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§)) = 0) |
118 | 100, 117 | sylan2 594 |
. . . . 5
β’ ((π β§ π¦ β (ran πΉ β (ran πΉ β {0}))) β Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§)) = 0) |
119 | 93, 96, 118, 3 | fsumss 15617 |
. . . 4
β’ (π β Ξ£π¦ β (ran πΉ β {0})Ξ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§)) = Ξ£π¦ β ran πΉΞ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§))) |
120 | 39, 92, 119 | 3eqtrd 2781 |
. . 3
β’ (π β
(β«1βπΉ)
= Ξ£π¦ β ran πΉΞ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§))) |
121 | | itg1val 25063 |
. . . . 5
β’ (πΊ β dom β«1
β (β«1βπΊ) = Ξ£π§ β (ran πΊ β {0})(π§ Β· (volβ(β‘πΊ β {π§})))) |
122 | 4, 121 | syl 17 |
. . . 4
β’ (π β
(β«1βπΊ)
= Ξ£π§ β (ran
πΊ β {0})(π§ Β· (volβ(β‘πΊ β {π§})))) |
123 | 9 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π§ β (ran πΊ β {0})) β πΉ:ββΆβ) |
124 | 3 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π§ β (ran πΊ β {0})) β ran πΉ β Fin) |
125 | | inss1 4193 |
. . . . . . . . . 10
β’ ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) β (β‘πΉ β {π¦}) |
126 | 125 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) β (β‘πΉ β {π¦})) |
127 | 45 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β (β‘πΉ β {π¦}) β dom vol) |
128 | 48 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β (β‘πΊ β {π§}) β dom vol) |
129 | 127, 128,
50 | syl2anc 585 |
. . . . . . . . 9
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) β dom vol) |
130 | 10 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (ran πΊ β {0})) β ran πΉ β β) |
131 | 130 | sselda 3949 |
. . . . . . . . . . 11
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β π¦ β β) |
132 | 19 | ssdifssd 4107 |
. . . . . . . . . . . . 13
β’ (π β (ran πΊ β {0}) β
β) |
133 | 132 | sselda 3949 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (ran πΊ β {0})) β π§ β β) |
134 | 133 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β π§ β β) |
135 | | eldifsni 4755 |
. . . . . . . . . . . . 13
β’ (π§ β (ran πΊ β {0}) β π§ β 0) |
136 | 135 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β π§ β 0) |
137 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π¦ = 0 β§ π§ = 0) β π§ = 0) |
138 | 137 | necon3ai 2969 |
. . . . . . . . . . . 12
β’ (π§ β 0 β Β¬ (π¦ = 0 β§ π§ = 0)) |
139 | 136, 138 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β Β¬ (π¦ = 0 β§ π§ = 0)) |
140 | 131, 134,
139, 62 | syl21anc 837 |
. . . . . . . . . 10
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β (π¦πΌπ§) = (volβ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})))) |
141 | 15 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β πΌ:(β Γ
β)βΆβ) |
142 | 141, 131,
134 | fovcdmd 7531 |
. . . . . . . . . 10
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β (π¦πΌπ§) β β) |
143 | 140, 142 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β (volβ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§}))) β β) |
144 | 123, 124,
126, 129, 143 | itg1addlem1 25072 |
. . . . . . . 8
β’ ((π β§ π§ β (ran πΊ β {0})) β (volββͺ π¦ β ran πΉ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§}))) = Ξ£π¦ β ran πΉ(volβ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})))) |
145 | | incom 4166 |
. . . . . . . . . . . . 13
β’ ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) = ((β‘πΊ β {π§}) β© (β‘πΉ β {π¦})) |
146 | 145 | a1i 11 |
. . . . . . . . . . . 12
β’ (π¦ β ran πΉ β ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) = ((β‘πΊ β {π§}) β© (β‘πΉ β {π¦}))) |
147 | 146 | iuneq2i 4980 |
. . . . . . . . . . 11
β’ βͺ π¦ β ran πΉ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) = βͺ
π¦ β ran πΉ((β‘πΊ β {π§}) β© (β‘πΉ β {π¦})) |
148 | | iunin2 5036 |
. . . . . . . . . . 11
β’ βͺ π¦ β ran πΉ((β‘πΊ β {π§}) β© (β‘πΉ β {π¦})) = ((β‘πΊ β {π§}) β© βͺ
π¦ β ran πΉ(β‘πΉ β {π¦})) |
149 | 147, 148 | eqtri 2765 |
. . . . . . . . . 10
β’ βͺ π¦ β ran πΉ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})) = ((β‘πΊ β {π§}) β© βͺ
π¦ β ran πΉ(β‘πΉ β {π¦})) |
150 | | cnvimass 6038 |
. . . . . . . . . . . . 13
β’ (β‘πΊ β {π§}) β dom πΊ |
151 | 18 | fdmd 6684 |
. . . . . . . . . . . . . 14
β’ (π β dom πΊ = β) |
152 | 151 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β (ran πΊ β {0})) β dom πΊ = β) |
153 | 150, 152 | sseqtrid 4001 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (ran πΊ β {0})) β (β‘πΊ β {π§}) β β) |
154 | | iunid 5025 |
. . . . . . . . . . . . . . 15
β’ βͺ π¦ β ran πΉ{π¦} = ran πΉ |
155 | 154 | imaeq2i 6016 |
. . . . . . . . . . . . . 14
β’ (β‘πΉ β βͺ
π¦ β ran πΉ{π¦}) = (β‘πΉ β ran πΉ) |
156 | | imaiun 7197 |
. . . . . . . . . . . . . 14
β’ (β‘πΉ β βͺ
π¦ β ran πΉ{π¦}) = βͺ
π¦ β ran πΉ(β‘πΉ β {π¦}) |
157 | | cnvimarndm 6039 |
. . . . . . . . . . . . . 14
β’ (β‘πΉ β ran πΉ) = dom πΉ |
158 | 155, 156,
157 | 3eqtr3i 2773 |
. . . . . . . . . . . . 13
β’ βͺ π¦ β ran πΉ(β‘πΉ β {π¦}) = dom πΉ |
159 | 9 | fdmd 6684 |
. . . . . . . . . . . . . 14
β’ (π β dom πΉ = β) |
160 | 159 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β (ran πΊ β {0})) β dom πΉ = β) |
161 | 158, 160 | eqtrid 2789 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β (ran πΊ β {0})) β βͺ π¦ β ran πΉ(β‘πΉ β {π¦}) = β) |
162 | 153, 161 | sseqtrrd 3990 |
. . . . . . . . . . 11
β’ ((π β§ π§ β (ran πΊ β {0})) β (β‘πΊ β {π§}) β βͺ π¦ β ran πΉ(β‘πΉ β {π¦})) |
163 | | df-ss 3932 |
. . . . . . . . . . 11
β’ ((β‘πΊ β {π§}) β βͺ π¦ β ran πΉ(β‘πΉ β {π¦}) β ((β‘πΊ β {π§}) β© βͺ
π¦ β ran πΉ(β‘πΉ β {π¦})) = (β‘πΊ β {π§})) |
164 | 162, 163 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π§ β (ran πΊ β {0})) β ((β‘πΊ β {π§}) β© βͺ
π¦ β ran πΉ(β‘πΉ β {π¦})) = (β‘πΊ β {π§})) |
165 | 149, 164 | eqtr2id 2790 |
. . . . . . . . 9
β’ ((π β§ π§ β (ran πΊ β {0})) β (β‘πΊ β {π§}) = βͺ
π¦ β ran πΉ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§}))) |
166 | 165 | fveq2d 6851 |
. . . . . . . 8
β’ ((π β§ π§ β (ran πΊ β {0})) β (volβ(β‘πΊ β {π§})) = (volββͺ π¦ β ran πΉ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})))) |
167 | 140 | sumeq2dv 15595 |
. . . . . . . 8
β’ ((π β§ π§ β (ran πΊ β {0})) β Ξ£π¦ β ran πΉ(π¦πΌπ§) = Ξ£π¦ β ran πΉ(volβ((β‘πΉ β {π¦}) β© (β‘πΊ β {π§})))) |
168 | 144, 166,
167 | 3eqtr4d 2787 |
. . . . . . 7
β’ ((π β§ π§ β (ran πΊ β {0})) β (volβ(β‘πΊ β {π§})) = Ξ£π¦ β ran πΉ(π¦πΌπ§)) |
169 | 168 | oveq2d 7378 |
. . . . . 6
β’ ((π β§ π§ β (ran πΊ β {0})) β (π§ Β· (volβ(β‘πΊ β {π§}))) = (π§ Β· Ξ£π¦ β ran πΉ(π¦πΌπ§))) |
170 | 133 | recnd 11190 |
. . . . . . 7
β’ ((π β§ π§ β (ran πΊ β {0})) β π§ β β) |
171 | 142 | recnd 11190 |
. . . . . . 7
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β (π¦πΌπ§) β β) |
172 | 124, 170,
171 | fsummulc2 15676 |
. . . . . 6
β’ ((π β§ π§ β (ran πΊ β {0})) β (π§ Β· Ξ£π¦ β ran πΉ(π¦πΌπ§)) = Ξ£π¦ β ran πΉ(π§ Β· (π¦πΌπ§))) |
173 | 169, 172 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π§ β (ran πΊ β {0})) β (π§ Β· (volβ(β‘πΊ β {π§}))) = Ξ£π¦ β ran πΉ(π§ Β· (π¦πΌπ§))) |
174 | 173 | sumeq2dv 15595 |
. . . 4
β’ (π β Ξ£π§ β (ran πΊ β {0})(π§ Β· (volβ(β‘πΊ β {π§}))) = Ξ£π§ β (ran πΊ β {0})Ξ£π¦ β ran πΉ(π§ Β· (π¦πΌπ§))) |
175 | | difssd 4097 |
. . . . . 6
β’ (π β (ran πΊ β {0}) β ran πΊ) |
176 | 170 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β π§ β β) |
177 | 176, 171 | mulcld 11182 |
. . . . . . 7
β’ (((π β§ π§ β (ran πΊ β {0})) β§ π¦ β ran πΉ) β (π§ Β· (π¦πΌπ§)) β β) |
178 | 124, 177 | fsumcl 15625 |
. . . . . 6
β’ ((π β§ π§ β (ran πΊ β {0})) β Ξ£π¦ β ran πΉ(π§ Β· (π¦πΌπ§)) β β) |
179 | | dfin4 4232 |
. . . . . . . . 9
β’ (ran
πΊ β© {0}) = (ran πΊ β (ran πΊ β {0})) |
180 | | inss2 4194 |
. . . . . . . . 9
β’ (ran
πΊ β© {0}) β
{0} |
181 | 179, 180 | eqsstrri 3984 |
. . . . . . . 8
β’ (ran
πΊ β (ran πΊ β {0})) β
{0} |
182 | 181 | sseli 3945 |
. . . . . . 7
β’ (π§ β (ran πΊ β (ran πΊ β {0})) β π§ β {0}) |
183 | | elsni 4608 |
. . . . . . . . . . . 12
β’ (π§ β {0} β π§ = 0) |
184 | 183 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π§ β {0}) β§ π¦ β ran πΉ) β π§ = 0) |
185 | 184 | oveq1d 7377 |
. . . . . . . . . 10
β’ (((π β§ π§ β {0}) β§ π¦ β ran πΉ) β (π§ Β· (π¦πΌπ§)) = (0 Β· (π¦πΌπ§))) |
186 | 15 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β {0}) β§ π¦ β ran πΉ) β πΌ:(β Γ
β)βΆβ) |
187 | 11 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β {0}) β§ π¦ β ran πΉ) β π¦ β β) |
188 | 184, 105 | eqeltrdi 2846 |
. . . . . . . . . . . . 13
β’ (((π β§ π§ β {0}) β§ π¦ β ran πΉ) β π§ β β) |
189 | 186, 187,
188 | fovcdmd 7531 |
. . . . . . . . . . . 12
β’ (((π β§ π§ β {0}) β§ π¦ β ran πΉ) β (π¦πΌπ§) β β) |
190 | 189 | recnd 11190 |
. . . . . . . . . . 11
β’ (((π β§ π§ β {0}) β§ π¦ β ran πΉ) β (π¦πΌπ§) β β) |
191 | 190 | mul02d 11360 |
. . . . . . . . . 10
β’ (((π β§ π§ β {0}) β§ π¦ β ran πΉ) β (0 Β· (π¦πΌπ§)) = 0) |
192 | 185, 191 | eqtrd 2777 |
. . . . . . . . 9
β’ (((π β§ π§ β {0}) β§ π¦ β ran πΉ) β (π§ Β· (π¦πΌπ§)) = 0) |
193 | 192 | sumeq2dv 15595 |
. . . . . . . 8
β’ ((π β§ π§ β {0}) β Ξ£π¦ β ran πΉ(π§ Β· (π¦πΌπ§)) = Ξ£π¦ β ran πΉ0) |
194 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π§ β {0}) β ran πΉ β Fin) |
195 | 194 | olcd 873 |
. . . . . . . . 9
β’ ((π β§ π§ β {0}) β (ran πΉ β (β€β₯β0)
β¨ ran πΉ β
Fin)) |
196 | | sumz 15614 |
. . . . . . . . 9
β’ ((ran
πΉ β
(β€β₯β0) β¨ ran πΉ β Fin) β Ξ£π¦ β ran πΉ0 = 0) |
197 | 195, 196 | syl 17 |
. . . . . . . 8
β’ ((π β§ π§ β {0}) β Ξ£π¦ β ran πΉ0 = 0) |
198 | 193, 197 | eqtrd 2777 |
. . . . . . 7
β’ ((π β§ π§ β {0}) β Ξ£π¦ β ran πΉ(π§ Β· (π¦πΌπ§)) = 0) |
199 | 182, 198 | sylan2 594 |
. . . . . 6
β’ ((π β§ π§ β (ran πΊ β (ran πΊ β {0}))) β Ξ£π¦ β ran πΉ(π§ Β· (π¦πΌπ§)) = 0) |
200 | 175, 178,
199, 6 | fsumss 15617 |
. . . . 5
β’ (π β Ξ£π§ β (ran πΊ β {0})Ξ£π¦ β ran πΉ(π§ Β· (π¦πΌπ§)) = Ξ£π§ β ran πΊΞ£π¦ β ran πΉ(π§ Β· (π¦πΌπ§))) |
201 | 20 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β π§ β β) |
202 | 201 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β π§ β β) |
203 | 15 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β πΌ:(β Γ
β)βΆβ) |
204 | 10 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π§ β ran πΊ) β ran πΉ β β) |
205 | 204 | sselda 3949 |
. . . . . . . . . 10
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β π¦ β β) |
206 | 203, 205,
201 | fovcdmd 7531 |
. . . . . . . . 9
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β (π¦πΌπ§) β β) |
207 | 206 | recnd 11190 |
. . . . . . . 8
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β (π¦πΌπ§) β β) |
208 | 202, 207 | mulcld 11182 |
. . . . . . 7
β’ (((π β§ π§ β ran πΊ) β§ π¦ β ran πΉ) β (π§ Β· (π¦πΌπ§)) β β) |
209 | 208 | anasss 468 |
. . . . . 6
β’ ((π β§ (π§ β ran πΊ β§ π¦ β ran πΉ)) β (π§ Β· (π¦πΌπ§)) β β) |
210 | 6, 3, 209 | fsumcom 15667 |
. . . . 5
β’ (π β Ξ£π§ β ran πΊΞ£π¦ β ran πΉ(π§ Β· (π¦πΌπ§)) = Ξ£π¦ β ran πΉΞ£π§ β ran πΊ(π§ Β· (π¦πΌπ§))) |
211 | 200, 210 | eqtrd 2777 |
. . . 4
β’ (π β Ξ£π§ β (ran πΊ β {0})Ξ£π¦ β ran πΉ(π§ Β· (π¦πΌπ§)) = Ξ£π¦ β ran πΉΞ£π§ β ran πΊ(π§ Β· (π¦πΌπ§))) |
212 | 122, 174,
211 | 3eqtrd 2781 |
. . 3
β’ (π β
(β«1βπΊ)
= Ξ£π¦ β ran πΉΞ£π§ β ran πΊ(π§ Β· (π¦πΌπ§))) |
213 | 120, 212 | oveq12d 7380 |
. 2
β’ (π β
((β«1βπΉ) + (β«1βπΊ)) = (Ξ£π¦ β ran πΉΞ£π§ β ran πΊ(π¦ Β· (π¦πΌπ§)) + Ξ£π¦ β ran πΉΞ£π§ β ran πΊ(π§ Β· (π¦πΌπ§)))) |
214 | 29, 37, 213 | 3eqtr4d 2787 |
1
β’ (π β
(β«1β(πΉ
βf + πΊ)) =
((β«1βπΉ) + (β«1βπΊ))) |