Metamath Proof Explorer

Theorem 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 ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( ℝ D ( ∗ ∘ 𝐹 ) ) = ( ∗ ∘ ( ℝ D 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 dvf ⊢ ( ℝ D ( ∗ ∘ 𝐹 ) ) : dom ( ℝ D ( ∗ ∘ 𝐹 ) ) ⟶ ℂ
2 ffun ⊢ ( ( ℝ D ( ∗ ∘ 𝐹 ) ) : dom ( ℝ D ( ∗ ∘ 𝐹 ) ) ⟶ ℂ → Fun ( ℝ D ( ∗ ∘ 𝐹 ) ) )
3 1 2 ax-mp ⊢ Fun ( ℝ D ( ∗ ∘ 𝐹 ) )
4 simpll ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → 𝐹 : 𝑋 ⟶ ℂ )
5 simplr ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → 𝑋 ⊆ ℝ )
6 simpr ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → 𝑥 ∈ dom ( ℝ D 𝐹 ) )
7 4 5 6 dvcjbr ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → 𝑥 ( ℝ D ( ∗ ∘ 𝐹 ) ) ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
8 funbrfv ⊢ ( Fun ( ℝ D ( ∗ ∘ 𝐹 ) ) → ( 𝑥 ( ℝ D ( ∗ ∘ 𝐹 ) ) ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) → ( ( ℝ D ( ∗ ∘ 𝐹 ) ) ‘ 𝑥 ) = ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
9 3 7 8 mpsyl ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → ( ( ℝ D ( ∗ ∘ 𝐹 ) ) ‘ 𝑥 ) = ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
10 9 mpteq2dva ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( 𝑥 ∈ dom ( ℝ D 𝐹 ) ↦ ( ( ℝ D ( ∗ ∘ 𝐹 ) ) ‘ 𝑥 ) ) = ( 𝑥 ∈ dom ( ℝ D 𝐹 ) ↦ ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
11 cjf ⊢ ∗ : ℂ ⟶ ℂ
12 fco ⊢ ( ( ∗ : ℂ ⟶ ℂ ∧ 𝐹 : 𝑋 ⟶ ℂ ) → ( ∗ ∘ 𝐹 ) : 𝑋 ⟶ ℂ )
13 11 12 mpan ⊢ ( 𝐹 : 𝑋 ⟶ ℂ → ( ∗ ∘ 𝐹 ) : 𝑋 ⟶ ℂ )
14 13 ad2antrr ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D ( ∗ ∘ 𝐹 ) ) ) → ( ∗ ∘ 𝐹 ) : 𝑋 ⟶ ℂ )
15 simplr ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D ( ∗ ∘ 𝐹 ) ) ) → 𝑋 ⊆ ℝ )
16 simpr ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D ( ∗ ∘ 𝐹 ) ) ) → 𝑥 ∈ dom ( ℝ D ( ∗ ∘ 𝐹 ) ) )
17 14 15 16 dvcjbr ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D ( ∗ ∘ 𝐹 ) ) ) → 𝑥 ( ℝ D ( ∗ ∘ ( ∗ ∘ 𝐹 ) ) ) ( ∗ ‘ ( ( ℝ D ( ∗ ∘ 𝐹 ) ) ‘ 𝑥 ) ) )
18 vex ⊢ 𝑥 ∈ V
19 fvex ⊢ ( ∗ ‘ ( ( ℝ D ( ∗ ∘ 𝐹 ) ) ‘ 𝑥 ) ) ∈ V
20 18 19 breldm ⊢ ( 𝑥 ( ℝ D ( ∗ ∘ ( ∗ ∘ 𝐹 ) ) ) ( ∗ ‘ ( ( ℝ D ( ∗ ∘ 𝐹 ) ) ‘ 𝑥 ) ) → 𝑥 ∈ dom ( ℝ D ( ∗ ∘ ( ∗ ∘ 𝐹 ) ) ) )
21 17 20 syl ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D ( ∗ ∘ 𝐹 ) ) ) → 𝑥 ∈ dom ( ℝ D ( ∗ ∘ ( ∗ ∘ 𝐹 ) ) ) )
22 21 ex ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( 𝑥 ∈ dom ( ℝ D ( ∗ ∘ 𝐹 ) ) → 𝑥 ∈ dom ( ℝ D ( ∗ ∘ ( ∗ ∘ 𝐹 ) ) ) ) )
23 22 ssrdv ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → dom ( ℝ D ( ∗ ∘ 𝐹 ) ) ⊆ dom ( ℝ D ( ∗ ∘ ( ∗ ∘ 𝐹 ) ) ) )
24 ffvelcdm ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
25 24 adantlr ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
26 25 cjcjd ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ∗ ‘ ( ∗ ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝐹 ‘ 𝑥 ) )
27 26 mpteq2dva ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( 𝑥 ∈ 𝑋 ↦ ( ∗ ‘ ( ∗ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) )
28 25 cjcld ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ 𝑋 ) → ( ∗ ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℂ )
29 simpl ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → 𝐹 : 𝑋 ⟶ ℂ )
30 29 feqmptd ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → 𝐹 = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 ‘ 𝑥 ) ) )
31 11 a1i ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ∗ : ℂ ⟶ ℂ )
32 31 feqmptd ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ∗ = ( 𝑦 ∈ ℂ ↦ ( ∗ ‘ 𝑦 ) ) )
33 fveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ∗ ‘ 𝑦 ) = ( ∗ ‘ ( 𝐹 ‘ 𝑥 ) ) )
34 25 30 32 33 fmptco ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( ∗ ∘ 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ( ∗ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
35 fveq2 ⊢ ( 𝑦 = ( ∗ ‘ ( 𝐹 ‘ 𝑥 ) ) → ( ∗ ‘ 𝑦 ) = ( ∗ ‘ ( ∗ ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
36 28 34 32 35 fmptco ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( ∗ ∘ ( ∗ ∘ 𝐹 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ∗ ‘ ( ∗ ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) )
37 27 36 30 3eqtr4d ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( ∗ ∘ ( ∗ ∘ 𝐹 ) ) = 𝐹 )
38 37 oveq2d ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( ℝ D ( ∗ ∘ ( ∗ ∘ 𝐹 ) ) ) = ( ℝ D 𝐹 ) )
39 38 dmeqd ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → dom ( ℝ D ( ∗ ∘ ( ∗ ∘ 𝐹 ) ) ) = dom ( ℝ D 𝐹 ) )
40 23 39 sseqtrd ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → dom ( ℝ D ( ∗ ∘ 𝐹 ) ) ⊆ dom ( ℝ D 𝐹 ) )
41 fvex ⊢ ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ∈ V
42 18 41 breldm ⊢ ( 𝑥 ( ℝ D ( ∗ ∘ 𝐹 ) ) ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) → 𝑥 ∈ dom ( ℝ D ( ∗ ∘ 𝐹 ) ) )
43 7 42 syl ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → 𝑥 ∈ dom ( ℝ D ( ∗ ∘ 𝐹 ) ) )
44 40 43 eqelssd ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → dom ( ℝ D ( ∗ ∘ 𝐹 ) ) = dom ( ℝ D 𝐹 ) )
45 44 feq2d ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( ( ℝ D ( ∗ ∘ 𝐹 ) ) : dom ( ℝ D ( ∗ ∘ 𝐹 ) ) ⟶ ℂ ↔ ( ℝ D ( ∗ ∘ 𝐹 ) ) : dom ( ℝ D 𝐹 ) ⟶ ℂ ) )
46 1 45 mpbii ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( ℝ D ( ∗ ∘ 𝐹 ) ) : dom ( ℝ D 𝐹 ) ⟶ ℂ )
47 46 feqmptd ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( ℝ D ( ∗ ∘ 𝐹 ) ) = ( 𝑥 ∈ dom ( ℝ D 𝐹 ) ↦ ( ( ℝ D ( ∗ ∘ 𝐹 ) ) ‘ 𝑥 ) ) )
48 dvf ⊢ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ
49 48 ffvelcdmi ⊢ ( 𝑥 ∈ dom ( ℝ D 𝐹 ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
50 49 adantl ⊢ ( ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) ∧ 𝑥 ∈ dom ( ℝ D 𝐹 ) ) → ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
51 48 a1i ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℂ )
52 51 feqmptd ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( ℝ D 𝐹 ) = ( 𝑥 ∈ dom ( ℝ D 𝐹 ) ↦ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
53 fveq2 ⊢ ( 𝑦 = ( ( ℝ D 𝐹 ) ‘ 𝑥 ) → ( ∗ ‘ 𝑦 ) = ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) )
54 50 52 32 53 fmptco ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( ∗ ∘ ( ℝ D 𝐹 ) ) = ( 𝑥 ∈ dom ( ℝ D 𝐹 ) ↦ ( ∗ ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ) )
55 10 47 54 3eqtr4d ⊢ ( ( 𝐹 : 𝑋 ⟶ ℂ ∧ 𝑋 ⊆ ℝ ) → ( ℝ D ( ∗ ∘ 𝐹 ) ) = ( ∗ ∘ ( ℝ D 𝐹 ) ) )