itgaddnc

Description: Choice-free analogue of itgadd . (Contributed by Brendan Leahy, 11-Nov-2017)

	Ref	Expression
Hypotheses	ibladdnc.1	$⊢ (φ \land x \in A) \to B \in V$
	ibladdnc.2	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
	ibladdnc.3	$⊢ (φ \land x \in A) \to C \in V$
	ibladdnc.4	$⊢ φ \to (x \in A ⟼ C) \in 𝐿^{1}$
	ibladdnc.m	$⊢ φ \to (x \in A ⟼ B + C) \in MblFn$
Assertion	itgaddnc	$⊢ φ \to \int_{A} (B + C) d x = \int_{A} B d x + \int_{A} C d x$

Proof

Step	Hyp	Ref	Expression
1		ibladdnc.1	$⊢ (φ \land x \in A) \to B \in V$
2		ibladdnc.2	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
3		ibladdnc.3	$⊢ (φ \land x \in A) \to C \in V$
4		ibladdnc.4	$⊢ φ \to (x \in A ⟼ C) \in 𝐿^{1}$
5		ibladdnc.m	$⊢ φ \to (x \in A ⟼ B + C) \in MblFn$
6		iblmbf	$⊢ (x \in A ⟼ B) \in 𝐿^{1} \to (x \in A ⟼ B) \in MblFn$
7	2 6	syl	$⊢ φ \to (x \in A ⟼ B) \in MblFn$
8	7 1	mbfmptcl	$⊢ (φ \land x \in A) \to B \in ℂ$
9		iblmbf	$⊢ (x \in A ⟼ C) \in 𝐿^{1} \to (x \in A ⟼ C) \in MblFn$
10	4 9	syl	$⊢ φ \to (x \in A ⟼ C) \in MblFn$
11	10 3	mbfmptcl	$⊢ (φ \land x \in A) \to C \in ℂ$
12	8 11	readdd	$⊢ (φ \land x \in A) \to ℜ (B + C) = ℜ (B) + ℜ (C)$
13	12	itgeq2dv	$⊢ φ \to \int_{A} ℜ (B + C) d x = \int_{A} (ℜ (B) + ℜ (C)) d x$
14	8	recld	$⊢ (φ \land x \in A) \to ℜ (B) \in ℝ$
15	8	iblcn	$⊢ φ \to ((x \in A ⟼ B) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ ℜ (B)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (B)) \in 𝐿^{1}))$
16	2 15	mpbid	$⊢ φ \to ((x \in A ⟼ ℜ (B)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (B)) \in 𝐿^{1})$
17	16	simpld	$⊢ φ \to (x \in A ⟼ ℜ (B)) \in 𝐿^{1}$
18	11	recld	$⊢ (φ \land x \in A) \to ℜ (C) \in ℝ$
19	11	iblcn	$⊢ φ \to ((x \in A ⟼ C) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ ℜ (C)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (C)) \in 𝐿^{1}))$
20	4 19	mpbid	$⊢ φ \to ((x \in A ⟼ ℜ (C)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (C)) \in 𝐿^{1})$
21	20	simpld	$⊢ φ \to (x \in A ⟼ ℜ (C)) \in 𝐿^{1}$
22	8 11	addcld	$⊢ (φ \land x \in A) \to B + C \in ℂ$
23		eqidd	$⊢ φ \to (x \in A ⟼ B + C) = (x \in A ⟼ B + C)$
24		ref	$⊢ ℜ : ℂ ⟶ ℝ$
25	24	a1i	$⊢ φ \to ℜ : ℂ ⟶ ℝ$
26	25	feqmptd	$⊢ φ \to ℜ = (y \in ℂ ⟼ ℜ (y))$
27		fveq2	$⊢ y = B + C \to ℜ (y) = ℜ (B + C)$
28	22 23 26 27	fmptco	$⊢ φ \to ℜ \circ (x \in A ⟼ B + C) = (x \in A ⟼ ℜ (B + C))$
29	12	mpteq2dva	$⊢ φ \to (x \in A ⟼ ℜ (B + C)) = (x \in A ⟼ ℜ (B) + ℜ (C))$
30	28 29	eqtrd	$⊢ φ \to ℜ \circ (x \in A ⟼ B + C) = (x \in A ⟼ ℜ (B) + ℜ (C))$
31	22	fmpttd	$⊢ φ \to (x \in A ⟼ B + C) : A ⟶ ℂ$
32		ismbfcn	$⊢ (x \in A ⟼ B + C) : A ⟶ ℂ \to ((x \in A ⟼ B + C) \in MblFn \leftrightarrow (ℜ \circ (x \in A ⟼ B + C) \in MblFn \land ℑ \circ (x \in A ⟼ B + C) \in MblFn))$
33	31 32	syl	$⊢ φ \to ((x \in A ⟼ B + C) \in MblFn \leftrightarrow (ℜ \circ (x \in A ⟼ B + C) \in MblFn \land ℑ \circ (x \in A ⟼ B + C) \in MblFn))$
34	5 33	mpbid	$⊢ φ \to (ℜ \circ (x \in A ⟼ B + C) \in MblFn \land ℑ \circ (x \in A ⟼ B + C) \in MblFn)$
35	34	simpld	$⊢ φ \to ℜ \circ (x \in A ⟼ B + C) \in MblFn$
36	30 35	eqeltrrd	$⊢ φ \to (x \in A ⟼ ℜ (B) + ℜ (C)) \in MblFn$
37	14 17 18 21 36 14 18	itgaddnclem2	$⊢ φ \to \int_{A} (ℜ (B) + ℜ (C)) d x = \int_{A} ℜ (B) d x + \int_{A} ℜ (C) d x$
38	13 37	eqtrd	$⊢ φ \to \int_{A} ℜ (B + C) d x = \int_{A} ℜ (B) d x + \int_{A} ℜ (C) d x$
39	8 11	imaddd	$⊢ (φ \land x \in A) \to ℑ (B + C) = ℑ (B) + ℑ (C)$
40	39	itgeq2dv	$⊢ φ \to \int_{A} ℑ (B + C) d x = \int_{A} (ℑ (B) + ℑ (C)) d x$
41	8	imcld	$⊢ (φ \land x \in A) \to ℑ (B) \in ℝ$
42	16	simprd	$⊢ φ \to (x \in A ⟼ ℑ (B)) \in 𝐿^{1}$
43	11	imcld	$⊢ (φ \land x \in A) \to ℑ (C) \in ℝ$
44	20	simprd	$⊢ φ \to (x \in A ⟼ ℑ (C)) \in 𝐿^{1}$
45		imf	$⊢ ℑ : ℂ ⟶ ℝ$
46	45	a1i	$⊢ φ \to ℑ : ℂ ⟶ ℝ$
47	46	feqmptd	$⊢ φ \to ℑ = (y \in ℂ ⟼ ℑ (y))$
48		fveq2	$⊢ y = B + C \to ℑ (y) = ℑ (B + C)$
49	22 23 47 48	fmptco	$⊢ φ \to ℑ \circ (x \in A ⟼ B + C) = (x \in A ⟼ ℑ (B + C))$
50	39	mpteq2dva	$⊢ φ \to (x \in A ⟼ ℑ (B + C)) = (x \in A ⟼ ℑ (B) + ℑ (C))$
51	49 50	eqtrd	$⊢ φ \to ℑ \circ (x \in A ⟼ B + C) = (x \in A ⟼ ℑ (B) + ℑ (C))$
52	34	simprd	$⊢ φ \to ℑ \circ (x \in A ⟼ B + C) \in MblFn$
53	51 52	eqeltrrd	$⊢ φ \to (x \in A ⟼ ℑ (B) + ℑ (C)) \in MblFn$
54	41 42 43 44 53 41 43	itgaddnclem2	$⊢ φ \to \int_{A} (ℑ (B) + ℑ (C)) d x = \int_{A} ℑ (B) d x + \int_{A} ℑ (C) d x$
55	40 54	eqtrd	$⊢ φ \to \int_{A} ℑ (B + C) d x = \int_{A} ℑ (B) d x + \int_{A} ℑ (C) d x$
56	55	oveq2d	$⊢ φ \to i \int_{A} ℑ (B + C) d x = i (\int_{A} ℑ (B) d x + \int_{A} ℑ (C) d x)$
57		ax-icn	$⊢ i \in ℂ$
58	57	a1i	$⊢ φ \to i \in ℂ$
59	41 42	itgcl	$⊢ φ \to \int_{A} ℑ (B) d x \in ℂ$
60	43 44	itgcl	$⊢ φ \to \int_{A} ℑ (C) d x \in ℂ$
61	58 59 60	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$
62	56 61	eqtrd	$⊢ φ \to i \int_{A} ℑ (B + C) d x = i \int_{A} ℑ (B) d x + i \int_{A} ℑ (C) d x$
63	38 62	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$
64	14 17	itgcl	$⊢ φ \to \int_{A} ℜ (B) d x \in ℂ$
65	18 21	itgcl	$⊢ φ \to \int_{A} ℜ (C) d x \in ℂ$
66		mulcl	$⊢ (i \in ℂ \land \int_{A} ℑ (B) d x \in ℂ) \to i \int_{A} ℑ (B) d x \in ℂ$
67	57 59 66	sylancr	$⊢ φ \to i \int_{A} ℑ (B) d x \in ℂ$
68		mulcl	$⊢ (i \in ℂ \land \int_{A} ℑ (C) d x \in ℂ) \to i \int_{A} ℑ (C) d x \in ℂ$
69	57 60 68	sylancr	$⊢ φ \to i \int_{A} ℑ (C) d x \in ℂ$
70	64 65 67 69	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$
71	63 70	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$
72		ovexd	$⊢ (φ \land x \in A) \to B + C \in V$
73	1 2 3 4 5	ibladdnc	$⊢ φ \to (x \in A ⟼ B + C) \in 𝐿^{1}$
74	72 73	itgcnval	$⊢ φ \to \int_{A} (B + C) d x = \int_{A} ℜ (B + C) d x + i \int_{A} ℑ (B + C) d x$
75	1 2	itgcnval	$⊢ φ \to \int_{A} B d x = \int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x$
76	3 4	itgcnval	$⊢ φ \to \int_{A} C d x = \int_{A} ℜ (C) d x + i \int_{A} ℑ (C) d x$
77	75 76	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$
78	71 74 77	3eqtr4d	$⊢ φ \to \int_{A} (B + C) d x = \int_{A} B d x + \int_{A} C d x$

Metamath Proof Explorer

Theorem itgaddnc

Proof