Metamath Proof Explorer

Theorem ibladdnc

Description: Choice-free analogue of itgadd . A measurability hypothesis is necessitated by the loss of mbfadd ; for large classes of functions, such as continuous functions, it should be relatively easy to show. (Contributed by Brendan Leahy, 1-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 ibladdnc 
|- ( ph -> ( x e. A |-> ( B + C ) ) e. L^1 )

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 8 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. RR )
10 iblmbf 
 |-  ( ( x e. A |-> C ) e. L^1 -> ( x e. A |-> C ) e. MblFn )
11 4 10 syl 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )
12 11 3 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
13 12 recld 
 |-  ( ( ph /\ x e. A ) -> ( Re ` C ) e. RR )
14 8 12 readdd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( B + C ) ) = ( ( Re ` B ) + ( Re ` C ) ) )
15 8 ismbfcn2 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn <-> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) ) )
16 7 15 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( Re ` B ) ) e. MblFn /\ ( x e. A |-> ( Im ` B ) ) e. MblFn ) )
17 16 simpld 
 |-  ( ph -> ( x e. A |-> ( Re ` B ) ) e. MblFn )
18 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) )
19 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) )
20 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) )
21 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) )
22 18 19 20 21 1 iblcnlem 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR ) ) ) )
23 2 22 mpbid 
 |-  ( ph -> ( ( x e. A |-> B ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR ) ) )
24 23 simp2d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR ) )
25 24 simpld 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` B ) ) , ( Re ` B ) , 0 ) ) ) e. RR )
26 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` C ) ) , ( Re ` C ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` C ) ) , ( Re ` C ) , 0 ) ) )
27 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` C ) ) , -u ( Re ` C ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` C ) ) , -u ( Re ` C ) , 0 ) ) )
28 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` C ) ) , ( Im ` C ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` C ) ) , ( Im ` C ) , 0 ) ) )
29 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` C ) ) , -u ( Im ` C ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` C ) ) , -u ( Im ` C ) , 0 ) ) )
30 26 27 28 29 3 iblcnlem 
 |-  ( ph -> ( ( x e. A |-> C ) e. L^1 <-> ( ( x e. A |-> C ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` C ) ) , ( Re ` C ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` C ) ) , -u ( Re ` C ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` C ) ) , ( Im ` C ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` C ) ) , -u ( Im ` C ) , 0 ) ) ) e. RR ) ) ) )
31 4 30 mpbid 
 |-  ( ph -> ( ( x e. A |-> C ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` C ) ) , ( Re ` C ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` C ) ) , -u ( Re ` C ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` C ) ) , ( Im ` C ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` C ) ) , -u ( Im ` C ) , 0 ) ) ) e. RR ) ) )
32 31 simp2d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` C ) ) , ( Re ` C ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` C ) ) , -u ( Re ` C ) , 0 ) ) ) e. RR ) )
33 32 simpld 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` C ) ) , ( Re ` C ) , 0 ) ) ) e. RR )
34 9 13 14 17 25 33 ibladdnclem 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B + C ) ) ) , ( Re ` ( B + C ) ) , 0 ) ) ) e. RR )
35 9 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` B ) e. RR )
36 13 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` C ) e. RR )
37 14 negeqd 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` ( B + C ) ) = -u ( ( Re ` B ) + ( Re ` C ) ) )
38 9 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` B ) e. CC )
39 13 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` C ) e. CC )
40 38 39 negdid 
 |-  ( ( ph /\ x e. A ) -> -u ( ( Re ` B ) + ( Re ` C ) ) = ( -u ( Re ` B ) + -u ( Re ` C ) ) )
41 37 40 eqtrd 
 |-  ( ( ph /\ x e. A ) -> -u ( Re ` ( B + C ) ) = ( -u ( Re ` B ) + -u ( Re ` C ) ) )
42 9 17 mbfneg 
 |-  ( ph -> ( x e. A |-> -u ( Re ` B ) ) e. MblFn )
43 24 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` B ) ) , -u ( Re ` B ) , 0 ) ) ) e. RR )
44 32 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` C ) ) , -u ( Re ` C ) , 0 ) ) ) e. RR )
45 35 36 41 42 43 44 ibladdnclem 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` ( B + C ) ) ) , -u ( Re ` ( B + C ) ) , 0 ) ) ) e. RR )
46 34 45 jca 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B + C ) ) ) , ( Re ` ( B + C ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` ( B + C ) ) ) , -u ( Re ` ( B + C ) ) , 0 ) ) ) e. RR ) )
47 8 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. RR )
48 12 imcld 
 |-  ( ( ph /\ x e. A ) -> ( Im ` C ) e. RR )
49 8 12 imaddd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` ( B + C ) ) = ( ( Im ` B ) + ( Im ` C ) ) )
50 16 simprd 
 |-  ( ph -> ( x e. A |-> ( Im ` B ) ) e. MblFn )
51 23 simp3d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR ) )
52 51 simpld 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` B ) ) , ( Im ` B ) , 0 ) ) ) e. RR )
53 31 simp3d 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` C ) ) , ( Im ` C ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` C ) ) , -u ( Im ` C ) , 0 ) ) ) e. RR ) )
54 53 simpld 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` C ) ) , ( Im ` C ) , 0 ) ) ) e. RR )
55 47 48 49 50 52 54 ibladdnclem 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` ( B + C ) ) ) , ( Im ` ( B + C ) ) , 0 ) ) ) e. RR )
56 47 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` B ) e. RR )
57 48 renegcld 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` C ) e. RR )
58 49 negeqd 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` ( B + C ) ) = -u ( ( Im ` B ) + ( Im ` C ) ) )
59 47 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` B ) e. CC )
60 48 recnd 
 |-  ( ( ph /\ x e. A ) -> ( Im ` C ) e. CC )
61 59 60 negdid 
 |-  ( ( ph /\ x e. A ) -> -u ( ( Im ` B ) + ( Im ` C ) ) = ( -u ( Im ` B ) + -u ( Im ` C ) ) )
62 58 61 eqtrd 
 |-  ( ( ph /\ x e. A ) -> -u ( Im ` ( B + C ) ) = ( -u ( Im ` B ) + -u ( Im ` C ) ) )
63 47 50 mbfneg 
 |-  ( ph -> ( x e. A |-> -u ( Im ` B ) ) e. MblFn )
64 51 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` B ) ) , -u ( Im ` B ) , 0 ) ) ) e. RR )
65 53 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` C ) ) , -u ( Im ` C ) , 0 ) ) ) e. RR )
66 56 57 62 63 64 65 ibladdnclem 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` ( B + C ) ) ) , -u ( Im ` ( B + C ) ) , 0 ) ) ) e. RR )
67 55 66 jca 
 |-  ( ph -> ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` ( B + C ) ) ) , ( Im ` ( B + C ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` ( B + C ) ) ) , -u ( Im ` ( B + C ) ) , 0 ) ) ) e. RR ) )
68 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B + C ) ) ) , ( Re ` ( B + C ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B + C ) ) ) , ( Re ` ( B + C ) ) , 0 ) ) )
69 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` ( B + C ) ) ) , -u ( Re ` ( B + C ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` ( B + C ) ) ) , -u ( Re ` ( B + C ) ) , 0 ) ) )
70 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` ( B + C ) ) ) , ( Im ` ( B + C ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` ( B + C ) ) ) , ( Im ` ( B + C ) ) , 0 ) ) )
71 eqid 
 |-  ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` ( B + C ) ) ) , -u ( Im ` ( B + C ) ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` ( B + C ) ) ) , -u ( Im ` ( B + C ) ) , 0 ) ) )
72 ovexd 
 |-  ( ( ph /\ x e. A ) -> ( B + C ) e. _V )
73 68 69 70 71 72 iblcnlem 
 |-  ( ph -> ( ( x e. A |-> ( B + C ) ) e. L^1 <-> ( ( x e. A |-> ( B + C ) ) e. MblFn /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B + C ) ) ) , ( Re ` ( B + C ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Re ` ( B + C ) ) ) , -u ( Re ` ( B + C ) ) , 0 ) ) ) e. RR ) /\ ( ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Im ` ( B + C ) ) ) , ( Im ` ( B + C ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ -u ( Im ` ( B + C ) ) ) , -u ( Im ` ( B + C ) ) , 0 ) ) ) e. RR ) ) ) )
74 5 46 67 73 mpbir3and 
 |-  ( ph -> ( x e. A |-> ( B + C ) ) e. L^1 )