Theorem iblsub

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

	Ref	Expression
Hypotheses	itgadd.1	|- ( ( ph /\ x e. A ) -> B e. V )
	itgadd.2	|- ( ph -> ( x e. A |-> B ) e. L^1 )
	itgadd.3	|- ( ( ph /\ x e. A ) -> C e. V )
	itgadd.4	|- ( ph -> ( x e. A |-> C ) e. L^1 )
Assertion	iblsub	|- ( ph -> ( x e. A |-> ( B - C ) ) e. L^1 )

Proof

Step	Hyp	Ref	Expression
1		itgadd.1	|- ( ( ph /\ x e. A ) -> B e. V )
2		itgadd.2	|- ( ph -> ( x e. A |-> B ) e. L^1 )
3		itgadd.3	|- ( ( ph /\ x e. A ) -> C e. V )
4		itgadd.4	|- ( ph -> ( x e. A |-> C ) e. L^1 )
5		iblmbf	|- ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
6	2 5	syl	|- ( ph -> ( x e. A |-> B ) e. MblFn )
7	6 1	mbfmptcl	|- ( ( ph /\ x e. A ) -> B e. CC )
8		iblmbf	|- ( ( x e. A |-> C ) e. L^1 -> ( x e. A |-> C ) e. MblFn )
9	4 8	syl	|- ( ph -> ( x e. A |-> C ) e. MblFn )
10	9 3	mbfmptcl	|- ( ( ph /\ x e. A ) -> C e. CC )
11	7 10	negsubd	|- ( ( ph /\ x e. A ) -> ( B + -u C ) = ( B - C ) )
12	11	mpteq2dva	|- ( ph -> ( x e. A |-> ( B + -u C ) ) = ( x e. A |-> ( B - C ) ) )
13	10	negcld	|- ( ( ph /\ x e. A ) -> -u C e. CC )
14	3 4	iblneg	|- ( ph -> ( x e. A |-> -u C ) e. L^1 )
15	7 2 13 14	ibladd	|- ( ph -> ( x e. A |-> ( B + -u C ) ) e. L^1 )
16	12 15	eqeltrrd	|- ( ph -> ( x e. A |-> ( B - C ) ) e. L^1 )