Metamath Proof Explorer

Theorem ibladd

Description: Add two integrals over the same domain. (Contributed by Mario Carneiro, 17-Aug-2014)

Ref Expression
Hypotheses itgadd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
itgadd.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
itgadd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
itgadd.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
Assertion ibladd ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 itgadd.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
2 itgadd.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
3 itgadd.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
4 itgadd.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
5 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) )
6 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) )
7 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) )
8 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) )
9 5 6 7 8 1 iblcnlem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) ) )
10 2 9 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) )
11 10 simp1d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
12 11 1 mbfdm2 ⊢ ( 𝜑 → 𝐴 ∈ dom vol )
13 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
14 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) )
15 12 1 3 13 14 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∘f + ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) )
16 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐶 ) ) , ( ℜ ‘ 𝐶 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐶 ) ) , ( ℜ ‘ 𝐶 ) , 0 ) ) )
17 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐶 ) ) , - ( ℜ ‘ 𝐶 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐶 ) ) , - ( ℜ ‘ 𝐶 ) , 0 ) ) )
18 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐶 ) ) , ( ℑ ‘ 𝐶 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐶 ) ) , ( ℑ ‘ 𝐶 ) , 0 ) ) )
19 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐶 ) ) , - ( ℑ ‘ 𝐶 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐶 ) ) , - ( ℑ ‘ 𝐶 ) , 0 ) ) )
20 16 17 18 19 3 iblcnlem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐶 ) ) , ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐶 ) ) , - ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐶 ) ) , ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐶 ) ) , - ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ) ) ) )
21 4 20 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐶 ) ) , ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐶 ) ) , - ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐶 ) ) , ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐶 ) ) , - ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ) ) )
22 21 simp1d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
23 11 22 mbfadd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∘f + ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ) ∈ MblFn )
24 15 23 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn )
25 11 1 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
26 25 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
27 22 3 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
28 27 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℝ )
29 25 27 readdd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐵 + 𝐶 ) ) = ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) )
30 25 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) ) )
31 11 30 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn ) )
32 31 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn )
33 27 ismbfcn2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ MblFn ) ) )
34 22 33 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ MblFn ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ MblFn ) )
35 34 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐶 ) ) ∈ MblFn )
36 10 simp2d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) )
37 36 simpld ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐵 ) ) , ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
38 21 simp2d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐶 ) ) , ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐶 ) ) , - ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ) )
39 38 simpld ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ 𝐶 ) ) , ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ )
40 26 28 29 32 35 37 39 ibladdlem ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ )
41 26 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℜ ‘ 𝐵 ) ∈ ℝ )
42 28 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℜ ‘ 𝐶 ) ∈ ℝ )
43 29 negeqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) = - ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) )
44 26 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℂ )
45 28 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℂ )
46 44 45 negdid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ( ℜ ‘ 𝐵 ) + ( ℜ ‘ 𝐶 ) ) = ( - ( ℜ ‘ 𝐵 ) + - ( ℜ ‘ 𝐶 ) ) )
47 43 46 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) = ( - ( ℜ ‘ 𝐵 ) + - ( ℜ ‘ 𝐶 ) ) )
48 26 32 mbfneg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - ( ℜ ‘ 𝐵 ) ) ∈ MblFn )
49 28 35 mbfneg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - ( ℜ ‘ 𝐶 ) ) ∈ MblFn )
50 36 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐵 ) ) , - ( ℜ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
51 38 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ 𝐶 ) ) , - ( ℜ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ )
52 41 42 47 48 49 50 51 ibladdlem ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ )
53 40 52 jca ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ) )
54 25 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
55 27 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℝ )
56 25 27 imaddd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ ( 𝐵 + 𝐶 ) ) = ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) )
57 31 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn )
58 34 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐶 ) ) ∈ MblFn )
59 10 simp3d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) )
60 59 simpld ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐵 ) ) , ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
61 21 simp3d ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐶 ) ) , ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐶 ) ) , - ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ ) )
62 61 simpld ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ 𝐶 ) ) , ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ )
63 54 55 56 57 58 60 62 ibladdlem ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ )
64 54 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ 𝐵 ) ∈ ℝ )
65 55 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ 𝐶 ) ∈ ℝ )
66 56 negeqd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) = - ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) )
67 54 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℂ )
68 55 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℂ )
69 67 68 negdid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ( ℑ ‘ 𝐵 ) + ( ℑ ‘ 𝐶 ) ) = ( - ( ℑ ‘ 𝐵 ) + - ( ℑ ‘ 𝐶 ) ) )
70 66 69 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) = ( - ( ℑ ‘ 𝐵 ) + - ( ℑ ‘ 𝐶 ) ) )
71 54 57 mbfneg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - ( ℑ ‘ 𝐵 ) ) ∈ MblFn )
72 55 58 mbfneg ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ - ( ℑ ‘ 𝐶 ) ) ∈ MblFn )
73 59 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐵 ) ) , - ( ℑ ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
74 61 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ 𝐶 ) ) , - ( ℑ ‘ 𝐶 ) , 0 ) ) ) ∈ ℝ )
75 64 65 70 71 72 73 74 ibladdlem ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ )
76 63 75 jca ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ) )
77 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) )
78 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) )
79 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) )
80 eqid ⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) )
81 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 + 𝐶 ) ∈ V )
82 77 78 79 80 81 iblcnlem ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ MblFn ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℜ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ) ∧ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) ) , - ( ℑ ‘ ( 𝐵 + 𝐶 ) ) , 0 ) ) ) ∈ ℝ ) ) ) )
83 24 53 76 82 mpbir3and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 + 𝐶 ) ) ∈ 𝐿1 )