Step | Hyp | Ref
| Expression |
1 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π₯0 |
2 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π₯
β€ |
3 | | nffvmpt1 6858 |
. . . . . . . . 9
β’
β²π₯((π₯ β π΄ β¦ π΅)βπ¦) |
4 | 1, 2, 3 | nfbr 5157 |
. . . . . . . 8
β’
β²π₯0 β€
((π₯ β π΄ β¦ π΅)βπ¦) |
5 | 4, 3, 1 | nfif 4521 |
. . . . . . 7
β’
β²π₯if(0
β€ ((π₯ β π΄ β¦ π΅)βπ¦), ((π₯ β π΄ β¦ π΅)βπ¦), 0) |
6 | | nfcv 2908 |
. . . . . . 7
β’
β²π¦if(0
β€ ((π₯ β π΄ β¦ π΅)βπ₯), ((π₯ β π΄ β¦ π΅)βπ₯), 0) |
7 | | fveq2 6847 |
. . . . . . . . 9
β’ (π¦ = π₯ β ((π₯ β π΄ β¦ π΅)βπ¦) = ((π₯ β π΄ β¦ π΅)βπ₯)) |
8 | 7 | breq2d 5122 |
. . . . . . . 8
β’ (π¦ = π₯ β (0 β€ ((π₯ β π΄ β¦ π΅)βπ¦) β 0 β€ ((π₯ β π΄ β¦ π΅)βπ₯))) |
9 | 8, 7 | ifbieq1d 4515 |
. . . . . . 7
β’ (π¦ = π₯ β if(0 β€ ((π₯ β π΄ β¦ π΅)βπ¦), ((π₯ β π΄ β¦ π΅)βπ¦), 0) = if(0 β€ ((π₯ β π΄ β¦ π΅)βπ₯), ((π₯ β π΄ β¦ π΅)βπ₯), 0)) |
10 | 5, 6, 9 | cbvmpt 5221 |
. . . . . 6
β’ (π¦ β π΄ β¦ if(0 β€ ((π₯ β π΄ β¦ π΅)βπ¦), ((π₯ β π΄ β¦ π΅)βπ¦), 0)) = (π₯ β π΄ β¦ if(0 β€ ((π₯ β π΄ β¦ π΅)βπ₯), ((π₯ β π΄ β¦ π΅)βπ₯), 0)) |
11 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β π₯ β π΄) |
12 | | mbfpos.1 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π΄) β π΅ β β) |
13 | | eqid 2737 |
. . . . . . . . . . 11
β’ (π₯ β π΄ β¦ π΅) = (π₯ β π΄ β¦ π΅) |
14 | 13 | fvmpt2 6964 |
. . . . . . . . . 10
β’ ((π₯ β π΄ β§ π΅ β β) β ((π₯ β π΄ β¦ π΅)βπ₯) = π΅) |
15 | 11, 12, 14 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β ((π₯ β π΄ β¦ π΅)βπ₯) = π΅) |
16 | 15 | breq2d 5122 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (0 β€ ((π₯ β π΄ β¦ π΅)βπ₯) β 0 β€ π΅)) |
17 | 16, 15 | ifbieq1d 4515 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β if(0 β€ ((π₯ β π΄ β¦ π΅)βπ₯), ((π₯ β π΄ β¦ π΅)βπ₯), 0) = if(0 β€ π΅, π΅, 0)) |
18 | 17 | mpteq2dva 5210 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ if(0 β€ ((π₯ β π΄ β¦ π΅)βπ₯), ((π₯ β π΄ β¦ π΅)βπ₯), 0)) = (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))) |
19 | 10, 18 | eqtrid 2789 |
. . . . 5
β’ (π β (π¦ β π΄ β¦ if(0 β€ ((π₯ β π΄ β¦ π΅)βπ¦), ((π₯ β π΄ β¦ π΅)βπ¦), 0)) = (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))) |
20 | 19 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π¦ β π΄ β¦ if(0 β€ ((π₯ β π΄ β¦ π΅)βπ¦), ((π₯ β π΄ β¦ π΅)βπ¦), 0)) = (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))) |
21 | 12 | fmpttd 7068 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
22 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π₯ β π΄ β¦ π΅):π΄βΆβ) |
23 | 22 | ffvelcdmda 7040 |
. . . . 5
β’ (((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β§ π¦ β π΄) β ((π₯ β π΄ β¦ π΅)βπ¦) β β) |
24 | | nfcv 2908 |
. . . . . . . . 9
β’
β²π¦((π₯ β π΄ β¦ π΅)βπ₯) |
25 | 3, 24, 7 | cbvmpt 5221 |
. . . . . . . 8
β’ (π¦ β π΄ β¦ ((π₯ β π΄ β¦ π΅)βπ¦)) = (π₯ β π΄ β¦ ((π₯ β π΄ β¦ π΅)βπ₯)) |
26 | 15 | mpteq2dva 5210 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ ((π₯ β π΄ β¦ π΅)βπ₯)) = (π₯ β π΄ β¦ π΅)) |
27 | 25, 26 | eqtrid 2789 |
. . . . . . 7
β’ (π β (π¦ β π΄ β¦ ((π₯ β π΄ β¦ π΅)βπ¦)) = (π₯ β π΄ β¦ π΅)) |
28 | 27 | eleq1d 2823 |
. . . . . 6
β’ (π β ((π¦ β π΄ β¦ ((π₯ β π΄ β¦ π΅)βπ¦)) β MblFn β (π₯ β π΄ β¦ π΅) β MblFn)) |
29 | 28 | biimpar 479 |
. . . . 5
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π¦ β π΄ β¦ ((π₯ β π΄ β¦ π΅)βπ¦)) β MblFn) |
30 | 23, 29 | mbfpos 25031 |
. . . 4
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π¦ β π΄ β¦ if(0 β€ ((π₯ β π΄ β¦ π΅)βπ¦), ((π₯ β π΄ β¦ π΅)βπ¦), 0)) β MblFn) |
31 | 20, 30 | eqeltrrd 2839 |
. . 3
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn) |
32 | 3 | nfneg 11404 |
. . . . . . . . 9
β’
β²π₯-((π₯ β π΄ β¦ π΅)βπ¦) |
33 | 1, 2, 32 | nfbr 5157 |
. . . . . . . 8
β’
β²π₯0 β€
-((π₯ β π΄ β¦ π΅)βπ¦) |
34 | 33, 32, 1 | nfif 4521 |
. . . . . . 7
β’
β²π₯if(0
β€ -((π₯ β π΄ β¦ π΅)βπ¦), -((π₯ β π΄ β¦ π΅)βπ¦), 0) |
35 | | nfcv 2908 |
. . . . . . 7
β’
β²π¦if(0
β€ -((π₯ β π΄ β¦ π΅)βπ₯), -((π₯ β π΄ β¦ π΅)βπ₯), 0) |
36 | 7 | negeqd 11402 |
. . . . . . . . 9
β’ (π¦ = π₯ β -((π₯ β π΄ β¦ π΅)βπ¦) = -((π₯ β π΄ β¦ π΅)βπ₯)) |
37 | 36 | breq2d 5122 |
. . . . . . . 8
β’ (π¦ = π₯ β (0 β€ -((π₯ β π΄ β¦ π΅)βπ¦) β 0 β€ -((π₯ β π΄ β¦ π΅)βπ₯))) |
38 | 37, 36 | ifbieq1d 4515 |
. . . . . . 7
β’ (π¦ = π₯ β if(0 β€ -((π₯ β π΄ β¦ π΅)βπ¦), -((π₯ β π΄ β¦ π΅)βπ¦), 0) = if(0 β€ -((π₯ β π΄ β¦ π΅)βπ₯), -((π₯ β π΄ β¦ π΅)βπ₯), 0)) |
39 | 34, 35, 38 | cbvmpt 5221 |
. . . . . 6
β’ (π¦ β π΄ β¦ if(0 β€ -((π₯ β π΄ β¦ π΅)βπ¦), -((π₯ β π΄ β¦ π΅)βπ¦), 0)) = (π₯ β π΄ β¦ if(0 β€ -((π₯ β π΄ β¦ π΅)βπ₯), -((π₯ β π΄ β¦ π΅)βπ₯), 0)) |
40 | 15 | negeqd 11402 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β -((π₯ β π΄ β¦ π΅)βπ₯) = -π΅) |
41 | 40 | breq2d 5122 |
. . . . . . . 8
β’ ((π β§ π₯ β π΄) β (0 β€ -((π₯ β π΄ β¦ π΅)βπ₯) β 0 β€ -π΅)) |
42 | 41, 40 | ifbieq1d 4515 |
. . . . . . 7
β’ ((π β§ π₯ β π΄) β if(0 β€ -((π₯ β π΄ β¦ π΅)βπ₯), -((π₯ β π΄ β¦ π΅)βπ₯), 0) = if(0 β€ -π΅, -π΅, 0)) |
43 | 42 | mpteq2dva 5210 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ if(0 β€ -((π₯ β π΄ β¦ π΅)βπ₯), -((π₯ β π΄ β¦ π΅)βπ₯), 0)) = (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))) |
44 | 39, 43 | eqtrid 2789 |
. . . . 5
β’ (π β (π¦ β π΄ β¦ if(0 β€ -((π₯ β π΄ β¦ π΅)βπ¦), -((π₯ β π΄ β¦ π΅)βπ¦), 0)) = (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))) |
45 | 44 | adantr 482 |
. . . 4
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π¦ β π΄ β¦ if(0 β€ -((π₯ β π΄ β¦ π΅)βπ¦), -((π₯ β π΄ β¦ π΅)βπ¦), 0)) = (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))) |
46 | 23 | renegcld 11589 |
. . . . 5
β’ (((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β§ π¦ β π΄) β -((π₯ β π΄ β¦ π΅)βπ¦) β β) |
47 | 23, 29 | mbfneg 25030 |
. . . . 5
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π¦ β π΄ β¦ -((π₯ β π΄ β¦ π΅)βπ¦)) β MblFn) |
48 | 46, 47 | mbfpos 25031 |
. . . 4
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π¦ β π΄ β¦ if(0 β€ -((π₯ β π΄ β¦ π΅)βπ¦), -((π₯ β π΄ β¦ π΅)βπ¦), 0)) β MblFn) |
49 | 45, 48 | eqeltrrd 2839 |
. . 3
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn) |
50 | 31, 49 | jca 513 |
. 2
β’ ((π β§ (π₯ β π΄ β¦ π΅) β MblFn) β ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn)) |
51 | 27 | adantr 482 |
. . 3
β’ ((π β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn)) β (π¦ β π΄ β¦ ((π₯ β π΄ β¦ π΅)βπ¦)) = (π₯ β π΄ β¦ π΅)) |
52 | 21 | ffvelcdmda 7040 |
. . . . 5
β’ ((π β§ π¦ β π΄) β ((π₯ β π΄ β¦ π΅)βπ¦) β β) |
53 | 52 | adantlr 714 |
. . . 4
β’ (((π β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn)) β§ π¦ β π΄) β ((π₯ β π΄ β¦ π΅)βπ¦) β β) |
54 | 19 | adantr 482 |
. . . . 5
β’ ((π β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn)) β (π¦ β π΄ β¦ if(0 β€ ((π₯ β π΄ β¦ π΅)βπ¦), ((π₯ β π΄ β¦ π΅)βπ¦), 0)) = (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0))) |
55 | | simprl 770 |
. . . . 5
β’ ((π β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn)) β (π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn) |
56 | 54, 55 | eqeltrd 2838 |
. . . 4
β’ ((π β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn)) β (π¦ β π΄ β¦ if(0 β€ ((π₯ β π΄ β¦ π΅)βπ¦), ((π₯ β π΄ β¦ π΅)βπ¦), 0)) β MblFn) |
57 | 44 | adantr 482 |
. . . . 5
β’ ((π β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn)) β (π¦ β π΄ β¦ if(0 β€ -((π₯ β π΄ β¦ π΅)βπ¦), -((π₯ β π΄ β¦ π΅)βπ¦), 0)) = (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0))) |
58 | | simprr 772 |
. . . . 5
β’ ((π β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn)) β (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn) |
59 | 57, 58 | eqeltrd 2838 |
. . . 4
β’ ((π β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn)) β (π¦ β π΄ β¦ if(0 β€ -((π₯ β π΄ β¦ π΅)βπ¦), -((π₯ β π΄ β¦ π΅)βπ¦), 0)) β MblFn) |
60 | 53, 56, 59 | mbfposr 25032 |
. . 3
β’ ((π β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn)) β (π¦ β π΄ β¦ ((π₯ β π΄ β¦ π΅)βπ¦)) β MblFn) |
61 | 51, 60 | eqeltrrd 2839 |
. 2
β’ ((π β§ ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn)) β (π₯ β π΄ β¦ π΅) β MblFn) |
62 | 50, 61 | impbida 800 |
1
β’ (π β ((π₯ β π΄ β¦ π΅) β MblFn β ((π₯ β π΄ β¦ if(0 β€ π΅, π΅, 0)) β MblFn β§ (π₯ β π΄ β¦ if(0 β€ -π΅, -π΅, 0)) β MblFn))) |