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 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
ibladdnc.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
ibladdnc.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
ibladdnc.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
ibladdnc.m ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn )
Assertion ibladdnc ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ 𝐿1 )

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 8 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
10 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
11 4 10 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
12 11 3 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
13 12 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℝ )
14 8 12 readdd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 + 𝐶 ) ) = ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) )
15 8 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) ) )
16 7 15 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) )
17 16 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn )
18 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) )
19 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) )
20 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) )
21 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) )
22 18 19 20 21 1 iblcnlem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ) )
23 2 22 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) )
24 23 simp2d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) )
25 24 simpld ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
26 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐶 ) ) , ( ℜ ‘ 𝐶 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐶 ) ) , ( ℜ ‘ 𝐶 ) , 0 ) ) )
27 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐶 ) ) , - ( ℜ ‘ 𝐶 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐶 ) ) , - ( ℜ ‘ 𝐶 ) , 0 ) ) )
28 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐶 ) ) , ( ℑ ‘ 𝐶 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐶 ) ) , ( ℑ ‘ 𝐶 ) , 0 ) ) )
29 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐶 ) ) , - ( ℑ ‘ 𝐶 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐶 ) ) , - ( ℑ ‘ 𝐶 ) , 0 ) ) )
30 26 27 28 29 3 iblcnlem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐶 ) ) , ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐶 ) ) , - ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐶 ) ) , ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐶 ) ) , - ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ) ) ) )
31 4 30 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐶 ) ) , ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐶 ) ) , - ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐶 ) ) , ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐶 ) ) , - ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ) ) )
32 31 simp2d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐶 ) ) , ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐶 ) ) , - ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ) )
33 32 simpld ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐶 ) ) , ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ )
34 9 13 14 17 25 33 ibladdnclem ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ )
35 9 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℜ ‘ 𝐵 ) ∈ ℝ )
36 13 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℜ ‘ 𝐶 ) ∈ ℝ )
37 14 negeqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) = - ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) )
38 9 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℂ )
39 13 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℂ )
40 38 39 negdid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) = ( - ( ℜ ‘ 𝐵 ) + - ( ℜ ‘ 𝐶 ) ) )
41 37 40 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) = ( - ( ℜ ‘ 𝐵 ) + - ( ℜ ‘ 𝐶 ) ) )
42 9 17 mbfneg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - ( ℜ ‘ 𝐵 ) ) ∈ MblFn )
43 24 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
44 32 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐶 ) ) , - ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ )
45 35 36 41 42 43 44 ibladdnclem ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ )
46 34 45 jca ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ) )
47 8 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
48 12 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℝ )
49 8 12 imaddd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ ( 𝐵 + 𝐶 ) ) = ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) )
50 16 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn )
51 23 simp3d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) )
52 51 simpld ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
53 31 simp3d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐶 ) ) , ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐶 ) ) , - ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ) )
54 53 simpld ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐶 ) ) , ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ )
55 47 48 49 50 52 54 ibladdnclem ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ )
56 47 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ 𝐵 ) ∈ ℝ )
57 48 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ 𝐶 ) ∈ ℝ )
58 49 negeqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) = - ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) )
59 47 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℂ )
60 48 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℂ )
61 59 60 negdid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) = ( - ( ℑ ‘ 𝐵 ) + - ( ℑ ‘ 𝐶 ) ) )
62 58 61 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) = ( - ( ℑ ‘ 𝐵 ) + - ( ℑ ‘ 𝐶 ) ) )
63 47 50 mbfneg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - ( ℑ ‘ 𝐵 ) ) ∈ MblFn )
64 51 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
65 53 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐶 ) ) , - ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ )
66 56 57 62 63 64 65 ibladdnclem ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ )
67 55 66 jca ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ) )
68 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) )
69 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) )
70 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) )
71 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) )
72 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ V )
73 68 69 70 71 72 iblcnlem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ) ) ) )
74 5 46 67 73 mpbir3and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ 𝐿1 )