Step | Hyp | Ref
| Expression |
1 | | mbfadd.1 |
. . . . . . . 8
β’ (π β πΉ β MblFn) |
2 | | mbff 25005 |
. . . . . . . 8
β’ (πΉ β MblFn β πΉ:dom πΉβΆβ) |
3 | 1, 2 | syl 17 |
. . . . . . 7
β’ (π β πΉ:dom πΉβΆβ) |
4 | | elinel1 4160 |
. . . . . . 7
β’ (π₯ β (dom πΉ β© dom πΊ) β π₯ β dom πΉ) |
5 | | ffvelcdm 7037 |
. . . . . . 7
β’ ((πΉ:dom πΉβΆβ β§ π₯ β dom πΉ) β (πΉβπ₯) β β) |
6 | 3, 4, 5 | syl2an 597 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (πΉβπ₯) β β) |
7 | | mbfadd.2 |
. . . . . . . 8
β’ (π β πΊ β MblFn) |
8 | | mbff 25005 |
. . . . . . . 8
β’ (πΊ β MblFn β πΊ:dom πΊβΆβ) |
9 | 7, 8 | syl 17 |
. . . . . . 7
β’ (π β πΊ:dom πΊβΆβ) |
10 | | elinel2 4161 |
. . . . . . 7
β’ (π₯ β (dom πΉ β© dom πΊ) β π₯ β dom πΊ) |
11 | | ffvelcdm 7037 |
. . . . . . 7
β’ ((πΊ:dom πΊβΆβ β§ π₯ β dom πΊ) β (πΊβπ₯) β β) |
12 | 9, 10, 11 | syl2an 597 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (πΊβπ₯) β β) |
13 | 6, 12 | negsubd 11525 |
. . . . 5
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β ((πΉβπ₯) + -(πΊβπ₯)) = ((πΉβπ₯) β (πΊβπ₯))) |
14 | 13 | eqcomd 2743 |
. . . 4
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β ((πΉβπ₯) β (πΊβπ₯)) = ((πΉβπ₯) + -(πΊβπ₯))) |
15 | 14 | mpteq2dva 5210 |
. . 3
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) β (πΊβπ₯))) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) + -(πΊβπ₯)))) |
16 | 3 | ffnd 6674 |
. . . 4
β’ (π β πΉ Fn dom πΉ) |
17 | 9 | ffnd 6674 |
. . . 4
β’ (π β πΊ Fn dom πΊ) |
18 | | mbfdm 25006 |
. . . . 5
β’ (πΉ β MblFn β dom πΉ β dom
vol) |
19 | 1, 18 | syl 17 |
. . . 4
β’ (π β dom πΉ β dom vol) |
20 | | mbfdm 25006 |
. . . . 5
β’ (πΊ β MblFn β dom πΊ β dom
vol) |
21 | 7, 20 | syl 17 |
. . . 4
β’ (π β dom πΊ β dom vol) |
22 | | eqid 2737 |
. . . 4
β’ (dom
πΉ β© dom πΊ) = (dom πΉ β© dom πΊ) |
23 | | eqidd 2738 |
. . . 4
β’ ((π β§ π₯ β dom πΉ) β (πΉβπ₯) = (πΉβπ₯)) |
24 | | eqidd 2738 |
. . . 4
β’ ((π β§ π₯ β dom πΊ) β (πΊβπ₯) = (πΊβπ₯)) |
25 | 16, 17, 19, 21, 22, 23, 24 | offval 7631 |
. . 3
β’ (π β (πΉ βf β πΊ) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) β (πΊβπ₯)))) |
26 | | inmbl 24922 |
. . . . 5
β’ ((dom
πΉ β dom vol β§ dom
πΊ β dom vol) β
(dom πΉ β© dom πΊ) β dom
vol) |
27 | 19, 21, 26 | syl2anc 585 |
. . . 4
β’ (π β (dom πΉ β© dom πΊ) β dom vol) |
28 | 12 | negcld 11506 |
. . . 4
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β -(πΊβπ₯) β β) |
29 | | eqidd 2738 |
. . . 4
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯)) = (π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯))) |
30 | | eqidd 2738 |
. . . 4
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ -(πΊβπ₯)) = (π₯ β (dom πΉ β© dom πΊ) β¦ -(πΊβπ₯))) |
31 | 27, 6, 28, 29, 30 | offval2 7642 |
. . 3
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯)) βf + (π₯ β (dom πΉ β© dom πΊ) β¦ -(πΊβπ₯))) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) + -(πΊβπ₯)))) |
32 | 15, 25, 31 | 3eqtr4d 2787 |
. 2
β’ (π β (πΉ βf β πΊ) = ((π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯)) βf + (π₯ β (dom πΉ β© dom πΊ) β¦ -(πΊβπ₯)))) |
33 | | inss1 4193 |
. . . . 5
β’ (dom
πΉ β© dom πΊ) β dom πΉ |
34 | | resmpt 5996 |
. . . . 5
β’ ((dom
πΉ β© dom πΊ) β dom πΉ β ((π₯ β dom πΉ β¦ (πΉβπ₯)) βΎ (dom πΉ β© dom πΊ)) = (π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯))) |
35 | 33, 34 | mp1i 13 |
. . . 4
β’ (π β ((π₯ β dom πΉ β¦ (πΉβπ₯)) βΎ (dom πΉ β© dom πΊ)) = (π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯))) |
36 | 3 | feqmptd 6915 |
. . . . . 6
β’ (π β πΉ = (π₯ β dom πΉ β¦ (πΉβπ₯))) |
37 | 36, 1 | eqeltrrd 2839 |
. . . . 5
β’ (π β (π₯ β dom πΉ β¦ (πΉβπ₯)) β MblFn) |
38 | | mbfres 25024 |
. . . . 5
β’ (((π₯ β dom πΉ β¦ (πΉβπ₯)) β MblFn β§ (dom πΉ β© dom πΊ) β dom vol) β ((π₯ β dom πΉ β¦ (πΉβπ₯)) βΎ (dom πΉ β© dom πΊ)) β MblFn) |
39 | 37, 27, 38 | syl2anc 585 |
. . . 4
β’ (π β ((π₯ β dom πΉ β¦ (πΉβπ₯)) βΎ (dom πΉ β© dom πΊ)) β MblFn) |
40 | 35, 39 | eqeltrrd 2839 |
. . 3
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯)) β MblFn) |
41 | | inss2 4194 |
. . . . . 6
β’ (dom
πΉ β© dom πΊ) β dom πΊ |
42 | | resmpt 5996 |
. . . . . 6
β’ ((dom
πΉ β© dom πΊ) β dom πΊ β ((π₯ β dom πΊ β¦ (πΊβπ₯)) βΎ (dom πΉ β© dom πΊ)) = (π₯ β (dom πΉ β© dom πΊ) β¦ (πΊβπ₯))) |
43 | 41, 42 | mp1i 13 |
. . . . 5
β’ (π β ((π₯ β dom πΊ β¦ (πΊβπ₯)) βΎ (dom πΉ β© dom πΊ)) = (π₯ β (dom πΉ β© dom πΊ) β¦ (πΊβπ₯))) |
44 | 9 | feqmptd 6915 |
. . . . . . 7
β’ (π β πΊ = (π₯ β dom πΊ β¦ (πΊβπ₯))) |
45 | 44, 7 | eqeltrrd 2839 |
. . . . . 6
β’ (π β (π₯ β dom πΊ β¦ (πΊβπ₯)) β MblFn) |
46 | | mbfres 25024 |
. . . . . 6
β’ (((π₯ β dom πΊ β¦ (πΊβπ₯)) β MblFn β§ (dom πΉ β© dom πΊ) β dom vol) β ((π₯ β dom πΊ β¦ (πΊβπ₯)) βΎ (dom πΉ β© dom πΊ)) β MblFn) |
47 | 45, 27, 46 | syl2anc 585 |
. . . . 5
β’ (π β ((π₯ β dom πΊ β¦ (πΊβπ₯)) βΎ (dom πΉ β© dom πΊ)) β MblFn) |
48 | 43, 47 | eqeltrrd 2839 |
. . . 4
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (πΊβπ₯)) β MblFn) |
49 | 12, 48 | mbfneg 25030 |
. . 3
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ -(πΊβπ₯)) β MblFn) |
50 | 40, 49 | mbfadd 25041 |
. 2
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯)) βf + (π₯ β (dom πΉ β© dom πΊ) β¦ -(πΊβπ₯))) β MblFn) |
51 | 32, 50 | eqeltrd 2838 |
1
β’ (π β (πΉ βf β πΊ) β MblFn) |