Metamath Proof Explorer


Theorem itgmulc2nc

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

Ref Expression
Hypotheses itgmulc2nc.1 ( 𝜑𝐶 ∈ ℂ )
itgmulc2nc.2 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
itgmulc2nc.3 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝐿1 )
itgmulc2nc.m ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn )
Assertion itgmulc2nc ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgmulc2nc.1 ( 𝜑𝐶 ∈ ℂ )
2 itgmulc2nc.2 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
3 itgmulc2nc.3 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝐿1 )
4 itgmulc2nc.m ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn )
5 1 recld ( 𝜑 → ( ℜ ‘ 𝐶 ) ∈ ℝ )
6 5 recnd ( 𝜑 → ( ℜ ‘ 𝐶 ) ∈ ℂ )
7 6 adantr ( ( 𝜑𝑥𝐴 ) → ( ℜ ‘ 𝐶 ) ∈ ℂ )
8 iblmbf ( ( 𝑥𝐴𝐵 ) ∈ 𝐿1 → ( 𝑥𝐴𝐵 ) ∈ MblFn )
9 3 8 syl ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ MblFn )
10 9 2 mbfmptcl ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
11 10 recld ( ( 𝜑𝑥𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
12 11 recnd ( ( 𝜑𝑥𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℂ )
13 7 12 mulcld ( ( 𝜑𝑥𝐴 ) → ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℂ )
14 10 iblcn ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) ) )
15 3 14 mpbid ( 𝜑 → ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) )
16 15 simpld ( 𝜑 → ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 )
17 ovexd ( ( 𝜑𝑥𝐴 ) → ( 𝐶 · 𝐵 ) ∈ V )
18 4 17 mbfdm2 ( 𝜑𝐴 ∈ dom vol )
19 fconstmpt ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) = ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐶 ) )
20 19 a1i ( 𝜑 → ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) = ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐶 ) ) )
21 eqidd ( 𝜑 → ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) = ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) )
22 18 7 11 20 21 offval2 ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) = ( 𝑥𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) )
23 iblmbf ( ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 → ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn )
24 16 23 syl ( 𝜑 → ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ MblFn )
25 12 fmpttd ( 𝜑 → ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) : 𝐴 ⟶ ℂ )
26 24 5 25 mbfmulc2re ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∈ MblFn )
27 22 26 eqeltrrd ( 𝜑 → ( 𝑥𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ MblFn )
28 6 11 16 27 iblmulc2nc ( 𝜑 → ( 𝑥𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
29 13 28 itgcl ( 𝜑 → ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
30 ax-icn i ∈ ℂ
31 10 imcld ( ( 𝜑𝑥𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
32 31 recnd ( ( 𝜑𝑥𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℂ )
33 7 32 mulcld ( ( 𝜑𝑥𝐴 ) → ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
34 15 simprd ( 𝜑 → ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 )
35 eqidd ( 𝜑 → ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) = ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) )
36 18 7 31 20 35 offval2 ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) = ( 𝑥𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
37 iblmbf ( ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 → ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn )
38 34 37 syl ( 𝜑 → ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ MblFn )
39 32 fmpttd ( 𝜑 → ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) : 𝐴 ⟶ ℂ )
40 38 5 39 mbfmulc2re ( 𝜑 → ( ( 𝐴 × { ( ℜ ‘ 𝐶 ) } ) ∘f · ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
41 36 40 eqeltrrd ( 𝜑 → ( 𝑥𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
42 6 31 34 41 iblmulc2nc ( 𝜑 → ( 𝑥𝐴 ↦ ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
43 33 42 itgcl ( 𝜑 → ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
44 mulcl ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ∈ ℂ )
45 30 43 44 sylancr ( 𝜑 → ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ∈ ℂ )
46 1 imcld ( 𝜑 → ( ℑ ‘ 𝐶 ) ∈ ℝ )
47 46 recnd ( 𝜑 → ( ℑ ‘ 𝐶 ) ∈ ℂ )
48 47 negcld ( 𝜑 → - ( ℑ ‘ 𝐶 ) ∈ ℂ )
49 48 adantr ( ( 𝜑𝑥𝐴 ) → - ( ℑ ‘ 𝐶 ) ∈ ℂ )
50 49 32 mulcld ( ( 𝜑𝑥𝐴 ) → ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
51 fconstmpt ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) = ( 𝑥𝐴 ↦ - ( ℑ ‘ 𝐶 ) )
52 51 a1i ( 𝜑 → ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) = ( 𝑥𝐴 ↦ - ( ℑ ‘ 𝐶 ) ) )
53 18 49 31 52 35 offval2 ( 𝜑 → ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) = ( 𝑥𝐴 ↦ ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
54 46 renegcld ( 𝜑 → - ( ℑ ‘ 𝐶 ) ∈ ℝ )
55 38 54 39 mbfmulc2re ( 𝜑 → ( ( 𝐴 × { - ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
56 53 55 eqeltrrd ( 𝜑 → ( 𝑥𝐴 ↦ ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
57 48 31 34 56 iblmulc2nc ( 𝜑 → ( 𝑥𝐴 ↦ ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
58 50 57 itgcl ( 𝜑 → ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
59 47 adantr ( ( 𝜑𝑥𝐴 ) → ( ℑ ‘ 𝐶 ) ∈ ℂ )
60 59 12 mulcld ( ( 𝜑𝑥𝐴 ) → ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ∈ ℂ )
61 fconstmpt ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) = ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐶 ) )
62 61 a1i ( 𝜑 → ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) = ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐶 ) ) )
63 18 59 11 62 21 offval2 ( 𝜑 → ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) = ( 𝑥𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) )
64 24 46 25 mbfmulc2re ( 𝜑 → ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ) ∈ MblFn )
65 63 64 eqeltrrd ( 𝜑 → ( 𝑥𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ MblFn )
66 47 11 16 65 iblmulc2nc ( 𝜑 → ( 𝑥𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
67 60 66 itgcl ( 𝜑 → ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
68 mulcl ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ∈ ℂ )
69 30 67 68 sylancr ( 𝜑 → ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ∈ ℂ )
70 29 45 58 69 add4d ( 𝜑 → ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) + ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) = ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) )
71 30 a1i ( 𝜑 → i ∈ ℂ )
72 71 47 mulcld ( 𝜑 → ( i · ( ℑ ‘ 𝐶 ) ) ∈ ℂ )
73 2 3 itgcl ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 ∈ ℂ )
74 6 72 73 adddird ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 𝐵 d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) ) )
75 2 3 itgcnval ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
76 75 oveq2d ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( ℜ ‘ 𝐶 ) · ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) )
77 11 16 itgcl ( 𝜑 → ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ∈ ℂ )
78 31 34 itgcl ( 𝜑 → ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℂ )
79 mulcl ( ( i ∈ ℂ ∧ ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℂ ) → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
80 30 78 79 sylancr ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
81 6 77 80 adddid ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( ℜ ‘ 𝐶 ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) )
82 6 11 16 27 5 11 itgmulc2nclem2 ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 )
83 6 71 78 mul12d ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( i · ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
84 6 31 34 41 5 31 itgmulc2nclem2 ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
85 84 oveq2d ( 𝜑 → ( i · ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
86 83 85 eqtrd ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
87 82 86 oveq12d ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( ℜ ‘ 𝐶 ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) )
88 76 81 87 3eqtrd ( 𝜑 → ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) )
89 75 oveq2d ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( i · ( ℑ ‘ 𝐶 ) ) · ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) )
90 72 77 80 adddid ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) )
91 71 47 77 mulassd ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) = ( i · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) ) )
92 47 11 16 65 46 11 itgmulc2nclem2 ( 𝜑 → ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 )
93 92 oveq2d ( 𝜑 → ( i · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) ) = ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) )
94 91 93 eqtrd ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) = ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) )
95 71 47 71 78 mul4d ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( ( i · i ) · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) )
96 ixi ( i · i ) = - 1
97 96 oveq1i ( ( i · i ) · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ( - 1 · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) )
98 47 78 mulcld ( 𝜑 → ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ∈ ℂ )
99 98 mulm1d ( 𝜑 → ( - 1 · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = - ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) )
100 97 99 syl5eq ( 𝜑 → ( ( i · i ) · ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = - ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) )
101 47 78 mulneg1d ( 𝜑 → ( - ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = - ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) )
102 48 31 34 56 54 31 itgmulc2nclem2 ( 𝜑 → ( - ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
103 101 102 eqtr3d ( 𝜑 → - ( ( ℑ ‘ 𝐶 ) · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) = ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
104 95 100 103 3eqtrd ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) = ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
105 94 104 oveq12d ( 𝜑 → ( ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
106 69 58 addcomd ( 𝜑 → ( ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) = ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
107 105 106 eqtrd ( 𝜑 → ( ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
108 89 90 107 3eqtrd ( 𝜑 → ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
109 88 108 oveq12d ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) · ∫ 𝐴 𝐵 d 𝑥 ) + ( ( i · ( ℑ ‘ 𝐶 ) ) · ∫ 𝐴 𝐵 d 𝑥 ) ) = ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) + ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) )
110 74 109 eqtrd ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) ) + ( ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) )
111 59 32 mulcld ( ( 𝜑𝑥𝐴 ) → ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
112 18 59 31 62 35 offval2 ( 𝜑 → ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) = ( 𝑥𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
113 38 46 39 mbfmulc2re ( 𝜑 → ( ( 𝐴 × { ( ℑ ‘ 𝐶 ) } ) ∘f · ( 𝑥𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
114 112 113 eqeltrrd ( 𝜑 → ( 𝑥𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ MblFn )
115 47 31 34 114 iblmulc2nc ( 𝜑 → ( 𝑥𝐴 ↦ ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ∈ 𝐿1 )
116 1 adantr ( ( 𝜑𝑥𝐴 ) → 𝐶 ∈ ℂ )
117 116 10 mulcld ( ( 𝜑𝑥𝐴 ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
118 eqidd ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) = ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) )
119 ref ℜ : ℂ ⟶ ℝ
120 119 a1i ( 𝜑 → ℜ : ℂ ⟶ ℝ )
121 120 feqmptd ( 𝜑 → ℜ = ( 𝑘 ∈ ℂ ↦ ( ℜ ‘ 𝑘 ) ) )
122 fveq2 ( 𝑘 = ( 𝐶 · 𝐵 ) → ( ℜ ‘ 𝑘 ) = ( ℜ ‘ ( 𝐶 · 𝐵 ) ) )
123 117 118 121 122 fmptco ( 𝜑 → ( ℜ ∘ ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐶 · 𝐵 ) ) ) )
124 116 10 remuld ( ( 𝜑𝑥𝐴 ) → ( ℜ ‘ ( 𝐶 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) )
125 124 mpteq2dva ( 𝜑 → ( 𝑥𝐴 ↦ ( ℜ ‘ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ) )
126 123 125 eqtrd ( 𝜑 → ( ℜ ∘ ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ) )
127 117 fmpttd ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) : 𝐴 ⟶ ℂ )
128 ismbfcn ( ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) : 𝐴 ⟶ ℂ → ( ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ) ) )
129 127 128 syl ( 𝜑 → ( ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn ↔ ( ( ℜ ∘ ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ) ) )
130 4 129 mpbid ( 𝜑 → ( ( ℜ ∘ ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ∧ ( ℑ ∘ ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn ) )
131 130 simpld ( 𝜑 → ( ℜ ∘ ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn )
132 126 131 eqeltrrd ( 𝜑 → ( 𝑥𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) ) ∈ MblFn )
133 13 28 111 115 132 itgsubnc ( 𝜑 → ∫ 𝐴 ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) d 𝑥 = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 − ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
134 124 itgeq2dv ( 𝜑 → ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 = ∫ 𝐴 ( ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) − ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) ) d 𝑥 )
135 111 115 itgneg ( 𝜑 → - ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 = ∫ 𝐴 - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
136 59 32 mulneg1d ( ( 𝜑𝑥𝐴 ) → ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) = - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) )
137 136 itgeq2dv ( 𝜑 → ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 = ∫ 𝐴 - ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
138 135 137 eqtr4d ( 𝜑 → - ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 = ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 )
139 138 oveq2d ( 𝜑 → ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + - ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
140 111 115 itgcl ( 𝜑 → ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ∈ ℂ )
141 29 140 negsubd ( 𝜑 → ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + - ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 − ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
142 139 141 eqtr3d ( 𝜑 → ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 − ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
143 133 134 142 3eqtr4d ( 𝜑 → ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) )
144 116 10 immuld ( ( 𝜑𝑥𝐴 ) → ( ℑ ‘ ( 𝐶 · 𝐵 ) ) = ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) )
145 144 itgeq2dv ( 𝜑 → ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 = ∫ 𝐴 ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) d 𝑥 )
146 imf ℑ : ℂ ⟶ ℝ
147 146 a1i ( 𝜑 → ℑ : ℂ ⟶ ℝ )
148 147 feqmptd ( 𝜑 → ℑ = ( 𝑘 ∈ ℂ ↦ ( ℑ ‘ 𝑘 ) ) )
149 fveq2 ( 𝑘 = ( 𝐶 · 𝐵 ) → ( ℑ ‘ 𝑘 ) = ( ℑ ‘ ( 𝐶 · 𝐵 ) ) )
150 117 118 148 149 fmptco ( 𝜑 → ( ℑ ∘ ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐶 · 𝐵 ) ) ) )
151 144 mpteq2dva ( 𝜑 → ( 𝑥𝐴 ↦ ( ℑ ‘ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ) )
152 150 151 eqtrd ( 𝜑 → ( ℑ ∘ ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) = ( 𝑥𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ) )
153 130 simprd ( 𝜑 → ( ℑ ∘ ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ) ∈ MblFn )
154 152 153 eqeltrrd ( 𝜑 → ( 𝑥𝐴 ↦ ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) ) ∈ MblFn )
155 33 42 60 66 154 itgaddnc ( 𝜑 → ∫ 𝐴 ( ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) + ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) ) d 𝑥 = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) )
156 145 155 eqtrd ( 𝜑 → ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 = ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) )
157 156 oveq2d ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) = ( i · ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
158 71 43 67 adddid ( 𝜑 → ( i · ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) = ( ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
159 157 158 eqtrd ( 𝜑 → ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) = ( ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) )
160 143 159 oveq12d ( 𝜑 → ( ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) ) = ( ( ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 + ∫ 𝐴 ( - ( ℑ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( ( i · ∫ 𝐴 ( ( ℜ ‘ 𝐶 ) · ( ℑ ‘ 𝐵 ) ) d 𝑥 ) + ( i · ∫ 𝐴 ( ( ℑ ‘ 𝐶 ) · ( ℜ ‘ 𝐵 ) ) d 𝑥 ) ) ) )
161 70 110 160 3eqtr4d ( 𝜑 → ( ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) · ∫ 𝐴 𝐵 d 𝑥 ) = ( ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) ) )
162 1 replimd ( 𝜑𝐶 = ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) )
163 162 oveq1d ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ( ( ( ℜ ‘ 𝐶 ) + ( i · ( ℑ ‘ 𝐶 ) ) ) · ∫ 𝐴 𝐵 d 𝑥 ) )
164 1 2 3 4 iblmulc2nc ( 𝜑 → ( 𝑥𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ 𝐿1 )
165 117 164 itgcnval ( 𝜑 → ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ ( 𝐶 · 𝐵 ) ) d 𝑥 ) ) )
166 161 163 165 3eqtr4d ( 𝜑 → ( 𝐶 · ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( 𝐶 · 𝐵 ) d 𝑥 )