Metamath Proof Explorer

Theorem itgmulc2

Description: Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgmulc2.1 ⊢φ→C∈ℂ
itgmulc2.2 ⊢φ∧x∈A→B∈V
itgmulc2.3 ⊢φ→x∈A⟼B∈𝐿1
Assertion itgmulc2 ⊢φ→C⁢∫ABdx=∫AC⁢Bdx

Proof

Step Hyp Ref Expression
1 itgmulc2.1 ⊢φ→C∈ℂ
2 itgmulc2.2 ⊢φ∧x∈A→B∈V
3 itgmulc2.3 ⊢φ→x∈A⟼B∈𝐿1
4 1 recld ⊢φ→ℜ⁡C∈ℝ
5 4 recnd ⊢φ→ℜ⁡C∈ℂ
6 5 adantr ⊢φ∧x∈A→ℜ⁡C∈ℂ
7 iblmbf ⊢x∈A⟼B∈𝐿1→x∈A⟼B∈MblFn
8 3 7 syl ⊢φ→x∈A⟼B∈MblFn
9 8 2 mbfmptcl ⊢φ∧x∈A→B∈ℂ
10 9 recld ⊢φ∧x∈A→ℜ⁡B∈ℝ
11 10 recnd ⊢φ∧x∈A→ℜ⁡B∈ℂ
12 6 11 mulcld ⊢φ∧x∈A→ℜ⁡C⁢ℜ⁡B∈ℂ
13 9 iblcn ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼ℜ⁡B∈𝐿1∧x∈A⟼ℑ⁡B∈𝐿1
14 3 13 mpbid ⊢φ→x∈A⟼ℜ⁡B∈𝐿1∧x∈A⟼ℑ⁡B∈𝐿1
15 14 simpld ⊢φ→x∈A⟼ℜ⁡B∈𝐿1
16 5 10 15 iblmulc2 ⊢φ→x∈A⟼ℜ⁡C⁢ℜ⁡B∈𝐿1
17 12 16 itgcl ⊢φ→∫Aℜ⁡C⁢ℜ⁡Bdx∈ℂ
18 ax-icn ⊢i∈ℂ
19 9 imcld ⊢φ∧x∈A→ℑ⁡B∈ℝ
20 19 recnd ⊢φ∧x∈A→ℑ⁡B∈ℂ
21 6 20 mulcld ⊢φ∧x∈A→ℜ⁡C⁢ℑ⁡B∈ℂ
22 14 simprd ⊢φ→x∈A⟼ℑ⁡B∈𝐿1
23 5 19 22 iblmulc2 ⊢φ→x∈A⟼ℜ⁡C⁢ℑ⁡B∈𝐿1
24 21 23 itgcl ⊢φ→∫Aℜ⁡C⁢ℑ⁡Bdx∈ℂ
25 mulcl ⊢i∈ℂ∧∫Aℜ⁡C⁢ℑ⁡Bdx∈ℂ→i⁢∫Aℜ⁡C⁢ℑ⁡Bdx∈ℂ
26 18 24 25 sylancr ⊢φ→i⁢∫Aℜ⁡C⁢ℑ⁡Bdx∈ℂ
27 1 imcld ⊢φ→ℑ⁡C∈ℝ
28 27 renegcld ⊢φ→−ℑ⁡C∈ℝ
29 28 recnd ⊢φ→−ℑ⁡C∈ℂ
30 29 adantr ⊢φ∧x∈A→−ℑ⁡C∈ℂ
31 30 20 mulcld ⊢φ∧x∈A→−ℑ⁡C⁢ℑ⁡B∈ℂ
32 29 19 22 iblmulc2 ⊢φ→x∈A⟼−ℑ⁡C⁢ℑ⁡B∈𝐿1
33 31 32 itgcl ⊢φ→∫A−ℑ⁡C⁢ℑ⁡Bdx∈ℂ
34 27 recnd ⊢φ→ℑ⁡C∈ℂ
35 34 adantr ⊢φ∧x∈A→ℑ⁡C∈ℂ
36 35 11 mulcld ⊢φ∧x∈A→ℑ⁡C⁢ℜ⁡B∈ℂ
37 34 10 15 iblmulc2 ⊢φ→x∈A⟼ℑ⁡C⁢ℜ⁡B∈𝐿1
38 36 37 itgcl ⊢φ→∫Aℑ⁡C⁢ℜ⁡Bdx∈ℂ
39 mulcl ⊢i∈ℂ∧∫Aℑ⁡C⁢ℜ⁡Bdx∈ℂ→i⁢∫Aℑ⁡C⁢ℜ⁡Bdx∈ℂ
40 18 38 39 sylancr ⊢φ→i⁢∫Aℑ⁡C⁢ℜ⁡Bdx∈ℂ
41 17 26 33 40 add4d ⊢φ→∫Aℜ⁡C⁢ℜ⁡Bdx+i⁢∫Aℜ⁡C⁢ℑ⁡Bdx+∫A−ℑ⁡C⁢ℑ⁡Bdx+i⁢∫Aℑ⁡C⁢ℜ⁡Bdx=∫Aℜ⁡C⁢ℜ⁡Bdx+∫A−ℑ⁡C⁢ℑ⁡Bdx+i⁢∫Aℜ⁡C⁢ℑ⁡Bdx+i⁢∫Aℑ⁡C⁢ℜ⁡Bdx
42 2 3 itgcl ⊢φ→∫ABdx∈ℂ
43 mulcl ⊢i∈ℂ∧ℑ⁡C∈ℂ→i⁢ℑ⁡C∈ℂ
44 18 34 43 sylancr ⊢φ→i⁢ℑ⁡C∈ℂ
45 2 3 itgcnval ⊢φ→∫ABdx=∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx
46 45 oveq2d ⊢φ→ℜ⁡C⁢∫ABdx=ℜ⁡C⁢∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx
47 10 15 itgcl ⊢φ→∫Aℜ⁡Bdx∈ℂ
48 19 22 itgcl ⊢φ→∫Aℑ⁡Bdx∈ℂ
49 mulcl ⊢i∈ℂ∧∫Aℑ⁡Bdx∈ℂ→i⁢∫Aℑ⁡Bdx∈ℂ
50 18 48 49 sylancr ⊢φ→i⁢∫Aℑ⁡Bdx∈ℂ
51 5 47 50 adddid ⊢φ→ℜ⁡C⁢∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx=ℜ⁡C⁢∫Aℜ⁡Bdx+ℜ⁡C⁢i⁢∫Aℑ⁡Bdx
52 5 10 15 4 10 itgmulc2lem2 ⊢φ→ℜ⁡C⁢∫Aℜ⁡Bdx=∫Aℜ⁡C⁢ℜ⁡Bdx
53 18 a1i ⊢φ→i∈ℂ
54 5 53 48 mul12d ⊢φ→ℜ⁡C⁢i⁢∫Aℑ⁡Bdx=i⁢ℜ⁡C⁢∫Aℑ⁡Bdx
55 5 19 22 4 19 itgmulc2lem2 ⊢φ→ℜ⁡C⁢∫Aℑ⁡Bdx=∫Aℜ⁡C⁢ℑ⁡Bdx
56 55 oveq2d ⊢φ→i⁢ℜ⁡C⁢∫Aℑ⁡Bdx=i⁢∫Aℜ⁡C⁢ℑ⁡Bdx
57 54 56 eqtrd ⊢φ→ℜ⁡C⁢i⁢∫Aℑ⁡Bdx=i⁢∫Aℜ⁡C⁢ℑ⁡Bdx
58 52 57 oveq12d ⊢φ→ℜ⁡C⁢∫Aℜ⁡Bdx+ℜ⁡C⁢i⁢∫Aℑ⁡Bdx=∫Aℜ⁡C⁢ℜ⁡Bdx+i⁢∫Aℜ⁡C⁢ℑ⁡Bdx
59 46 51 58 3eqtrd ⊢φ→ℜ⁡C⁢∫ABdx=∫Aℜ⁡C⁢ℜ⁡Bdx+i⁢∫Aℜ⁡C⁢ℑ⁡Bdx
60 45 oveq2d ⊢φ→i⁢ℑ⁡C⁢∫ABdx=i⁢ℑ⁡C⁢∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx
61 44 47 50 adddid ⊢φ→i⁢ℑ⁡C⁢∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx=i⁢ℑ⁡C⁢∫Aℜ⁡Bdx+i⁢ℑ⁡C⁢i⁢∫Aℑ⁡Bdx
62 53 34 47 mulassd ⊢φ→i⁢ℑ⁡C⁢∫Aℜ⁡Bdx=i⁢ℑ⁡C⁢∫Aℜ⁡Bdx
63 34 10 15 27 10 itgmulc2lem2 ⊢φ→ℑ⁡C⁢∫Aℜ⁡Bdx=∫Aℑ⁡C⁢ℜ⁡Bdx
64 63 oveq2d ⊢φ→i⁢ℑ⁡C⁢∫Aℜ⁡Bdx=i⁢∫Aℑ⁡C⁢ℜ⁡Bdx
65 62 64 eqtrd ⊢φ→i⁢ℑ⁡C⁢∫Aℜ⁡Bdx=i⁢∫Aℑ⁡C⁢ℜ⁡Bdx
66 53 34 53 48 mul4d ⊢φ→i⁢ℑ⁡C⁢i⁢∫Aℑ⁡Bdx=i⁢i⁢ℑ⁡C⁢∫Aℑ⁡Bdx
67 ixi ⊢i⁢i=−1
68 67 oveq1i ⊢i⁢i⁢ℑ⁡C⁢∫Aℑ⁡Bdx=-1⁢ℑ⁡C⁢∫Aℑ⁡Bdx
69 34 48 mulcld ⊢φ→ℑ⁡C⁢∫Aℑ⁡Bdx∈ℂ
70 69 mulm1d ⊢φ→-1⁢ℑ⁡C⁢∫Aℑ⁡Bdx=−ℑ⁡C⁢∫Aℑ⁡Bdx
71 68 70 eqtrid ⊢φ→i⁢i⁢ℑ⁡C⁢∫Aℑ⁡Bdx=−ℑ⁡C⁢∫Aℑ⁡Bdx
72 34 48 mulneg1d ⊢φ→−ℑ⁡C⁢∫Aℑ⁡Bdx=−ℑ⁡C⁢∫Aℑ⁡Bdx
73 29 19 22 28 19 itgmulc2lem2 ⊢φ→−ℑ⁡C⁢∫Aℑ⁡Bdx=∫A−ℑ⁡C⁢ℑ⁡Bdx
74 72 73 eqtr3d ⊢φ→−ℑ⁡C⁢∫Aℑ⁡Bdx=∫A−ℑ⁡C⁢ℑ⁡Bdx
75 66 71 74 3eqtrd ⊢φ→i⁢ℑ⁡C⁢i⁢∫Aℑ⁡Bdx=∫A−ℑ⁡C⁢ℑ⁡Bdx
76 65 75 oveq12d ⊢φ→i⁢ℑ⁡C⁢∫Aℜ⁡Bdx+i⁢ℑ⁡C⁢i⁢∫Aℑ⁡Bdx=i⁢∫Aℑ⁡C⁢ℜ⁡Bdx+∫A−ℑ⁡C⁢ℑ⁡Bdx
77 40 33 76 comraddd ⊢φ→i⁢ℑ⁡C⁢∫Aℜ⁡Bdx+i⁢ℑ⁡C⁢i⁢∫Aℑ⁡Bdx=∫A−ℑ⁡C⁢ℑ⁡Bdx+i⁢∫Aℑ⁡C⁢ℜ⁡Bdx
78 60 61 77 3eqtrd ⊢φ→i⁢ℑ⁡C⁢∫ABdx=∫A−ℑ⁡C⁢ℑ⁡Bdx+i⁢∫Aℑ⁡C⁢ℜ⁡Bdx
79 59 78 oveq12d ⊢φ→ℜ⁡C⁢∫ABdx+i⁢ℑ⁡C⁢∫ABdx=∫Aℜ⁡C⁢ℜ⁡Bdx+i⁢∫Aℜ⁡C⁢ℑ⁡Bdx+∫A−ℑ⁡C⁢ℑ⁡Bdx+i⁢∫Aℑ⁡C⁢ℜ⁡Bdx
80 5 42 44 79 joinlmuladdmuld ⊢φ→ℜ⁡C+i⁢ℑ⁡C⁢∫ABdx=∫Aℜ⁡C⁢ℜ⁡Bdx+i⁢∫Aℜ⁡C⁢ℑ⁡Bdx+∫A−ℑ⁡C⁢ℑ⁡Bdx+i⁢∫Aℑ⁡C⁢ℜ⁡Bdx
81 35 20 mulcld ⊢φ∧x∈A→ℑ⁡C⁢ℑ⁡B∈ℂ
82 12 81 negsubd ⊢φ∧x∈A→ℜ⁡C⁢ℜ⁡B+−ℑ⁡C⁢ℑ⁡B=ℜ⁡C⁢ℜ⁡B−ℑ⁡C⁢ℑ⁡B
83 35 20 mulneg1d ⊢φ∧x∈A→−ℑ⁡C⁢ℑ⁡B=−ℑ⁡C⁢ℑ⁡B
84 83 oveq2d ⊢φ∧x∈A→ℜ⁡C⁢ℜ⁡B+−ℑ⁡C⁢ℑ⁡B=ℜ⁡C⁢ℜ⁡B+−ℑ⁡C⁢ℑ⁡B
85 1 adantr ⊢φ∧x∈A→C∈ℂ
86 85 9 remuld ⊢φ∧x∈A→ℜ⁡C⁢B=ℜ⁡C⁢ℜ⁡B−ℑ⁡C⁢ℑ⁡B
87 82 84 86 3eqtr4d ⊢φ∧x∈A→ℜ⁡C⁢ℜ⁡B+−ℑ⁡C⁢ℑ⁡B=ℜ⁡C⁢B
88 87 itgeq2dv ⊢φ→∫Aℜ⁡C⁢ℜ⁡B+−ℑ⁡C⁢ℑ⁡Bdx=∫Aℜ⁡C⁢Bdx
89 12 16 31 32 itgadd ⊢φ→∫Aℜ⁡C⁢ℜ⁡B+−ℑ⁡C⁢ℑ⁡Bdx=∫Aℜ⁡C⁢ℜ⁡Bdx+∫A−ℑ⁡C⁢ℑ⁡Bdx
90 88 89 eqtr3d ⊢φ→∫Aℜ⁡C⁢Bdx=∫Aℜ⁡C⁢ℜ⁡Bdx+∫A−ℑ⁡C⁢ℑ⁡Bdx
91 85 9 immuld ⊢φ∧x∈A→ℑ⁡C⁢B=ℜ⁡C⁢ℑ⁡B+ℑ⁡C⁢ℜ⁡B
92 91 itgeq2dv ⊢φ→∫Aℑ⁡C⁢Bdx=∫Aℜ⁡C⁢ℑ⁡B+ℑ⁡C⁢ℜ⁡Bdx
93 21 23 36 37 itgadd ⊢φ→∫Aℜ⁡C⁢ℑ⁡B+ℑ⁡C⁢ℜ⁡Bdx=∫Aℜ⁡C⁢ℑ⁡Bdx+∫Aℑ⁡C⁢ℜ⁡Bdx
94 92 93 eqtrd ⊢φ→∫Aℑ⁡C⁢Bdx=∫Aℜ⁡C⁢ℑ⁡Bdx+∫Aℑ⁡C⁢ℜ⁡Bdx
95 94 oveq2d ⊢φ→i⁢∫Aℑ⁡C⁢Bdx=i⁢∫Aℜ⁡C⁢ℑ⁡Bdx+∫Aℑ⁡C⁢ℜ⁡Bdx
96 53 24 38 adddid ⊢φ→i⁢∫Aℜ⁡C⁢ℑ⁡Bdx+∫Aℑ⁡C⁢ℜ⁡Bdx=i⁢∫Aℜ⁡C⁢ℑ⁡Bdx+i⁢∫Aℑ⁡C⁢ℜ⁡Bdx
97 95 96 eqtrd ⊢φ→i⁢∫Aℑ⁡C⁢Bdx=i⁢∫Aℜ⁡C⁢ℑ⁡Bdx+i⁢∫Aℑ⁡C⁢ℜ⁡Bdx
98 90 97 oveq12d ⊢φ→∫Aℜ⁡C⁢Bdx+i⁢∫Aℑ⁡C⁢Bdx=∫Aℜ⁡C⁢ℜ⁡Bdx+∫A−ℑ⁡C⁢ℑ⁡Bdx+i⁢∫Aℜ⁡C⁢ℑ⁡Bdx+i⁢∫Aℑ⁡C⁢ℜ⁡Bdx
99 41 80 98 3eqtr4d ⊢φ→ℜ⁡C+i⁢ℑ⁡C⁢∫ABdx=∫Aℜ⁡C⁢Bdx+i⁢∫Aℑ⁡C⁢Bdx
100 1 replimd ⊢φ→C=ℜ⁡C+i⁢ℑ⁡C
101 100 oveq1d ⊢φ→C⁢∫ABdx=ℜ⁡C+i⁢ℑ⁡C⁢∫ABdx
102 85 9 mulcld ⊢φ∧x∈A→C⁢B∈ℂ
103 1 2 3 iblmulc2 ⊢φ→x∈A⟼C⁢B∈𝐿1
104 102 103 itgcnval ⊢φ→∫AC⁢Bdx=∫Aℜ⁡C⁢Bdx+i⁢∫Aℑ⁡C⁢Bdx
105 99 101 104 3eqtr4d ⊢φ→C⁢∫ABdx=∫AC⁢Bdx