Step | Hyp | Ref
| Expression |
1 | | c0ex 11156 |
. . . . . . 7
β’ 0 β
V |
2 | 1 | fvconst2 7158 |
. . . . . 6
β’ (π₯ β π΄ β ((π΄ Γ {0})βπ₯) = 0) |
3 | 2 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β π΄) β ((π΄ Γ {0})βπ₯) = 0) |
4 | | simpr 486 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β π₯ β π΄) |
5 | | mbfpos.1 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β π΅ β β) |
6 | | eqid 2737 |
. . . . . . 7
β’ (π₯ β π΄ β¦ π΅) = (π₯ β π΄ β¦ π΅) |
7 | 6 | fvmpt2 6964 |
. . . . . 6
β’ ((π₯ β π΄ β§ π΅ β β) β ((π₯ β π΄ β¦ π΅)βπ₯) = π΅) |
8 | 4, 5, 7 | syl2anc 585 |
. . . . 5
β’ ((π β§ π₯ β π΄) β ((π₯ β π΄ β¦ π΅)βπ₯) = π΅) |
9 | 3, 8 | breq12d 5123 |
. . . 4
β’ ((π β§ π₯ β π΄) β (((π΄ Γ {0})βπ₯) β€ ((π₯ β π΄ β¦ π΅)βπ₯) β 0 β€ π΅)) |
10 | 9, 8, 3 | ifbieq12d 4519 |
. . 3
β’ ((π β§ π₯ β π΄) β if(((π΄ Γ {0})βπ₯) β€ ((π₯ β π΄ β¦ π΅)βπ₯), ((π₯ β π΄ β¦ π΅)βπ₯), ((π΄ Γ {0})βπ₯)) = if(0 β€ π΅, π΅, 0)) |
11 | 10 | mpteq2dva 5210 |
. 2
β’ (π β (π₯ β π΄ β¦ if(((π΄ Γ {0})βπ₯) β€ ((π₯ β π΄ β¦ π΅)βπ₯), ((π₯ β π΄ β¦ π΅)βπ₯), ((π΄ Γ {0})βπ₯))) = (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))) |
12 | | 0re 11164 |
. . . . 5
β’ 0 β
β |
13 | 12 | fconst6 6737 |
. . . 4
β’ (π΄ Γ {0}):π΄βΆβ |
14 | 13 | a1i 11 |
. . 3
β’ (π β (π΄ Γ {0}):π΄βΆβ) |
15 | | mbfpos.2 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ π΅) β MblFn) |
16 | 15, 5 | mbfdm2 25017 |
. . . 4
β’ (π β π΄ β dom vol) |
17 | | 0cnd 11155 |
. . . 4
β’ (π β 0 β
β) |
18 | | mbfconst 25013 |
. . . 4
β’ ((π΄ β dom vol β§ 0 β
β) β (π΄ Γ
{0}) β MblFn) |
19 | 16, 17, 18 | syl2anc 585 |
. . 3
β’ (π β (π΄ Γ {0}) β MblFn) |
20 | 5 | fmpttd 7068 |
. . 3
β’ (π β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
21 | | nfcv 2908 |
. . . 4
β’
β²π¦if(((π΄ Γ {0})βπ₯) β€ ((π₯ β π΄ β¦ π΅)βπ₯), ((π₯ β π΄ β¦ π΅)βπ₯), ((π΄ Γ {0})βπ₯)) |
22 | | nfcv 2908 |
. . . . . 6
β’
β²π₯((π΄ Γ {0})βπ¦) |
23 | | nfcv 2908 |
. . . . . 6
β’
β²π₯
β€ |
24 | | nffvmpt1 6858 |
. . . . . 6
β’
β²π₯((π₯ β π΄ β¦ π΅)βπ¦) |
25 | 22, 23, 24 | nfbr 5157 |
. . . . 5
β’
β²π₯((π΄ Γ {0})βπ¦) β€ ((π₯ β π΄ β¦ π΅)βπ¦) |
26 | 25, 24, 22 | nfif 4521 |
. . . 4
β’
β²π₯if(((π΄ Γ {0})βπ¦) β€ ((π₯ β π΄ β¦ π΅)βπ¦), ((π₯ β π΄ β¦ π΅)βπ¦), ((π΄ Γ {0})βπ¦)) |
27 | | fveq2 6847 |
. . . . . 6
β’ (π₯ = π¦ β ((π΄ Γ {0})βπ₯) = ((π΄ Γ {0})βπ¦)) |
28 | | fveq2 6847 |
. . . . . 6
β’ (π₯ = π¦ β ((π₯ β π΄ β¦ π΅)βπ₯) = ((π₯ β π΄ β¦ π΅)βπ¦)) |
29 | 27, 28 | breq12d 5123 |
. . . . 5
β’ (π₯ = π¦ β (((π΄ Γ {0})βπ₯) β€ ((π₯ β π΄ β¦ π΅)βπ₯) β ((π΄ Γ {0})βπ¦) β€ ((π₯ β π΄ β¦ π΅)βπ¦))) |
30 | 29, 28, 27 | ifbieq12d 4519 |
. . . 4
β’ (π₯ = π¦ β if(((π΄ Γ {0})βπ₯) β€ ((π₯ β π΄ β¦ π΅)βπ₯), ((π₯ β π΄ β¦ π΅)βπ₯), ((π΄ Γ {0})βπ₯)) = if(((π΄ Γ {0})βπ¦) β€ ((π₯ β π΄ β¦ π΅)βπ¦), ((π₯ β π΄ β¦ π΅)βπ¦), ((π΄ Γ {0})βπ¦))) |
31 | 21, 26, 30 | cbvmpt 5221 |
. . 3
β’ (π₯ β π΄ β¦ if(((π΄ Γ {0})βπ₯) β€ ((π₯ β π΄ β¦ π΅)βπ₯), ((π₯ β π΄ β¦ π΅)βπ₯), ((π΄ Γ {0})βπ₯))) = (π¦ β π΄ β¦ if(((π΄ Γ {0})βπ¦) β€ ((π₯ β π΄ β¦ π΅)βπ¦), ((π₯ β π΄ β¦ π΅)βπ¦), ((π΄ Γ {0})βπ¦))) |
32 | 14, 19, 20, 15, 31 | mbfmax 25029 |
. 2
β’ (π β (π₯ β π΄ β¦ if(((π΄ Γ {0})βπ₯) β€ ((π₯ β π΄ β¦ π΅)βπ₯), ((π₯ β π΄ β¦ π΅)βπ₯), ((π΄ Γ {0})βπ₯))) β MblFn) |
33 | 11, 32 | eqeltrrd 2839 |
1
β’ (π β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn) |