Metamath Proof Explorer

Theorem i1fibl

Description: A simple function is integrable. (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Assertion i1fibl 
|- ( F e. dom S.1 -> F e. L^1 )

Proof

Step Hyp Ref Expression
1 i1ff 
 |-  ( F e. dom S.1 -> F : RR --> RR )
2 1 feqmptd 
 |-  ( F e. dom S.1 -> F = ( x e. RR |-> ( F ` x ) ) )
3 i1fmbf 
 |-  ( F e. dom S.1 -> F e. MblFn )
4 2 3 eqeltrrd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> ( F ` x ) ) e. MblFn )
5 simpr 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> x e. RR )
6 5 biantrurd 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( 0 <_ ( F ` x ) <-> ( x e. RR /\ 0 <_ ( F ` x ) ) ) )
7 6 ifbid 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) = if ( ( x e. RR /\ 0 <_ ( F ` x ) ) , ( F ` x ) , 0 ) )
8 7 mpteq2dva 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( ( x e. RR /\ 0 <_ ( F ` x ) ) , ( F ` x ) , 0 ) ) )
9 8 fveq2d 
 |-  ( F e. dom S.1 -> ( S.2 ` ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. RR /\ 0 <_ ( F ` x ) ) , ( F ` x ) , 0 ) ) ) )
10 eqid 
 |-  ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) )
11 10 i1fpos 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) e. dom S.1 )
12 0re 
 |-  0 e. RR
13 1 ffvelcdmda 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( F ` x ) e. RR )
14 max1 
 |-  ( ( 0 e. RR /\ ( F ` x ) e. RR ) -> 0 <_ if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) )
15 12 13 14 sylancr 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> 0 <_ if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) )
16 15 ralrimiva 
 |-  ( F e. dom S.1 -> A. x e. RR 0 <_ if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) )
17 reex 
 |-  RR e. _V
18 17 a1i 
 |-  ( F e. dom S.1 -> RR e. _V )
19 12 a1i 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> 0 e. RR )
20 fvex 
 |-  ( F ` x ) e. _V
21 c0ex 
 |-  0 e. _V
22 20 21 ifex 
 |-  if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) e. _V
23 22 a1i 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) e. _V )
24 fconstmpt 
 |-  ( RR X. { 0 } ) = ( x e. RR |-> 0 )
25 24 a1i 
 |-  ( F e. dom S.1 -> ( RR X. { 0 } ) = ( x e. RR |-> 0 ) )
26 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 ) ) )
27 18 19 23 25 26 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 ) ) )
28 16 27 mpbird 
 |-  ( F e. dom S.1 -> ( RR X. { 0 } ) oR <_ ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) )
29 ax-resscn 
 |-  RR C_ CC
30 29 a1i 
 |-  ( F e. dom S.1 -> RR C_ CC )
31 22 10 fnmpti 
 |-  ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) Fn RR
32 31 a1i 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) Fn RR )
33 30 32 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 ) ) ) )
34 28 33 mpbird 
 |-  ( F e. dom S.1 -> 0p oR <_ ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) )
35 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 ) ) ) )
36 11 34 35 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 ) ) ) )
37 9 36 eqtr3d 
 |-  ( F e. dom S.1 -> ( S.2 ` ( x e. RR |-> if ( ( x e. RR /\ 0 <_ ( F ` x ) ) , ( F ` x ) , 0 ) ) ) = ( S.1 ` ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) )
38 itg1cl 
 |-  ( ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) e. dom S.1 -> ( S.1 ` ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) e. RR )
39 11 38 syl 
 |-  ( F e. dom S.1 -> ( S.1 ` ( x e. RR |-> if ( 0 <_ ( F ` x ) , ( F ` x ) , 0 ) ) ) e. RR )
40 37 39 eqeltrd 
 |-  ( F e. dom S.1 -> ( S.2 ` ( x e. RR |-> if ( ( x e. RR /\ 0 <_ ( F ` x ) ) , ( F ` x ) , 0 ) ) ) e. RR )
41 5 biantrurd 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( 0 <_ -u ( F ` x ) <-> ( x e. RR /\ 0 <_ -u ( F ` x ) ) ) )
42 41 ifbid 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) = if ( ( x e. RR /\ 0 <_ -u ( F ` x ) ) , -u ( F ` x ) , 0 ) )
43 42 mpteq2dva 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( ( x e. RR /\ 0 <_ -u ( F ` x ) ) , -u ( F ` x ) , 0 ) ) )
44 43 fveq2d 
 |-  ( F e. dom S.1 -> ( S.2 ` ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. RR /\ 0 <_ -u ( F ` x ) ) , -u ( F ` x ) , 0 ) ) ) )
45 neg1rr 
 |-  -u 1 e. RR
46 45 a1i 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> -u 1 e. RR )
47 fconstmpt 
 |-  ( RR X. { -u 1 } ) = ( x e. RR |-> -u 1 )
48 47 a1i 
 |-  ( F e. dom S.1 -> ( RR X. { -u 1 } ) = ( x e. RR |-> -u 1 ) )
49 18 46 13 48 2 offval2 
 |-  ( F e. dom S.1 -> ( ( RR X. { -u 1 } ) oF x. F ) = ( x e. RR |-> ( -u 1 x. ( F ` x ) ) ) )
50 13 recnd 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( F ` x ) e. CC )
51 50 mulm1d 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> ( -u 1 x. ( F ` x ) ) = -u ( F ` x ) )
52 51 mpteq2dva 
 |-  ( F e. dom S.1 -> ( x e. RR |-> ( -u 1 x. ( F ` x ) ) ) = ( x e. RR |-> -u ( F ` x ) ) )
53 49 52 eqtrd 
 |-  ( F e. dom S.1 -> ( ( RR X. { -u 1 } ) oF x. F ) = ( x e. RR |-> -u ( F ` x ) ) )
54 id 
 |-  ( F e. dom S.1 -> F e. dom S.1 )
55 45 a1i 
 |-  ( F e. dom S.1 -> -u 1 e. RR )
56 54 55 i1fmulc 
 |-  ( F e. dom S.1 -> ( ( RR X. { -u 1 } ) oF x. F ) e. dom S.1 )
57 53 56 eqeltrrd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> -u ( F ` x ) ) e. dom S.1 )
58 57 i1fposd 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) e. dom S.1 )
59 13 renegcld 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> -u ( F ` x ) e. RR )
60 max1 
 |-  ( ( 0 e. RR /\ -u ( F ` x ) e. RR ) -> 0 <_ if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) )
61 12 59 60 sylancr 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> 0 <_ if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) )
62 61 ralrimiva 
 |-  ( F e. dom S.1 -> A. x e. RR 0 <_ if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) )
63 negex 
 |-  -u ( F ` x ) e. _V
64 63 21 ifex 
 |-  if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) e. _V
65 64 a1i 
 |-  ( ( F e. dom S.1 /\ x e. RR ) -> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) e. _V )
66 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 ) ) )
67 18 19 65 25 66 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 ) ) )
68 62 67 mpbird 
 |-  ( F e. dom S.1 -> ( RR X. { 0 } ) oR <_ ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) )
69 eqid 
 |-  ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) )
70 64 69 fnmpti 
 |-  ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) Fn RR
71 70 a1i 
 |-  ( F e. dom S.1 -> ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) Fn RR )
72 30 71 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 ) ) ) )
73 68 72 mpbird 
 |-  ( F e. dom S.1 -> 0p oR <_ ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) )
74 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 ) ) ) )
75 58 73 74 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 ) ) ) )
76 44 75 eqtr3d 
 |-  ( F e. dom S.1 -> ( S.2 ` ( x e. RR |-> if ( ( x e. RR /\ 0 <_ -u ( F ` x ) ) , -u ( F ` x ) , 0 ) ) ) = ( S.1 ` ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) )
77 itg1cl 
 |-  ( ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) e. dom S.1 -> ( S.1 ` ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) e. RR )
78 58 77 syl 
 |-  ( F e. dom S.1 -> ( S.1 ` ( x e. RR |-> if ( 0 <_ -u ( F ` x ) , -u ( F ` x ) , 0 ) ) ) e. RR )
79 76 78 eqeltrd 
 |-  ( F e. dom S.1 -> ( S.2 ` ( x e. RR |-> if ( ( x e. RR /\ 0 <_ -u ( F ` x ) ) , -u ( F ` x ) , 0 ) ) ) e. RR )
80 13 iblrelem 
 |-  ( F e. dom S.1 -> ( ( x e. RR |-> ( F ` x ) ) e. L^1 <-> ( ( x e. RR |-> ( F ` x ) ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( ( x e. RR /\ 0 <_ ( F ` x ) ) , ( F ` x ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. RR /\ 0 <_ -u ( F ` x ) ) , -u ( F ` x ) , 0 ) ) ) e. RR ) ) )
81 4 40 79 80 mpbir3and 
 |-  ( F e. dom S.1 -> ( x e. RR |-> ( F ` x ) ) e. L^1 )
82 2 81 eqeltrd 
 |-  ( F e. dom S.1 -> F e. L^1 )