Step | Hyp | Ref
| Expression |
1 | | mbfmul.3 |
. . . 4
β’ (π β πΉ:π΄βΆβ) |
2 | 1 | ffnd 6673 |
. . 3
β’ (π β πΉ Fn π΄) |
3 | | mbfmul.4 |
. . . 4
β’ (π β πΊ:π΄βΆβ) |
4 | 3 | ffnd 6673 |
. . 3
β’ (π β πΊ Fn π΄) |
5 | 1 | fdmd 6683 |
. . . 4
β’ (π β dom πΉ = π΄) |
6 | | mbfmul.1 |
. . . . 5
β’ (π β πΉ β MblFn) |
7 | | mbfdm 25013 |
. . . . 5
β’ (πΉ β MblFn β dom πΉ β dom
vol) |
8 | 6, 7 | syl 17 |
. . . 4
β’ (π β dom πΉ β dom vol) |
9 | 5, 8 | eqeltrrd 2835 |
. . 3
β’ (π β π΄ β dom vol) |
10 | | inidm 4182 |
. . 3
β’ (π΄ β© π΄) = π΄ |
11 | | eqidd 2734 |
. . 3
β’ ((π β§ π₯ β π΄) β (πΉβπ₯) = (πΉβπ₯)) |
12 | | eqidd 2734 |
. . 3
β’ ((π β§ π₯ β π΄) β (πΊβπ₯) = (πΊβπ₯)) |
13 | 2, 4, 9, 9, 10, 11, 12 | offval 7630 |
. 2
β’ (π β (πΉ βf Β· πΊ) = (π₯ β π΄ β¦ ((πΉβπ₯) Β· (πΊβπ₯)))) |
14 | | nnuz 12814 |
. . 3
β’ β =
(β€β₯β1) |
15 | | 1zzd 12542 |
. . 3
β’ (π β 1 β
β€) |
16 | | 1zzd 12542 |
. . . 4
β’ ((π β§ π₯ β π΄) β 1 β β€) |
17 | | mbfmul.6 |
. . . 4
β’ ((π β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)) |
18 | | nnex 12167 |
. . . . . 6
β’ β
β V |
19 | 18 | mptex 7177 |
. . . . 5
β’ (π β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) β V |
20 | 19 | a1i 11 |
. . . 4
β’ ((π β§ π₯ β π΄) β (π β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) β V) |
21 | | mbfmul.8 |
. . . 4
β’ ((π β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)) β (πΊβπ₯)) |
22 | | mbfmul.5 |
. . . . . . . . . . 11
β’ (π β π:ββΆdom
β«1) |
23 | 22 | ffvelcdmda 7039 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβπ) β dom
β«1) |
24 | | i1ff 25063 |
. . . . . . . . . 10
β’ ((πβπ) β dom β«1 β (πβπ):ββΆβ) |
25 | 23, 24 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβπ):ββΆβ) |
26 | 25 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π β β) β (πβπ):ββΆβ) |
27 | | mblss 24918 |
. . . . . . . . . . 11
β’ (π΄ β dom vol β π΄ β
β) |
28 | 9, 27 | syl 17 |
. . . . . . . . . 10
β’ (π β π΄ β β) |
29 | 28 | sselda 3948 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β π₯ β β) |
30 | 29 | adantr 482 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π β β) β π₯ β β) |
31 | 26, 30 | ffvelcdmd 7040 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ π β β) β ((πβπ)βπ₯) β β) |
32 | 31 | recnd 11191 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ π β β) β ((πβπ)βπ₯) β β) |
33 | 32 | fmpttd 7067 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)):ββΆβ) |
34 | 33 | ffvelcdmda 7039 |
. . . 4
β’ (((π β§ π₯ β π΄) β§ π β β) β ((π β β β¦ ((πβπ)βπ₯))βπ) β β) |
35 | | mbfmul.7 |
. . . . . . . . . . 11
β’ (π β π:ββΆdom
β«1) |
36 | 35 | ffvelcdmda 7039 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πβπ) β dom
β«1) |
37 | | i1ff 25063 |
. . . . . . . . . 10
β’ ((πβπ) β dom β«1 β (πβπ):ββΆβ) |
38 | 36, 37 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πβπ):ββΆβ) |
39 | 38 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π₯ β π΄) β§ π β β) β (πβπ):ββΆβ) |
40 | 39, 30 | ffvelcdmd 7040 |
. . . . . . 7
β’ (((π β§ π₯ β π΄) β§ π β β) β ((πβπ)βπ₯) β β) |
41 | 40 | recnd 11191 |
. . . . . 6
β’ (((π β§ π₯ β π΄) β§ π β β) β ((πβπ)βπ₯) β β) |
42 | 41 | fmpttd 7067 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (π β β β¦ ((πβπ)βπ₯)):ββΆβ) |
43 | 42 | ffvelcdmda 7039 |
. . . 4
β’ (((π β§ π₯ β π΄) β§ π β β) β ((π β β β¦ ((πβπ)βπ₯))βπ) β β) |
44 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = π β (πβπ) = (πβπ)) |
45 | 44 | fveq1d 6848 |
. . . . . . . 8
β’ (π = π β ((πβπ)βπ₯) = ((πβπ)βπ₯)) |
46 | | fveq2 6846 |
. . . . . . . . 9
β’ (π = π β (πβπ) = (πβπ)) |
47 | 46 | fveq1d 6848 |
. . . . . . . 8
β’ (π = π β ((πβπ)βπ₯) = ((πβπ)βπ₯)) |
48 | 45, 47 | oveq12d 7379 |
. . . . . . 7
β’ (π = π β (((πβπ)βπ₯) Β· ((πβπ)βπ₯)) = (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) |
49 | | eqid 2733 |
. . . . . . 7
β’ (π β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) = (π β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) |
50 | | ovex 7394 |
. . . . . . 7
β’ (((πβπ)βπ₯) Β· ((πβπ)βπ₯)) β V |
51 | 48, 49, 50 | fvmpt 6952 |
. . . . . 6
β’ (π β β β ((π β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯)))βπ) = (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) |
52 | 51 | adantl 483 |
. . . . 5
β’ (((π β§ π₯ β π΄) β§ π β β) β ((π β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯)))βπ) = (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) |
53 | | eqid 2733 |
. . . . . . . 8
β’ (π β β β¦ ((πβπ)βπ₯)) = (π β β β¦ ((πβπ)βπ₯)) |
54 | | fvex 6859 |
. . . . . . . 8
β’ ((πβπ)βπ₯) β V |
55 | 45, 53, 54 | fvmpt 6952 |
. . . . . . 7
β’ (π β β β ((π β β β¦ ((πβπ)βπ₯))βπ) = ((πβπ)βπ₯)) |
56 | | eqid 2733 |
. . . . . . . 8
β’ (π β β β¦ ((πβπ)βπ₯)) = (π β β β¦ ((πβπ)βπ₯)) |
57 | | fvex 6859 |
. . . . . . . 8
β’ ((πβπ)βπ₯) β V |
58 | 47, 56, 57 | fvmpt 6952 |
. . . . . . 7
β’ (π β β β ((π β β β¦ ((πβπ)βπ₯))βπ) = ((πβπ)βπ₯)) |
59 | 55, 58 | oveq12d 7379 |
. . . . . 6
β’ (π β β β (((π β β β¦ ((πβπ)βπ₯))βπ) Β· ((π β β β¦ ((πβπ)βπ₯))βπ)) = (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) |
60 | 59 | adantl 483 |
. . . . 5
β’ (((π β§ π₯ β π΄) β§ π β β) β (((π β β β¦ ((πβπ)βπ₯))βπ) Β· ((π β β β¦ ((πβπ)βπ₯))βπ)) = (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) |
61 | 52, 60 | eqtr4d 2776 |
. . . 4
β’ (((π β§ π₯ β π΄) β§ π β β) β ((π β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯)))βπ) = (((π β β β¦ ((πβπ)βπ₯))βπ) Β· ((π β β β¦ ((πβπ)βπ₯))βπ))) |
62 | 14, 16, 17, 20, 21, 34, 43, 61 | climmul 15524 |
. . 3
β’ ((π β§ π₯ β π΄) β (π β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) β ((πΉβπ₯) Β· (πΊβπ₯))) |
63 | 28 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β π΄ β β) |
64 | 63 | resmptd 5998 |
. . . 4
β’ ((π β§ π β β) β ((π₯ β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) βΎ π΄) = (π₯ β π΄ β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯)))) |
65 | 25 | ffnd 6673 |
. . . . . . 7
β’ ((π β§ π β β) β (πβπ) Fn β) |
66 | 38 | ffnd 6673 |
. . . . . . 7
β’ ((π β§ π β β) β (πβπ) Fn β) |
67 | | reex 11150 |
. . . . . . . 8
β’ β
β V |
68 | 67 | a1i 11 |
. . . . . . 7
β’ ((π β§ π β β) β β β
V) |
69 | | inidm 4182 |
. . . . . . 7
β’ (β
β© β) = β |
70 | | eqidd 2734 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β β) β ((πβπ)βπ₯) = ((πβπ)βπ₯)) |
71 | | eqidd 2734 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β β) β ((πβπ)βπ₯) = ((πβπ)βπ₯)) |
72 | 65, 66, 68, 68, 69, 70, 71 | offval 7630 |
. . . . . 6
β’ ((π β§ π β β) β ((πβπ) βf Β· (πβπ)) = (π₯ β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯)))) |
73 | 23, 36 | i1fmul 25083 |
. . . . . . 7
β’ ((π β§ π β β) β ((πβπ) βf Β· (πβπ)) β dom
β«1) |
74 | | i1fmbf 25062 |
. . . . . . 7
β’ (((πβπ) βf Β· (πβπ)) β dom β«1 β
((πβπ) βf Β·
(πβπ)) β MblFn) |
75 | 73, 74 | syl 17 |
. . . . . 6
β’ ((π β§ π β β) β ((πβπ) βf Β· (πβπ)) β MblFn) |
76 | 72, 75 | eqeltrrd 2835 |
. . . . 5
β’ ((π β§ π β β) β (π₯ β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) β MblFn) |
77 | 9 | adantr 482 |
. . . . 5
β’ ((π β§ π β β) β π΄ β dom vol) |
78 | | mbfres 25031 |
. . . . 5
β’ (((π₯ β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) β MblFn β§ π΄ β dom vol) β ((π₯ β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) βΎ π΄) β MblFn) |
79 | 76, 77, 78 | syl2anc 585 |
. . . 4
β’ ((π β§ π β β) β ((π₯ β β β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) βΎ π΄) β MblFn) |
80 | 64, 79 | eqeltrrd 2835 |
. . 3
β’ ((π β§ π β β) β (π₯ β π΄ β¦ (((πβπ)βπ₯) Β· ((πβπ)βπ₯))) β MblFn) |
81 | | ovex 7394 |
. . . 4
β’ (((πβπ)βπ₯) Β· ((πβπ)βπ₯)) β V |
82 | 81 | a1i 11 |
. . 3
β’ ((π β§ (π β β β§ π₯ β π΄)) β (((πβπ)βπ₯) Β· ((πβπ)βπ₯)) β V) |
83 | 14, 15, 62, 80, 82 | mbflim 25055 |
. 2
β’ (π β (π₯ β π΄ β¦ ((πΉβπ₯) Β· (πΊβπ₯))) β MblFn) |
84 | 13, 83 | eqeltrd 2834 |
1
β’ (π β (πΉ βf Β· πΊ) β MblFn) |