This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgim

Description: Imaginary part of an integral. (Contributed by Mario Carneiro, 14-Aug-2014)

Ref Expression
Hypotheses itgcnval.1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
itgcnval.2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
Assertion itgim ( 𝜑 → ( ℑ ‘ ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 )

Proof

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 crimd ⊢ ( 𝜑 → ( ℑ ‘ ( ∫ 𝐴 ( ℜ ‘ 𝐵 ) d 𝑥 + ( i · ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 ) ) ) = ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 )
17 4 16 eqtrd ⊢ ( 𝜑 → ( ℑ ‘ ∫ 𝐴 𝐵 d 𝑥 ) = ∫ 𝐴 ( ℑ ‘ 𝐵 ) d 𝑥 )