itgadd

Description: Add two integrals over the same domain. (Contributed by Mario Carneiro, 17-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	itgadd	$⊢ φ \to \int_{A} (B + C) d x = \int_{A} B d x + \int_{A} C d x$

Proof

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	7 10	readdd	$⊢ (φ \land x \in A) \to ℜ (B + C) = ℜ (B) + ℜ (C)$
12	11	itgeq2dv	$⊢ φ \to \int_{A} ℜ (B + C) d x = \int_{A} (ℜ (B) + ℜ (C)) d x$
13	7	recld	$⊢ (φ \land x \in A) \to ℜ (B) \in ℝ$
14	7	iblcn	$⊢ φ \to ((x \in A ⟼ B) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ ℜ (B)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (B)) \in 𝐿^{1}))$
15	2 14	mpbid	$⊢ φ \to ((x \in A ⟼ ℜ (B)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (B)) \in 𝐿^{1})$
16	15	simpld	$⊢ φ \to (x \in A ⟼ ℜ (B)) \in 𝐿^{1}$
17	10	recld	$⊢ (φ \land x \in A) \to ℜ (C) \in ℝ$
18	10	iblcn	$⊢ φ \to ((x \in A ⟼ C) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ ℜ (C)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (C)) \in 𝐿^{1}))$
19	4 18	mpbid	$⊢ φ \to ((x \in A ⟼ ℜ (C)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (C)) \in 𝐿^{1})$
20	19	simpld	$⊢ φ \to (x \in A ⟼ ℜ (C)) \in 𝐿^{1}$
21	13 16 17 20 13 17	itgaddlem2	$⊢ φ \to \int_{A} (ℜ (B) + ℜ (C)) d x = \int_{A} ℜ (B) d x + \int_{A} ℜ (C) d x$
22	12 21	eqtrd	$⊢ φ \to \int_{A} ℜ (B + C) d x = \int_{A} ℜ (B) d x + \int_{A} ℜ (C) d x$
23	7 10	imaddd	$⊢ (φ \land x \in A) \to ℑ (B + C) = ℑ (B) + ℑ (C)$
24	23	itgeq2dv	$⊢ φ \to \int_{A} ℑ (B + C) d x = \int_{A} (ℑ (B) + ℑ (C)) d x$
25	7	imcld	$⊢ (φ \land x \in A) \to ℑ (B) \in ℝ$
26	15	simprd	$⊢ φ \to (x \in A ⟼ ℑ (B)) \in 𝐿^{1}$
27	10	imcld	$⊢ (φ \land x \in A) \to ℑ (C) \in ℝ$
28	19	simprd	$⊢ φ \to (x \in A ⟼ ℑ (C)) \in 𝐿^{1}$
29	25 26 27 28 25 27	itgaddlem2	$⊢ φ \to \int_{A} (ℑ (B) + ℑ (C)) d x = \int_{A} ℑ (B) d x + \int_{A} ℑ (C) d x$
30	24 29	eqtrd	$⊢ φ \to \int_{A} ℑ (B + C) d x = \int_{A} ℑ (B) d x + \int_{A} ℑ (C) d x$
31	30	oveq2d	$⊢ φ \to i \int_{A} ℑ (B + C) d x = i (\int_{A} ℑ (B) d x + \int_{A} ℑ (C) d x)$
32		ax-icn	$⊢ i \in ℂ$
33	32	a1i	$⊢ φ \to i \in ℂ$
34	25 26	itgcl	$⊢ φ \to \int_{A} ℑ (B) d x \in ℂ$
35	27 28	itgcl	$⊢ φ \to \int_{A} ℑ (C) d x \in ℂ$
36	33 34 35	adddid	$⊢ φ \to i (\int_{A} ℑ (B) d x + \int_{A} ℑ (C) d x) = i \int_{A} ℑ (B) d x + i \int_{A} ℑ (C) d x$
37	31 36	eqtrd	$⊢ φ \to i \int_{A} ℑ (B + C) d x = i \int_{A} ℑ (B) d x + i \int_{A} ℑ (C) d x$
38	22 37	oveq12d	$⊢ φ \to \int_{A} ℜ (B + C) d x + i \int_{A} ℑ (B + C) d x = \int_{A} ℜ (B) d x + \int_{A} ℜ (C) d x + i \int_{A} ℑ (B) d x + i \int_{A} ℑ (C) d x$
39	13 16	itgcl	$⊢ φ \to \int_{A} ℜ (B) d x \in ℂ$
40	17 20	itgcl	$⊢ φ \to \int_{A} ℜ (C) d x \in ℂ$
41		mulcl	$⊢ (i \in ℂ \land \int_{A} ℑ (B) d x \in ℂ) \to i \int_{A} ℑ (B) d x \in ℂ$
42	32 34 41	sylancr	$⊢ φ \to i \int_{A} ℑ (B) d x \in ℂ$
43		mulcl	$⊢ (i \in ℂ \land \int_{A} ℑ (C) d x \in ℂ) \to i \int_{A} ℑ (C) d x \in ℂ$
44	32 35 43	sylancr	$⊢ φ \to i \int_{A} ℑ (C) d x \in ℂ$
45	39 40 42 44	add4d	$⊢ φ \to \int_{A} ℜ (B) d x + \int_{A} ℜ (C) d x + i \int_{A} ℑ (B) d x + i \int_{A} ℑ (C) d x = \int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x + \int_{A} ℜ (C) d x + i \int_{A} ℑ (C) d x$
46	38 45	eqtrd	$⊢ φ \to \int_{A} ℜ (B + C) d x + i \int_{A} ℑ (B + C) d x = \int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x + \int_{A} ℜ (C) d x + i \int_{A} ℑ (C) d x$
47		ovexd	$⊢ (φ \land x \in A) \to B + C \in V$
48	1 2 3 4	ibladd	$⊢ φ \to (x \in A ⟼ B + C) \in 𝐿^{1}$
49	47 48	itgcnval	$⊢ φ \to \int_{A} (B + C) d x = \int_{A} ℜ (B + C) d x + i \int_{A} ℑ (B + C) d x$
50	1 2	itgcnval	$⊢ φ \to \int_{A} B d x = \int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x$
51	3 4	itgcnval	$⊢ φ \to \int_{A} C d x = \int_{A} ℜ (C) d x + i \int_{A} ℑ (C) d x$
52	50 51	oveq12d	$⊢ φ \to \int_{A} B d x + \int_{A} C d x = \int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x + \int_{A} ℜ (C) d x + i \int_{A} ℑ (C) d x$
53	46 49 52	3eqtr4d	$⊢ φ \to \int_{A} (B + C) d x = \int_{A} B d x + \int_{A} C d x$

Metamath Proof Explorer

Theorem itgadd

Proof