Theorem itgsub

Description: Subtract two integrals over the same domain. (Contributed by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Hypotheses	itgadd.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	itgadd.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
	itgadd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
	itgadd.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
Assertion	itgsub	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 − 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 − ∫ 𝐴 𝐶 d 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		itgadd.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2		itgadd.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3		itgadd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
4		itgadd.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
5		iblmbf	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
6	2 5	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
7	6 1	mbfmptcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
8		iblmbf	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
9	4 8	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
10	9 3	mbfmptcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
11	10	negcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐶 ∈ ℂ )
12	3 4	iblneg	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐶 ) ∈ 𝐿1 )
13	7 2 11 12	itgadd	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + - 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 - 𝐶 d 𝑥 ) )
14	3 4	itgneg	⊢ ( 𝜑 → - ∫ 𝐴 𝐶 d 𝑥 = ∫ 𝐴 - 𝐶 d 𝑥 )
15	14	oveq2d	⊢ ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 + - ∫ 𝐴 𝐶 d 𝑥 ) = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 - 𝐶 d 𝑥 ) )
16	13 15	eqtr4d	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + - 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + - ∫ 𝐴 𝐶 d 𝑥 ) )
17	7 10	negsubd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + - 𝐶 ) = ( 𝐵 − 𝐶 ) )
18	17	itgeq2dv	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + - 𝐶 ) d 𝑥 = ∫ 𝐴 ( 𝐵 − 𝐶 ) d 𝑥 )
19	1 2	itgcl	⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ∈ ℂ )
20	3 4	itgcl	⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 ∈ ℂ )
21	19 20	negsubd	⊢ ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 + - ∫ 𝐴 𝐶 d 𝑥 ) = ( ∫ 𝐴 𝐵 d 𝑥 − ∫ 𝐴 𝐶 d 𝑥 ) )
22	16 18 21	3eqtr3d	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 − 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 − ∫ 𝐴 𝐶 d 𝑥 ) )