dvcj

Description: The derivative of the conjugate of a function. For the (more general) relation version, see dvcjbr . (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 10-Feb-2015)

		Ref	Expression
	Assertion	dvcj	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to ℝ D (* \circ F) = * \circ F_{ℝ}^{'}$

Proof

Step	Hyp	Ref	Expression
1		dvf	$⊢ {(* \circ F)}_{ℝ}^{'} : dom {(* \circ F)}_{ℝ}^{'} ⟶ ℂ$
2		ffun	$⊢ {(* \circ F)}_{ℝ}^{'} : dom {(* \circ F)}_{ℝ}^{'} ⟶ ℂ \to Fun {(* \circ F)}_{ℝ}^{'}$
3	1 2	ax-mp	$⊢ Fun {(* \circ F)}_{ℝ}^{'}$
4		simpll	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in dom F_{ℝ}^{'}) \to F : X ⟶ ℂ$
5		simplr	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in dom F_{ℝ}^{'}) \to X \subseteq ℝ$
6		simpr	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in dom F_{ℝ}^{'}) \to x \in dom F_{ℝ}^{'}$
7	4 5 6	dvcjbr	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in dom F_{ℝ}^{'}) \to x {(* \circ F)}_{ℝ}^{'} \overline{F_{ℝ}^{'} (x)}$
8		funbrfv	$⊢ Fun {(* \circ F)}_{ℝ}^{'} \to (x {(* \circ F)}_{ℝ}^{'} \overline{F_{ℝ}^{'} (x)} \to {(* \circ F)}_{ℝ}^{'} (x) = \overline{F_{ℝ}^{'} (x)})$
9	3 7 8	mpsyl	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in dom F_{ℝ}^{'}) \to {(* \circ F)}_{ℝ}^{'} (x) = \overline{F_{ℝ}^{'} (x)}$
10	9	mpteq2dva	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to (x \in dom F_{ℝ}^{'} ⟼ {(* \circ F)}_{ℝ}^{'} (x)) = (x \in dom F_{ℝ}^{'} ⟼ \overline{F_{ℝ}^{'} (x)})$
11		cjf	$⊢ * : ℂ ⟶ ℂ$
12		fco	$⊢ (* : ℂ ⟶ ℂ \land F : X ⟶ ℂ) \to (* \circ F) : X ⟶ ℂ$
13	11 12	mpan	$⊢ F : X ⟶ ℂ \to (* \circ F) : X ⟶ ℂ$
14	13	ad2antrr	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in dom {(* \circ F)}_{ℝ}^{'}) \to (* \circ F) : X ⟶ ℂ$
15		simplr	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in dom {(* \circ F)}_{ℝ}^{'}) \to X \subseteq ℝ$
16		simpr	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in dom {(* \circ F)}_{ℝ}^{'}) \to x \in dom {(* \circ F)}_{ℝ}^{'}$
17	14 15 16	dvcjbr	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in dom {(* \circ F)}_{ℝ}^{'}) \to x {(* \circ (* \circ F))}_{ℝ}^{'} \overline{{(* \circ F)}_{ℝ}^{'} (x)}$
18		vex	$⊢ x \in V$
19		fvex	$⊢ \overline{{(* \circ F)}_{ℝ}^{'} (x)} \in V$
20	18 19	breldm	$⊢ x {(* \circ (* \circ F))}_{ℝ}^{'} \overline{{(* \circ F)}_{ℝ}^{'} (x)} \to x \in dom {(* \circ (* \circ F))}_{ℝ}^{'}$
21	17 20	syl	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in dom {(* \circ F)}_{ℝ}^{'}) \to x \in dom {(* \circ (* \circ F))}_{ℝ}^{'}$
22	21	ex	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to (x \in dom {(* \circ F)}_{ℝ}^{'} \to x \in dom {(* \circ (* \circ F))}_{ℝ}^{'})$
23	22	ssrdv	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to dom {(* \circ F)}_{ℝ}^{'} \subseteq dom {(* \circ (* \circ F))}_{ℝ}^{'}$
24		ffvelcdm	$⊢ (F : X ⟶ ℂ \land x \in X) \to F (x) \in ℂ$
25	24	adantlr	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in X) \to F (x) \in ℂ$
26	25	cjcjd	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in X) \to \overline{\overline{F (x)}} = F (x)$
27	26	mpteq2dva	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to (x \in X ⟼ \overline{\overline{F (x)}}) = (x \in X ⟼ F (x))$
28	25	cjcld	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in X) \to \overline{F (x)} \in ℂ$
29		simpl	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to F : X ⟶ ℂ$
30	29	feqmptd	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to F = (x \in X ⟼ F (x))$
31	11	a1i	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to * : ℂ ⟶ ℂ$
32	31	feqmptd	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to * = (y \in ℂ ⟼ \overline{y})$
33		fveq2	$⊢ y = F (x) \to \overline{y} = \overline{F (x)}$
34	25 30 32 33	fmptco	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to * \circ F = (x \in X ⟼ \overline{F (x)})$
35		fveq2	$⊢ y = \overline{F (x)} \to \overline{y} = \overline{\overline{F (x)}}$
36	28 34 32 35	fmptco	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to * \circ (* \circ F) = (x \in X ⟼ \overline{\overline{F (x)}})$
37	27 36 30	3eqtr4d	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to * \circ (* \circ F) = F$
38	37	oveq2d	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to ℝ D (* \circ (* \circ F)) = ℝ D F$
39	38	dmeqd	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to dom {(* \circ (* \circ F))}_{ℝ}^{'} = dom F_{ℝ}^{'}$
40	23 39	sseqtrd	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to dom {(* \circ F)}_{ℝ}^{'} \subseteq dom F_{ℝ}^{'}$
41		fvex	$⊢ \overline{F_{ℝ}^{'} (x)} \in V$
42	18 41	breldm	$⊢ x {(* \circ F)}_{ℝ}^{'} \overline{F_{ℝ}^{'} (x)} \to x \in dom {(* \circ F)}_{ℝ}^{'}$
43	7 42	syl	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in dom F_{ℝ}^{'}) \to x \in dom {(* \circ F)}_{ℝ}^{'}$
44	40 43	eqelssd	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to dom {(* \circ F)}_{ℝ}^{'} = dom F_{ℝ}^{'}$
45	44	feq2d	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to ({(* \circ F)}_{ℝ}^{'} : dom {(* \circ F)}_{ℝ}^{'} ⟶ ℂ \leftrightarrow {(* \circ F)}_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ)$
46	1 45	mpbii	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to {(* \circ F)}_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
47	46	feqmptd	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to ℝ D (* \circ F) = (x \in dom F_{ℝ}^{'} ⟼ {(* \circ F)}_{ℝ}^{'} (x))$
48		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
49	48	ffvelcdmi	$⊢ x \in dom F_{ℝ}^{'} \to F_{ℝ}^{'} (x) \in ℂ$
50	49	adantl	$⊢ ((F : X ⟶ ℂ \land X \subseteq ℝ) \land x \in dom F_{ℝ}^{'}) \to F_{ℝ}^{'} (x) \in ℂ$
51	48	a1i	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
52	51	feqmptd	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to ℝ D F = (x \in dom F_{ℝ}^{'} ⟼ F_{ℝ}^{'} (x))$
53		fveq2	$⊢ y = F_{ℝ}^{'} (x) \to \overline{y} = \overline{F_{ℝ}^{'} (x)}$
54	50 52 32 53	fmptco	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to * \circ F_{ℝ}^{'} = (x \in dom F_{ℝ}^{'} ⟼ \overline{F_{ℝ}^{'} (x)})$
55	10 47 54	3eqtr4d	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to ℝ D (* \circ F) = * \circ F_{ℝ}^{'}$

Metamath Proof Explorer

Theorem dvcj

Proof