Step | Hyp | Ref
| Expression |
1 | | iblabs.3 |
. . 3
β’ πΊ = (π₯ β β β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) |
2 | | iblabs.4 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ (πΉβπ΅)) β
πΏ1) |
3 | | iblabs.5 |
. . . . . . . . 9
β’ ((π β§ π₯ β π΄) β (πΉβπ΅) β β) |
4 | 3 | iblrelem 25171 |
. . . . . . . 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 25017 |
. . . . 5
β’ (π β π΄ β dom vol) |
8 | | mblss 24911 |
. . . . 5
β’ (π΄ β dom vol β π΄ β
β) |
9 | 7, 8 | syl 17 |
. . . 4
β’ (π β π΄ β β) |
10 | | rembl 24920 |
. . . . 5
β’ β
β dom vol |
11 | 10 | a1i 11 |
. . . 4
β’ (π β β β dom
vol) |
12 | | iftrue 4497 |
. . . . . 6
β’ (π₯ β π΄ β if(π₯ β π΄, (absβ(πΉβπ΅)), 0) = (absβ(πΉβπ΅))) |
13 | 12 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β π΄) β if(π₯ β π΄, (absβ(πΉβπ΅)), 0) = (absβ(πΉβπ΅))) |
14 | 3 | recnd 11190 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β (πΉβπ΅) β β) |
15 | 14 | abscld 15328 |
. . . . 5
β’ ((π β§ π₯ β π΄) β (absβ(πΉβπ΅)) β β) |
16 | 13, 15 | eqeltrd 2838 |
. . . 4
β’ ((π β§ π₯ β π΄) β if(π₯ β π΄, (absβ(πΉβπ΅)), 0) β β) |
17 | | eldifn 4092 |
. . . . . 6
β’ (π₯ β (β β π΄) β Β¬ π₯ β π΄) |
18 | 17 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β (β β π΄)) β Β¬ π₯ β π΄) |
19 | | iffalse 4500 |
. . . . 5
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, (absβ(πΉβπ΅)), 0) = 0) |
20 | 18, 19 | syl 17 |
. . . 4
β’ ((π β§ π₯ β (β β π΄)) β if(π₯ β π΄, (absβ(πΉβπ΅)), 0) = 0) |
21 | 12 | mpteq2ia 5213 |
. . . . . 6
β’ (π₯ β π΄ β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) = (π₯ β π΄ β¦ (absβ(πΉβπ΅))) |
22 | | absf 15229 |
. . . . . . . 8
β’
abs:ββΆβ |
23 | 22 | a1i 11 |
. . . . . . 7
β’ (π β
abs:ββΆβ) |
24 | 23, 14 | cofmpt 7083 |
. . . . . 6
β’ (π β (abs β (π₯ β π΄ β¦ (πΉβπ΅))) = (π₯ β π΄ β¦ (absβ(πΉβπ΅)))) |
25 | 21, 24 | eqtr4id 2796 |
. . . . 5
β’ (π β (π₯ β π΄ β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) = (abs β (π₯ β π΄ β¦ (πΉβπ΅)))) |
26 | 14 | fmpttd 7068 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ (πΉβπ΅)):π΄βΆβ) |
27 | | ax-resscn 11115 |
. . . . . . . . 9
β’ β
β β |
28 | | ssid 3971 |
. . . . . . . . 9
β’ β
β β |
29 | | cncfss 24278 |
. . . . . . . . 9
β’ ((β
β β β§ β β β) β (ββcnββ) β (ββcnββ)) |
30 | 27, 28, 29 | mp2an 691 |
. . . . . . . 8
β’
(ββcnββ)
β (ββcnββ) |
31 | | abscncf 24280 |
. . . . . . . 8
β’ abs
β (ββcnββ) |
32 | 30, 31 | sselii 3946 |
. . . . . . 7
β’ abs
β (ββcnββ) |
33 | 32 | a1i 11 |
. . . . . 6
β’ (π β abs β
(ββcnββ)) |
34 | | cncombf 25038 |
. . . . . 6
β’ (((π₯ β π΄ β¦ (πΉβπ΅)) β MblFn β§ (π₯ β π΄ β¦ (πΉβπ΅)):π΄βΆβ β§ abs β
(ββcnββ)) β
(abs β (π₯ β
π΄ β¦ (πΉβπ΅))) β MblFn) |
35 | 6, 26, 33, 34 | syl3anc 1372 |
. . . . 5
β’ (π β (abs β (π₯ β π΄ β¦ (πΉβπ΅))) β MblFn) |
36 | 25, 35 | eqeltrd 2838 |
. . . 4
β’ (π β (π₯ β π΄ β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) β MblFn) |
37 | 9, 11, 16, 20, 36 | mbfss 25026 |
. . 3
β’ (π β (π₯ β β β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) β MblFn) |
38 | 1, 37 | eqeltrid 2842 |
. 2
β’ (π β πΊ β MblFn) |
39 | | reex 11149 |
. . . . . . . . 9
β’ β
β V |
40 | 39 | a1i 11 |
. . . . . . . 8
β’ (π β β β
V) |
41 | | ifan 4544 |
. . . . . . . . . 10
β’ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) = if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) |
42 | | 0re 11164 |
. . . . . . . . . . . . 13
β’ 0 β
β |
43 | | ifcl 4536 |
. . . . . . . . . . . . 13
β’ (((πΉβπ΅) β β β§ 0 β β)
β if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) β β) |
44 | 3, 42, 43 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) β β) |
45 | | max1 13111 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ (πΉβπ΅) β β) β 0 β€ if(0 β€
(πΉβπ΅), (πΉβπ΅), 0)) |
46 | 42, 3, 45 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β 0 β€ if(0 β€ (πΉβπ΅), (πΉβπ΅), 0)) |
47 | | elrege0 13378 |
. . . . . . . . . . . 12
β’ (if(0
β€ (πΉβπ΅), (πΉβπ΅), 0) β (0[,)+β) β (if(0
β€ (πΉβπ΅), (πΉβπ΅), 0) β β β§ 0 β€ if(0 β€
(πΉβπ΅), (πΉβπ΅), 0))) |
48 | 44, 46, 47 | sylanbrc 584 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) β
(0[,)+β)) |
49 | | 0e0icopnf 13382 |
. . . . . . . . . . . 12
β’ 0 β
(0[,)+β) |
50 | 49 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ π₯ β π΄) β 0 β
(0[,)+β)) |
51 | 48, 50 | ifclda 4526 |
. . . . . . . . . 10
β’ (π β if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) β
(0[,)+β)) |
52 | 41, 51 | eqeltrid 2842 |
. . . . . . . . 9
β’ (π β if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) β
(0[,)+β)) |
53 | 52 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) β
(0[,)+β)) |
54 | | ifan 4544 |
. . . . . . . . . 10
β’ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0) = if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0) |
55 | 3 | renegcld 11589 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β -(πΉβπ΅) β β) |
56 | | ifcl 4536 |
. . . . . . . . . . . . 13
β’ ((-(πΉβπ΅) β β β§ 0 β β)
β if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0) β β) |
57 | 55, 42, 56 | sylancl 587 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0) β β) |
58 | | max1 13111 |
. . . . . . . . . . . . 13
β’ ((0
β β β§ -(πΉβπ΅) β β) β 0 β€ if(0 β€
-(πΉβπ΅), -(πΉβπ΅), 0)) |
59 | 42, 55, 58 | sylancr 588 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β 0 β€ if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0)) |
60 | | elrege0 13378 |
. . . . . . . . . . . 12
β’ (if(0
β€ -(πΉβπ΅), -(πΉβπ΅), 0) β (0[,)+β) β (if(0
β€ -(πΉβπ΅), -(πΉβπ΅), 0) β β β§ 0 β€ if(0 β€
-(πΉβπ΅), -(πΉβπ΅), 0))) |
61 | 57, 59, 60 | sylanbrc 584 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0) β
(0[,)+β)) |
62 | 61, 50 | ifclda 4526 |
. . . . . . . . . 10
β’ (π β if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0) β
(0[,)+β)) |
63 | 54, 62 | eqeltrid 2842 |
. . . . . . . . 9
β’ (π β if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0) β
(0[,)+β)) |
64 | 63 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π₯ β β) β if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0) β
(0[,)+β)) |
65 | | eqidd 2738 |
. . . . . . . 8
β’ (π β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0))) |
66 | | eqidd 2738 |
. . . . . . . 8
β’ (π β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)) = (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))) |
67 | 40, 53, 64, 65, 66 | offval2 7642 |
. . . . . . 7
β’ (π β ((π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) βf + (π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))) = (π₯ β β β¦ (if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) + if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)))) |
68 | 41, 54 | oveq12i 7374 |
. . . . . . . . 9
β’
(if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) + if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)) = (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) |
69 | | max0add 15202 |
. . . . . . . . . . . . 13
β’ ((πΉβπ΅) β β β (if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) + if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0)) = (absβ(πΉβπ΅))) |
70 | 3, 69 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) + if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0)) = (absβ(πΉβπ΅))) |
71 | | iftrue 4497 |
. . . . . . . . . . . . . 14
β’ (π₯ β π΄ β if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) = if(0 β€ (πΉβπ΅), (πΉβπ΅), 0)) |
72 | 71 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) = if(0 β€ (πΉβπ΅), (πΉβπ΅), 0)) |
73 | | iftrue 4497 |
. . . . . . . . . . . . . 14
β’ (π₯ β π΄ β if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0) = if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0)) |
74 | 73 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π₯ β π΄) β if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0) = if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0)) |
75 | 72, 74 | oveq12d 7380 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π΄) β (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) = (if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) + if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0))) |
76 | 70, 75, 13 | 3eqtr4d 2787 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π΄) β (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) = if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) |
77 | 76 | ex 414 |
. . . . . . . . . 10
β’ (π β (π₯ β π΄ β (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) = if(π₯ β π΄, (absβ(πΉβπ΅)), 0))) |
78 | | 00id 11337 |
. . . . . . . . . . 11
β’ (0 + 0) =
0 |
79 | | iffalse 4500 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) = 0) |
80 | | iffalse 4500 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ β π΄ β if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0) = 0) |
81 | 79, 80 | oveq12d 7380 |
. . . . . . . . . . 11
β’ (Β¬
π₯ β π΄ β (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) = (0 + 0)) |
82 | 78, 81, 19 | 3eqtr4a 2803 |
. . . . . . . . . 10
β’ (Β¬
π₯ β π΄ β (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) = if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) |
83 | 77, 82 | pm2.61d1 180 |
. . . . . . . . 9
β’ (π β (if(π₯ β π΄, if(0 β€ (πΉβπ΅), (πΉβπ΅), 0), 0) + if(π₯ β π΄, if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0), 0)) = if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) |
84 | 68, 83 | eqtrid 2789 |
. . . . . . . 8
β’ (π β (if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) + if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)) = if(π₯ β π΄, (absβ(πΉβπ΅)), 0)) |
85 | 84 | mpteq2dv 5212 |
. . . . . . 7
β’ (π β (π₯ β β β¦ (if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) + if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))) = (π₯ β β β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0))) |
86 | 67, 85 | eqtrd 2777 |
. . . . . 6
β’ (π β ((π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) βf + (π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))) = (π₯ β β β¦ if(π₯ β π΄, (absβ(πΉβπ΅)), 0))) |
87 | 1, 86 | eqtr4id 2796 |
. . . . 5
β’ (π β πΊ = ((π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) βf + (π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)))) |
88 | 87 | fveq2d 6851 |
. . . 4
β’ (π β
(β«2βπΊ)
= (β«2β((π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) βf + (π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))))) |
89 | 52 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) β
(0[,)+β)) |
90 | 41, 79 | eqtrid 2789 |
. . . . . . 7
β’ (Β¬
π₯ β π΄ β if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) = 0) |
91 | 18, 90 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β (β β π΄)) β if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0) = 0) |
92 | | ibar 530 |
. . . . . . . . 9
β’ (π₯ β π΄ β (0 β€ (πΉβπ΅) β (π₯ β π΄ β§ 0 β€ (πΉβπ΅)))) |
93 | 92 | ifbid 4514 |
. . . . . . . 8
β’ (π₯ β π΄ β if(0 β€ (πΉβπ΅), (πΉβπ΅), 0) = if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) |
94 | 93 | mpteq2ia 5213 |
. . . . . . 7
β’ (π₯ β π΄ β¦ if(0 β€ (πΉβπ΅), (πΉβπ΅), 0)) = (π₯ β π΄ β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) |
95 | 3, 6 | mbfpos 25031 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ if(0 β€ (πΉβπ΅), (πΉβπ΅), 0)) β MblFn) |
96 | 94, 95 | eqeltrrid 2843 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) β MblFn) |
97 | 9, 11, 89, 91, 96 | mbfss 25026 |
. . . . 5
β’ (π β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) β MblFn) |
98 | 53 | fmpttd 7068 |
. . . . 5
β’ (π β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅),
0)):ββΆ(0[,)+β)) |
99 | 5 | simp2d 1144 |
. . . . 5
β’ (π β
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0))) β β) |
100 | 63 | adantr 482 |
. . . . . 6
β’ ((π β§ π₯ β π΄) β if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0) β
(0[,)+β)) |
101 | 54, 80 | eqtrid 2789 |
. . . . . . 7
β’ (Β¬
π₯ β π΄ β if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0) = 0) |
102 | 18, 101 | syl 17 |
. . . . . 6
β’ ((π β§ π₯ β (β β π΄)) β if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0) = 0) |
103 | | ibar 530 |
. . . . . . . . 9
β’ (π₯ β π΄ β (0 β€ -(πΉβπ΅) β (π₯ β π΄ β§ 0 β€ -(πΉβπ΅)))) |
104 | 103 | ifbid 4514 |
. . . . . . . 8
β’ (π₯ β π΄ β if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0) = if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)) |
105 | 104 | mpteq2ia 5213 |
. . . . . . 7
β’ (π₯ β π΄ β¦ if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0)) = (π₯ β π΄ β¦ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)) |
106 | 3, 6 | mbfneg 25030 |
. . . . . . . 8
β’ (π β (π₯ β π΄ β¦ -(πΉβπ΅)) β MblFn) |
107 | 55, 106 | mbfpos 25031 |
. . . . . . 7
β’ (π β (π₯ β π΄ β¦ if(0 β€ -(πΉβπ΅), -(πΉβπ΅), 0)) β MblFn) |
108 | 105, 107 | eqeltrrid 2843 |
. . . . . 6
β’ (π β (π₯ β π΄ β¦ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)) β MblFn) |
109 | 9, 11, 100, 102, 108 | mbfss 25026 |
. . . . 5
β’ (π β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)) β MblFn) |
110 | 64 | fmpttd 7068 |
. . . . 5
β’ (π β (π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅),
0)):ββΆ(0[,)+β)) |
111 | 5 | simp3d 1145 |
. . . . 5
β’ (π β
(β«2β(π₯
β β β¦ if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))) β β) |
112 | 97, 98, 99, 109, 110, 111 | itg2add 25140 |
. . . 4
β’ (π β
(β«2β((π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0)) βf + (π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)))) = ((β«2β(π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0))) + (β«2β(π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))))) |
113 | 88, 112 | eqtrd 2777 |
. . 3
β’ (π β
(β«2βπΊ)
= ((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0))) + (β«2β(π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0))))) |
114 | 99, 111 | readdcld 11191 |
. . 3
β’ (π β
((β«2β(π₯ β β β¦ if((π₯ β π΄ β§ 0 β€ (πΉβπ΅)), (πΉβπ΅), 0))) + (β«2β(π₯ β β β¦
if((π₯ β π΄ β§ 0 β€ -(πΉβπ΅)), -(πΉβπ΅), 0)))) β β) |
115 | 113, 114 | eqeltrd 2838 |
. 2
β’ (π β
(β«2βπΊ)
β β) |
116 | 38, 115 | jca 513 |
1
β’ (π β (πΊ β MblFn β§
(β«2βπΊ)
β β)) |