Theorem iblsub

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

	Ref	Expression
Hypotheses	itgadd.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
	itgadd.2	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
	itgadd.3	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
	itgadd.4	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$
Assertion	iblsub	$$⊢\phi \to \left(x\in A⟼B-C\right)\in {𝐿}^1$$

Proof

Step	Hyp	Ref	Expression
1		itgadd.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
2		itgadd.2	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$
3		itgadd.3	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
4		itgadd.4	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$
5		iblmbf	$$⊢\left(x\in A⟼B\right)\in {𝐿}^1\to \left(x\in A⟼B\right)\in MblFn$$
6	2 5	syl	$$⊢\phi \to \left(x\in A⟼B\right)\in MblFn$$
7	6 1	mbfmptcl	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
8		iblmbf	$$⊢\left(x\in A⟼C\right)\in {𝐿}^1\to \left(x\in A⟼C\right)\in MblFn$$
9	4 8	syl	$$⊢\phi \to \left(x\in A⟼C\right)\in MblFn$$
10	9 3	mbfmptcl	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℂ$$
11	7 10	negsubd	$$⊢\left(\phi \wedge x\in A\right)\to B+\left(-C\right)=B-C$$
12	11	mpteq2dva	$$⊢\phi \to \left(x\in A⟼B+\left(-C\right)\right)=\left(x\in A⟼B-C\right)$$
13	10	negcld	$$⊢\left(\phi \wedge x\in A\right)\to -C\in ℂ$$
14	3 4	iblneg	$$⊢\phi \to \left(x\in A⟼-C\right)\in {𝐿}^1$$
15	7 2 13 14	ibladd	$$⊢\phi \to \left(x\in A⟼B+\left(-C\right)\right)\in {𝐿}^1$$
16	12 15	eqeltrrd	$$⊢\phi \to \left(x\in A⟼B-C\right)\in {𝐿}^1$$