Step |
Hyp |
Ref |
Expression |
1 |
|
itgcnval.1 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 ) |
2 |
|
itgcnval.2 |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ) |
3 |
1 2
|
itgcnval |
⊢ ( 𝜑 → ∫ 𝐴 𝐵 d 𝑥 = ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) |
4 |
3
|
fveq2d |
⊢ ( 𝜑 → ( ℜ ‘ ∫ 𝐴 𝐵 d 𝑥 ) = ( ℜ ‘ ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) ) |
5 |
|
iblmbf |
⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) |
6 |
2 5
|
syl |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn ) |
7 |
6 1
|
mbfmptcl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ ) |
8 |
7
|
recld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ ) |
9 |
7
|
iblcn |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) ) ) |
10 |
2 9
|
mpbid |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) ) |
11 |
10
|
simpld |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ) |
12 |
8 11
|
itgrecl |
⊢ ( 𝜑 → ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ∈ ℝ ) |
13 |
7
|
imcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ ) |
14 |
10
|
simprd |
⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) |
15 |
13 14
|
itgrecl |
⊢ ( 𝜑 → ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ∈ ℝ ) |
16 |
12 15
|
crred |
⊢ ( 𝜑 → ( ℜ ‘ ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) |
17 |
4 16
|
eqtrd |
⊢ ( 𝜑 → ( ℜ ‘ ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 ) |