MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvcjbr Structured version   Visualization version   GIF version

Theorem dvcjbr 24701
Description: The derivative of the conjugate of a function. For the (simpler but more limited) function version, see dvcj 24702. (This doesn't follow from dvcobr 24698 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.)
Hypotheses
Ref Expression
dvcj.f (𝜑𝐹:𝑋⟶ℂ)
dvcj.x (𝜑𝑋 ⊆ ℝ)
dvcj.c (𝜑𝐶 ∈ dom (ℝ D 𝐹))
Assertion
Ref Expression
dvcjbr (𝜑𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D 𝐹)‘𝐶)))

Proof of Theorem dvcjbr
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ax-resscn 10673 . . . . 5 ℝ ⊆ ℂ
21a1i 11 . . . 4 (𝜑 → ℝ ⊆ ℂ)
3 dvcj.f . . . 4 (𝜑𝐹:𝑋⟶ℂ)
4 dvcj.x . . . 4 (𝜑𝑋 ⊆ ℝ)
5 eqid 2738 . . . . 5 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
65tgioo2 23556 . . . 4 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
72, 3, 4, 6, 5dvbssntr 24652 . . 3 (𝜑 → dom (ℝ D 𝐹) ⊆ ((int‘(topGen‘ran (,)))‘𝑋))
8 dvcj.c . . 3 (𝜑𝐶 ∈ dom (ℝ D 𝐹))
97, 8sseldd 3879 . 2 (𝜑𝐶 ∈ ((int‘(topGen‘ran (,)))‘𝑋))
104, 1sstrdi 3890 . . . . . 6 (𝜑𝑋 ⊆ ℂ)
111a1i 11 . . . . . . . . 9 ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → ℝ ⊆ ℂ)
12 simpl 486 . . . . . . . . 9 ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → 𝐹:𝑋⟶ℂ)
13 simpr 488 . . . . . . . . 9 ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → 𝑋 ⊆ ℝ)
1411, 12, 13dvbss 24653 . . . . . . . 8 ((𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ ℝ) → dom (ℝ D 𝐹) ⊆ 𝑋)
153, 4, 14syl2anc 587 . . . . . . 7 (𝜑 → dom (ℝ D 𝐹) ⊆ 𝑋)
1615, 8sseldd 3879 . . . . . 6 (𝜑𝐶𝑋)
173, 10, 16dvlem 24648 . . . . 5 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶)) ∈ ℂ)
1817fmpttd 6890 . . . 4 (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶))):(𝑋 ∖ {𝐶})⟶ℂ)
19 ssidd 3901 . . . 4 (𝜑 → ℂ ⊆ ℂ)
205cnfldtopon 23536 . . . . 5 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
2120toponrestid 21673 . . . 4 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
22 dvf 24659 . . . . . . . 8 (ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ
23 ffun 6508 . . . . . . . 8 ((ℝ D 𝐹):dom (ℝ D 𝐹)⟶ℂ → Fun (ℝ D 𝐹))
24 funfvbrb 6829 . . . . . . . 8 (Fun (ℝ D 𝐹) → (𝐶 ∈ dom (ℝ D 𝐹) ↔ 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶)))
2522, 23, 24mp2b 10 . . . . . . 7 (𝐶 ∈ dom (ℝ D 𝐹) ↔ 𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶))
268, 25sylib 221 . . . . . 6 (𝜑𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶))
27 eqid 2738 . . . . . . 7 (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶)))
286, 5, 27, 2, 3, 4eldv 24650 . . . . . 6 (𝜑 → (𝐶(ℝ D 𝐹)((ℝ D 𝐹)‘𝐶) ↔ (𝐶 ∈ ((int‘(topGen‘ran (,)))‘𝑋) ∧ ((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶))) lim 𝐶))))
2926, 28mpbid 235 . . . . 5 (𝜑 → (𝐶 ∈ ((int‘(topGen‘ran (,)))‘𝑋) ∧ ((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶))) lim 𝐶)))
3029simprd 499 . . . 4 (𝜑 → ((ℝ D 𝐹)‘𝐶) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶))) lim 𝐶))
31 cjcncf 23657 . . . . . 6 ∗ ∈ (ℂ–cn→ℂ)
325cncfcn1 23664 . . . . . 6 (ℂ–cn→ℂ) = ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
3331, 32eleqtri 2831 . . . . 5 ∗ ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld))
3422ffvelrni 6861 . . . . . 6 (𝐶 ∈ dom (ℝ D 𝐹) → ((ℝ D 𝐹)‘𝐶) ∈ ℂ)
358, 34syl 17 . . . . 5 (𝜑 → ((ℝ D 𝐹)‘𝐶) ∈ ℂ)
36 unicntop 23539 . . . . . 6 ℂ = (TopOpen‘ℂfld)
3736cncnpi 22030 . . . . 5 ((∗ ∈ ((TopOpen‘ℂfld) Cn (TopOpen‘ℂfld)) ∧ ((ℝ D 𝐹)‘𝐶) ∈ ℂ) → ∗ ∈ (((TopOpen‘ℂfld) CnP (TopOpen‘ℂfld))‘((ℝ D 𝐹)‘𝐶)))
3833, 35, 37sylancr 590 . . . 4 (𝜑 → ∗ ∈ (((TopOpen‘ℂfld) CnP (TopOpen‘ℂfld))‘((ℝ D 𝐹)‘𝐶)))
3918, 19, 5, 21, 30, 38limccnp 24643 . . 3 (𝜑 → (∗‘((ℝ D 𝐹)‘𝐶)) ∈ ((∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶)))) lim 𝐶))
40 cjf 14554 . . . . . . 7 ∗:ℂ⟶ℂ
4140a1i 11 . . . . . 6 (𝜑 → ∗:ℂ⟶ℂ)
4241, 17cofmpt 6905 . . . . 5 (𝜑 → (∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (∗‘(((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶)))))
433adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐹:𝑋⟶ℂ)
44 eldifi 4018 . . . . . . . . . . 11 (𝑥 ∈ (𝑋 ∖ {𝐶}) → 𝑥𝑋)
4544adantl 485 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥𝑋)
4643, 45ffvelrnd 6863 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝐹𝑥) ∈ ℂ)
473, 16ffvelrnd 6863 . . . . . . . . . 10 (𝜑 → (𝐹𝐶) ∈ ℂ)
4847adantr 484 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝐹𝐶) ∈ ℂ)
4946, 48subcld 11076 . . . . . . . 8 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → ((𝐹𝑥) − (𝐹𝐶)) ∈ ℂ)
504sselda 3878 . . . . . . . . . . 11 ((𝜑𝑥𝑋) → 𝑥 ∈ ℝ)
5144, 50sylan2 596 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ ℝ)
524, 16sseldd 3879 . . . . . . . . . . 11 (𝜑𝐶 ∈ ℝ)
5352adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐶 ∈ ℝ)
5451, 53resubcld 11147 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥𝐶) ∈ ℝ)
5554recnd 10748 . . . . . . . 8 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥𝐶) ∈ ℂ)
5651recnd 10748 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥 ∈ ℂ)
5753recnd 10748 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝐶 ∈ ℂ)
58 eldifsni 4679 . . . . . . . . . 10 (𝑥 ∈ (𝑋 ∖ {𝐶}) → 𝑥𝐶)
5958adantl 485 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → 𝑥𝐶)
6056, 57, 59subne0d 11085 . . . . . . . 8 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → (𝑥𝐶) ≠ 0)
6149, 55, 60cjdivd 14673 . . . . . . 7 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶))) = ((∗‘((𝐹𝑥) − (𝐹𝐶))) / (∗‘(𝑥𝐶))))
62 cjsub 14599 . . . . . . . . . 10 (((𝐹𝑥) ∈ ℂ ∧ (𝐹𝐶) ∈ ℂ) → (∗‘((𝐹𝑥) − (𝐹𝐶))) = ((∗‘(𝐹𝑥)) − (∗‘(𝐹𝐶))))
6346, 48, 62syl2anc 587 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘((𝐹𝑥) − (𝐹𝐶))) = ((∗‘(𝐹𝑥)) − (∗‘(𝐹𝐶))))
64 fvco3 6768 . . . . . . . . . . 11 ((𝐹:𝑋⟶ℂ ∧ 𝑥𝑋) → ((∗ ∘ 𝐹)‘𝑥) = (∗‘(𝐹𝑥)))
653, 44, 64syl2an 599 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗ ∘ 𝐹)‘𝑥) = (∗‘(𝐹𝑥)))
66 fvco3 6768 . . . . . . . . . . . 12 ((𝐹:𝑋⟶ℂ ∧ 𝐶𝑋) → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹𝐶)))
673, 16, 66syl2anc 587 . . . . . . . . . . 11 (𝜑 → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹𝐶)))
6867adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗ ∘ 𝐹)‘𝐶) = (∗‘(𝐹𝐶)))
6965, 68oveq12d 7189 . . . . . . . . 9 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → (((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) = ((∗‘(𝐹𝑥)) − (∗‘(𝐹𝐶))))
7063, 69eqtr4d 2776 . . . . . . . 8 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘((𝐹𝑥) − (𝐹𝐶))) = (((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)))
7154cjred 14676 . . . . . . . 8 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(𝑥𝐶)) = (𝑥𝐶))
7270, 71oveq12d 7189 . . . . . . 7 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → ((∗‘((𝐹𝑥) − (𝐹𝐶))) / (∗‘(𝑥𝐶))) = ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥𝐶)))
7361, 72eqtrd 2773 . . . . . 6 ((𝜑𝑥 ∈ (𝑋 ∖ {𝐶})) → (∗‘(((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶))) = ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥𝐶)))
7473mpteq2dva 5126 . . . . 5 (𝜑 → (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (∗‘(((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥𝐶))))
7542, 74eqtrd 2773 . . . 4 (𝜑 → (∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶)))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥𝐶))))
7675oveq1d 7186 . . 3 (𝜑 → ((∗ ∘ (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ (((𝐹𝑥) − (𝐹𝐶)) / (𝑥𝐶)))) lim 𝐶) = ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥𝐶))) lim 𝐶))
7739, 76eleqtrd 2835 . 2 (𝜑 → (∗‘((ℝ D 𝐹)‘𝐶)) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥𝐶))) lim 𝐶))
78 eqid 2738 . . 3 (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥𝐶))) = (𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥𝐶)))
79 fco 6529 . . . 4 ((∗:ℂ⟶ℂ ∧ 𝐹:𝑋⟶ℂ) → (∗ ∘ 𝐹):𝑋⟶ℂ)
8040, 3, 79sylancr 590 . . 3 (𝜑 → (∗ ∘ 𝐹):𝑋⟶ℂ)
816, 5, 78, 2, 80, 4eldv 24650 . 2 (𝜑 → (𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D 𝐹)‘𝐶)) ↔ (𝐶 ∈ ((int‘(topGen‘ran (,)))‘𝑋) ∧ (∗‘((ℝ D 𝐹)‘𝐶)) ∈ ((𝑥 ∈ (𝑋 ∖ {𝐶}) ↦ ((((∗ ∘ 𝐹)‘𝑥) − ((∗ ∘ 𝐹)‘𝐶)) / (𝑥𝐶))) lim 𝐶))))
829, 77, 81mpbir2and 713 1 (𝜑𝐶(ℝ D (∗ ∘ 𝐹))(∗‘((ℝ D 𝐹)‘𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1542  wcel 2113  wne 2934  cdif 3841  wss 3844  {csn 4517   class class class wbr 5031  cmpt 5111  dom cdm 5526  ran crn 5527  ccom 5530  Fun wfun 6334  wf 6336  cfv 6340  (class class class)co 7171  cc 10614  cr 10615  cmin 10949   / cdiv 11376  (,)cioo 12822  ccj 14546  TopOpenctopn 16799  topGenctg 16815  fldccnfld 20218  intcnt 21769   Cn ccn 21976   CnP ccnp 21977  cnccncf 23629   lim climc 24614   D cdv 24615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5233  ax-pr 5297  ax-un 7480  ax-cnex 10672  ax-resscn 10673  ax-1cn 10674  ax-icn 10675  ax-addcl 10676  ax-addrcl 10677  ax-mulcl 10678  ax-mulrcl 10679  ax-mulcom 10680  ax-addass 10681  ax-mulass 10682  ax-distr 10683  ax-i2m1 10684  ax-1ne0 10685  ax-1rid 10686  ax-rnegex 10687  ax-rrecex 10688  ax-cnre 10689  ax-pre-lttri 10690  ax-pre-lttrn 10691  ax-pre-ltadd 10692  ax-pre-mulgt0 10693  ax-pre-sup 10694
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-reu 3060  df-rmo 3061  df-rab 3062  df-v 3400  df-sbc 3683  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-pss 3863  df-nul 4213  df-if 4416  df-pw 4491  df-sn 4518  df-pr 4520  df-tp 4522  df-op 4524  df-uni 4798  df-int 4838  df-iun 4884  df-iin 4885  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5484  df-we 5486  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-ord 6176  df-on 6177  df-lim 6178  df-suc 6179  df-iota 6298  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7128  df-ov 7174  df-oprab 7175  df-mpo 7176  df-om 7601  df-1st 7715  df-2nd 7716  df-wrecs 7977  df-recs 8038  df-rdg 8076  df-1o 8132  df-er 8321  df-map 8440  df-pm 8441  df-en 8557  df-dom 8558  df-sdom 8559  df-fin 8560  df-fi 8949  df-sup 8980  df-inf 8981  df-pnf 10756  df-mnf 10757  df-xr 10758  df-ltxr 10759  df-le 10760  df-sub 10951  df-neg 10952  df-div 11377  df-nn 11718  df-2 11780  df-3 11781  df-4 11782  df-5 11783  df-6 11784  df-7 11785  df-8 11786  df-9 11787  df-n0 11978  df-z 12064  df-dec 12181  df-uz 12326  df-q 12432  df-rp 12474  df-xneg 12591  df-xadd 12592  df-xmul 12593  df-ioo 12826  df-icc 12829  df-fz 12983  df-seq 13462  df-exp 13523  df-cj 14549  df-re 14550  df-im 14551  df-sqrt 14685  df-abs 14686  df-struct 16589  df-ndx 16590  df-slot 16591  df-base 16593  df-plusg 16682  df-mulr 16683  df-starv 16684  df-tset 16688  df-ple 16689  df-ds 16691  df-unif 16692  df-rest 16800  df-topn 16801  df-topgen 16821  df-psmet 20210  df-xmet 20211  df-met 20212  df-bl 20213  df-mopn 20214  df-fbas 20215  df-fg 20216  df-cnfld 20219  df-top 21646  df-topon 21663  df-topsp 21685  df-bases 21698  df-cld 21771  df-ntr 21772  df-cls 21773  df-nei 21850  df-lp 21888  df-perf 21889  df-cn 21979  df-cnp 21980  df-haus 22067  df-fil 22598  df-fm 22690  df-flim 22691  df-flf 22692  df-xms 23074  df-ms 23075  df-cncf 23631  df-limc 24618  df-dv 24619
This theorem is referenced by:  dvcj  24702
  Copyright terms: Public domain W3C validator