Metamath Proof Explorer

Theorem itgcnval

Description: Decompose the integral of a complex function into real and imaginary parts. (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypotheses itgcnval.1 ⊢φ∧x∈A→B∈V
itgcnval.2 ⊢φ→x∈A⟼B∈𝐿1
Assertion itgcnval ⊢φ→∫ABdx=∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx

Proof

Step Hyp Ref Expression
1 itgcnval.1 ⊢φ∧x∈A→B∈V
2 itgcnval.2 ⊢φ→x∈A⟼B∈𝐿1
3 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0
4 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
5 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0
6 eqid ⊢∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0=∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
7 3 4 5 6 1 2 itgcnlem ⊢φ→∫ABdx=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0-∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0+i⁢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
8 iblmbf ⊢x∈A⟼B∈𝐿1→x∈A⟼B∈MblFn
9 2 8 syl ⊢φ→x∈A⟼B∈MblFn
10 9 1 mbfmptcl ⊢φ∧x∈A→B∈ℂ
11 10 recld ⊢φ∧x∈A→ℜ⁡B∈ℝ
12 10 iblcn ⊢φ→x∈A⟼B∈𝐿1↔x∈A⟼ℜ⁡B∈𝐿1∧x∈A⟼ℑ⁡B∈𝐿1
13 2 12 mpbid ⊢φ→x∈A⟼ℜ⁡B∈𝐿1∧x∈A⟼ℑ⁡B∈𝐿1
14 13 simpld ⊢φ→x∈A⟼ℜ⁡B∈𝐿1
15 11 14 itgrevallem1 ⊢φ→∫Aℜ⁡Bdx=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0
16 10 imcld ⊢φ∧x∈A→ℑ⁡B∈ℝ
17 13 simprd ⊢φ→x∈A⟼ℑ⁡B∈𝐿1
18 16 17 itgrevallem1 ⊢φ→∫Aℑ⁡Bdx=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
19 18 oveq2d ⊢φ→i⁢∫Aℑ⁡Bdx=i⁢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
20 15 19 oveq12d ⊢φ→∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx=∫2⁡x∈ℝ⟼ifx∈A∧0≤ℜ⁡Bℜ⁡B0-∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℜ⁡B−ℜ⁡B0+i⁢∫2⁡x∈ℝ⟼ifx∈A∧0≤ℑ⁡Bℑ⁡B0−∫2⁡x∈ℝ⟼ifx∈A∧0≤−ℑ⁡B−ℑ⁡B0
21 7 20 eqtr4d ⊢φ→∫ABdx=∫Aℜ⁡Bdx+i⁢∫Aℑ⁡Bdx