Step | Hyp | Ref
| Expression |
1 | | iblabsnclem.1 |
. . 3
β’ πΊ = (π₯ β β β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) |
2 | | iblabsnclem.2 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ (πΉβπ΅)) β
πΏ1) |
3 | | iblabsnclem.3 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (πΉβπ΅) β β) |
4 | 3 | iblrelem 25158 |
. . . . . . . 8
β’ (π β ((π₯ β π΄ β¦ (πΉβπ΅)) β πΏ1 β
((π₯ β π΄ β¦ (πΉβπ΅)) β MblFn β§
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0))) β β β§
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))) β β))) |
5 | 2, 4 | mpbid 231 |
. . . . . . 7
β’ (π β ((π₯ β π΄ β¦ (πΉβπ΅)) β MblFn β§
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0))) β β β§
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))) β β)) |
6 | 5 | simp1d 1143 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (πΉβπ΅)) β MblFn) |
7 | 6, 3 | mbfdm2 25004 |
. . . . 5
β’ (π β π΄ β dom vol) |
8 | | mblss 24898 |
. . . . 5
β’ (π΄ β dom vol β π΄ β
β) |
9 | 7, 8 | syl 17 |
. . . 4
β’ (π β π΄ β β) |
10 | | rembl 24907 |
. . . . 5
β’ β
β dom vol |
11 | 10 | a1i 11 |
. . . 4
β’ (π β β β dom
vol) |
12 | 3 | recnd 11184 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (πΉβπ΅) β β) |
13 | 12 | abscld 15322 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (absβ(πΉβπ΅)) β β) |
14 | | 0re 11158 |
. . . . 5
β’ 0 β
β |
15 | | ifcl 4532 |
. . . . 5
β’
(((absβ(πΉβπ΅)) β β β§ 0 β β)
β if(π₯ β π΄, (absβ(πΉβπ΅)), 0) β β) |
16 | 13, 14, 15 | sylancl 587 |
. . . 4
β’ ((π β§ π₯ β π΄) β if(π₯ β π΄, (absβ(πΉβπ΅)), 0) β β) |
17 | | eldifn 4088 |
. . . . . 6
β’ (π₯ β (β β π΄) β Β¬ π₯ β π΄) |
18 | 17 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β (β β π΄)) β Β¬ π₯ β π΄) |
19 | | iffalse 4496 |
. . . . 5
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, (absβ(πΉβπ΅)), 0) = 0) |
20 | 18, 19 | syl 17 |
. . . 4
β’ ((π β§ π₯ β (β β π΄)) β if(π₯ β π΄, (absβ(πΉβπ΅)), 0) = 0) |
21 | | iftrue 4493 |
. . . . . 6
β’ (π₯ β π΄ β if(π₯ β π΄, (absβ(πΉβπ΅)), 0) = (absβ(πΉβπ΅))) |
22 | 21 | mpteq2ia 5209 |
. . . . 5
β’ (π₯ β π΄ β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) = (π₯ β π΄ β¦ (absβ(πΉβπ΅))) |
23 | 13 | fmpttd 7064 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (absβ(πΉβπ΅))):π΄βΆβ) |
24 | 13 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (absβ(πΉβπ΅)) β β) |
25 | 24 | biantrurd 534 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (π¦ < (absβ(πΉβπ΅)) β ((absβ(πΉβπ΅)) β β β§ π¦ < (absβ(πΉβπ΅))))) |
26 | 3 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (πΉβπ΅) β β) |
27 | | simplr 768 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β π¦ β β) |
28 | 26, 27 | absled 15316 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((absβ(πΉβπ΅)) β€ π¦ β (-π¦ β€ (πΉβπ΅) β§ (πΉβπ΅) β€ π¦))) |
29 | 28 | notbid 318 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (Β¬ (absβ(πΉβπ΅)) β€ π¦ β Β¬ (-π¦ β€ (πΉβπ΅) β§ (πΉβπ΅) β€ π¦))) |
30 | 27, 24 | ltnled 11303 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (π¦ < (absβ(πΉβπ΅)) β Β¬ (absβ(πΉβπ΅)) β€ π¦)) |
31 | | renegcl 11465 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β β β -π¦ β
β) |
32 | 31 | rexrd 11206 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β -π¦ β
β*) |
33 | 32 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β -π¦ β β*) |
34 | | elioomnf 13362 |
. . . . . . . . . . . . . . 15
β’ (-π¦ β β*
β ((πΉβπ΅) β (-β(,)-π¦) β ((πΉβπ΅) β β β§ (πΉβπ΅) < -π¦))) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((πΉβπ΅) β (-β(,)-π¦) β ((πΉβπ΅) β β β§ (πΉβπ΅) < -π¦))) |
36 | 26 | biantrurd 534 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((πΉβπ΅) < -π¦ β ((πΉβπ΅) β β β§ (πΉβπ΅) < -π¦))) |
37 | 27 | renegcld 11583 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β -π¦ β β) |
38 | 26, 37 | ltnled 11303 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((πΉβπ΅) < -π¦ β Β¬ -π¦ β€ (πΉβπ΅))) |
39 | 35, 36, 38 | 3bitr2d 307 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((πΉβπ΅) β (-β(,)-π¦) β Β¬ -π¦ β€ (πΉβπ΅))) |
40 | | rexr 11202 |
. . . . . . . . . . . . . . . 16
β’ (π¦ β β β π¦ β
β*) |
41 | 40 | ad2antlr 726 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β π¦ β β*) |
42 | | elioopnf 13361 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β*
β ((πΉβπ΅) β (π¦(,)+β) β ((πΉβπ΅) β β β§ π¦ < (πΉβπ΅)))) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((πΉβπ΅) β (π¦(,)+β) β ((πΉβπ΅) β β β§ π¦ < (πΉβπ΅)))) |
44 | 26 | biantrurd 534 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (π¦ < (πΉβπ΅) β ((πΉβπ΅) β β β§ π¦ < (πΉβπ΅)))) |
45 | 27, 26 | ltnled 11303 |
. . . . . . . . . . . . . 14
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (π¦ < (πΉβπ΅) β Β¬ (πΉβπ΅) β€ π¦)) |
46 | 43, 44, 45 | 3bitr2d 307 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((πΉβπ΅) β (π¦(,)+β) β Β¬ (πΉβπ΅) β€ π¦)) |
47 | 39, 46 | orbi12d 918 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (((πΉβπ΅) β (-β(,)-π¦) β¨ (πΉβπ΅) β (π¦(,)+β)) β (Β¬ -π¦ β€ (πΉβπ΅) β¨ Β¬ (πΉβπ΅) β€ π¦))) |
48 | | ianor 981 |
. . . . . . . . . . . 12
β’ (Β¬
(-π¦ β€ (πΉβπ΅) β§ (πΉβπ΅) β€ π¦) β (Β¬ -π¦ β€ (πΉβπ΅) β¨ Β¬ (πΉβπ΅) β€ π¦)) |
49 | 47, 48 | bitr4di 289 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (((πΉβπ΅) β (-β(,)-π¦) β¨ (πΉβπ΅) β (π¦(,)+β)) β Β¬ (-π¦ β€ (πΉβπ΅) β§ (πΉβπ΅) β€ π¦))) |
50 | 29, 30, 49 | 3bitr4rd 312 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β (((πΉβπ΅) β (-β(,)-π¦) β¨ (πΉβπ΅) β (π¦(,)+β)) β π¦ < (absβ(πΉβπ΅)))) |
51 | | elioopnf 13361 |
. . . . . . . . . . 11
β’ (π¦ β β*
β ((absβ(πΉβπ΅)) β (π¦(,)+β) β ((absβ(πΉβπ΅)) β β β§ π¦ < (absβ(πΉβπ΅))))) |
52 | 41, 51 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((absβ(πΉβπ΅)) β (π¦(,)+β) β ((absβ(πΉβπ΅)) β β β§ π¦ < (absβ(πΉβπ΅))))) |
53 | 25, 50, 52 | 3bitr4rd 312 |
. . . . . . . . 9
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((absβ(πΉβπ΅)) β (π¦(,)+β) β ((πΉβπ΅) β (-β(,)-π¦) β¨ (πΉβπ΅) β (π¦(,)+β)))) |
54 | 53 | rabbidva 3415 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β {π₯ β π΄ β£ (absβ(πΉβπ΅)) β (π¦(,)+β)} = {π₯ β π΄ β£ ((πΉβπ΅) β (-β(,)-π¦) β¨ (πΉβπ΅) β (π¦(,)+β))}) |
55 | | eqid 2737 |
. . . . . . . . 9
β’ (π₯ β π΄ β¦ (absβ(πΉβπ΅))) = (π₯ β π΄ β¦ (absβ(πΉβπ΅))) |
56 | 55 | mptpreima 6191 |
. . . . . . . 8
β’ (β‘(π₯ β π΄ β¦ (absβ(πΉβπ΅))) β (π¦(,)+β)) = {π₯ β π΄ β£ (absβ(πΉβπ΅)) β (π¦(,)+β)} |
57 | | eqid 2737 |
. . . . . . . . . . 11
β’ (π₯ β π΄ β¦ (πΉβπ΅)) = (π₯ β π΄ β¦ (πΉβπ΅)) |
58 | 57 | mptpreima 6191 |
. . . . . . . . . 10
β’ (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-β(,)-π¦)) = {π₯ β π΄ β£ (πΉβπ΅) β (-β(,)-π¦)} |
59 | 57 | mptpreima 6191 |
. . . . . . . . . 10
β’ (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (π¦(,)+β)) = {π₯ β π΄ β£ (πΉβπ΅) β (π¦(,)+β)} |
60 | 58, 59 | uneq12i 4122 |
. . . . . . . . 9
β’ ((β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-β(,)-π¦)) βͺ (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (π¦(,)+β))) = ({π₯ β π΄ β£ (πΉβπ΅) β (-β(,)-π¦)} βͺ {π₯ β π΄ β£ (πΉβπ΅) β (π¦(,)+β)}) |
61 | | unrab 4266 |
. . . . . . . . 9
β’ ({π₯ β π΄ β£ (πΉβπ΅) β (-β(,)-π¦)} βͺ {π₯ β π΄ β£ (πΉβπ΅) β (π¦(,)+β)}) = {π₯ β π΄ β£ ((πΉβπ΅) β (-β(,)-π¦) β¨ (πΉβπ΅) β (π¦(,)+β))} |
62 | 60, 61 | eqtri 2765 |
. . . . . . . 8
β’ ((β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-β(,)-π¦)) βͺ (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (π¦(,)+β))) = {π₯ β π΄ β£ ((πΉβπ΅) β (-β(,)-π¦) β¨ (πΉβπ΅) β (π¦(,)+β))} |
63 | 54, 56, 62 | 3eqtr4g 2802 |
. . . . . . 7
β’ ((π β§ π¦ β β) β (β‘(π₯ β π΄ β¦ (absβ(πΉβπ΅))) β (π¦(,)+β)) = ((β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-β(,)-π¦)) βͺ (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (π¦(,)+β)))) |
64 | | iblmbf 25135 |
. . . . . . . . . 10
β’ ((π₯ β π΄ β¦ (πΉβπ΅)) β πΏ1 β
(π₯ β π΄ β¦ (πΉβπ΅)) β MblFn) |
65 | 2, 64 | syl 17 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ (πΉβπ΅)) β MblFn) |
66 | 3 | fmpttd 7064 |
. . . . . . . . 9
β’ (π β (π₯ β π΄ β¦ (πΉβπ΅)):π΄βΆβ) |
67 | | mbfima 24997 |
. . . . . . . . . 10
β’ (((π₯ β π΄ β¦ (πΉβπ΅)) β MblFn β§ (π₯ β π΄ β¦ (πΉβπ΅)):π΄βΆβ) β (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-β(,)-π¦)) β dom vol) |
68 | | mbfima 24997 |
. . . . . . . . . 10
β’ (((π₯ β π΄ β¦ (πΉβπ΅)) β MblFn β§ (π₯ β π΄ β¦ (πΉβπ΅)):π΄βΆβ) β (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (π¦(,)+β)) β dom
vol) |
69 | | unmbl 24904 |
. . . . . . . . . 10
β’ (((β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-β(,)-π¦)) β dom vol β§ (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (π¦(,)+β)) β dom vol) β ((β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-β(,)-π¦)) βͺ (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (π¦(,)+β))) β dom
vol) |
70 | 67, 68, 69 | syl2anc 585 |
. . . . . . . . 9
β’ (((π₯ β π΄ β¦ (πΉβπ΅)) β MblFn β§ (π₯ β π΄ β¦ (πΉβπ΅)):π΄βΆβ) β ((β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-β(,)-π¦)) βͺ (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (π¦(,)+β))) β dom
vol) |
71 | 65, 66, 70 | syl2anc 585 |
. . . . . . . 8
β’ (π β ((β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-β(,)-π¦)) βͺ (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (π¦(,)+β))) β dom
vol) |
72 | 71 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β β) β ((β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-β(,)-π¦)) βͺ (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (π¦(,)+β))) β dom
vol) |
73 | 63, 72 | eqeltrd 2838 |
. . . . . 6
β’ ((π β§ π¦ β β) β (β‘(π₯ β π΄ β¦ (absβ(πΉβπ΅))) β (π¦(,)+β)) β dom
vol) |
74 | | elioomnf 13362 |
. . . . . . . . . . . . . 14
β’ (π¦ β β*
β ((absβ(πΉβπ΅)) β (-β(,)π¦) β ((absβ(πΉβπ΅)) β β β§ (absβ(πΉβπ΅)) < π¦))) |
75 | 41, 74 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((absβ(πΉβπ΅)) β (-β(,)π¦) β ((absβ(πΉβπ΅)) β β β§ (absβ(πΉβπ΅)) < π¦))) |
76 | 24 | biantrurd 534 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((absβ(πΉβπ΅)) < π¦ β ((absβ(πΉβπ΅)) β β β§ (absβ(πΉβπ΅)) < π¦))) |
77 | 26, 27 | absltd 15315 |
. . . . . . . . . . . . 13
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((absβ(πΉβπ΅)) < π¦ β (-π¦ < (πΉβπ΅) β§ (πΉβπ΅) < π¦))) |
78 | 75, 76, 77 | 3bitr2d 307 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((absβ(πΉβπ΅)) β (-β(,)π¦) β (-π¦ < (πΉβπ΅) β§ (πΉβπ΅) < π¦))) |
79 | 26 | biantrurd 534 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((-π¦ < (πΉβπ΅) β§ (πΉβπ΅) < π¦) β ((πΉβπ΅) β β β§ (-π¦ < (πΉβπ΅) β§ (πΉβπ΅) < π¦)))) |
80 | 78, 79 | bitrd 279 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((absβ(πΉβπ΅)) β (-β(,)π¦) β ((πΉβπ΅) β β β§ (-π¦ < (πΉβπ΅) β§ (πΉβπ΅) < π¦)))) |
81 | | 3anass 1096 |
. . . . . . . . . . 11
β’ (((πΉβπ΅) β β β§ -π¦ < (πΉβπ΅) β§ (πΉβπ΅) < π¦) β ((πΉβπ΅) β β β§ (-π¦ < (πΉβπ΅) β§ (πΉβπ΅) < π¦))) |
82 | 80, 81 | bitr4di 289 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((absβ(πΉβπ΅)) β (-β(,)π¦) β ((πΉβπ΅) β β β§ -π¦ < (πΉβπ΅) β§ (πΉβπ΅) < π¦))) |
83 | | elioo2 13306 |
. . . . . . . . . . . 12
β’ ((-π¦ β β*
β§ π¦ β
β*) β ((πΉβπ΅) β (-π¦(,)π¦) β ((πΉβπ΅) β β β§ -π¦ < (πΉβπ΅) β§ (πΉβπ΅) < π¦))) |
84 | 32, 40, 83 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π¦ β β β ((πΉβπ΅) β (-π¦(,)π¦) β ((πΉβπ΅) β β β§ -π¦ < (πΉβπ΅) β§ (πΉβπ΅) < π¦))) |
85 | 84 | ad2antlr 726 |
. . . . . . . . . 10
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((πΉβπ΅) β (-π¦(,)π¦) β ((πΉβπ΅) β β β§ -π¦ < (πΉβπ΅) β§ (πΉβπ΅) < π¦))) |
86 | 82, 85 | bitr4d 282 |
. . . . . . . . 9
β’ (((π β§ π¦ β β) β§ π₯ β π΄) β ((absβ(πΉβπ΅)) β (-β(,)π¦) β (πΉβπ΅) β (-π¦(,)π¦))) |
87 | 86 | rabbidva 3415 |
. . . . . . . 8
β’ ((π β§ π¦ β β) β {π₯ β π΄ β£ (absβ(πΉβπ΅)) β (-β(,)π¦)} = {π₯ β π΄ β£ (πΉβπ΅) β (-π¦(,)π¦)}) |
88 | 55 | mptpreima 6191 |
. . . . . . . 8
β’ (β‘(π₯ β π΄ β¦ (absβ(πΉβπ΅))) β (-β(,)π¦)) = {π₯ β π΄ β£ (absβ(πΉβπ΅)) β (-β(,)π¦)} |
89 | 57 | mptpreima 6191 |
. . . . . . . 8
β’ (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-π¦(,)π¦)) = {π₯ β π΄ β£ (πΉβπ΅) β (-π¦(,)π¦)} |
90 | 87, 88, 89 | 3eqtr4g 2802 |
. . . . . . 7
β’ ((π β§ π¦ β β) β (β‘(π₯ β π΄ β¦ (absβ(πΉβπ΅))) β (-β(,)π¦)) = (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-π¦(,)π¦))) |
91 | | mbfima 24997 |
. . . . . . . . 9
β’ (((π₯ β π΄ β¦ (πΉβπ΅)) β MblFn β§ (π₯ β π΄ β¦ (πΉβπ΅)):π΄βΆβ) β (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-π¦(,)π¦)) β dom vol) |
92 | 65, 66, 91 | syl2anc 585 |
. . . . . . . 8
β’ (π β (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-π¦(,)π¦)) β dom vol) |
93 | 92 | adantr 482 |
. . . . . . 7
β’ ((π β§ π¦ β β) β (β‘(π₯ β π΄ β¦ (πΉβπ΅)) β (-π¦(,)π¦)) β dom vol) |
94 | 90, 93 | eqeltrd 2838 |
. . . . . 6
β’ ((π β§ π¦ β β) β (β‘(π₯ β π΄ β¦ (absβ(πΉβπ΅))) β (-β(,)π¦)) β dom vol) |
95 | 23, 7, 73, 94 | ismbf2d 25007 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ (absβ(πΉβπ΅))) β MblFn) |
96 | 22, 95 | eqeltrid 2842 |
. . . 4
β’ (π β (π₯ β π΄ β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) β MblFn) |
97 | 9, 11, 16, 20, 96 | mbfss 25013 |
. . 3
β’ (π β (π₯ β β β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) β MblFn) |
98 | 1, 97 | eqeltrid 2842 |
. 2
β’ (π β πΊ β MblFn) |
99 | | reex 11143 |
. . . . . . . . 9
β’ β
β V |
100 | 99 | a1i 11 |
. . . . . . . 8
β’ (π β β β
V) |
101 | | ifan 4540 |
. . . . . . . . . 10
β’ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) = if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) |
102 | | ifcl 4532 |
. . . . . . . . . . . . 13
β’ (((πΉβπ΅) β β β§ 0 β β)
β if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) β β) |
103 | 3, 14, 102 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) β β) |
104 | | max1 13105 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ (πΉβπ΅) β β) β 0 β€ if(0 β€
(πΉβπ΅), (πΉβπ΅), 0)) |
105 | 14, 3, 104 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β 0 β€ if(0 β€ (πΉβπ΅), (πΉβπ΅), 0)) |
106 | | elrege0 13372 |
. . . . . . . . . . . 12
β’ (if(0
β€ (πΉβπ΅), (πΉβπ΅), 0) β (0[,)+β) β (if(0
β€ (πΉβπ΅), (πΉβπ΅), 0) β β β§ 0 β€ if(0 β€
(πΉβπ΅), (πΉβπ΅), 0))) |
107 | 103, 105,
106 | sylanbrc 584 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) β
(0[,)+β)) |
108 | | 0e0icopnf 13376 |
. . . . . . . . . . . 12
β’ 0 β
(0[,)+β) |
109 | 108 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ π₯ β π΄) β 0 β
(0[,)+β)) |
110 | 107, 109 | ifclda 4522 |
. . . . . . . . . 10
β’ (π β if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) β
(0[,)+β)) |
111 | 101, 110 | eqeltrid 2842 |
. . . . . . . . 9
β’ (π β if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) β
(0[,)+β)) |
112 | 111 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) β
(0[,)+β)) |
113 | | ifan 4540 |
. . . . . . . . . 10
β’ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0) = if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0) |
114 | 3 | renegcld 11583 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β -(πΉβπ΅) β β) |
115 | | ifcl 4532 |
. . . . . . . . . . . . 13
β’ ((-(πΉβπ΅) β β β§ 0 β β)
β if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0) β β) |
116 | 114, 14, 115 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0) β β) |
117 | | max1 13105 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ -(πΉβπ΅) β β) β 0 β€ if(0 β€
-(πΉβπ΅), -(πΉβπ΅), 0)) |
118 | 14, 114, 117 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β 0 β€ if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0)) |
119 | | elrege0 13372 |
. . . . . . . . . . . 12
β’ (if(0
β€ -(πΉβπ΅), -(πΉβπ΅), 0) β (0[,)+β) β (if(0
β€ -(πΉβπ΅), -(πΉβπ΅), 0) β β β§ 0 β€ if(0 β€
-(πΉβπ΅), -(πΉβπ΅), 0))) |
120 | 116, 118,
119 | sylanbrc 584 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0) β
(0[,)+β)) |
121 | 120, 109 | ifclda 4522 |
. . . . . . . . . 10
β’ (π β if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0) β
(0[,)+β)) |
122 | 113, 121 | eqeltrid 2842 |
. . . . . . . . 9
β’ (π β if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0) β
(0[,)+β)) |
123 | 122 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0) β
(0[,)+β)) |
124 | | eqidd 2738 |
. . . . . . . 8
β’ (π β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0))) |
125 | | eqidd 2738 |
. . . . . . . 8
β’ (π β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)) = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))) |
126 | 100, 112,
123, 124, 125 | offval2 7638 |
. . . . . . 7
β’ (π β ((π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) βf + (π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))) = (π₯ β β β¦ (if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) + if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)))) |
127 | 101, 113 | oveq12i 7370 |
. . . . . . . . 9
β’
(if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) + if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)) = (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) |
128 | | max0add 15196 |
. . . . . . . . . . . . 13
β’ ((πΉβπ΅) β β β (if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) + if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0)) = (absβ(πΉβπ΅))) |
129 | 3, 128 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) + if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0)) = (absβ(πΉβπ΅))) |
130 | | iftrue 4493 |
. . . . . . . . . . . . . 14
β’ (π₯ β π΄ β if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) = if(0 β€ (πΉβπ΅), (πΉβπ΅), 0)) |
131 | 130 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) = if(0 β€ (πΉβπ΅), (πΉβπ΅), 0)) |
132 | | iftrue 4493 |
. . . . . . . . . . . . . 14
β’ (π₯ β π΄ β if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0) = if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0)) |
133 | 132 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0) = if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0)) |
134 | 131, 133 | oveq12d 7376 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) = (if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) + if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0))) |
135 | 21 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β if(π₯ β π΄, (absβ(πΉβπ΅)), 0) = (absβ(πΉβπ΅))) |
136 | 129, 134,
135 | 3eqtr4d 2787 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) = if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) |
137 | 136 | ex 414 |
. . . . . . . . . 10
β’ (π β (π₯ β π΄ β (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) = if(π₯ β π΄, (absβ(πΉβπ΅)), 0))) |
138 | | 00id 11331 |
. . . . . . . . . . 11
β’ (0 + 0) =
0 |
139 | | iffalse 4496 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) = 0) |
140 | | iffalse 4496 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0) = 0) |
141 | 139, 140 | oveq12d 7376 |
. . . . . . . . . . 11
β’ (Β¬
π₯ β π΄ β (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) = (0 + 0)) |
142 | 138, 141,
19 | 3eqtr4a 2803 |
. . . . . . . . . 10
β’ (Β¬
π₯ β π΄ β (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) = if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) |
143 | 137, 142 | pm2.61d1 180 |
. . . . . . . . 9
β’ (π β (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) = if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) |
144 | 127, 143 | eqtrid 2789 |
. . . . . . . 8
β’ (π β (if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) + if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)) = if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) |
145 | 144 | mpteq2dv 5208 |
. . . . . . 7
β’ (π β (π₯ β β β¦ (if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) + if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))) = (π₯ β β β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0))) |
146 | 126, 145 | eqtrd 2777 |
. . . . . 6
β’ (π β ((π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) βf + (π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))) = (π₯ β β β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0))) |
147 | 1, 146 | eqtr4id 2796 |
. . . . 5
β’ (π β πΊ = ((π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) βf + (π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)))) |
148 | 147 | fveq2d 6847 |
. . . 4
β’ (π β
(β«2βπΊ)
= (β«2β((π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) βf + (π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))))) |
149 | 111 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) β
(0[,)+β)) |
150 | 101, 139 | eqtrid 2789 |
. . . . . . 7
β’ (Β¬
π₯ β π΄ β if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) = 0) |
151 | 18, 150 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β (β β π΄)) β if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) = 0) |
152 | | ibar 530 |
. . . . . . . . 9
β’ (π₯ β π΄ β (0 β€ (πΉβπ΅) β (π₯ β π΄ β§ 0 β€ (πΉβπ΅)))) |
153 | 152 | ifbid 4510 |
. . . . . . . 8
β’ (π₯ β π΄ β if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) = if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) |
154 | 153 | mpteq2ia 5209 |
. . . . . . 7
β’ (π₯ β π΄ β¦ if(0 β€ (πΉβπ΅), (πΉβπ΅), 0)) = (π₯ β π΄ β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) |
155 | 3, 6 | mbfpos 25018 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ if(0 β€ (πΉβπ΅), (πΉβπ΅), 0)) β MblFn) |
156 | 154, 155 | eqeltrrid 2843 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) β MblFn) |
157 | 9, 11, 149, 151, 156 | mbfss 25013 |
. . . . 5
β’ (π β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) β MblFn) |
158 | 112 | fmpttd 7064 |
. . . . 5
β’ (π β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅),
0)):ββΆ(0[,)+β)) |
159 | 5 | simp2d 1144 |
. . . . 5
β’ (π β
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0))) β β) |
160 | 123 | fmpttd 7064 |
. . . . 5
β’ (π β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅),
0)):ββΆ(0[,)+β)) |
161 | 5 | simp3d 1145 |
. . . . 5
β’ (π β
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))) β β) |
162 | 157, 158,
159, 160, 161 | itg2addnc 36135 |
. . . 4
β’ (π β
(β«2β((π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) βf + (π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)))) = ((β«2β(π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0))) + (β«2β(π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))))) |
163 | 148, 162 | eqtrd 2777 |
. . 3
β’ (π β
(β«2βπΊ)
= ((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0))) + (β«2β(π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))))) |
164 | 159, 161 | readdcld 11185 |
. . 3
β’ (π β
((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0))) + (β«2β(π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)))) β β) |
165 | 163, 164 | eqeltrd 2838 |
. 2
β’ (π β
(β«2βπΊ)
β β) |
166 | 98, 165 | jca 513 |
1
β’ (π β (πΊ β MblFn β§
(β«2βπΊ)
β β)) |