dvcjbr

Description: The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj . (This doesn't follow from dvcobr because * is not a function on the reals, and even if we used complex derivatives, * is not complex-differentiable.) (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 10-Feb-2015)

	Ref	Expression
Hypotheses	dvcj.f	$⊢ φ \to F : X ⟶ ℂ$
	dvcj.x	$⊢ φ \to X \subseteq ℝ$
	dvcj.c	$⊢ φ \to C \in dom F_{ℝ}^{'}$
Assertion	dvcjbr	$⊢ φ \to C {(* \circ F)}_{ℝ}^{'} \overline{F_{ℝ}^{'} (C)}$

Proof

Step	Hyp	Ref	Expression
1		dvcj.f	$⊢ φ \to F : X ⟶ ℂ$
2		dvcj.x	$⊢ φ \to X \subseteq ℝ$
3		dvcj.c	$⊢ φ \to C \in dom F_{ℝ}^{'}$
4		ax-resscn	$⊢ ℝ \subseteq ℂ$
5	4	a1i	$⊢ φ \to ℝ \subseteq ℂ$
6		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
7	6	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
8	5 1 2 7 6	dvbssntr	$⊢ φ \to dom F_{ℝ}^{'} \subseteq int (topGen (ran (.))) (X)$
9	8 3	sseldd	$⊢ φ \to C \in int (topGen (ran (.))) (X)$
10	2 4	sstrdi	$⊢ φ \to X \subseteq ℂ$
11	4	a1i	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to ℝ \subseteq ℂ$
12		simpl	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to F : X ⟶ ℂ$
13		simpr	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to X \subseteq ℝ$
14	11 12 13	dvbss	$⊢ (F : X ⟶ ℂ \land X \subseteq ℝ) \to dom F_{ℝ}^{'} \subseteq X$
15	1 2 14	syl2anc	$⊢ φ \to dom F_{ℝ}^{'} \subseteq X$
16	15 3	sseldd	$⊢ φ \to C \in X$
17	1 10 16	dvlem	$⊢ (φ \land x \in (X ∖ \{C\})) \to \frac{F (x) - F (C)}{x - C} \in ℂ$
18	17	fmpttd	$⊢ φ \to (x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C}) : X ∖ \{C\} ⟶ ℂ$
19		ssidd	$⊢ φ \to ℂ \subseteq ℂ$
20	6	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
21	20	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
22		dvf	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ$
23		ffun	$⊢ F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℂ \to Fun F_{ℝ}^{'}$
24		funfvbrb	$⊢ Fun F_{ℝ}^{'} \to (C \in dom F_{ℝ}^{'} \leftrightarrow C F_{ℝ}^{'} F_{ℝ}^{'} (C))$
25	22 23 24	mp2b	$⊢ C \in dom F_{ℝ}^{'} \leftrightarrow C F_{ℝ}^{'} F_{ℝ}^{'} (C)$
26	3 25	sylib	$⊢ φ \to C F_{ℝ}^{'} F_{ℝ}^{'} (C)$
27		eqid	$⊢ (x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C}) = (x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C})$
28	7 6 27 5 1 2	eldv	$⊢ φ \to (C F_{ℝ}^{'} F_{ℝ}^{'} (C) \leftrightarrow (C \in int (topGen (ran (.))) (X) \land F_{ℝ}^{'} (C) \in ((x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C}) {lim}_{ℂ} C)))$
29	26 28	mpbid	$⊢ φ \to (C \in int (topGen (ran (.))) (X) \land F_{ℝ}^{'} (C) \in ((x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C}) {lim}_{ℂ} C))$
30	29	simprd	$⊢ φ \to F_{ℝ}^{'} (C) \in ((x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C}) {lim}_{ℂ} C)$
31		cjcncf	$⊢ * : ℂ \underset{cn}{⟶} ℂ$
32	6	cncfcn1	$⊢ ℂ \underset{cn}{⟶} ℂ = TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld})$
33	31 32	eleqtri	$⊢ * \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld}))$
34	22	ffvelrni	$⊢ C \in dom F_{ℝ}^{'} \to F_{ℝ}^{'} (C) \in ℂ$
35	3 34	syl	$⊢ φ \to F_{ℝ}^{'} (C) \in ℂ$
36		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
37	36	cncnpi	$⊢ (* \in (TopOpen (ℂ_{fld}) Cn TopOpen (ℂ_{fld})) \land F_{ℝ}^{'} (C) \in ℂ) \to * \in (TopOpen (ℂ_{fld}) CnP TopOpen (ℂ_{fld})) (F_{ℝ}^{'} (C))$
38	33 35 37	sylancr	$⊢ φ \to * \in (TopOpen (ℂ_{fld}) CnP TopOpen (ℂ_{fld})) (F_{ℝ}^{'} (C))$
39	18 19 6 21 30 38	limccnp	$⊢ φ \to \overline{F_{ℝ}^{'} (C)} \in ((* \circ (x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C})) {lim}_{ℂ} C)$
40		cjf	$⊢ * : ℂ ⟶ ℂ$
41	40	a1i	$⊢ φ \to * : ℂ ⟶ ℂ$
42	41 17	cofmpt	$⊢ φ \to * \circ (x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C}) = (x \in (X ∖ \{C\}) ⟼ \overline{\frac{F (x) - F (C)}{x - C}})$
43	1	adantr	$⊢ (φ \land x \in (X ∖ \{C\})) \to F : X ⟶ ℂ$
44		eldifi	$⊢ x \in (X ∖ \{C\}) \to x \in X$
45	44	adantl	$⊢ (φ \land x \in (X ∖ \{C\})) \to x \in X$
46	43 45	ffvelrnd	$⊢ (φ \land x \in (X ∖ \{C\})) \to F (x) \in ℂ$
47	1 16	ffvelrnd	$⊢ φ \to F (C) \in ℂ$
48	47	adantr	$⊢ (φ \land x \in (X ∖ \{C\})) \to F (C) \in ℂ$
49	46 48	subcld	$⊢ (φ \land x \in (X ∖ \{C\})) \to F (x) - F (C) \in ℂ$
50	2	sselda	$⊢ (φ \land x \in X) \to x \in ℝ$
51	44 50	sylan2	$⊢ (φ \land x \in (X ∖ \{C\})) \to x \in ℝ$
52	2 16	sseldd	$⊢ φ \to C \in ℝ$
53	52	adantr	$⊢ (φ \land x \in (X ∖ \{C\})) \to C \in ℝ$
54	51 53	resubcld	$⊢ (φ \land x \in (X ∖ \{C\})) \to x - C \in ℝ$
55	54	recnd	$⊢ (φ \land x \in (X ∖ \{C\})) \to x - C \in ℂ$
56	51	recnd	$⊢ (φ \land x \in (X ∖ \{C\})) \to x \in ℂ$
57	53	recnd	$⊢ (φ \land x \in (X ∖ \{C\})) \to C \in ℂ$
58		eldifsni	$⊢ x \in (X ∖ \{C\}) \to x \neq C$
59	58	adantl	$⊢ (φ \land x \in (X ∖ \{C\})) \to x \neq C$
60	56 57 59	subne0d	$⊢ (φ \land x \in (X ∖ \{C\})) \to x - C \neq 0$
61	49 55 60	cjdivd	$⊢ (φ \land x \in (X ∖ \{C\})) \to \overline{\frac{F (x) - F (C)}{x - C}} = \frac{\overline{F (x) - F (C)}}{\overline{x - C}}$
62		cjsub	$⊢ (F (x) \in ℂ \land F (C) \in ℂ) \to \overline{F (x) - F (C)} = \overline{F (x)} - \overline{F (C)}$
63	46 48 62	syl2anc	$⊢ (φ \land x \in (X ∖ \{C\})) \to \overline{F (x) - F (C)} = \overline{F (x)} - \overline{F (C)}$
64		fvco3	$⊢ (F : X ⟶ ℂ \land x \in X) \to (* \circ F) (x) = \overline{F (x)}$
65	1 44 64	syl2an	$⊢ (φ \land x \in (X ∖ \{C\})) \to (* \circ F) (x) = \overline{F (x)}$
66		fvco3	$⊢ (F : X ⟶ ℂ \land C \in X) \to (* \circ F) (C) = \overline{F (C)}$
67	1 16 66	syl2anc	$⊢ φ \to (* \circ F) (C) = \overline{F (C)}$
68	67	adantr	$⊢ (φ \land x \in (X ∖ \{C\})) \to (* \circ F) (C) = \overline{F (C)}$
69	65 68	oveq12d	$⊢ (φ \land x \in (X ∖ \{C\})) \to (* \circ F) (x) - (* \circ F) (C) = \overline{F (x)} - \overline{F (C)}$
70	63 69	eqtr4d	$⊢ (φ \land x \in (X ∖ \{C\})) \to \overline{F (x) - F (C)} = (* \circ F) (x) - (* \circ F) (C)$
71	54	cjred	$⊢ (φ \land x \in (X ∖ \{C\})) \to \overline{x - C} = x - C$
72	70 71	oveq12d	$⊢ (φ \land x \in (X ∖ \{C\})) \to \frac{\overline{F (x) - F (C)}}{\overline{x - C}} = \frac{(* \circ F) (x) - (* \circ F) (C)}{x - C}$
73	61 72	eqtrd	$⊢ (φ \land x \in (X ∖ \{C\})) \to \overline{\frac{F (x) - F (C)}{x - C}} = \frac{(* \circ F) (x) - (* \circ F) (C)}{x - C}$
74	73	mpteq2dva	$⊢ φ \to (x \in (X ∖ \{C\}) ⟼ \overline{\frac{F (x) - F (C)}{x - C}}) = (x \in (X ∖ \{C\}) ⟼ \frac{(* \circ F) (x) - (* \circ F) (C)}{x - C})$
75	42 74	eqtrd	$⊢ φ \to * \circ (x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C}) = (x \in (X ∖ \{C\}) ⟼ \frac{(* \circ F) (x) - (* \circ F) (C)}{x - C})$
76	75	oveq1d	$⊢ φ \to (* \circ (x \in (X ∖ \{C\}) ⟼ \frac{F (x) - F (C)}{x - C})) {lim}_{ℂ} C = (x \in (X ∖ \{C\}) ⟼ \frac{(* \circ F) (x) - (* \circ F) (C)}{x - C}) {lim}_{ℂ} C$
77	39 76	eleqtrd	$⊢ φ \to \overline{F_{ℝ}^{'} (C)} \in ((x \in (X ∖ \{C\}) ⟼ \frac{(* \circ F) (x) - (* \circ F) (C)}{x - C}) {lim}_{ℂ} C)$
78		eqid	$⊢ (x \in (X ∖ \{C\}) ⟼ \frac{(* \circ F) (x) - (* \circ F) (C)}{x - C}) = (x \in (X ∖ \{C\}) ⟼ \frac{(* \circ F) (x) - (* \circ F) (C)}{x - C})$
79		fco	$⊢ (* : ℂ ⟶ ℂ \land F : X ⟶ ℂ) \to (* \circ F) : X ⟶ ℂ$
80	40 1 79	sylancr	$⊢ φ \to (* \circ F) : X ⟶ ℂ$
81	7 6 78 5 80 2	eldv	$⊢ φ \to (C {(* \circ F)}_{ℝ}^{'} \overline{F_{ℝ}^{'} (C)} \leftrightarrow (C \in int (topGen (ran (.))) (X) \land \overline{F_{ℝ}^{'} (C)} \in ((x \in (X ∖ \{C\}) ⟼ \frac{(* \circ F) (x) - (* \circ F) (C)}{x - C}) {lim}_{ℂ} C)))$
82	9 77 81	mpbir2and	$⊢ φ \to C {(* \circ F)}_{ℝ}^{'} \overline{F_{ℝ}^{'} (C)}$

Metamath Proof Explorer

Theorem dvcjbr

Proof