Theorem iblsub

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	iblsub	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) ) ∈ 𝐿1 )

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	7 10	negsubd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + - 𝐶 ) = ( 𝐵 − 𝐶 ) )
12	11	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) ) )
13	10	negcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - 𝐶 ∈ ℂ )
14	3 4	iblneg	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - 𝐶 ) ∈ 𝐿1 )
15	7 2 13 14	ibladd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + - 𝐶 ) ) ∈ 𝐿1 )
16	12 15	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 − 𝐶 ) ) ∈ 𝐿1 )