Step | Hyp | Ref
| Expression |
1 | | iftrue 4496 |
. . . . . . . 8
β’ (π¦ β π΄ β if(π¦ β π΄, (πΉβπ¦), 0) = (πΉβπ¦)) |
2 | 1 | mpteq2ia 5212 |
. . . . . . 7
β’ (π¦ β π΄ β¦ if(π¦ β π΄, (πΉβπ¦), 0)) = (π¦ β π΄ β¦ (πΉβπ¦)) |
3 | | mbfi1flim.2 |
. . . . . . . . 9
β’ (π β πΉ:π΄βΆβ) |
4 | 3 | feqmptd 6914 |
. . . . . . . 8
β’ (π β πΉ = (π¦ β π΄ β¦ (πΉβπ¦))) |
5 | | mbfi1flim.1 |
. . . . . . . 8
β’ (π β πΉ β MblFn) |
6 | 4, 5 | eqeltrrd 2835 |
. . . . . . 7
β’ (π β (π¦ β π΄ β¦ (πΉβπ¦)) β MblFn) |
7 | 2, 6 | eqeltrid 2838 |
. . . . . 6
β’ (π β (π¦ β π΄ β¦ if(π¦ β π΄, (πΉβπ¦), 0)) β MblFn) |
8 | | fvex 6859 |
. . . . . . . 8
β’ (πΉβπ¦) β V |
9 | | c0ex 11157 |
. . . . . . . 8
β’ 0 β
V |
10 | 8, 9 | ifex 4540 |
. . . . . . 7
β’ if(π¦ β π΄, (πΉβπ¦), 0) β V |
11 | 10 | a1i 11 |
. . . . . 6
β’ ((π β§ π¦ β π΄) β if(π¦ β π΄, (πΉβπ¦), 0) β V) |
12 | 7, 11 | mbfdm2 25024 |
. . . . 5
β’ (π β π΄ β dom vol) |
13 | | mblss 24918 |
. . . . 5
β’ (π΄ β dom vol β π΄ β
β) |
14 | 12, 13 | syl 17 |
. . . 4
β’ (π β π΄ β β) |
15 | | rembl 24927 |
. . . . 5
β’ β
β dom vol |
16 | 15 | a1i 11 |
. . . 4
β’ (π β β β dom
vol) |
17 | | eldifn 4091 |
. . . . . 6
β’ (π¦ β (β β π΄) β Β¬ π¦ β π΄) |
18 | 17 | adantl 483 |
. . . . 5
β’ ((π β§ π¦ β (β β π΄)) β Β¬ π¦ β π΄) |
19 | 18 | iffalsed 4501 |
. . . 4
β’ ((π β§ π¦ β (β β π΄)) β if(π¦ β π΄, (πΉβπ¦), 0) = 0) |
20 | 14, 16, 11, 19, 7 | mbfss 25033 |
. . 3
β’ (π β (π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0)) β MblFn) |
21 | 3 | ffvelcdmda 7039 |
. . . . . 6
β’ ((π β§ π¦ β π΄) β (πΉβπ¦) β β) |
22 | | 0red 11166 |
. . . . . 6
β’ ((π β§ Β¬ π¦ β π΄) β 0 β β) |
23 | 21, 22 | ifclda 4525 |
. . . . 5
β’ (π β if(π¦ β π΄, (πΉβπ¦), 0) β β) |
24 | 23 | adantr 482 |
. . . 4
β’ ((π β§ π¦ β β) β if(π¦ β π΄, (πΉβπ¦), 0) β β) |
25 | 24 | fmpttd 7067 |
. . 3
β’ (π β (π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦),
0)):ββΆβ) |
26 | 20, 25 | mbfi1flimlem 25110 |
. 2
β’ (π β βπ(π:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β ((π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0))βπ₯))) |
27 | | ssralv 4014 |
. . . . . 6
β’ (π΄ β β β
(βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β ((π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0))βπ₯) β βπ₯ β π΄ (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0))βπ₯))) |
28 | 14, 27 | syl 17 |
. . . . 5
β’ (π β (βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0))βπ₯) β βπ₯ β π΄ (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0))βπ₯))) |
29 | 14 | sselda 3948 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β π₯ β β) |
30 | | eleq1w 2817 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β (π¦ β π΄ β π₯ β π΄)) |
31 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π¦ = π₯ β (πΉβπ¦) = (πΉβπ₯)) |
32 | 30, 31 | ifbieq1d 4514 |
. . . . . . . . . 10
β’ (π¦ = π₯ β if(π¦ β π΄, (πΉβπ¦), 0) = if(π₯ β π΄, (πΉβπ₯), 0)) |
33 | | eqid 2733 |
. . . . . . . . . 10
β’ (π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0)) = (π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0)) |
34 | | fvex 6859 |
. . . . . . . . . . 11
β’ (πΉβπ₯) β V |
35 | 34, 9 | ifex 4540 |
. . . . . . . . . 10
β’ if(π₯ β π΄, (πΉβπ₯), 0) β V |
36 | 32, 33, 35 | fvmpt 6952 |
. . . . . . . . 9
β’ (π₯ β β β ((π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0))βπ₯) = if(π₯ β π΄, (πΉβπ₯), 0)) |
37 | 29, 36 | syl 17 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β ((π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0))βπ₯) = if(π₯ β π΄, (πΉβπ₯), 0)) |
38 | | iftrue 4496 |
. . . . . . . . 9
β’ (π₯ β π΄ β if(π₯ β π΄, (πΉβπ₯), 0) = (πΉβπ₯)) |
39 | 38 | adantl 483 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β if(π₯ β π΄, (πΉβπ₯), 0) = (πΉβπ₯)) |
40 | 37, 39 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β ((π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0))βπ₯) = (πΉβπ₯)) |
41 | 40 | breq2d 5121 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β ((π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0))βπ₯) β (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯))) |
42 | 41 | ralbidva 3169 |
. . . . 5
β’ (π β (βπ₯ β π΄ (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0))βπ₯) β βπ₯ β π΄ (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯))) |
43 | 28, 42 | sylibd 238 |
. . . 4
β’ (π β (βπ₯ β β (π β β β¦ ((πβπ)βπ₯)) β ((π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0))βπ₯) β βπ₯ β π΄ (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯))) |
44 | 43 | anim2d 613 |
. . 3
β’ (π β ((π:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β ((π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0))βπ₯)) β (π:ββΆdom β«1 β§
βπ₯ β π΄ (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)))) |
45 | 44 | eximdv 1921 |
. 2
β’ (π β (βπ(π:ββΆdom β«1 β§
βπ₯ β β
(π β β β¦
((πβπ)βπ₯)) β ((π¦ β β β¦ if(π¦ β π΄, (πΉβπ¦), 0))βπ₯)) β βπ(π:ββΆdom β«1 β§
βπ₯ β π΄ (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯)))) |
46 | 26, 45 | mpd 15 |
1
β’ (π β βπ(π:ββΆdom β«1 β§
βπ₯ β π΄ (π β β β¦ ((πβπ)βπ₯)) β (πΉβπ₯))) |