Metamath Proof Explorer

Theorem 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 ⊢φ→F:X⟶ℂ
dvcj.x ⊢φ→X⊆ℝ
dvcj.c ⊢φ→C∈dom⁡Fℝ′
Assertion dvcjbr ⊢φ→C*∘Fℝ′Fℝ′⁡C‾

Proof

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