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	$⊢ (φ \land x \in X) \to A \in ℂ$
	dvmptcj.b	$⊢ (φ \land x \in X) \to B \in V$
	dvmptcj.da	$⊢ φ \to \frac{d (x \in X⟼ A)}{d_{ℝ} x} = (x \in X ⟼ B)$
Assertion	dvmptcj	$⊢ φ \to \frac{d (x \in X⟼ \overline{A})}{d_{ℝ} x} = (x \in X ⟼ \overline{B})$

Proof

Step	Hyp	Ref	Expression
1		dvmptcj.a	$⊢ (φ \land x \in X) \to A \in ℂ$
2		dvmptcj.b	$⊢ (φ \land x \in X) \to B \in V$
3		dvmptcj.da	$⊢ φ \to \frac{d (x \in X⟼ A)}{d_{ℝ} x} = (x \in X ⟼ B)$
4	1	fmpttd	$⊢ φ \to (x \in X ⟼ A) : X ⟶ ℂ$
5	3	dmeqd	$⊢ φ \to dom \frac{d (x \in X⟼ A)}{d_{ℝ} x} = dom (x \in X ⟼ B)$
6	2	ralrimiva	$⊢ φ \to \forall x \in X B \in V$
7		dmmptg	$⊢ \forall x \in X B \in V \to dom (x \in X ⟼ B) = X$
8	6 7	syl	$⊢ φ \to dom (x \in X ⟼ B) = X$
9	5 8	eqtrd	$⊢ φ \to dom \frac{d (x \in X⟼ A)}{d_{ℝ} x} = X$
10		dvbsss	$⊢ dom \frac{d (x \in X⟼ A)}{d_{ℝ} x} \subseteq ℝ$
11	9 10	eqsstrrdi	$⊢ φ \to X \subseteq ℝ$
12		dvcj	$⊢ ((x \in X ⟼ A) : X ⟶ ℂ \land X \subseteq ℝ) \to ℝ D (* \circ (x \in X ⟼ A)) = * \circ \frac{d (x \in X⟼ A)}{d_{ℝ} x}$
13	4 11 12	syl2anc	$⊢ φ \to ℝ D (* \circ (x \in X ⟼ A)) = * \circ \frac{d (x \in X⟼ A)}{d_{ℝ} x}$
14		cjf	$⊢ * : ℂ ⟶ ℂ$
15	14	a1i	$⊢ φ \to * : ℂ ⟶ ℂ$
16	15 1	cofmpt	$⊢ φ \to * \circ (x \in X ⟼ A) = (x \in X ⟼ \overline{A})$
17	16	oveq2d	$⊢ φ \to ℝ D (* \circ (x \in X ⟼ A)) = \frac{d (x \in X⟼ \overline{A})}{d_{ℝ} x}$
18		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
19	18	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
20	19 1 2 3	dvmptcl	$⊢ (φ \land x \in X) \to B \in ℂ$
21	15	feqmptd	$⊢ φ \to * = (y \in ℂ ⟼ \overline{y})$
22		fveq2	$⊢ y = B \to \overline{y} = \overline{B}$
23	20 3 21 22	fmptco	$⊢ φ \to * \circ \frac{d (x \in X⟼ A)}{d_{ℝ} x} = (x \in X ⟼ \overline{B})$
24	13 17 23	3eqtr3d	$⊢ φ \to \frac{d (x \in X⟼ \overline{A})}{d_{ℝ} x} = (x \in X ⟼ \overline{B})$

Metamath Proof Explorer

Theorem dvmptcj

Proof