Step | Hyp | Ref
| Expression |
1 | | mbfadd.1 |
. . . . 5
β’ (π β πΉ β MblFn) |
2 | | mbff 25005 |
. . . . 5
β’ (πΉ β MblFn β πΉ:dom πΉβΆβ) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β πΉ:dom πΉβΆβ) |
4 | 3 | ffnd 6674 |
. . 3
β’ (π β πΉ Fn dom πΉ) |
5 | | mbfadd.2 |
. . . . 5
β’ (π β πΊ β MblFn) |
6 | | mbff 25005 |
. . . . 5
β’ (πΊ β MblFn β πΊ:dom πΊβΆβ) |
7 | 5, 6 | syl 17 |
. . . 4
β’ (π β πΊ:dom πΊβΆβ) |
8 | 7 | ffnd 6674 |
. . 3
β’ (π β πΊ Fn dom πΊ) |
9 | | mbfdm 25006 |
. . . 4
β’ (πΉ β MblFn β dom πΉ β dom
vol) |
10 | 1, 9 | syl 17 |
. . 3
β’ (π β dom πΉ β dom vol) |
11 | | mbfdm 25006 |
. . . 4
β’ (πΊ β MblFn β dom πΊ β dom
vol) |
12 | 5, 11 | syl 17 |
. . 3
β’ (π β dom πΊ β dom vol) |
13 | | eqid 2737 |
. . 3
β’ (dom
πΉ β© dom πΊ) = (dom πΉ β© dom πΊ) |
14 | | eqidd 2738 |
. . 3
β’ ((π β§ π₯ β dom πΉ) β (πΉβπ₯) = (πΉβπ₯)) |
15 | | eqidd 2738 |
. . 3
β’ ((π β§ π₯ β dom πΊ) β (πΊβπ₯) = (πΊβπ₯)) |
16 | 4, 8, 10, 12, 13, 14, 15 | offval 7631 |
. 2
β’ (π β (πΉ βf + πΊ) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) + (πΊβπ₯)))) |
17 | | elinel1 4160 |
. . . . . . . 8
β’ (π₯ β (dom πΉ β© dom πΊ) β π₯ β dom πΉ) |
18 | | ffvelcdm 7037 |
. . . . . . . 8
β’ ((πΉ:dom πΉβΆβ β§ π₯ β dom πΉ) β (πΉβπ₯) β β) |
19 | 3, 17, 18 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (πΉβπ₯) β β) |
20 | | elinel2 4161 |
. . . . . . . 8
β’ (π₯ β (dom πΉ β© dom πΊ) β π₯ β dom πΊ) |
21 | | ffvelcdm 7037 |
. . . . . . . 8
β’ ((πΊ:dom πΊβΆβ β§ π₯ β dom πΊ) β (πΊβπ₯) β β) |
22 | 7, 20, 21 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (πΊβπ₯) β β) |
23 | 19, 22 | readdd 15106 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (ββ((πΉβπ₯) + (πΊβπ₯))) = ((ββ(πΉβπ₯)) + (ββ(πΊβπ₯)))) |
24 | 23 | mpteq2dva 5210 |
. . . . 5
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) + (πΊβπ₯)))) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((ββ(πΉβπ₯)) + (ββ(πΊβπ₯))))) |
25 | | inmbl 24922 |
. . . . . . 7
β’ ((dom
πΉ β dom vol β§ dom
πΊ β dom vol) β
(dom πΉ β© dom πΊ) β dom
vol) |
26 | 10, 12, 25 | syl2anc 585 |
. . . . . 6
β’ (π β (dom πΉ β© dom πΊ) β dom vol) |
27 | 19 | recld 15086 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (ββ(πΉβπ₯)) β β) |
28 | 22 | recld 15086 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (ββ(πΊβπ₯)) β β) |
29 | | eqidd 2738 |
. . . . . 6
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) = (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯)))) |
30 | | eqidd 2738 |
. . . . . 6
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) = (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) |
31 | 26, 27, 28, 29, 30 | offval2 7642 |
. . . . 5
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf + (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((ββ(πΉβπ₯)) + (ββ(πΊβπ₯))))) |
32 | 24, 31 | eqtr4d 2780 |
. . . 4
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) + (πΊβπ₯)))) = ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf + (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))))) |
33 | | inss1 4193 |
. . . . . . . . 9
β’ (dom
πΉ β© dom πΊ) β dom πΉ |
34 | | resmpt 5996 |
. . . . . . . . 9
β’ ((dom
πΉ β© dom πΊ) β dom πΉ β ((π₯ β dom πΉ β¦ (πΉβπ₯)) βΎ (dom πΉ β© dom πΊ)) = (π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯))) |
35 | 33, 34 | ax-mp 5 |
. . . . . . . 8
β’ ((π₯ β dom πΉ β¦ (πΉβπ₯)) βΎ (dom πΉ β© dom πΊ)) = (π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯)) |
36 | 3 | feqmptd 6915 |
. . . . . . . . . 10
β’ (π β πΉ = (π₯ β dom πΉ β¦ (πΉβπ₯))) |
37 | 36, 1 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (π β (π₯ β dom πΉ β¦ (πΉβπ₯)) β MblFn) |
38 | | mbfres 25024 |
. . . . . . . . 9
β’ (((π₯ β dom πΉ β¦ (πΉβπ₯)) β MblFn β§ (dom πΉ β© dom πΊ) β dom vol) β ((π₯ β dom πΉ β¦ (πΉβπ₯)) βΎ (dom πΉ β© dom πΊ)) β MblFn) |
39 | 37, 26, 38 | syl2anc 585 |
. . . . . . . 8
β’ (π β ((π₯ β dom πΉ β¦ (πΉβπ₯)) βΎ (dom πΉ β© dom πΊ)) β MblFn) |
40 | 35, 39 | eqeltrrid 2843 |
. . . . . . 7
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯)) β MblFn) |
41 | 19 | ismbfcn2 25018 |
. . . . . . 7
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯)) β MblFn β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) β MblFn β§ (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) β MblFn))) |
42 | 40, 41 | mpbid 231 |
. . . . . 6
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) β MblFn β§ (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) β MblFn)) |
43 | 42 | simpld 496 |
. . . . 5
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) β MblFn) |
44 | | inss2 4194 |
. . . . . . . . 9
β’ (dom
πΉ β© dom πΊ) β dom πΊ |
45 | | resmpt 5996 |
. . . . . . . . 9
β’ ((dom
πΉ β© dom πΊ) β dom πΊ β ((π₯ β dom πΊ β¦ (πΊβπ₯)) βΎ (dom πΉ β© dom πΊ)) = (π₯ β (dom πΉ β© dom πΊ) β¦ (πΊβπ₯))) |
46 | 44, 45 | ax-mp 5 |
. . . . . . . 8
β’ ((π₯ β dom πΊ β¦ (πΊβπ₯)) βΎ (dom πΉ β© dom πΊ)) = (π₯ β (dom πΉ β© dom πΊ) β¦ (πΊβπ₯)) |
47 | 7 | feqmptd 6915 |
. . . . . . . . . 10
β’ (π β πΊ = (π₯ β dom πΊ β¦ (πΊβπ₯))) |
48 | 47, 5 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (π β (π₯ β dom πΊ β¦ (πΊβπ₯)) β MblFn) |
49 | | mbfres 25024 |
. . . . . . . . 9
β’ (((π₯ β dom πΊ β¦ (πΊβπ₯)) β MblFn β§ (dom πΉ β© dom πΊ) β dom vol) β ((π₯ β dom πΊ β¦ (πΊβπ₯)) βΎ (dom πΉ β© dom πΊ)) β MblFn) |
50 | 48, 26, 49 | syl2anc 585 |
. . . . . . . 8
β’ (π β ((π₯ β dom πΊ β¦ (πΊβπ₯)) βΎ (dom πΉ β© dom πΊ)) β MblFn) |
51 | 46, 50 | eqeltrrid 2843 |
. . . . . . 7
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (πΊβπ₯)) β MblFn) |
52 | 22 | ismbfcn2 25018 |
. . . . . . 7
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (πΊβπ₯)) β MblFn β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) β MblFn β§ (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) β MblFn))) |
53 | 51, 52 | mpbid 231 |
. . . . . 6
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) β MblFn β§ (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) β MblFn)) |
54 | 53 | simpld 496 |
. . . . 5
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) β MblFn) |
55 | 27 | fmpttd 7068 |
. . . . 5
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))):(dom πΉ β© dom πΊ)βΆβ) |
56 | 28 | fmpttd 7068 |
. . . . 5
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))):(dom πΉ β© dom πΊ)βΆβ) |
57 | 43, 54, 55, 56 | mbfaddlem 25040 |
. . . 4
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf + (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) β MblFn) |
58 | 32, 57 | eqeltrd 2838 |
. . 3
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) + (πΊβπ₯)))) β MblFn) |
59 | 19, 22 | imaddd 15107 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (ββ((πΉβπ₯) + (πΊβπ₯))) = ((ββ(πΉβπ₯)) + (ββ(πΊβπ₯)))) |
60 | 59 | mpteq2dva 5210 |
. . . . 5
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) + (πΊβπ₯)))) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((ββ(πΉβπ₯)) + (ββ(πΊβπ₯))))) |
61 | 19 | imcld 15087 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (ββ(πΉβπ₯)) β β) |
62 | 22 | imcld 15087 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (ββ(πΊβπ₯)) β β) |
63 | | eqidd 2738 |
. . . . . 6
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) = (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯)))) |
64 | | eqidd 2738 |
. . . . . 6
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) = (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) |
65 | 26, 61, 62, 63, 64 | offval2 7642 |
. . . . 5
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf + (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((ββ(πΉβπ₯)) + (ββ(πΊβπ₯))))) |
66 | 60, 65 | eqtr4d 2780 |
. . . 4
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) + (πΊβπ₯)))) = ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf + (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))))) |
67 | 42 | simprd 497 |
. . . . 5
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) β MblFn) |
68 | 53 | simprd 497 |
. . . . 5
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) β MblFn) |
69 | 61 | fmpttd 7068 |
. . . . 5
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))):(dom πΉ β© dom πΊ)βΆβ) |
70 | 62 | fmpttd 7068 |
. . . . 5
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))):(dom πΉ β© dom πΊ)βΆβ) |
71 | 67, 68, 69, 70 | mbfaddlem 25040 |
. . . 4
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf + (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) β MblFn) |
72 | 66, 71 | eqeltrd 2838 |
. . 3
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) + (πΊβπ₯)))) β MblFn) |
73 | 19, 22 | addcld 11181 |
. . . 4
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β ((πΉβπ₯) + (πΊβπ₯)) β β) |
74 | 73 | ismbfcn2 25018 |
. . 3
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) + (πΊβπ₯))) β MblFn β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) + (πΊβπ₯)))) β MblFn β§ (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) + (πΊβπ₯)))) β MblFn))) |
75 | 58, 72, 74 | mpbir2and 712 |
. 2
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) + (πΊβπ₯))) β MblFn) |
76 | 16, 75 | eqeltrd 2838 |
1
β’ (π β (πΉ βf + πΊ) β MblFn) |