Theorem itg1sub

Description: The integral of a difference of two simple functions. (Contributed by Mario Carneiro, 6-Aug-2014)

	Ref	Expression
Assertion	itg1sub	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( 𝐹 ∘f − 𝐺 ) ) = ( ( ∫1 ‘ 𝐹 ) − ( ∫1 ‘ 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐹 ∈ dom ∫1 )
2		simpr	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → 𝐺 ∈ dom ∫1 )
3		neg1rr	⊢ - 1 ∈ ℝ
4	3	a1i	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → - 1 ∈ ℝ )
5	2 4	i1fmulc	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ∈ dom ∫1 )
6	1 5	itg1add	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( 𝐹 ∘f + ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( ( ∫1 ‘ 𝐹 ) + ( ∫1 ‘ ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) ) )
7	2 4	itg1mulc	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) = ( - 1 · ( ∫1 ‘ 𝐺 ) ) )
8		itg1cl	⊢ ( 𝐺 ∈ dom ∫1 → ( ∫1 ‘ 𝐺 ) ∈ ℝ )
9	8	recnd	⊢ ( 𝐺 ∈ dom ∫1 → ( ∫1 ‘ 𝐺 ) ∈ ℂ )
10	2 9	syl	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ 𝐺 ) ∈ ℂ )
11	10	mulm1d	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( - 1 · ( ∫1 ‘ 𝐺 ) ) = - ( ∫1 ‘ 𝐺 ) )
12	7 11	eqtrd	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) = - ( ∫1 ‘ 𝐺 ) )
13	12	oveq2d	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ( ∫1 ‘ 𝐹 ) + ( ∫1 ‘ ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( ( ∫1 ‘ 𝐹 ) + - ( ∫1 ‘ 𝐺 ) ) )
14	6 13	eqtrd	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( 𝐹 ∘f + ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( ( ∫1 ‘ 𝐹 ) + - ( ∫1 ‘ 𝐺 ) ) )
15		reex	⊢ ℝ ∈ V
16		i1ff	⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℝ )
17		ax-resscn	⊢ ℝ ⊆ ℂ
18		fss	⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐹 : ℝ ⟶ ℂ )
19	16 17 18	sylancl	⊢ ( 𝐹 ∈ dom ∫1 → 𝐹 : ℝ ⟶ ℂ )
20		i1ff	⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℝ )
21		fss	⊢ ( ( 𝐺 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐺 : ℝ ⟶ ℂ )
22	20 17 21	sylancl	⊢ ( 𝐺 ∈ dom ∫1 → 𝐺 : ℝ ⟶ ℂ )
23		ofnegsub	⊢ ( ( ℝ ∈ V ∧ 𝐹 : ℝ ⟶ ℂ ∧ 𝐺 : ℝ ⟶ ℂ ) → ( 𝐹 ∘f + ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )
24	15 19 22 23	mp3an3an	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( 𝐹 ∘f + ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) = ( 𝐹 ∘f − 𝐺 ) )
25	24	fveq2d	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( 𝐹 ∘f + ( ( ℝ × { - 1 } ) ∘f · 𝐺 ) ) ) = ( ∫1 ‘ ( 𝐹 ∘f − 𝐺 ) ) )
26		itg1cl	⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) ∈ ℝ )
27	26	recnd	⊢ ( 𝐹 ∈ dom ∫1 → ( ∫1 ‘ 𝐹 ) ∈ ℂ )
28		negsub	⊢ ( ( ( ∫1 ‘ 𝐹 ) ∈ ℂ ∧ ( ∫1 ‘ 𝐺 ) ∈ ℂ ) → ( ( ∫1 ‘ 𝐹 ) + - ( ∫1 ‘ 𝐺 ) ) = ( ( ∫1 ‘ 𝐹 ) − ( ∫1 ‘ 𝐺 ) ) )
29	27 9 28	syl2an	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ( ∫1 ‘ 𝐹 ) + - ( ∫1 ‘ 𝐺 ) ) = ( ( ∫1 ‘ 𝐹 ) − ( ∫1 ‘ 𝐺 ) ) )
30	14 25 29	3eqtr3d	⊢ ( ( 𝐹 ∈ dom ∫1 ∧ 𝐺 ∈ dom ∫1 ) → ( ∫1 ‘ ( 𝐹 ∘f − 𝐺 ) ) = ( ( ∫1 ‘ 𝐹 ) − ( ∫1 ‘ 𝐺 ) ) )