This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐹 ∈ dom ∫1 → ∫ ℝ ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( ∫1 ‘ 𝐹 ) )

Proof

Step Hyp Ref Expression
1 i1ff ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
2 1 ffvelcdmda ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
3 1 feqmptd ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
4 i1fibl ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 ∈ 𝐿1 )
5 3 4 eqeltrrd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐿1 )
6 2 5 itgreval ⊢ ( 𝐹 ∈ dom ∫1 → ∫ ℝ ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( ∫ ℝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 − ∫ ℝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 ) )
7 0re ⊢ 0 ∈ ℝ
8 ifcl ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℝ )
9 2 7 8 sylancl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℝ )
10 max1 ⊢ ( ( 0 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
11 7 2 10 sylancr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
12 id ⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 ∈ dom ∫1 )
13 3 12 eqeltrrd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ∈ dom ∫1 )
14 13 i1fposd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 )
15 i1fibl ⊢ ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 )
16 14 15 syl ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 )
17 9 11 16 itgitg2 ⊢ ( 𝐹 ∈ dom ∫1 → ∫ ℝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
18 11 ralrimiva ⊢ ( 𝐹 ∈ dom ∫1 → ∀ 𝑥 ∈ ℝ 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
19 reex ⊢ ℝ ∈ V
20 19 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ℝ ∈ V )
21 7 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℝ )
22 fconstmpt ⊢ ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 )
23 22 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ( ℝ × { 0 } ) = ( 𝑥 ∈ ℝ ↦ 0 ) )
24 eqidd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
25 20 21 9 23 24 ofrfval2 ⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ 0 ≤ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
26 18 25 mpbird ⊢ ( 𝐹 ∈ dom ∫1 → ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
27 ax-resscn ⊢ ℝ ⊆ ℂ
28 27 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ℝ ⊆ ℂ )
29 9 fmpttd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ℝ )
30 29 ffnd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) Fn ℝ )
31 28 30 0pledm ⊢ ( 𝐹 ∈ dom ∫1 → ( 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
32 26 31 mpbird ⊢ ( 𝐹 ∈ dom ∫1 → 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
33 itg2itg1 ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
34 14 32 33 syl2anc ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
35 17 34 eqtrd ⊢ ( 𝐹 ∈ dom ∫1 → ∫ ℝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
36 2 renegcld ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → - ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
37 ifcl ⊢ ( ( - ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℝ )
38 36 7 37 sylancl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ℝ )
39 max1 ⊢ ( ( 0 ∈ ℝ ∧ - ( 𝐹 ‘ 𝑥 ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) )
40 7 36 39 sylancr ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) )
41 neg1rr ⊢ - 1 ∈ ℝ
42 41 a1i ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → - 1 ∈ ℝ )
43 fconstmpt ⊢ ( ℝ × { - 1 } ) = ( 𝑥 ∈ ℝ ↦ - 1 )
44 43 a1i ⊢ ( 𝐹 ∈ dom ∫1 → ( ℝ × { - 1 } ) = ( 𝑥 ∈ ℝ ↦ - 1 ) )
45 20 42 2 44 3 offval2 ⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { - 1 } ) ∘f · 𝐹 ) = ( 𝑥 ∈ ℝ ↦ ( - 1 · ( 𝐹 ‘ 𝑥 ) ) ) )
46 2 recnd ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
47 46 mulm1d ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( - 1 · ( 𝐹 ‘ 𝑥 ) ) = - ( 𝐹 ‘ 𝑥 ) )
48 47 mpteq2dva ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ ( - 1 · ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ ↦ - ( 𝐹 ‘ 𝑥 ) ) )
49 45 48 eqtrd ⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { - 1 } ) ∘f · 𝐹 ) = ( 𝑥 ∈ ℝ ↦ - ( 𝐹 ‘ 𝑥 ) ) )
50 41 a1i ⊢ ( 𝐹 ∈ dom ∫1 → - 1 ∈ ℝ )
51 12 50 i1fmulc ⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { - 1 } ) ∘f · 𝐹 ) ∈ dom ∫1 )
52 49 51 eqeltrrd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ - ( 𝐹 ‘ 𝑥 ) ) ∈ dom ∫1 )
53 52 i1fposd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 )
54 i1fibl ⊢ ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 )
55 53 54 syl ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ 𝐿1 )
56 38 40 55 itgitg2 ⊢ ( 𝐹 ∈ dom ∫1 → ∫ ℝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
57 40 ralrimiva ⊢ ( 𝐹 ∈ dom ∫1 → ∀ 𝑥 ∈ ℝ 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) )
58 eqidd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
59 20 21 38 23 58 ofrfval2 ⊢ ( 𝐹 ∈ dom ∫1 → ( ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ 0 ≤ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
60 57 59 mpbird ⊢ ( 𝐹 ∈ dom ∫1 → ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
61 38 fmpttd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ℝ )
62 61 ffnd ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) Fn ℝ )
63 28 62 0pledm ⊢ ( 𝐹 ∈ dom ∫1 → ( 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ( ℝ × { 0 } ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
64 60 63 mpbird ⊢ ( 𝐹 ∈ dom ∫1 → 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
65 itg2itg1 ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∈ dom ∫1 ∧ 0𝑝 ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
66 53 64 65 syl2anc ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
67 56 66 eqtrd ⊢ ( 𝐹 ∈ dom ∫1 → ∫ ℝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 = ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
68 35 67 oveq12d ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫ ℝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 − ∫ ℝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 ) = ( ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) − ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) )
69 itg1sub ⊢ ( ( ( 𝑥 ∈ ℝ ↦ 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 ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘f − ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) = ( ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) − ( ∫1 ‘ ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) )
71 68 70 eqtr4d ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫ ℝ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 − ∫ ℝ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) d 𝑥 ) = ( ∫1 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘f − ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) )
72 max0sub ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ → ( if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) − if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝐹 ‘ 𝑥 ) )
73 2 72 syl ⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝑥 ∈ ℝ ) → ( if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) − if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝐹 ‘ 𝑥 ) )
74 73 mpteq2dva ⊢ ( 𝐹 ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ ( if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) − if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
75 20 9 38 24 58 offval2 ⊢ ( 𝐹 ∈ dom ∫1 → ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘f − ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) − if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
76 74 75 3 3eqtr4d ⊢ ( 𝐹 ∈ dom ∫1 → ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘f − ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = 𝐹 )
77 76 fveq2d ⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘f − ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ - ( 𝐹 ‘ 𝑥 ) , - ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) = ( ∫1 ‘ 𝐹 ) )
78 6 71 77 3eqtrd ⊢ ( 𝐹 ∈ dom ∫1 → ∫ ℝ ( 𝐹 ‘ 𝑥 ) d 𝑥 = ( ∫1 ‘ 𝐹 ) )