Step | Hyp | Ref
| Expression |
1 | | nfcv 2908 |
. . . . . 6
β’
β²π¦if(π₯ β π΄, πΆ, 0) |
2 | | nfv 1918 |
. . . . . . 7
β’
β²π₯ π¦ β π΄ |
3 | | nfcsb1v 3885 |
. . . . . . 7
β’
β²π₯β¦π¦ / π₯β¦πΆ |
4 | | nfcv 2908 |
. . . . . . 7
β’
β²π₯0 |
5 | 2, 3, 4 | nfif 4521 |
. . . . . 6
β’
β²π₯if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0) |
6 | | eleq1w 2821 |
. . . . . . 7
β’ (π₯ = π¦ β (π₯ β π΄ β π¦ β π΄)) |
7 | | csbeq1a 3874 |
. . . . . . 7
β’ (π₯ = π¦ β πΆ = β¦π¦ / π₯β¦πΆ) |
8 | 6, 7 | ifbieq1d 4515 |
. . . . . 6
β’ (π₯ = π¦ β if(π₯ β π΄, πΆ, 0) = if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) |
9 | 1, 5, 8 | cbvmpt 5221 |
. . . . 5
β’ (π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) = (π¦ β π΅ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) |
10 | | itgss3.1 |
. . . . . . 7
β’ (π β π΄ β π΅) |
11 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β¦ πΆ) β πΏ1) β π΄ β π΅) |
12 | | nfcv 2908 |
. . . . . . . . . . . 12
β’
β²π¦πΆ |
13 | 12, 3, 7 | cbvmpt 5221 |
. . . . . . . . . . 11
β’ (π₯ β π΄ β¦ πΆ) = (π¦ β π΄ β¦ β¦π¦ / π₯β¦πΆ) |
14 | | iftrue 4497 |
. . . . . . . . . . . 12
β’ (π¦ β π΄ β if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0) = β¦π¦ / π₯β¦πΆ) |
15 | 14 | mpteq2ia 5213 |
. . . . . . . . . . 11
β’ (π¦ β π΄ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) = (π¦ β π΄ β¦ β¦π¦ / π₯β¦πΆ) |
16 | 13, 15 | eqtr4i 2768 |
. . . . . . . . . 10
β’ (π₯ β π΄ β¦ πΆ) = (π¦ β π΄ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) |
17 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΄ β¦ πΆ) β πΏ1) β
(π₯ β π΄ β¦ πΆ) β
πΏ1) |
18 | 16, 17 | eqeltrrid 2843 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΄ β¦ πΆ) β πΏ1) β
(π¦ β π΄ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) β
πΏ1) |
19 | | iblmbf 25148 |
. . . . . . . . 9
β’ ((π¦ β π΄ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) β πΏ1 β
(π¦ β π΄ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) β MblFn) |
20 | 18, 19 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΄ β¦ πΆ) β πΏ1) β
(π¦ β π΄ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) β MblFn) |
21 | 10 | sselda 3949 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β π₯ β π΅) |
22 | | itgss3.4 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΅) β πΆ β β) |
23 | 21, 22 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β πΆ β β) |
24 | 23 | fmpttd 7068 |
. . . . . . . . . . 11
β’ (π β (π₯ β π΄ β¦ πΆ):π΄βΆβ) |
25 | 24 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΄ β¦ πΆ) β πΏ1) β
(π₯ β π΄ β¦ πΆ):π΄βΆβ) |
26 | 16 | feq1i 6664 |
. . . . . . . . . 10
β’ ((π₯ β π΄ β¦ πΆ):π΄βΆβ β (π¦ β π΄ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)):π΄βΆβ) |
27 | 25, 26 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΄ β¦ πΆ) β πΏ1) β
(π¦ β π΄ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)):π΄βΆβ) |
28 | 27 | fvmptelcdm 7066 |
. . . . . . . 8
β’ (((π β§ (π₯ β π΄ β¦ πΆ) β πΏ1) β§ π¦ β π΄) β if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0) β β) |
29 | 20, 28 | mbfdm2 25017 |
. . . . . . 7
β’ ((π β§ (π₯ β π΄ β¦ πΆ) β πΏ1) β π΄ β dom
vol) |
30 | | undif 4446 |
. . . . . . . . . 10
β’ (π΄ β π΅ β (π΄ βͺ (π΅ β π΄)) = π΅) |
31 | 10, 30 | sylib 217 |
. . . . . . . . 9
β’ (π β (π΄ βͺ (π΅ β π΄)) = π΅) |
32 | 31 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π΄ β dom vol) β (π΄ βͺ (π΅ β π΄)) = π΅) |
33 | | id 22 |
. . . . . . . . 9
β’ (π΄ β dom vol β π΄ β dom
vol) |
34 | | itgss3.2 |
. . . . . . . . . . 11
β’ (π β π΅ β β) |
35 | 34 | ssdifssd 4107 |
. . . . . . . . . 10
β’ (π β (π΅ β π΄) β β) |
36 | | itgss3.3 |
. . . . . . . . . 10
β’ (π β (vol*β(π΅ β π΄)) = 0) |
37 | | nulmbl 24915 |
. . . . . . . . . 10
β’ (((π΅ β π΄) β β β§ (vol*β(π΅ β π΄)) = 0) β (π΅ β π΄) β dom vol) |
38 | 35, 36, 37 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π΅ β π΄) β dom vol) |
39 | | unmbl 24917 |
. . . . . . . . 9
β’ ((π΄ β dom vol β§ (π΅ β π΄) β dom vol) β (π΄ βͺ (π΅ β π΄)) β dom vol) |
40 | 33, 38, 39 | syl2anr 598 |
. . . . . . . 8
β’ ((π β§ π΄ β dom vol) β (π΄ βͺ (π΅ β π΄)) β dom vol) |
41 | 32, 40 | eqeltrrd 2839 |
. . . . . . 7
β’ ((π β§ π΄ β dom vol) β π΅ β dom vol) |
42 | 29, 41 | syldan 592 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β¦ πΆ) β πΏ1) β π΅ β dom
vol) |
43 | | eldifn 4092 |
. . . . . . . 8
β’ (π¦ β (π΅ β π΄) β Β¬ π¦ β π΄) |
44 | 43 | adantl 483 |
. . . . . . 7
β’ (((π β§ (π₯ β π΄ β¦ πΆ) β πΏ1) β§ π¦ β (π΅ β π΄)) β Β¬ π¦ β π΄) |
45 | 44 | iffalsed 4502 |
. . . . . 6
β’ (((π β§ (π₯ β π΄ β¦ πΆ) β πΏ1) β§ π¦ β (π΅ β π΄)) β if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0) = 0) |
46 | 11, 42, 28, 45, 18 | iblss2 25186 |
. . . . 5
β’ ((π β§ (π₯ β π΄ β¦ πΆ) β πΏ1) β
(π¦ β π΅ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) β
πΏ1) |
47 | 9, 46 | eqeltrid 2842 |
. . . 4
β’ ((π β§ (π₯ β π΄ β¦ πΆ) β πΏ1) β
(π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β
πΏ1) |
48 | | iftrue 4497 |
. . . . . . 7
β’ (π₯ β π΄ β if(π₯ β π΄, πΆ, 0) = πΆ) |
49 | 48 | mpteq2ia 5213 |
. . . . . 6
β’ (π₯ β π΄ β¦ if(π₯ β π΄, πΆ, 0)) = (π₯ β π΄ β¦ πΆ) |
50 | 1, 5, 8 | cbvmpt 5221 |
. . . . . 6
β’ (π₯ β π΄ β¦ if(π₯ β π΄, πΆ, 0)) = (π¦ β π΄ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) |
51 | 49, 50 | eqtr3i 2767 |
. . . . 5
β’ (π₯ β π΄ β¦ πΆ) = (π¦ β π΄ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) |
52 | 10 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β πΏ1) β
π΄ β π΅) |
53 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β πΏ1) β
(π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β
πΏ1) |
54 | 9, 53 | eqeltrrid 2843 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β πΏ1) β
(π¦ β π΅ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) β
πΏ1) |
55 | | iblmbf 25148 |
. . . . . . . . 9
β’ ((π¦ β π΅ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) β πΏ1 β
(π¦ β π΅ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) β MblFn) |
56 | 54, 55 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β πΏ1) β
(π¦ β π΅ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) β MblFn) |
57 | | 0cn 11154 |
. . . . . . . . . . . . 13
β’ 0 β
β |
58 | | ifcl 4536 |
. . . . . . . . . . . . 13
β’ ((πΆ β β β§ 0 β
β) β if(π₯ β
π΄, πΆ, 0) β β) |
59 | 22, 57, 58 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΅) β if(π₯ β π΄, πΆ, 0) β β) |
60 | 59 | fmpttd 7068 |
. . . . . . . . . . 11
β’ (π β (π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)):π΅βΆβ) |
61 | 9 | feq1i 6664 |
. . . . . . . . . . 11
β’ ((π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)):π΅βΆβ β (π¦ β π΅ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)):π΅βΆβ) |
62 | 60, 61 | sylib 217 |
. . . . . . . . . 10
β’ (π β (π¦ β π΅ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)):π΅βΆβ) |
63 | 62 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β πΏ1) β
(π¦ β π΅ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)):π΅βΆβ) |
64 | 63 | fvmptelcdm 7066 |
. . . . . . . 8
β’ (((π β§ (π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β πΏ1) β§
π¦ β π΅) β if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0) β β) |
65 | 56, 64 | mbfdm2 25017 |
. . . . . . 7
β’ ((π β§ (π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β πΏ1) β
π΅ β dom
vol) |
66 | | dfss4 4223 |
. . . . . . . . . 10
β’ (π΄ β π΅ β (π΅ β (π΅ β π΄)) = π΄) |
67 | 10, 66 | sylib 217 |
. . . . . . . . 9
β’ (π β (π΅ β (π΅ β π΄)) = π΄) |
68 | 67 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π΅ β dom vol) β (π΅ β (π΅ β π΄)) = π΄) |
69 | | id 22 |
. . . . . . . . 9
β’ (π΅ β dom vol β π΅ β dom
vol) |
70 | | difmbl 24923 |
. . . . . . . . 9
β’ ((π΅ β dom vol β§ (π΅ β π΄) β dom vol) β (π΅ β (π΅ β π΄)) β dom vol) |
71 | 69, 38, 70 | syl2anr 598 |
. . . . . . . 8
β’ ((π β§ π΅ β dom vol) β (π΅ β (π΅ β π΄)) β dom vol) |
72 | 68, 71 | eqeltrrd 2839 |
. . . . . . 7
β’ ((π β§ π΅ β dom vol) β π΄ β dom vol) |
73 | 65, 72 | syldan 592 |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β πΏ1) β
π΄ β dom
vol) |
74 | 52, 73, 64, 54 | iblss 25185 |
. . . . 5
β’ ((π β§ (π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β πΏ1) β
(π¦ β π΄ β¦ if(π¦ β π΄, β¦π¦ / π₯β¦πΆ, 0)) β
πΏ1) |
75 | 51, 74 | eqeltrid 2842 |
. . . 4
β’ ((π β§ (π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β πΏ1) β
(π₯ β π΄ β¦ πΆ) β
πΏ1) |
76 | 47, 75 | impbida 800 |
. . 3
β’ (π β ((π₯ β π΄ β¦ πΆ) β πΏ1 β (π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β
πΏ1)) |
77 | 67 | eleq2d 2824 |
. . . . . . 7
β’ (π β (π₯ β (π΅ β (π΅ β π΄)) β π₯ β π΄)) |
78 | 77 | biimpa 478 |
. . . . . 6
β’ ((π β§ π₯ β (π΅ β (π΅ β π΄))) β π₯ β π΄) |
79 | 78, 48 | syl 17 |
. . . . 5
β’ ((π β§ π₯ β (π΅ β (π΅ β π΄))) β if(π₯ β π΄, πΆ, 0) = πΆ) |
80 | 59, 22, 35, 36, 79 | itgeqa 25194 |
. . . 4
β’ (π β (((π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β πΏ1 β
(π₯ β π΅ β¦ πΆ) β πΏ1) β§
β«π΅if(π₯ β π΄, πΆ, 0) dπ₯ = β«π΅πΆ dπ₯)) |
81 | 80 | simpld 496 |
. . 3
β’ (π β ((π₯ β π΅ β¦ if(π₯ β π΄, πΆ, 0)) β πΏ1 β
(π₯ β π΅ β¦ πΆ) β
πΏ1)) |
82 | 76, 81 | bitrd 279 |
. 2
β’ (π β ((π₯ β π΄ β¦ πΆ) β πΏ1 β (π₯ β π΅ β¦ πΆ) β
πΏ1)) |
83 | | itgss2 25193 |
. . . 4
β’ (π΄ β π΅ β β«π΄πΆ dπ₯ = β«π΅if(π₯ β π΄, πΆ, 0) dπ₯) |
84 | 10, 83 | syl 17 |
. . 3
β’ (π β β«π΄πΆ dπ₯ = β«π΅if(π₯ β π΄, πΆ, 0) dπ₯) |
85 | 80 | simprd 497 |
. . 3
β’ (π β β«π΅if(π₯ β π΄, πΆ, 0) dπ₯ = β«π΅πΆ dπ₯) |
86 | 84, 85 | eqtrd 2777 |
. 2
β’ (π β β«π΄πΆ dπ₯ = β«π΅πΆ dπ₯) |
87 | 82, 86 | jca 513 |
1
β’ (π β (((π₯ β π΄ β¦ πΆ) β πΏ1 β (π₯ β π΅ β¦ πΆ) β πΏ1) β§
β«π΄πΆ dπ₯ = β«π΅πΆ dπ₯)) |