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 ‘ 𝐹 ) )