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 ⊢ φ → ∫ A B dx = ∫ A ℜ ⁡ B dx + i ⁢ ∫ A ℑ ⁡ B dx

Proof

Step Hyp Ref Expression
1 itgcnval.1 ⊢ φ ∧ x ∈ A → B ∈ V
2 itgcnval.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
3 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0
4 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
5 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0
6 eqid ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
7 3 4 5 6 1 2 itgcnlem ⊢ φ → ∫ A B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 - ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 + i ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
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 ℜ ⁡ B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0
16 10 imcld ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ ℝ
17 13 simprd ⊢ φ → x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1
18 16 17 itgrevallem1 ⊢ φ → ∫ A ℑ ⁡ B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
19 18 oveq2d ⊢ φ → i ⁢ ∫ A ℑ ⁡ B dx = i ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
20 15 19 oveq12d ⊢ φ → ∫ A ℜ ⁡ B dx + i ⁢ ∫ A ℑ ⁡ B dx = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B ℜ ⁡ B 0 - ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℜ ⁡ B − ℜ ⁡ B 0 + i ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℑ ⁡ B ℑ ⁡ B 0 − ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ − ℑ ⁡ B − ℑ ⁡ B 0
21 7 20 eqtr4d ⊢ φ → ∫ A B dx = ∫ A ℜ ⁡ B dx + i ⁢ ∫ A ℑ ⁡ B dx