Metamath Proof Explorer

Theorem itgitg1

Description: Transfer an integral using S.1 to an equivalent integral using S. . (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Assertion itgitg1 
|- ( F e. dom S.1 -> S. RR ( F ` x ) _d x = ( S.1 ` F ) )

Proof

Step Hyp Ref Expression
1 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
2 1 ffvelrnda 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( F ` x ) e. RR )
3 1 feqmptd 
 |-  ( F e. dom S.1 -> F = ( x e. RR |-> ( F ` x ) ) )
4 i1fibl 
 |-  ( F e. dom S.1 -> F e. L^1 )
5 3 4 eqeltrrd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> ( F ` x ) ) e. L^1 )
6 2 5 itgreval 
 |-  ( F e. dom S.1 -> S. RR ( F ` x ) _d x = ( S. RR if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) _d x - S. RR if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) _d x ) )
7 0re 
 |-  0 e. RR
8 ifcl 
 |-  ( ( ( F ` x ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) e. RR )
9 2 7 8 sylancl 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) e. RR )
10 max1 
 |-  ( ( 0 e. RR /\ ( F ` x ) e. RR ) -> 0 <_ if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) )
11 7 2 10 sylancr 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> 0 <_ if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) )
12 id 
 |-  ( F e. dom S.1 -> F e. dom S.1 )
13 3 12 eqeltrrd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> ( F ` x ) ) e. dom S.1 )
14 13 i1fposd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) e. dom S.1 )
15 i1fibl 
 |-  ( ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) e. dom S.1 -> ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) e. L^1 )
16 14 15 syl 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) e. L^1 )
17 9 11 16 itgitg2 
 |-  ( F e. dom S.1 -> S. RR if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) _d x = ( S.2 ` ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) )
18 11 ralrimiva 
 |-  ( F e. dom S.1 -> A. x e. RR 0 <_ if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) )
19 reex 
 |-  RR e. _V
20 19 a1i 
 |-  ( F e. dom S.1 -> RR e. _V )
21 7 a1i 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> 0 e. RR )
22 fconstmpt 
 |-  ( RR X. { 0 } ) = ( x e. RR |-> 0 )
23 22 a1i 
 |-  ( F e. dom S.1 -> ( RR X. { 0 } ) = ( x e. RR |-> 0 ) )
24 eqidd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) )
25 20 21 9 23 24 ofrfval2 
 |-  ( F e. dom S.1 -> ( ( RR X. { 0 } ) oR <_ ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) <-> A. x e. RR 0 <_ if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) )
26 18 25 mpbird 
 |-  ( F e. dom S.1 -> ( RR X. { 0 } ) oR <_ ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) )
27 ax-resscn 
 |-  RR C_ CC
28 27 a1i 
 |-  ( F e. dom S.1 -> RR C_ CC )
29 9 fmpttd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) : RR --> RR )
30 29 ffnd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) Fn RR )
31 28 30 0pledm 
 |-  ( F e. dom S.1 -> ( 0p oR <_ ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) <-> ( RR X. { 0 } ) oR <_ ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) )
32 26 31 mpbird 
 |-  ( F e. dom S.1 -> 0p oR <_ ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) )
33 itg2itg1 
 |-  ( ( ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) e. dom S.1 /\ 0p oR <_ ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) -> ( S.2 ` ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) = ( S.1 ` ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) )
34 14 32 33 syl2anc 
 |-  ( F e. dom S.1 -> ( S.2 ` ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) = ( S.1 ` ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) )
35 17 34 eqtrd 
 |-  ( F e. dom S.1 -> S. RR if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) _d x = ( S.1 ` ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) )
36 2 renegcld 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> -u ( F ` x ) e. RR )
37 ifcl 
 |-  ( ( -u ( F ` x ) e. RR /\ 0 e. RR ) -> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) e. RR )
38 36 7 37 sylancl 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) e. RR )
39 max1 
 |-  ( ( 0 e. RR /\ -u ( F ` x ) e. RR ) -> 0 <_ if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) )
40 7 36 39 sylancr 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> 0 <_ if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) )
41 neg1rr 
 |-  -u 1 e. RR
42 41 a1i 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> -u 1 e. RR )
43 fconstmpt 
 |-  ( RR X. { -u 1 } ) = ( x e. RR |-> -u 1 )
44 43 a1i 
 |-  ( F e. dom S.1 -> ( RR X. { -u 1 } ) = ( x e. RR |-> -u 1 ) )
45 20 42 2 44 3 offval2 
 |-  ( F e. dom S.1 -> ( ( RR X. { -u 1 } ) oF x. F ) = ( x e. RR |-> ( -u 1 x. ( F ` x ) ) ) )
46 2 recnd 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( F ` x ) e. CC )
47 46 mulm1d 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( -u 1 x. ( F ` x ) ) = -u ( F ` x ) )
48 47 mpteq2dva 
 |-  ( F e. dom S.1 -> ( x e. RR |-> ( -u 1 x. ( F ` x ) ) ) = ( x e. RR |-> -u ( F ` x ) ) )
49 45 48 eqtrd 
 |-  ( F e. dom S.1 -> ( ( RR X. { -u 1 } ) oF x. F ) = ( x e. RR |-> -u ( F ` x ) ) )
50 41 a1i 
 |-  ( F e. dom S.1 -> -u 1 e. RR )
51 12 50 i1fmulc 
 |-  ( F e. dom S.1 -> ( ( RR X. { -u 1 } ) oF x. F ) e. dom S.1 )
52 49 51 eqeltrrd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> -u ( F ` x ) ) e. dom S.1 )
53 52 i1fposd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) e. dom S.1 )
54 i1fibl 
 |-  ( ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) e. dom S.1 -> ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) e. L^1 )
55 53 54 syl 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) e. L^1 )
56 38 40 55 itgitg2 
 |-  ( F e. dom S.1 -> S. RR if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) _d x = ( S.2 ` ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) )
57 40 ralrimiva 
 |-  ( F e. dom S.1 -> A. x e. RR 0 <_ if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) )
58 eqidd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) )
59 20 21 38 23 58 ofrfval2 
 |-  ( F e. dom S.1 -> ( ( RR X. { 0 } ) oR <_ ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) <-> A. x e. RR 0 <_ if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) )
60 57 59 mpbird 
 |-  ( F e. dom S.1 -> ( RR X. { 0 } ) oR <_ ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) )
61 38 fmpttd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) : RR --> RR )
62 61 ffnd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) Fn RR )
63 28 62 0pledm 
 |-  ( F e. dom S.1 -> ( 0p oR <_ ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) <-> ( RR X. { 0 } ) oR <_ ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) )
64 60 63 mpbird 
 |-  ( F e. dom S.1 -> 0p oR <_ ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) )
65 itg2itg1 
 |-  ( ( ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) e. dom S.1 /\ 0p oR <_ ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) -> ( S.2 ` ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) = ( S.1 ` ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) )
66 53 64 65 syl2anc 
 |-  ( F e. dom S.1 -> ( S.2 ` ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) = ( S.1 ` ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) )
67 56 66 eqtrd 
 |-  ( F e. dom S.1 -> S. RR if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) _d x = ( S.1 ` ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) )
68 35 67 oveq12d 
 |-  ( F e. dom S.1 -> ( S. RR if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) _d x - S. RR if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) _d x ) = ( ( S.1 ` ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) - ( S.1 ` ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) ) )
69 itg1sub 
 |-  ( ( ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) e. dom S.1 /\ ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) e. dom S.1 ) -> ( S.1 ` ( ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) oF - ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) ) = ( ( S.1 ` ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) - ( S.1 ` ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) ) )
70 14 53 69 syl2anc 
 |-  ( F e. dom S.1 -> ( S.1 ` ( ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) oF - ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) ) = ( ( S.1 ` ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) - ( S.1 ` ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) ) )
71 68 70 eqtr4d 
 |-  ( F e. dom S.1 -> ( S. RR if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) _d x - S. RR if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) _d x ) = ( S.1 ` ( ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) oF - ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) ) )
72 max0sub 
 |-  ( ( F ` x ) e. RR -> ( if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) - if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) = ( F ` x ) )
73 2 72 syl 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) - if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) = ( F ` x ) )
74 73 mpteq2dva 
 |-  ( F e. dom S.1 -> ( x e. RR |-> ( if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) - if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) = ( x e. RR |-> ( F ` x ) ) )
75 20 9 38 24 58 offval2 
 |-  ( F e. dom S.1 -> ( ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) oF - ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) = ( x e. RR |-> ( if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) - if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) )
76 74 75 3 3eqtr4d 
 |-  ( F e. dom S.1 -> ( ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) oF - ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) = F )
77 76 fveq2d 
 |-  ( F e. dom S.1 -> ( S.1 ` ( ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) oF - ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) ) = ( S.1 ` F ) )
78 6 71 77 3eqtrd 
 |-  ( F e. dom S.1 -> S. RR ( F ` x ) _d x = ( S.1 ` F ) )