Step | Hyp | Ref
| Expression |
1 | | i1ff 25063 |
. . . 4
β’ (πΉ β dom β«1
β πΉ:ββΆβ) |
2 | 1 | ffvelcdmda 7039 |
. . 3
β’ ((πΉ β dom β«1
β§ π₯ β β)
β (πΉβπ₯) β
β) |
3 | 1 | feqmptd 6914 |
. . . 4
β’ (πΉ β dom β«1
β πΉ = (π₯ β β β¦ (πΉβπ₯))) |
4 | | i1fibl 25195 |
. . . 4
β’ (πΉ β dom β«1
β πΉ β
πΏ1) |
5 | 3, 4 | eqeltrrd 2835 |
. . 3
β’ (πΉ β dom β«1
β (π₯ β β
β¦ (πΉβπ₯)) β
πΏ1) |
6 | 2, 5 | itgreval 25184 |
. 2
β’ (πΉ β dom β«1
β β«β(πΉβπ₯) dπ₯ = (β«βif(0 β€ (πΉβπ₯), (πΉβπ₯), 0) dπ₯ β β«βif(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0) dπ₯)) |
7 | | 0re 11165 |
. . . . . . 7
β’ 0 β
β |
8 | | ifcl 4535 |
. . . . . . 7
β’ (((πΉβπ₯) β β β§ 0 β β)
β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β β) |
9 | 2, 7, 8 | sylancl 587 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ π₯ β β)
β if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β β) |
10 | | max1 13113 |
. . . . . . 7
β’ ((0
β β β§ (πΉβπ₯) β β) β 0 β€ if(0 β€
(πΉβπ₯), (πΉβπ₯), 0)) |
11 | 7, 2, 10 | sylancr 588 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ π₯ β β)
β 0 β€ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) |
12 | | id 22 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β πΉ β dom
β«1) |
13 | 3, 12 | eqeltrrd 2835 |
. . . . . . . 8
β’ (πΉ β dom β«1
β (π₯ β β
β¦ (πΉβπ₯)) β dom
β«1) |
14 | 13 | i1fposd 25095 |
. . . . . . 7
β’ (πΉ β dom β«1
β (π₯ β β
β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) β dom
β«1) |
15 | | i1fibl 25195 |
. . . . . . 7
β’ ((π₯ β β β¦ if(0
β€ (πΉβπ₯), (πΉβπ₯), 0)) β dom β«1 β
(π₯ β β β¦
if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) β
πΏ1) |
16 | 14, 15 | syl 17 |
. . . . . 6
β’ (πΉ β dom β«1
β (π₯ β β
β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) β
πΏ1) |
17 | 9, 11, 16 | itgitg2 25194 |
. . . . 5
β’ (πΉ β dom β«1
β β«βif(0 β€ (πΉβπ₯), (πΉβπ₯), 0) dπ₯ = (β«2β(π₯ β β β¦ if(0
β€ (πΉβπ₯), (πΉβπ₯), 0)))) |
18 | 11 | ralrimiva 3140 |
. . . . . . . 8
β’ (πΉ β dom β«1
β βπ₯ β
β 0 β€ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) |
19 | | reex 11150 |
. . . . . . . . . 10
β’ β
β V |
20 | 19 | a1i 11 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β β β V) |
21 | 7 | a1i 11 |
. . . . . . . . 9
β’ ((πΉ β dom β«1
β§ π₯ β β)
β 0 β β) |
22 | | fconstmpt 5698 |
. . . . . . . . . 10
β’ (β
Γ {0}) = (π₯ β
β β¦ 0) |
23 | 22 | a1i 11 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β (β Γ {0}) = (π₯ β β β¦ 0)) |
24 | | eqidd 2734 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β (π₯ β β
β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) = (π₯ β β β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0))) |
25 | 20, 21, 9, 23, 24 | ofrfval2 7642 |
. . . . . . . 8
β’ (πΉ β dom β«1
β ((β Γ {0}) βr β€ (π₯ β β β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) β βπ₯ β β 0 β€ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0))) |
26 | 18, 25 | mpbird 257 |
. . . . . . 7
β’ (πΉ β dom β«1
β (β Γ {0}) βr β€ (π₯ β β β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0))) |
27 | | ax-resscn 11116 |
. . . . . . . . 9
β’ β
β β |
28 | 27 | a1i 11 |
. . . . . . . 8
β’ (πΉ β dom β«1
β β β β) |
29 | 9 | fmpttd 7067 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β (π₯ β β
β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯),
0)):ββΆβ) |
30 | 29 | ffnd 6673 |
. . . . . . . 8
β’ (πΉ β dom β«1
β (π₯ β β
β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) Fn β) |
31 | 28, 30 | 0pledm 25060 |
. . . . . . 7
β’ (πΉ β dom β«1
β (0π βr β€ (π₯ β β β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) β (β Γ {0})
βr β€ (π₯
β β β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)))) |
32 | 26, 31 | mpbird 257 |
. . . . . 6
β’ (πΉ β dom β«1
β 0π βr β€ (π₯ β β β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0))) |
33 | | itg2itg1 25124 |
. . . . . 6
β’ (((π₯ β β β¦ if(0
β€ (πΉβπ₯), (πΉβπ₯), 0)) β dom β«1 β§
0π βr β€ (π₯ β β β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0))) β
(β«2β(π₯
β β β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0))) = (β«1β(π₯ β β β¦ if(0
β€ (πΉβπ₯), (πΉβπ₯), 0)))) |
34 | 14, 32, 33 | syl2anc 585 |
. . . . 5
β’ (πΉ β dom β«1
β (β«2β(π₯ β β β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0))) = (β«1β(π₯ β β β¦ if(0
β€ (πΉβπ₯), (πΉβπ₯), 0)))) |
35 | 17, 34 | eqtrd 2773 |
. . . 4
β’ (πΉ β dom β«1
β β«βif(0 β€ (πΉβπ₯), (πΉβπ₯), 0) dπ₯ = (β«1β(π₯ β β β¦ if(0
β€ (πΉβπ₯), (πΉβπ₯), 0)))) |
36 | 2 | renegcld 11590 |
. . . . . . 7
β’ ((πΉ β dom β«1
β§ π₯ β β)
β -(πΉβπ₯) β
β) |
37 | | ifcl 4535 |
. . . . . . 7
β’ ((-(πΉβπ₯) β β β§ 0 β β)
β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0) β β) |
38 | 36, 7, 37 | sylancl 587 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ π₯ β β)
β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0) β β) |
39 | | max1 13113 |
. . . . . . 7
β’ ((0
β β β§ -(πΉβπ₯) β β) β 0 β€ if(0 β€
-(πΉβπ₯), -(πΉβπ₯), 0)) |
40 | 7, 36, 39 | sylancr 588 |
. . . . . 6
β’ ((πΉ β dom β«1
β§ π₯ β β)
β 0 β€ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) |
41 | | neg1rr 12276 |
. . . . . . . . . . . 12
β’ -1 β
β |
42 | 41 | a1i 11 |
. . . . . . . . . . 11
β’ ((πΉ β dom β«1
β§ π₯ β β)
β -1 β β) |
43 | | fconstmpt 5698 |
. . . . . . . . . . . 12
β’ (β
Γ {-1}) = (π₯ β
β β¦ -1) |
44 | 43 | a1i 11 |
. . . . . . . . . . 11
β’ (πΉ β dom β«1
β (β Γ {-1}) = (π₯ β β β¦ -1)) |
45 | 20, 42, 2, 44, 3 | offval2 7641 |
. . . . . . . . . 10
β’ (πΉ β dom β«1
β ((β Γ {-1}) βf Β· πΉ) = (π₯ β β β¦ (-1 Β· (πΉβπ₯)))) |
46 | 2 | recnd 11191 |
. . . . . . . . . . . 12
β’ ((πΉ β dom β«1
β§ π₯ β β)
β (πΉβπ₯) β
β) |
47 | 46 | mulm1d 11615 |
. . . . . . . . . . 11
β’ ((πΉ β dom β«1
β§ π₯ β β)
β (-1 Β· (πΉβπ₯)) = -(πΉβπ₯)) |
48 | 47 | mpteq2dva 5209 |
. . . . . . . . . 10
β’ (πΉ β dom β«1
β (π₯ β β
β¦ (-1 Β· (πΉβπ₯))) = (π₯ β β β¦ -(πΉβπ₯))) |
49 | 45, 48 | eqtrd 2773 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β ((β Γ {-1}) βf Β· πΉ) = (π₯ β β β¦ -(πΉβπ₯))) |
50 | 41 | a1i 11 |
. . . . . . . . . 10
β’ (πΉ β dom β«1
β -1 β β) |
51 | 12, 50 | i1fmulc 25091 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β ((β Γ {-1}) βf Β· πΉ) β dom
β«1) |
52 | 49, 51 | eqeltrrd 2835 |
. . . . . . . 8
β’ (πΉ β dom β«1
β (π₯ β β
β¦ -(πΉβπ₯)) β dom
β«1) |
53 | 52 | i1fposd 25095 |
. . . . . . 7
β’ (πΉ β dom β«1
β (π₯ β β
β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) β dom
β«1) |
54 | | i1fibl 25195 |
. . . . . . 7
β’ ((π₯ β β β¦ if(0
β€ -(πΉβπ₯), -(πΉβπ₯), 0)) β dom β«1 β
(π₯ β β β¦
if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) β
πΏ1) |
55 | 53, 54 | syl 17 |
. . . . . 6
β’ (πΉ β dom β«1
β (π₯ β β
β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) β
πΏ1) |
56 | 38, 40, 55 | itgitg2 25194 |
. . . . 5
β’ (πΉ β dom β«1
β β«βif(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0) dπ₯ = (β«2β(π₯ β β β¦ if(0
β€ -(πΉβπ₯), -(πΉβπ₯), 0)))) |
57 | 40 | ralrimiva 3140 |
. . . . . . . 8
β’ (πΉ β dom β«1
β βπ₯ β
β 0 β€ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) |
58 | | eqidd 2734 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β (π₯ β β
β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) = (π₯ β β β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) |
59 | 20, 21, 38, 23, 58 | ofrfval2 7642 |
. . . . . . . 8
β’ (πΉ β dom β«1
β ((β Γ {0}) βr β€ (π₯ β β β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) β βπ₯ β β 0 β€ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) |
60 | 57, 59 | mpbird 257 |
. . . . . . 7
β’ (πΉ β dom β«1
β (β Γ {0}) βr β€ (π₯ β β β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) |
61 | 38 | fmpttd 7067 |
. . . . . . . . 9
β’ (πΉ β dom β«1
β (π₯ β β
β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯),
0)):ββΆβ) |
62 | 61 | ffnd 6673 |
. . . . . . . 8
β’ (πΉ β dom β«1
β (π₯ β β
β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) Fn β) |
63 | 28, 62 | 0pledm 25060 |
. . . . . . 7
β’ (πΉ β dom β«1
β (0π βr β€ (π₯ β β β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) β (β Γ {0})
βr β€ (π₯
β β β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)))) |
64 | 60, 63 | mpbird 257 |
. . . . . 6
β’ (πΉ β dom β«1
β 0π βr β€ (π₯ β β β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) |
65 | | itg2itg1 25124 |
. . . . . 6
β’ (((π₯ β β β¦ if(0
β€ -(πΉβπ₯), -(πΉβπ₯), 0)) β dom β«1 β§
0π βr β€ (π₯ β β β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) β
(β«2β(π₯
β β β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) = (β«1β(π₯ β β β¦ if(0
β€ -(πΉβπ₯), -(πΉβπ₯), 0)))) |
66 | 53, 64, 65 | syl2anc 585 |
. . . . 5
β’ (πΉ β dom β«1
β (β«2β(π₯ β β β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) = (β«1β(π₯ β β β¦ if(0
β€ -(πΉβπ₯), -(πΉβπ₯), 0)))) |
67 | 56, 66 | eqtrd 2773 |
. . . 4
β’ (πΉ β dom β«1
β β«βif(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0) dπ₯ = (β«1β(π₯ β β β¦ if(0
β€ -(πΉβπ₯), -(πΉβπ₯), 0)))) |
68 | 35, 67 | oveq12d 7379 |
. . 3
β’ (πΉ β dom β«1
β (β«βif(0 β€ (πΉβπ₯), (πΉβπ₯), 0) dπ₯ β β«βif(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0) dπ₯) = ((β«1β(π₯ β β β¦ if(0
β€ (πΉβπ₯), (πΉβπ₯), 0))) β
(β«1β(π₯
β β β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))))) |
69 | | itg1sub 25097 |
. . . 4
β’ (((π₯ β β β¦ if(0
β€ (πΉβπ₯), (πΉβπ₯), 0)) β dom β«1 β§
(π₯ β β β¦
if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) β dom β«1) β
(β«1β((π₯ β β β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) βf β (π₯ β β β¦ if(0
β€ -(πΉβπ₯), -(πΉβπ₯), 0)))) = ((β«1β(π₯ β β β¦ if(0
β€ (πΉβπ₯), (πΉβπ₯), 0))) β
(β«1β(π₯
β β β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))))) |
70 | 14, 53, 69 | syl2anc 585 |
. . 3
β’ (πΉ β dom β«1
β (β«1β((π₯ β β β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) βf β (π₯ β β β¦ if(0
β€ -(πΉβπ₯), -(πΉβπ₯), 0)))) = ((β«1β(π₯ β β β¦ if(0
β€ (πΉβπ₯), (πΉβπ₯), 0))) β
(β«1β(π₯
β β β¦ if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))))) |
71 | 68, 70 | eqtr4d 2776 |
. 2
β’ (πΉ β dom β«1
β (β«βif(0 β€ (πΉβπ₯), (πΉβπ₯), 0) dπ₯ β β«βif(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0) dπ₯) = (β«1β((π₯ β β β¦ if(0
β€ (πΉβπ₯), (πΉβπ₯), 0)) βf β (π₯ β β β¦ if(0
β€ -(πΉβπ₯), -(πΉβπ₯), 0))))) |
72 | | max0sub 13124 |
. . . . . 6
β’ ((πΉβπ₯) β β β (if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) = (πΉβπ₯)) |
73 | 2, 72 | syl 17 |
. . . . 5
β’ ((πΉ β dom β«1
β§ π₯ β β)
β (if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)) = (πΉβπ₯)) |
74 | 73 | mpteq2dva 5209 |
. . . 4
β’ (πΉ β dom β«1
β (π₯ β β
β¦ (if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0))) = (π₯ β β β¦ (πΉβπ₯))) |
75 | 20, 9, 38, 24, 58 | offval2 7641 |
. . . 4
β’ (πΉ β dom β«1
β ((π₯ β β
β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) βf β (π₯ β β β¦ if(0
β€ -(πΉβπ₯), -(πΉβπ₯), 0))) = (π₯ β β β¦ (if(0 β€ (πΉβπ₯), (πΉβπ₯), 0) β if(0 β€ -(πΉβπ₯), -(πΉβπ₯), 0)))) |
76 | 74, 75, 3 | 3eqtr4d 2783 |
. . 3
β’ (πΉ β dom β«1
β ((π₯ β β
β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) βf β (π₯ β β β¦ if(0
β€ -(πΉβπ₯), -(πΉβπ₯), 0))) = πΉ) |
77 | 76 | fveq2d 6850 |
. 2
β’ (πΉ β dom β«1
β (β«1β((π₯ β β β¦ if(0 β€ (πΉβπ₯), (πΉβπ₯), 0)) βf β (π₯ β β β¦ if(0
β€ -(πΉβπ₯), -(πΉβπ₯), 0)))) = (β«1βπΉ)) |
78 | 6, 71, 77 | 3eqtrd 2777 |
1
β’ (πΉ β dom β«1
β β«β(πΉβπ₯) dπ₯ = (β«1βπΉ)) |