Step | Hyp | Ref
| Expression |
1 | | mbfmul.1 |
. . . . 5
β’ (π β πΉ β MblFn) |
2 | | mbff 25005 |
. . . . 5
β’ (πΉ β MblFn β πΉ:dom πΉβΆβ) |
3 | 1, 2 | syl 17 |
. . . 4
β’ (π β πΉ:dom πΉβΆβ) |
4 | 3 | ffnd 6670 |
. . 3
β’ (π β πΉ Fn dom πΉ) |
5 | | mbfmul.2 |
. . . . 5
β’ (π β πΊ β MblFn) |
6 | | mbff 25005 |
. . . . 5
β’ (πΊ β MblFn β πΊ:dom πΊβΆβ) |
7 | 5, 6 | syl 17 |
. . . 4
β’ (π β πΊ:dom πΊβΆβ) |
8 | 7 | ffnd 6670 |
. . 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 2733 |
. . 3
β’ (dom
πΉ β© dom πΊ) = (dom πΉ β© dom πΊ) |
14 | | eqidd 2734 |
. . 3
β’ ((π β§ π₯ β dom πΉ) β (πΉβπ₯) = (πΉβπ₯)) |
15 | | eqidd 2734 |
. . 3
β’ ((π β§ π₯ β dom πΊ) β (πΊβπ₯) = (πΊβπ₯)) |
16 | 4, 8, 10, 12, 13, 14, 15 | offval 7627 |
. 2
β’ (π β (πΉ βf Β· πΊ) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) Β· (πΊβπ₯)))) |
17 | | elinel1 4156 |
. . . . . . . 8
β’ (π₯ β (dom πΉ β© dom πΊ) β π₯ β dom πΉ) |
18 | | ffvelcdm 7033 |
. . . . . . . 8
β’ ((πΉ:dom πΉβΆβ β§ π₯ β dom πΉ) β (πΉβπ₯) β β) |
19 | 3, 17, 18 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (πΉβπ₯) β β) |
20 | | elinel2 4157 |
. . . . . . . 8
β’ (π₯ β (dom πΉ β© dom πΊ) β π₯ β dom πΊ) |
21 | | ffvelcdm 7033 |
. . . . . . . 8
β’ ((πΊ:dom πΊβΆβ β§ π₯ β dom πΊ) β (πΊβπ₯) β β) |
22 | 7, 20, 21 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (πΊβπ₯) β β) |
23 | 19, 22 | remuld 15109 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (ββ((πΉβπ₯) Β· (πΊβπ₯))) = (((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))) β ((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))))) |
24 | 23 | mpteq2dva 5206 |
. . . . 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 | | ovexd 7393 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β ((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))) β V) |
28 | | ovexd 7393 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β ((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))) β V) |
29 | 19 | recld 15085 |
. . . . . . 7
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (ββ(πΉβπ₯)) β β) |
30 | 22 | recld 15085 |
. . . . . . 7
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (ββ(πΊβπ₯)) β β) |
31 | | eqidd 2734 |
. . . . . . 7
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) = (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯)))) |
32 | | eqidd 2734 |
. . . . . . 7
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) = (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) |
33 | 26, 29, 30, 31, 32 | offval2 7638 |
. . . . . 6
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))))) |
34 | 19 | imcld 15086 |
. . . . . . 7
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (ββ(πΉβπ₯)) β β) |
35 | 22 | imcld 15086 |
. . . . . . 7
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (ββ(πΊβπ₯)) β β) |
36 | | eqidd 2734 |
. . . . . . 7
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) = (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯)))) |
37 | | eqidd 2734 |
. . . . . . 7
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) = (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) |
38 | 26, 34, 35, 36, 37 | offval2 7638 |
. . . . . 6
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))))) |
39 | 26, 27, 28, 33, 38 | offval2 7638 |
. . . . 5
β’ (π β (((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) βf β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))))) = (π₯ β (dom πΉ β© dom πΊ) β¦ (((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))) β ((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯)))))) |
40 | 24, 39 | eqtr4d 2776 |
. . . 4
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) Β· (πΊβπ₯)))) = (((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) βf β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))))) |
41 | | inss1 4189 |
. . . . . . . . . 10
β’ (dom
πΉ β© dom πΊ) β dom πΉ |
42 | | resmpt 5992 |
. . . . . . . . . 10
β’ ((dom
πΉ β© dom πΊ) β dom πΉ β ((π₯ β dom πΉ β¦ (πΉβπ₯)) βΎ (dom πΉ β© dom πΊ)) = (π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯))) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . 9
β’ ((π₯ β dom πΉ β¦ (πΉβπ₯)) βΎ (dom πΉ β© dom πΊ)) = (π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯)) |
44 | 3 | feqmptd 6911 |
. . . . . . . . . . 11
β’ (π β πΉ = (π₯ β dom πΉ β¦ (πΉβπ₯))) |
45 | 44, 1 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ (π β (π₯ β dom πΉ β¦ (πΉβπ₯)) β MblFn) |
46 | | mbfres 25024 |
. . . . . . . . . 10
β’ (((π₯ β dom πΉ β¦ (πΉβπ₯)) β MblFn β§ (dom πΉ β© dom πΊ) β dom vol) β ((π₯ β dom πΉ β¦ (πΉβπ₯)) βΎ (dom πΉ β© dom πΊ)) β MblFn) |
47 | 45, 26, 46 | syl2anc 585 |
. . . . . . . . 9
β’ (π β ((π₯ β dom πΉ β¦ (πΉβπ₯)) βΎ (dom πΉ β© dom πΊ)) β MblFn) |
48 | 43, 47 | eqeltrrid 2839 |
. . . . . . . 8
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯)) β MblFn) |
49 | 19 | ismbfcn2 25018 |
. . . . . . . 8
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (πΉβπ₯)) β MblFn β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) β MblFn β§ (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) β MblFn))) |
50 | 48, 49 | mpbid 231 |
. . . . . . 7
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) β MblFn β§ (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) β MblFn)) |
51 | 50 | simpld 496 |
. . . . . 6
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) β MblFn) |
52 | | inss2 4190 |
. . . . . . . . . 10
β’ (dom
πΉ β© dom πΊ) β dom πΊ |
53 | | resmpt 5992 |
. . . . . . . . . 10
β’ ((dom
πΉ β© dom πΊ) β dom πΊ β ((π₯ β dom πΊ β¦ (πΊβπ₯)) βΎ (dom πΉ β© dom πΊ)) = (π₯ β (dom πΉ β© dom πΊ) β¦ (πΊβπ₯))) |
54 | 52, 53 | ax-mp 5 |
. . . . . . . . 9
β’ ((π₯ β dom πΊ β¦ (πΊβπ₯)) βΎ (dom πΉ β© dom πΊ)) = (π₯ β (dom πΉ β© dom πΊ) β¦ (πΊβπ₯)) |
55 | 7 | feqmptd 6911 |
. . . . . . . . . . 11
β’ (π β πΊ = (π₯ β dom πΊ β¦ (πΊβπ₯))) |
56 | 55, 5 | eqeltrrd 2835 |
. . . . . . . . . 10
β’ (π β (π₯ β dom πΊ β¦ (πΊβπ₯)) β MblFn) |
57 | | mbfres 25024 |
. . . . . . . . . 10
β’ (((π₯ β dom πΊ β¦ (πΊβπ₯)) β MblFn β§ (dom πΉ β© dom πΊ) β dom vol) β ((π₯ β dom πΊ β¦ (πΊβπ₯)) βΎ (dom πΉ β© dom πΊ)) β MblFn) |
58 | 56, 26, 57 | syl2anc 585 |
. . . . . . . . 9
β’ (π β ((π₯ β dom πΊ β¦ (πΊβπ₯)) βΎ (dom πΉ β© dom πΊ)) β MblFn) |
59 | 54, 58 | eqeltrrid 2839 |
. . . . . . . 8
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (πΊβπ₯)) β MblFn) |
60 | 22 | ismbfcn2 25018 |
. . . . . . . 8
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (πΊβπ₯)) β MblFn β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) β MblFn β§ (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) β MblFn))) |
61 | 59, 60 | mpbid 231 |
. . . . . . 7
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) β MblFn β§ (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) β MblFn)) |
62 | 61 | simpld 496 |
. . . . . 6
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) β MblFn) |
63 | 29 | fmpttd 7064 |
. . . . . 6
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))):(dom πΉ β© dom πΊ)βΆβ) |
64 | 30 | fmpttd 7064 |
. . . . . 6
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))):(dom πΉ β© dom πΊ)βΆβ) |
65 | 51, 62, 63, 64 | mbfmullem 25106 |
. . . . 5
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) β MblFn) |
66 | 50 | simprd 497 |
. . . . . 6
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) β MblFn) |
67 | 61 | simprd 497 |
. . . . . 6
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))) β MblFn) |
68 | 34 | fmpttd 7064 |
. . . . . 6
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))):(dom πΉ β© dom πΊ)βΆβ) |
69 | 35 | fmpttd 7064 |
. . . . . 6
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))):(dom πΉ β© dom πΊ)βΆβ) |
70 | 66, 67, 68, 69 | mbfmullem 25106 |
. . . . 5
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) β MblFn) |
71 | 65, 70 | mbfsub 25042 |
. . . 4
β’ (π β (((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) βf β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))))) β MblFn) |
72 | 40, 71 | eqeltrd 2834 |
. . 3
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) Β· (πΊβπ₯)))) β MblFn) |
73 | 19, 22 | immuld 15110 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β (ββ((πΉβπ₯) Β· (πΊβπ₯))) = (((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))) + ((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))))) |
74 | 73 | mpteq2dva 5206 |
. . . . 5
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) Β· (πΊβπ₯)))) = (π₯ β (dom πΉ β© dom πΊ) β¦ (((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))) + ((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯)))))) |
75 | | ovexd 7393 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β ((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))) β V) |
76 | | ovexd 7393 |
. . . . . 6
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β ((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))) β V) |
77 | 26, 29, 35, 31, 37 | offval2 7638 |
. . . . . 6
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))))) |
78 | 26, 34, 30, 36, 32 | offval2 7638 |
. . . . . 6
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) = (π₯ β (dom πΉ β© dom πΊ) β¦ ((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))))) |
79 | 26, 75, 76, 77, 78 | offval2 7638 |
. . . . 5
β’ (π β (((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) βf + ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))))) = (π₯ β (dom πΉ β© dom πΊ) β¦ (((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯))) + ((ββ(πΉβπ₯)) Β· (ββ(πΊβπ₯)))))) |
80 | 74, 79 | eqtr4d 2776 |
. . . 4
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) Β· (πΊβπ₯)))) = (((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) βf + ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))))) |
81 | 51, 67, 63, 69 | mbfmullem 25106 |
. . . . 5
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) β MblFn) |
82 | 66, 62, 68, 64 | mbfmullem 25106 |
. . . . 5
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) β MblFn) |
83 | 81, 82 | mbfadd 25041 |
. . . 4
β’ (π β (((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯)))) βf + ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΉβπ₯))) βf Β· (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ(πΊβπ₯))))) β MblFn) |
84 | 80, 83 | eqeltrd 2834 |
. . 3
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) Β· (πΊβπ₯)))) β MblFn) |
85 | 19, 22 | mulcld 11180 |
. . . 4
β’ ((π β§ π₯ β (dom πΉ β© dom πΊ)) β ((πΉβπ₯) Β· (πΊβπ₯)) β β) |
86 | 85 | ismbfcn2 25018 |
. . 3
β’ (π β ((π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) Β· (πΊβπ₯))) β MblFn β ((π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) Β· (πΊβπ₯)))) β MblFn β§ (π₯ β (dom πΉ β© dom πΊ) β¦ (ββ((πΉβπ₯) Β· (πΊβπ₯)))) β MblFn))) |
87 | 72, 84, 86 | mpbir2and 712 |
. 2
β’ (π β (π₯ β (dom πΉ β© dom πΊ) β¦ ((πΉβπ₯) Β· (πΊβπ₯))) β MblFn) |
88 | 16, 87 | eqeltrd 2834 |
1
β’ (π β (πΉ βf Β· πΊ) β MblFn) |