Theorem itgaddnc

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

	Ref	Expression
Hypotheses	ibladdnc.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
	ibladdnc.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
	ibladdnc.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
	ibladdnc.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
	ibladdnc.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn )
Assertion	itgaddnc	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		ibladdnc.1	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2		ibladdnc.2	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3		ibladdnc.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
4		ibladdnc.4	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
5		ibladdnc.m	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn )
6		iblmbf	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
7	2 6	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
8	7 1	mbfmptcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
9		iblmbf	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
10	4 9	syl	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
11	10 3	mbfmptcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
12	8 11	readdd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 + 𝐶 ) ) = ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) )
13	12	itgeq2dv	⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 = ∫ 𝐴 ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) d 𝑥 )
14	8	recld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
15	8	iblcn	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) ) )
16	2 15	mpbid	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) )
17	16	simpld	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 )
18	11	recld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℝ )
19	11	iblcn	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ 𝐿1 ) ) )
20	4 19	mpbid	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ 𝐿1 ) )
21	20	simpld	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ 𝐿1 )
22	8 11	addcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ ℂ )
23		eqidd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) )
24		ref	⊢ ℜ : ℂ ⟶ ℝ
25	24	a1i	⊢ ( 𝜑 → ℜ : ℂ ⟶ ℝ )
26	25	feqmptd	⊢ ( 𝜑 → ℜ = ( 𝑦 ∈ ℂ ↦ ( ℜ ‘ 𝑦 ) ) )
27		fveq2	⊢ ( 𝑦 = ( 𝐵 + 𝐶 ) → ( ℜ ‘ 𝑦 ) = ( ℜ ‘ ( 𝐵 + 𝐶 ) ) )
28	22 23 26 27	fmptco	⊢ ( 𝜑 → ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) )
29	12	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) ) )
30	28 29	eqtrd	⊢ ( 𝜑 → ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) ) )
31	22	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) : 𝐴 ⟶ ℂ )
32		ismbfcn	⊢ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) : 𝐴 ⟶ ℂ → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn ) ) )
33	31 32	syl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn ) ) )
34	5 33	mpbid	⊢ ( 𝜑 → ( ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn ) )
35	34	simpld	⊢ ( 𝜑 → ( ℜ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn )
36	30 35	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) ) ∈ MblFn )
37	14 17 18 21 36 14 18	itgaddnclem2	⊢ ( 𝜑 → ∫ 𝐴 ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ) )
38	13 37	eqtrd	⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ) )
39	8 11	imaddd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ ( 𝐵 + 𝐶 ) ) = ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) )
40	39	itgeq2dv	⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 = ∫ 𝐴 ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) d 𝑥 )
41	8	imcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
42	16	simprd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 )
43	11	imcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℝ )
44	20	simprd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ 𝐿1 )
45		imf	⊢ ℑ : ℂ ⟶ ℝ
46	45	a1i	⊢ ( 𝜑 → ℑ : ℂ ⟶ ℝ )
47	46	feqmptd	⊢ ( 𝜑 → ℑ = ( 𝑦 ∈ ℂ ↦ ( ℑ ‘ 𝑦 ) ) )
48		fveq2	⊢ ( 𝑦 = ( 𝐵 + 𝐶 ) → ( ℑ ‘ 𝑦 ) = ( ℑ ‘ ( 𝐵 + 𝐶 ) ) )
49	22 23 47 48	fmptco	⊢ ( 𝜑 → ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) )
50	39	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) ) )
51	49 50	eqtrd	⊢ ( 𝜑 → ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) = ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) ) )
52	34	simprd	⊢ ( 𝜑 → ( ℑ ∘ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ) ∈ MblFn )
53	51 52	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) ) ∈ MblFn )
54	41 42 43 44 53 41 43	itgaddnclem2	⊢ ( 𝜑 → ∫ 𝐴 ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) d 𝑥 = ( ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) )
55	40 54	eqtrd	⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 = ( ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) )
56	55	oveq2d	⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) = ( i · ( ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) )
57		ax-icn	⊢ i ∈ ℂ
58	57	a1i	⊢ ( 𝜑 → i ∈ ℂ )
59	41 42	itgcl	⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℂ )
60	43 44	itgcl	⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ∈ ℂ )
61	58 59 60	adddid	⊢ ( 𝜑 → ( i · ( ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) = ( ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) )
62	56 61	eqtrd	⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) = ( ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) )
63	38 62	oveq12d	⊢ ( 𝜑 → ( ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) ) = ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ) + ( ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) )
64	14 17	itgcl	⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ∈ ℂ )
65	18 21	itgcl	⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ∈ ℂ )
66		mulcl	⊢ ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
67	57 59 66	sylancr	⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
68		mulcl	⊢ ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ∈ ℂ )
69	57 60 68	sylancr	⊢ ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ∈ ℂ )
70	64 65 67 69	add4d	⊢ ( 𝜑 → ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 ) + ( ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) = ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) + ( ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) )
71	63 70	eqtrd	⊢ ( 𝜑 → ( ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) ) = ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) + ( ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) )
72		ovexd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ V )
73	1 2 3 4 5	ibladdnc	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ 𝐿1 )
74	72 73	itgcnval	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐵 + 𝐶 ) ) d 𝑥 ) ) )
75	1 2	itgcnval	⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
76	3 4	itgcnval	⊢ ( 𝜑 → ∫ 𝐴 𝐶 d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) )
77	75 76	oveq12d	⊢ ( 𝜑 → ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) = ( ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) + ( ∫ 𝐴 ( ℜ ‘ 𝐶 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐶 ) d 𝑥 ) ) ) )
78	71 74 77	3eqtr4d	⊢ ( 𝜑 → ∫ 𝐴 ( 𝐵 + 𝐶 ) d 𝑥 = ( ∫ 𝐴 𝐵 d 𝑥 + ∫ 𝐴 𝐶 d 𝑥 ) )