Metamath Proof Explorer

Theorem itgaddnc

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

Ref Expression
Hypotheses ibladdnc.1 
|- ( ( ph /\ x e. A ) -> B e. V )
ibladdnc.2 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
ibladdnc.3 
|- ( ( ph /\ x e. A ) -> C e. V )
ibladdnc.4 
|- ( ph -> ( x e. A |-> C ) e. L^1 )
ibladdnc.m 
|- ( ph -> ( x e. A |-> ( B + C ) ) e. MblFn )
Assertion itgaddnc 
|- ( ph -> S. A ( B + C ) _d x = ( S. A B _d x + S. A C _d x ) )

Proof

Step Hyp Ref Expression
1 ibladdnc.1 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 ibladdnc.2 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
3 ibladdnc.3 
 |-  ( ( ph /\ x e. A ) -> C e. V )
4 ibladdnc.4 
 |-  ( ph -> ( x e. A |-> C ) e. L^1 )
5 ibladdnc.m 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) e. MblFn )
6 iblmbf 
 |-  ( ( x e. A |-> B ) e. L^1 -> ( x e. A |-> B ) e. MblFn )
7 2 6 syl 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
8 7 1 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
9 iblmbf 
 |-  ( ( x e. A |-> C ) e. L^1 -> ( x e. A |-> C ) e. MblFn )
10 4 9 syl 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )
11 10 3 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
12 8 11 readdd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( B + C ) ) = ( ( Re ` B ) + ( Re ` C ) ) )
13 12 itgeq2dv 
 |-  ( ph -> S. A ( Re ` ( B + C ) ) _d x = S. A ( ( Re ` B ) + ( Re ` C ) ) _d x )
14 8 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR )
15 8 iblcn 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) ) )
16 2 15 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. L^1 /\ ( x e. A |-> ( Im ` B ) ) e. L^1 ) )
17 16 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) e. L^1 )
18 11 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` C ) e. RR )
19 11 iblcn 
 |-  ( ph -> ( ( x e. A |-> C ) e. L^1 <-> ( ( x e. A |-> ( Re ` C ) ) e. L^1 /\ ( x e. A |-> ( Im ` C ) ) e. L^1 ) ) )
20 4 19 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` C ) ) e. L^1 /\ ( x e. A |-> ( Im ` C ) ) e. L^1 ) )
21 20 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` C ) ) e. L^1 )
22 8 11 addcld 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) e. CC )
23 eqidd 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) = ( x e. A |-> ( B + C ) ) )
24 ref 
 |-  Re : CC --> RR
25 24 a1i 
 |-  ( ph -> Re : CC --> RR )
26 25 feqmptd 
 |-  ( ph -> Re = ( y e. CC |-> ( Re ` y ) ) )
27 fveq2 
 |-  ( y = ( B + C ) -> ( Re ` y ) = ( Re ` ( B + C ) ) )
28 22 23 26 27 fmptco 
 |-  ( ph -> ( Re o. ( x e. A |-> ( B + C ) ) ) = ( x e. A |-> ( Re ` ( B + C ) ) ) )
29 12 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( Re ` ( B + C ) ) ) = ( x e. A |-> ( ( Re ` B ) + ( Re ` C ) ) ) )
30 28 29 eqtrd 
 |-  ( ph -> ( Re o. ( x e. A |-> ( B + C ) ) ) = ( x e. A |-> ( ( Re ` B ) + ( Re ` C ) ) ) )
31 22 fmpttd 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) : A --> CC )
32 ismbfcn 
 |-  ( ( x e. A |-> ( B + C ) ) : A --> CC -> ( ( x e. A |-> ( B + C ) ) e. MblFn <-> ( ( Re o. ( x e. A |-> ( B + C ) ) ) e. MblFn /\ ( Im o. ( x e. A |-> ( B + C ) ) ) e. MblFn ) ) )
33 31 32 syl 
 |-  ( ph -> ( ( x e. A |-> ( B + C ) ) e. MblFn <-> ( ( Re o. ( x e. A |-> ( B + C ) ) ) e. MblFn /\ ( Im o. ( x e. A |-> ( B + C ) ) ) e. MblFn ) ) )
34 5 33 mpbid 
 |-  ( ph -> ( ( Re o. ( x e. A |-> ( B + C ) ) ) e. MblFn /\ ( Im o. ( x e. A |-> ( B + C ) ) ) e. MblFn ) )
35 34 simpld 
 |-  ( ph -> ( Re o. ( x e. A |-> ( B + C ) ) ) e. MblFn )
36 30 35 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( ( Re ` B ) + ( Re ` C ) ) ) e. MblFn )
37 14 17 18 21 36 14 18 itgaddnclem2 
 |-  ( ph -> S. A ( ( Re ` B ) + ( Re ` C ) ) _d x = ( S. A ( Re ` B ) _d x + S. A ( Re ` C ) _d x ) )
38 13 37 eqtrd 
 |-  ( ph -> S. A ( Re ` ( B + C ) ) _d x = ( S. A ( Re ` B ) _d x + S. A ( Re ` C ) _d x ) )
39 8 11 imaddd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` ( B + C ) ) = ( ( Im ` B ) + ( Im ` C ) ) )
40 39 itgeq2dv 
 |-  ( ph -> S. A ( Im ` ( B + C ) ) _d x = S. A ( ( Im ` B ) + ( Im ` C ) ) _d x )
41 8 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR )
42 16 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) e. L^1 )
43 11 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` C ) e. RR )
44 20 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` C ) ) e. L^1 )
45 imf 
 |-  Im : CC --> RR
46 45 a1i 
 |-  ( ph -> Im : CC --> RR )
47 46 feqmptd 
 |-  ( ph -> Im = ( y e. CC |-> ( Im ` y ) ) )
48 fveq2 
 |-  ( y = ( B + C ) -> ( Im ` y ) = ( Im ` ( B + C ) ) )
49 22 23 47 48 fmptco 
 |-  ( ph -> ( Im o. ( x e. A |-> ( B + C ) ) ) = ( x e. A |-> ( Im ` ( B + C ) ) ) )
50 39 mpteq2dva 
 |-  ( ph -> ( x e. A |-> ( Im ` ( B + C ) ) ) = ( x e. A |-> ( ( Im ` B ) + ( Im ` C ) ) ) )
51 49 50 eqtrd 
 |-  ( ph -> ( Im o. ( x e. A |-> ( B + C ) ) ) = ( x e. A |-> ( ( Im ` B ) + ( Im ` C ) ) ) )
52 34 simprd 
 |-  ( ph -> ( Im o. ( x e. A |-> ( B + C ) ) ) e. MblFn )
53 51 52 eqeltrrd 
 |-  ( ph -> ( x e. A |-> ( ( Im ` B ) + ( Im ` C ) ) ) e. MblFn )
54 41 42 43 44 53 41 43 itgaddnclem2 
 |-  ( ph -> S. A ( ( Im ` B ) + ( Im ` C ) ) _d x = ( S. A ( Im ` B ) _d x + S. A ( Im ` C ) _d x ) )
55 40 54 eqtrd 
 |-  ( ph -> S. A ( Im ` ( B + C ) ) _d x = ( S. A ( Im ` B ) _d x + S. A ( Im ` C ) _d x ) )
56 55 oveq2d 
 |-  ( ph -> ( _i x. S. A ( Im ` ( B + C ) ) _d x ) = ( _i x. ( S. A ( Im ` B ) _d x + S. A ( Im ` C ) _d x ) ) )
57 ax-icn 
 |-  _i e. CC
58 57 a1i 
 |-  ( ph -> _i e. CC )
59 41 42 itgcl 
 |-  ( ph -> S. A ( Im ` B ) _d x e. CC )
60 43 44 itgcl 
 |-  ( ph -> S. A ( Im ` C ) _d x e. CC )
61 58 59 60 adddid 
 |-  ( ph -> ( _i x. ( S. A ( Im ` B ) _d x + S. A ( Im ` C ) _d x ) ) = ( ( _i x. S. A ( Im ` B ) _d x ) + ( _i x. S. A ( Im ` C ) _d x ) ) )
62 56 61 eqtrd 
 |-  ( ph -> ( _i x. S. A ( Im ` ( B + C ) ) _d x ) = ( ( _i x. S. A ( Im ` B ) _d x ) + ( _i x. S. A ( Im ` C ) _d x ) ) )
63 38 62 oveq12d 
 |-  ( ph -> ( S. A ( Re ` ( B + C ) ) _d x + ( _i x. S. A ( Im ` ( B + C ) ) _d x ) ) = ( ( S. A ( Re ` B ) _d x + S. A ( Re ` C ) _d x ) + ( ( _i x. S. A ( Im ` B ) _d x ) + ( _i x. S. A ( Im ` C ) _d x ) ) ) )
64 14 17 itgcl 
 |-  ( ph -> S. A ( Re ` B ) _d x e. CC )
65 18 21 itgcl 
 |-  ( ph -> S. A ( Re ` C ) _d x e. CC )
66 mulcl 
 |-  ( ( _i e. CC /\ S. A ( Im ` B ) _d x e. CC ) -> ( _i x. S. A ( Im ` B ) _d x ) e. CC )
67 57 59 66 sylancr 
 |-  ( ph -> ( _i x. S. A ( Im ` B ) _d x ) e. CC )
68 mulcl 
 |-  ( ( _i e. CC /\ S. A ( Im ` C ) _d x e. CC ) -> ( _i x. S. A ( Im ` C ) _d x ) e. CC )
69 57 60 68 sylancr 
 |-  ( ph -> ( _i x. S. A ( Im ` C ) _d x ) e. CC )
70 64 65 67 69 add4d 
 |-  ( ph -> ( ( S. A ( Re ` B ) _d x + S. A ( Re ` C ) _d x ) + ( ( _i x. S. A ( Im ` B ) _d x ) + ( _i x. S. A ( Im ` C ) _d x ) ) ) = ( ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) + ( S. A ( Re ` C ) _d x + ( _i x. S. A ( Im ` C ) _d x ) ) ) )
71 63 70 eqtrd 
 |-  ( ph -> ( S. A ( Re ` ( B + C ) ) _d x + ( _i x. S. A ( Im ` ( B + C ) ) _d x ) ) = ( ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) + ( S. A ( Re ` C ) _d x + ( _i x. S. A ( Im ` C ) _d x ) ) ) )
72 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) e. _V )
73 1 2 3 4 5 ibladdnc 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) e. L^1 )
74 72 73 itgcnval 
 |-  ( ph -> S. A ( B + C ) _d x = ( S. A ( Re ` ( B + C ) ) _d x + ( _i x. S. A ( Im ` ( B + C ) ) _d x ) ) )
75 1 2 itgcnval 
 |-  ( ph -> S. A B _d x = ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) )
76 3 4 itgcnval 
 |-  ( ph -> S. A C _d x = ( S. A ( Re ` C ) _d x + ( _i x. S. A ( Im ` C ) _d x ) ) )
77 75 76 oveq12d 
 |-  ( ph -> ( S. A B _d x + S. A C _d x ) = ( ( S. A ( Re ` B ) _d x + ( _i x. S. A ( Im ` B ) _d x ) ) + ( S. A ( Re ` C ) _d x + ( _i x. S. A ( Im ` C ) _d x ) ) ) )
78 71 74 77 3eqtr4d 
 |-  ( ph -> S. A ( B + C ) _d x = ( S. A B _d x + S. A C _d x ) )