itgsub

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

	Ref	Expression
Hypotheses	itgadd.1	$⊢ (φ \land x \in A) \to B \in V$
	itgadd.2	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
	itgadd.3	$⊢ (φ \land x \in A) \to C \in V$
	itgadd.4	$⊢ φ \to (x \in A ⟼ C) \in 𝐿^{1}$
Assertion	itgsub	$⊢ φ \to \int_{A} (B - C) d x = \int_{A} B d x - \int_{A} C d x$

Step	Hyp	Ref	Expression
1		itgadd.1	$⊢ (φ \land x \in A) \to B \in V$
2		itgadd.2	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
3		itgadd.3	$⊢ (φ \land x \in A) \to C \in V$
4		itgadd.4	$⊢ φ \to (x \in A ⟼ C) \in 𝐿^{1}$
5		iblmbf	$⊢ (x \in A ⟼ B) \in 𝐿^{1} \to (x \in A ⟼ B) \in MblFn$
6	2 5	syl	$⊢ φ \to (x \in A ⟼ B) \in MblFn$
7	6 1	mbfmptcl	$⊢ (φ \land x \in A) \to B \in ℂ$
8		iblmbf	$⊢ (x \in A ⟼ C) \in 𝐿^{1} \to (x \in A ⟼ C) \in MblFn$
9	4 8	syl	$⊢ φ \to (x \in A ⟼ C) \in MblFn$
10	9 3	mbfmptcl	$⊢ (φ \land x \in A) \to C \in ℂ$
11	10	negcld	$⊢ (φ \land x \in A) \to - C \in ℂ$
12	3 4	iblneg	$⊢ φ \to (x \in A ⟼ - C) \in 𝐿^{1}$
13	7 2 11 12	itgadd	$⊢ φ \to \int_{A} (B + (- C)) d x = \int_{A} B d x + \int_{A} (- C) d x$
14	3 4	itgneg	$⊢ φ \to - \int_{A} C d x = \int_{A} (- C) d x$
15	14	oveq2d	$⊢ φ \to \int_{A} B d x + (- \int_{A} C d x) = \int_{A} B d x + \int_{A} (- C) d x$
16	13 15	eqtr4d	$⊢ φ \to \int_{A} (B + (- C)) d x = \int_{A} B d x + (- \int_{A} C d x)$
17	7 10	negsubd	$⊢ (φ \land x \in A) \to B + (- C) = B - C$
18	17	itgeq2dv	$⊢ φ \to \int_{A} (B + (- C)) d x = \int_{A} (B - C) d x$
19	1 2	itgcl	$⊢ φ \to \int_{A} B d x \in ℂ$
20	3 4	itgcl	$⊢ φ \to \int_{A} C d x \in ℂ$
21	19 20	negsubd	$⊢ φ \to \int_{A} B d x + (- \int_{A} C d x) = \int_{A} B d x - \int_{A} C d x$
22	16 18 21	3eqtr3d	$⊢ φ \to \int_{A} (B - C) d x = \int_{A} B d x - \int_{A} C d x$

Metamath Proof Explorer