itgim

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

Step	Hyp	Ref	Expression
1		itgcnval.1	$⊢ (φ \land x \in A) \to B \in V$
2		itgcnval.2	$⊢ φ \to (x \in A ⟼ B) \in 𝐿^{1}$
3	1 2	itgcnval	$⊢ φ \to \int_{A} B d x = \int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x$
4	3	fveq2d	$⊢ φ \to ℑ (\int_{A} B d x) = ℑ (\int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x)$
5		iblmbf	$⊢ (x \in A ⟼ B) \in 𝐿^{1} \to (x \in A ⟼ B) \in MblFn$
6	2 5	syl	$⊢ φ \to (x \in A ⟼ B) \in MblFn$
7	6 1	mbfmptcl	$⊢ (φ \land x \in A) \to B \in ℂ$
8	7	recld	$⊢ (φ \land x \in A) \to ℜ (B) \in ℝ$
9	7	iblcn	$⊢ φ \to ((x \in A ⟼ B) \in 𝐿^{1} \leftrightarrow ((x \in A ⟼ ℜ (B)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (B)) \in 𝐿^{1}))$
10	2 9	mpbid	$⊢ φ \to ((x \in A ⟼ ℜ (B)) \in 𝐿^{1} \land (x \in A ⟼ ℑ (B)) \in 𝐿^{1})$
11	10	simpld	$⊢ φ \to (x \in A ⟼ ℜ (B)) \in 𝐿^{1}$
12	8 11	itgrecl	$⊢ φ \to \int_{A} ℜ (B) d x \in ℝ$
13	7	imcld	$⊢ (φ \land x \in A) \to ℑ (B) \in ℝ$
14	10	simprd	$⊢ φ \to (x \in A ⟼ ℑ (B)) \in 𝐿^{1}$
15	13 14	itgrecl	$⊢ φ \to \int_{A} ℑ (B) d x \in ℝ$
16	12 15	crimd	$⊢ φ \to ℑ (\int_{A} ℜ (B) d x + i \int_{A} ℑ (B) d x) = \int_{A} ℑ (B) d x$
17	4 16	eqtrd	$⊢ φ \to ℑ (\int_{A} B d x) = \int_{A} ℑ (B) d x$

Metamath Proof Explorer