Theorem dvmptcj

Description: Function-builder for derivative, conjugate rule. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		dvmptcj.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
2		dvmptcj.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
3		dvmptcj.da	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
4	1	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
5	3	dmeqd	⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
6	2	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 )
7		dmmptg	⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
8	6 7	syl	⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
9	5 8	eqtrd	⊢ ( 𝜑 → dom ( ℝ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = 𝑋 )
10		dvbsss	⊢ dom ( ℝ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ⊆ ℝ
11	9 10	eqsstrrdi	⊢ ( 𝜑 → 𝑋 ⊆ ℝ )
12		dvcj	⊢ ( ( ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( ℝ D ( ∗ ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) = ( ∗ ∘ ( ℝ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) )
13	4 11 12	syl2anc	⊢ ( 𝜑 → ( ℝ D ( ∗ ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) = ( ∗ ∘ ( ℝ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) )
14		cjf	⊢ ∗ : ℂ ⟶ ℂ
15	14	a1i	⊢ ( 𝜑 → ∗ : ℂ ⟶ ℂ )
16	15 1	cofmpt	⊢ ( 𝜑 → ( ∗ ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ∗ ‘ 𝐴 ) ) )
17	16	oveq2d	⊢ ( 𝜑 → ( ℝ D ( ∗ ∘ ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) = ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ∗ ‘ 𝐴 ) ) ) )
18		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
19	18	a1i	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
20	19 1 2 3	dvmptcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
21	15	feqmptd	⊢ ( 𝜑 → ∗ = ( 𝑦 ∈ ℂ ↦ ( ∗ ‘ 𝑦 ) ) )
22		fveq2	⊢ ( 𝑦 = 𝐵 → ( ∗ ‘ 𝑦 ) = ( ∗ ‘ 𝐵 ) )
23	20 3 21 22	fmptco	⊢ ( 𝜑 → ( ∗ ∘ ( ℝ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ∗ ‘ 𝐵 ) ) )
24	13 17 23	3eqtr3d	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ∗ ‘ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ∗ ‘ 𝐵 ) ) )