ibladd

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	ibladd	$⊢ φ \to (x \in A ⟼ B + C) \in 𝐿^{1}$

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		eqid	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (B)), ℜ (B), 0))) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (B)), ℜ (B), 0)))$
6		eqid	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (B)), - ℜ (B), 0))) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (B)), - ℜ (B), 0)))$
7		eqid	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (B)), ℑ (B), 0))) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (B)), ℑ (B), 0)))$
8		eqid	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (B)), - ℑ (B), 0))) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (B)), - ℑ (B), 0)))$
9	5 6 7 8 1	iblcnlem	$⊢ φ \to ((x \in A ⟼ B) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ B) \in MblFn \land (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (B)), ℜ (B), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (B)), - ℜ (B), 0))) \in ℝ) \land (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (B)), ℑ (B), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (B)), - ℑ (B), 0))) \in ℝ)))$
10	2 9	mpbid	$⊢ φ \to ((x \in A ⟼ B) \in MblFn \land (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (B)), ℜ (B), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (B)), - ℜ (B), 0))) \in ℝ) \land (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (B)), ℑ (B), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (B)), - ℑ (B), 0))) \in ℝ))$
11	10	simp1d	$⊢ φ \to (x \in A ⟼ B) \in MblFn$
12	11 1	mbfdm2	$⊢ φ \to A \in dom vol$
13		eqidd	$⊢ φ \to (x \in A ⟼ B) = (x \in A ⟼ B)$
14		eqidd	$⊢ φ \to (x \in A ⟼ C) = (x \in A ⟼ C)$
15	12 1 3 13 14	offval2	$⊢ φ \to (x \in A ⟼ B) +_{f} (x \in A ⟼ C) = (x \in A ⟼ B + C)$
16		eqid	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (C)), ℜ (C), 0))) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (C)), ℜ (C), 0)))$
17		eqid	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (C)), - ℜ (C), 0))) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (C)), - ℜ (C), 0)))$
18		eqid	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (C)), ℑ (C), 0))) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (C)), ℑ (C), 0)))$
19		eqid	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (C)), - ℑ (C), 0))) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (C)), - ℑ (C), 0)))$
20	16 17 18 19 3	iblcnlem	$⊢ φ \to ((x \in A ⟼ C) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ C) \in MblFn \land (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (C)), ℜ (C), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (C)), - ℜ (C), 0))) \in ℝ) \land (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (C)), ℑ (C), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (C)), - ℑ (C), 0))) \in ℝ)))$
21	4 20	mpbid	$⊢ φ \to ((x \in A ⟼ C) \in MblFn \land (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (C)), ℜ (C), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (C)), - ℜ (C), 0))) \in ℝ) \land (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (C)), ℑ (C), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (C)), - ℑ (C), 0))) \in ℝ))$
22	21	simp1d	$⊢ φ \to (x \in A ⟼ C) \in MblFn$
23	11 22	mbfadd	$⊢ φ \to (x \in A ⟼ B) +_{f} (x \in A ⟼ C) \in MblFn$
24	15 23	eqeltrrd	$⊢ φ \to (x \in A ⟼ B + C) \in MblFn$
25	11 1	mbfmptcl	$⊢ (φ \land x \in A) \to B \in ℂ$
26	25	recld	$⊢ (φ \land x \in A) \to ℜ (B) \in ℝ$
27	22 3	mbfmptcl	$⊢ (φ \land x \in A) \to C \in ℂ$
28	27	recld	$⊢ (φ \land x \in A) \to ℜ (C) \in ℝ$
29	25 27	readdd	$⊢ (φ \land x \in A) \to ℜ (B + C) = ℜ (B) + ℜ (C)$
30	25	ismbfcn2	$⊢ φ \to ((x \in A ⟼ B) \in MblFn \leftrightarrow ((x \in A ⟼ ℜ (B)) \in MblFn \land (x \in A ⟼ ℑ (B)) \in MblFn))$
31	11 30	mpbid	$⊢ φ \to ((x \in A ⟼ ℜ (B)) \in MblFn \land (x \in A ⟼ ℑ (B)) \in MblFn)$
32	31	simpld	$⊢ φ \to (x \in A ⟼ ℜ (B)) \in MblFn$
33	27	ismbfcn2	$⊢ φ \to ((x \in A ⟼ C) \in MblFn \leftrightarrow ((x \in A ⟼ ℜ (C)) \in MblFn \land (x \in A ⟼ ℑ (C)) \in MblFn))$
34	22 33	mpbid	$⊢ φ \to ((x \in A ⟼ ℜ (C)) \in MblFn \land (x \in A ⟼ ℑ (C)) \in MblFn)$
35	34	simpld	$⊢ φ \to (x \in A ⟼ ℜ (C)) \in MblFn$
36	10	simp2d	$⊢ φ \to (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (B)), ℜ (B), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (B)), - ℜ (B), 0))) \in ℝ)$
37	36	simpld	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (B)), ℜ (B), 0))) \in ℝ$
38	21	simp2d	$⊢ φ \to (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (C)), ℜ (C), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (C)), - ℜ (C), 0))) \in ℝ)$
39	38	simpld	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (C)), ℜ (C), 0))) \in ℝ$
40	26 28 29 32 35 37 39	ibladdlem	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (B + C)), ℜ (B + C), 0))) \in ℝ$
41	26	renegcld	$⊢ (φ \land x \in A) \to - ℜ (B) \in ℝ$
42	28	renegcld	$⊢ (φ \land x \in A) \to - ℜ (C) \in ℝ$
43	29	negeqd	$⊢ (φ \land x \in A) \to - ℜ (B + C) = - (ℜ (B) + ℜ (C))$
44	26	recnd	$⊢ (φ \land x \in A) \to ℜ (B) \in ℂ$
45	28	recnd	$⊢ (φ \land x \in A) \to ℜ (C) \in ℂ$
46	44 45	negdid	$⊢ (φ \land x \in A) \to - (ℜ (B) + ℜ (C)) = - ℜ (B) + (- ℜ (C))$
47	43 46	eqtrd	$⊢ (φ \land x \in A) \to - ℜ (B + C) = - ℜ (B) + (- ℜ (C))$
48	26 32	mbfneg	$⊢ φ \to (x \in A ⟼ - ℜ (B)) \in MblFn$
49	28 35	mbfneg	$⊢ φ \to (x \in A ⟼ - ℜ (C)) \in MblFn$
50	36	simprd	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (B)), - ℜ (B), 0))) \in ℝ$
51	38	simprd	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (C)), - ℜ (C), 0))) \in ℝ$
52	41 42 47 48 49 50 51	ibladdlem	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (B + C)), - ℜ (B + C), 0))) \in ℝ$
53	40 52	jca	$⊢ φ \to (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (B + C)), ℜ (B + C), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (B + C)), - ℜ (B + C), 0))) \in ℝ)$
54	25	imcld	$⊢ (φ \land x \in A) \to ℑ (B) \in ℝ$
55	27	imcld	$⊢ (φ \land x \in A) \to ℑ (C) \in ℝ$
56	25 27	imaddd	$⊢ (φ \land x \in A) \to ℑ (B + C) = ℑ (B) + ℑ (C)$
57	31	simprd	$⊢ φ \to (x \in A ⟼ ℑ (B)) \in MblFn$
58	34	simprd	$⊢ φ \to (x \in A ⟼ ℑ (C)) \in MblFn$
59	10	simp3d	$⊢ φ \to (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (B)), ℑ (B), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (B)), - ℑ (B), 0))) \in ℝ)$
60	59	simpld	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (B)), ℑ (B), 0))) \in ℝ$
61	21	simp3d	$⊢ φ \to (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (C)), ℑ (C), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (C)), - ℑ (C), 0))) \in ℝ)$
62	61	simpld	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (C)), ℑ (C), 0))) \in ℝ$
63	54 55 56 57 58 60 62	ibladdlem	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (B + C)), ℑ (B + C), 0))) \in ℝ$
64	54	renegcld	$⊢ (φ \land x \in A) \to - ℑ (B) \in ℝ$
65	55	renegcld	$⊢ (φ \land x \in A) \to - ℑ (C) \in ℝ$
66	56	negeqd	$⊢ (φ \land x \in A) \to - ℑ (B + C) = - (ℑ (B) + ℑ (C))$
67	54	recnd	$⊢ (φ \land x \in A) \to ℑ (B) \in ℂ$
68	55	recnd	$⊢ (φ \land x \in A) \to ℑ (C) \in ℂ$
69	67 68	negdid	$⊢ (φ \land x \in A) \to - (ℑ (B) + ℑ (C)) = - ℑ (B) + (- ℑ (C))$
70	66 69	eqtrd	$⊢ (φ \land x \in A) \to - ℑ (B + C) = - ℑ (B) + (- ℑ (C))$
71	54 57	mbfneg	$⊢ φ \to (x \in A ⟼ - ℑ (B)) \in MblFn$
72	55 58	mbfneg	$⊢ φ \to (x \in A ⟼ - ℑ (C)) \in MblFn$
73	59	simprd	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (B)), - ℑ (B), 0))) \in ℝ$
74	61	simprd	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (C)), - ℑ (C), 0))) \in ℝ$
75	64 65 70 71 72 73 74	ibladdlem	$⊢ φ \to \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (B + C)), - ℑ (B + C), 0))) \in ℝ$
76	63 75	jca	$⊢ φ \to (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (B + C)), ℑ (B + C), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (B + C)), - ℑ (B + C), 0))) \in ℝ)$
77		eqid	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (B + C)), ℜ (B + C), 0))) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (B + C)), ℜ (B + C), 0)))$
78		eqid	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (B + C)), - ℜ (B + C), 0))) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (B + C)), - ℜ (B + C), 0)))$
79		eqid	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (B + C)), ℑ (B + C), 0))) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (B + C)), ℑ (B + C), 0)))$
80		eqid	$⊢ \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (B + C)), - ℑ (B + C), 0))) = \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (B + C)), - ℑ (B + C), 0)))$
81		ovexd	$⊢ (φ \land x \in A) \to B + C \in V$
82	77 78 79 80 81	iblcnlem	$⊢ φ \to ((x \in A ⟼ B + C) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ B + C) \in MblFn \land (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℜ (B + C)), ℜ (B + C), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℜ (B + C)), - ℜ (B + C), 0))) \in ℝ) \land (\int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq ℑ (B + C)), ℑ (B + C), 0))) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if ((x \in A \land 0 \leq - ℑ (B + C)), - ℑ (B + C), 0))) \in ℝ)))$
83	24 53 76 82	mpbir3and	$⊢ φ \to (x \in A ⟼ B + C) \in 𝐿^{1}$

Metamath Proof Explorer

Theorem ibladd

Proof