Theorem dvmptim

Description: Function-builder for derivative, imaginary part. (Contributed by Mario Carneiro, 1-Sep-2014)

	Ref	Expression
Hypotheses	dvmptcj.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
	dvmptcj.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
	dvmptcj.da	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
Assertion	dvmptim	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ℑ ‘ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ℑ ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvmptcj.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
2		dvmptcj.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
3		dvmptcj.da	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
4		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
5	4	a1i	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
6	1	cjcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
7	1 6	subcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
8	5 1 2 3	dvmptcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
9	8	cjcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∗ ‘ 𝐵 ) ∈ ℂ )
10	8 9	subcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 − ( ∗ ‘ 𝐵 ) ) ∈ ℂ )
11	1 2 3	dvmptcj	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ∗ ‘ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ∗ ‘ 𝐵 ) ) )
12	5 1 2 3 6 9 11	dvmptsub	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 − ( ∗ ‘ 𝐵 ) ) ) )
13		2mulicn	⊢ ( 2 · i ) ∈ ℂ
14		2muline0	⊢ ( 2 · i ) ≠ 0
15	13 14	reccli	⊢ ( 1 / ( 2 · i ) ) ∈ ℂ
16	15	a1i	⊢ ( 𝜑 → ( 1 / ( 2 · i ) ) ∈ ℂ )
17	5 7 10 12 16	dvmptcmul	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / ( 2 · i ) ) · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / ( 2 · i ) ) · ( 𝐵 − ( ∗ ‘ 𝐵 ) ) ) ) )
18		imval2	⊢ ( 𝐴 ∈ ℂ → ( ℑ ‘ 𝐴 ) = ( ( 𝐴 − ( ∗ ‘ 𝐴 ) ) / ( 2 · i ) ) )
19	1 18	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ℑ ‘ 𝐴 ) = ( ( 𝐴 − ( ∗ ‘ 𝐴 ) ) / ( 2 · i ) ) )
20		divrec2	⊢ ( ( ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ∈ ℂ ∧ ( 2 · i ) ∈ ℂ ∧ ( 2 · i ) ≠ 0 ) → ( ( 𝐴 − ( ∗ ‘ 𝐴 ) ) / ( 2 · i ) ) = ( ( 1 / ( 2 · i ) ) · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) )
21	13 14 20	mp3an23	⊢ ( ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ∈ ℂ → ( ( 𝐴 − ( ∗ ‘ 𝐴 ) ) / ( 2 · i ) ) = ( ( 1 / ( 2 · i ) ) · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) )
22	7 21	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐴 − ( ∗ ‘ 𝐴 ) ) / ( 2 · i ) ) = ( ( 1 / ( 2 · i ) ) · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) )
23	19 22	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ℑ ‘ 𝐴 ) = ( ( 1 / ( 2 · i ) ) · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) )
24	23	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ℑ ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / ( 2 · i ) ) · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) ) )
25	24	oveq2d	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ℑ ‘ 𝐴 ) ) ) = ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / ( 2 · i ) ) · ( 𝐴 − ( ∗ ‘ 𝐴 ) ) ) ) ) )
26		imval2	⊢ ( 𝐵 ∈ ℂ → ( ℑ ‘ 𝐵 ) = ( ( 𝐵 − ( ∗ ‘ 𝐵 ) ) / ( 2 · i ) ) )
27	8 26	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ℑ ‘ 𝐵 ) = ( ( 𝐵 − ( ∗ ‘ 𝐵 ) ) / ( 2 · i ) ) )
28		divrec2	⊢ ( ( ( 𝐵 − ( ∗ ‘ 𝐵 ) ) ∈ ℂ ∧ ( 2 · i ) ∈ ℂ ∧ ( 2 · i ) ≠ 0 ) → ( ( 𝐵 − ( ∗ ‘ 𝐵 ) ) / ( 2 · i ) ) = ( ( 1 / ( 2 · i ) ) · ( 𝐵 − ( ∗ ‘ 𝐵 ) ) ) )
29	13 14 28	mp3an23	⊢ ( ( 𝐵 − ( ∗ ‘ 𝐵 ) ) ∈ ℂ → ( ( 𝐵 − ( ∗ ‘ 𝐵 ) ) / ( 2 · i ) ) = ( ( 1 / ( 2 · i ) ) · ( 𝐵 − ( ∗ ‘ 𝐵 ) ) ) )
30	10 29	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐵 − ( ∗ ‘ 𝐵 ) ) / ( 2 · i ) ) = ( ( 1 / ( 2 · i ) ) · ( 𝐵 − ( ∗ ‘ 𝐵 ) ) ) )
31	27 30	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ℑ ‘ 𝐵 ) = ( ( 1 / ( 2 · i ) ) · ( 𝐵 − ( ∗ ‘ 𝐵 ) ) ) )
32	31	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ℑ ‘ 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / ( 2 · i ) ) · ( 𝐵 − ( ∗ ‘ 𝐵 ) ) ) ) )
33	17 25 32	3eqtr4d	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ℑ ‘ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ℑ ‘ 𝐵 ) ) )