# Metamath Proof Explorer

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

Ref Expression
Hypotheses ibladdnc.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
ibladdnc.2 ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}$
ibladdnc.3 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in {V}$
ibladdnc.4 ${⊢}{\phi }\to \left({x}\in {A}⟼{C}\right)\in {𝐿}^{1}$
ibladdnc.m ${⊢}{\phi }\to \left({x}\in {A}⟼{B}+{C}\right)\in MblFn$
Assertion itgaddnc ${⊢}{\phi }\to {\int }_{{A}}\left({B}+{C}\right)d{x}={\int }_{{A}}{B}d{x}+{\int }_{{A}}{C}d{x}$

### Proof

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