Metamath Proof Explorer

Theorem i1fibl

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

Ref Expression
Assertion i1fibl ( 𝐹 ∈ dom ∫1 → 𝐹 ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
2 1 feqmptd ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
3 i1fmbf ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 ∈ MblFn )
4 2 3 eqeltrrd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ MblFn )
5 simpr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
6 5 biantrurd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ) )
7 6 ifbid ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( ( 𝑥 ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
8 7 mpteq2dva ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
9 8 fveq2d ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
10 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
11 10 i1fpos ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 )
12 0re ⊢ 0 ∈ ℝ
13 1 ffvelrnda ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
14 max1 ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
15 12 13 14 sylancr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
16 15 ralrimiva ⊢ ( 𝐹 ∈ dom ∫1 → ∀ 𝑥 ∈ ℝ 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
17 reex ⊢ ℝ ∈ V
18 17 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ℝ ∈ V )
19 12 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℝ )
20 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
21 c0ex ⊢ 0 ∈ V
22 20 21 ifex ⊢ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V
23 22 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V )
24 fconstmpt ⊢ ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 )
25 24 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 ) )
26 eqidd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
27 18 19 23 25 26 ofrfval2 ⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
28 16 27 mpbird ⊢ ( 𝐹 ∈ dom ∫1 → ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
29 ax-resscn ⊢ ℝ ⊆ ℂ
30 29 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ℝ ⊆ ℂ )
31 22 10 fnmpti ⊢ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) Fn ℝ
32 31 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) Fn ℝ )
33 30 32 0pledm ⊢ ( 𝐹 ∈ dom ∫1 → ( 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
34 28 33 mpbird ⊢ ( 𝐹 ∈ dom ∫1 → 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
35 itg2itg1 ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
36 11 34 35 syl2anc ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
37 9 36 eqtr3d ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
38 itg1cl ⊢ ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
39 11 38 syl ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
40 37 39 eqeltrd ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
41 5 biantrurd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑥 ∈ ℝ ∧ 0 ≤ - ( 𝐹 ‘ 𝑥 ) ) ) )
42 41 ifbid ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( ( 𝑥 ∈ ℝ ∧ 0 ≤ - ( 𝐹 ‘ 𝑥 ) ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) )
43 42 mpteq2dva ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ℝ ∧ 0 ≤ - ( 𝐹 ‘ 𝑥 ) ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
44 43 fveq2d ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ℝ ∧ 0 ≤ - ( 𝐹 ‘ 𝑥 ) ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
45 neg1rr ⊢ - 1 ∈ ℝ
46 45 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → - 1 ∈ ℝ )
47 fconstmpt ⊢ ( ℝ × { - 1 } ) = ( 𝑥 ∈ ℝ ↦ - 1 )
48 47 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ( ℝ × { - 1 } ) = ( 𝑥 ∈ ℝ ↦ - 1 ) )
49 18 46 13 48 2 offval2 ⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { - 1 } ) ∘f · 𝐹 ) = ( 𝑥 ∈ ℝ ↦ ( - 1 · ( 𝐹 ‘ 𝑥 ) ) ) )
50 13 recnd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
51 50 mulm1d ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( - 1 · ( 𝐹 ‘ 𝑥 ) ) = - ( 𝐹 ‘ 𝑥 ) )
52 51 mpteq2dva ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ ( - 1 · ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ - ( 𝐹 ‘ 𝑥 ) ) )
53 49 52 eqtrd ⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { - 1 } ) ∘f · 𝐹 ) = ( 𝑥 ∈ ℝ ↦ - ( 𝐹 ‘ 𝑥 ) ) )
54 id ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 ∈ dom ∫1 )
55 45 a1i ⊢ ( 𝐹 ∈ dom ∫1 → - 1 ∈ ℝ )
56 54 55 i1fmulc ⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { - 1 } ) ∘f · 𝐹 ) ∈ dom ∫1 )
57 53 56 eqeltrrd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ - ( 𝐹 ‘ 𝑥 ) ) ∈ dom ∫1 )
58 57 i1fposd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 )
59 13 renegcld ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → - ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
60 max1 ⊢ ( ( 0 ∈ ℝ ∧ - ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) )
61 12 59 60 sylancr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) )
62 61 ralrimiva ⊢ ( 𝐹 ∈ dom ∫1 → ∀ 𝑥 ∈ ℝ 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) )
63 negex ⊢ - ( 𝐹 ‘ 𝑥 ) ∈ V
64 63 21 ifex ⊢ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V
65 64 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ V )
66 eqidd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
67 18 19 65 25 66 ofrfval2 ⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
68 62 67 mpbird ⊢ ( 𝐹 ∈ dom ∫1 → ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
69 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) )
70 64 69 fnmpti ⊢ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) Fn ℝ
71 70 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) Fn ℝ )
72 30 71 0pledm ⊢ ( 𝐹 ∈ dom ∫1 → ( 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
73 68 72 mpbird ⊢ ( 𝐹 ∈ dom ∫1 → 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
74 itg2itg1 ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
75 58 73 74 syl2anc ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
76 44 75 eqtr3d ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ℝ ∧ 0 ≤ - ( 𝐹 ‘ 𝑥 ) ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
77 itg1cl ⊢ ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
78 58 77 syl ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
79 76 78 eqeltrd ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ℝ ∧ 0 ≤ - ( 𝐹 ‘ 𝑥 ) ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
80 13 iblrelem ⊢ ( 𝐹 ∈ dom ∫1 → ( ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ ℝ ∧ 0 ≤ - ( 𝐹 ‘ 𝑥 ) ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ ) ) )
81 4 40 79 80 mpbir3and ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
82 2 81 eqeltrd ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 ∈ 𝐿1 )