Metamath Proof Explorer

Theorem dvsinax

Description: Derivative exercise: the derivative with respect to y of sin(Ay), given a constant A . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Assertion dvsinax ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sinf ⊢ sin : ℂ ⟶ ℂ
2 1 a1i ⊢ ( 𝐴 ∈ ℂ → sin : ℂ ⟶ ℂ )
3 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝐴 · 𝑦 ) ∈ ℂ )
4 3 fmpttd ⊢ ( 𝐴 ∈ ℂ → ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) : ℂ ⟶ ℂ )
5 fcompt ⊢ ( ( sin : ℂ ⟶ ℂ ∧ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) : ℂ ⟶ ℂ ) → ( sin ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ( 𝑤 ∈ ℂ ↦ ( sin ‘ ( ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ‘ 𝑤 ) ) ) )
6 2 4 5 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( sin ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ( 𝑤 ∈ ℂ ↦ ( sin ‘ ( ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ‘ 𝑤 ) ) ) )
7 eqidd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) )
8 oveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐴 · 𝑦 ) = ( 𝐴 · 𝑤 ) )
9 8 adantl ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ∧ 𝑦 = 𝑤 ) → ( 𝐴 · 𝑦 ) = ( 𝐴 · 𝑤 ) )
10 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → 𝑤 ∈ ℂ )
11 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 𝐴 · 𝑤 ) ∈ ℂ )
12 7 9 10 11 fvmptd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ‘ 𝑤 ) = ( 𝐴 · 𝑤 ) )
13 12 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( sin ‘ ( ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ‘ 𝑤 ) ) = ( sin ‘ ( 𝐴 · 𝑤 ) ) )
14 13 mpteq2dva ⊢ ( 𝐴 ∈ ℂ → ( 𝑤 ∈ ℂ ↦ ( sin ‘ ( ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑤 ) ) ) )
15 oveq2 ⊢ ( 𝑤 = 𝑦 → ( 𝐴 · 𝑤 ) = ( 𝐴 · 𝑦 ) )
16 15 fveq2d ⊢ ( 𝑤 = 𝑦 → ( sin ‘ ( 𝐴 · 𝑤 ) ) = ( sin ‘ ( 𝐴 · 𝑦 ) ) )
17 16 cbvmptv ⊢ ( 𝑤 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑤 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) )
18 17 a1i ⊢ ( 𝐴 ∈ ℂ → ( 𝑤 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑤 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) )
19 6 14 18 3eqtrrd ⊢ ( 𝐴 ∈ ℂ → ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) = ( sin ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) )
20 19 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( ℂ D ( sin ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ) )
21 cnelprrecn ⊢ ℂ ∈ { ℝ , ℂ }
22 21 a1i ⊢ ( 𝐴 ∈ ℂ → ℂ ∈ { ℝ , ℂ } )
23 dvsin ⊢ ( ℂ D sin ) = cos
24 23 dmeqi ⊢ dom ( ℂ D sin ) = dom cos
25 cosf ⊢ cos : ℂ ⟶ ℂ
26 25 fdmi ⊢ dom cos = ℂ
27 24 26 eqtri ⊢ dom ( ℂ D sin ) = ℂ
28 27 a1i ⊢ ( 𝐴 ∈ ℂ → dom ( ℂ D sin ) = ℂ )
29 id ⊢ ( 𝑦 = 𝑤 → 𝑦 = 𝑤 )
30 29 cbvmptv ⊢ ( 𝑦 ∈ ℂ ↦ 𝑦 ) = ( 𝑤 ∈ ℂ ↦ 𝑤 )
31 30 oveq2i ⊢ ( ( ℂ × { 𝐴 } ) ∘f · ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) = ( ( ℂ × { 𝐴 } ) ∘f · ( 𝑤 ∈ ℂ ↦ 𝑤 ) )
32 31 a1i ⊢ ( 𝐴 ∈ ℂ → ( ( ℂ × { 𝐴 } ) ∘f · ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) = ( ( ℂ × { 𝐴 } ) ∘f · ( 𝑤 ∈ ℂ ↦ 𝑤 ) ) )
33 cnex ⊢ ℂ ∈ V
34 33 a1i ⊢ ( 𝐴 ∈ ℂ → ℂ ∈ V )
35 snex ⊢ { 𝐴 } ∈ V
36 35 a1i ⊢ ( 𝐴 ∈ ℂ → { 𝐴 } ∈ V )
37 34 36 xpexd ⊢ ( 𝐴 ∈ ℂ → ( ℂ × { 𝐴 } ) ∈ V )
38 33 mptex ⊢ ( 𝑤 ∈ ℂ ↦ 𝑤 ) ∈ V
39 38 a1i ⊢ ( 𝐴 ∈ ℂ → ( 𝑤 ∈ ℂ ↦ 𝑤 ) ∈ V )
40 offval3 ⊢ ( ( ( ℂ × { 𝐴 } ) ∈ V ∧ ( 𝑤 ∈ ℂ ↦ 𝑤 ) ∈ V ) → ( ( ℂ × { 𝐴 } ) ∘f · ( 𝑤 ∈ ℂ ↦ 𝑤 ) ) = ( 𝑦 ∈ ( dom ( ℂ × { 𝐴 } ) ∩ dom ( 𝑤 ∈ ℂ ↦ 𝑤 ) ) ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑦 ) · ( ( 𝑤 ∈ ℂ ↦ 𝑤 ) ‘ 𝑦 ) ) ) )
41 37 39 40 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( ( ℂ × { 𝐴 } ) ∘f · ( 𝑤 ∈ ℂ ↦ 𝑤 ) ) = ( 𝑦 ∈ ( dom ( ℂ × { 𝐴 } ) ∩ dom ( 𝑤 ∈ ℂ ↦ 𝑤 ) ) ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑦 ) · ( ( 𝑤 ∈ ℂ ↦ 𝑤 ) ‘ 𝑦 ) ) ) )
42 fconst6g ⊢ ( 𝐴 ∈ ℂ → ( ℂ × { 𝐴 } ) : ℂ ⟶ ℂ )
43 42 fdmd ⊢ ( 𝐴 ∈ ℂ → dom ( ℂ × { 𝐴 } ) = ℂ )
44 eqid ⊢ ( 𝑤 ∈ ℂ ↦ 𝑤 ) = ( 𝑤 ∈ ℂ ↦ 𝑤 )
45 id ⊢ ( 𝑤 ∈ ℂ → 𝑤 ∈ ℂ )
46 44 45 fmpti ⊢ ( 𝑤 ∈ ℂ ↦ 𝑤 ) : ℂ ⟶ ℂ
47 46 fdmi ⊢ dom ( 𝑤 ∈ ℂ ↦ 𝑤 ) = ℂ
48 47 a1i ⊢ ( 𝐴 ∈ ℂ → dom ( 𝑤 ∈ ℂ ↦ 𝑤 ) = ℂ )
49 43 48 ineq12d ⊢ ( 𝐴 ∈ ℂ → ( dom ( ℂ × { 𝐴 } ) ∩ dom ( 𝑤 ∈ ℂ ↦ 𝑤 ) ) = ( ℂ ∩ ℂ ) )
50 inidm ⊢ ( ℂ ∩ ℂ ) = ℂ
51 50 a1i ⊢ ( 𝐴 ∈ ℂ → ( ℂ ∩ ℂ ) = ℂ )
52 49 51 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( dom ( ℂ × { 𝐴 } ) ∩ dom ( 𝑤 ∈ ℂ ↦ 𝑤 ) ) = ℂ )
53 52 mpteq1d ⊢ ( 𝐴 ∈ ℂ → ( 𝑦 ∈ ( dom ( ℂ × { 𝐴 } ) ∩ dom ( 𝑤 ∈ ℂ ↦ 𝑤 ) ) ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑦 ) · ( ( 𝑤 ∈ ℂ ↦ 𝑤 ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑦 ) · ( ( 𝑤 ∈ ℂ ↦ 𝑤 ) ‘ 𝑦 ) ) ) )
54 fvconst2g ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ 𝑦 ) = 𝐴 )
55 eqidd ⊢ ( 𝑦 ∈ ℂ → ( 𝑤 ∈ ℂ ↦ 𝑤 ) = ( 𝑤 ∈ ℂ ↦ 𝑤 ) )
56 simpr ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑤 = 𝑦 ) → 𝑤 = 𝑦 )
57 id ⊢ ( 𝑦 ∈ ℂ → 𝑦 ∈ ℂ )
58 55 56 57 57 fvmptd ⊢ ( 𝑦 ∈ ℂ → ( ( 𝑤 ∈ ℂ ↦ 𝑤 ) ‘ 𝑦 ) = 𝑦 )
59 58 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑤 ∈ ℂ ↦ 𝑤 ) ‘ 𝑦 ) = 𝑦 )
60 54 59 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( ( ℂ × { 𝐴 } ) ‘ 𝑦 ) · ( ( 𝑤 ∈ ℂ ↦ 𝑤 ) ‘ 𝑦 ) ) = ( 𝐴 · 𝑦 ) )
61 60 mpteq2dva ⊢ ( 𝐴 ∈ ℂ → ( 𝑦 ∈ ℂ ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑦 ) · ( ( 𝑤 ∈ ℂ ↦ 𝑤 ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) )
62 53 61 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( 𝑦 ∈ ( dom ( ℂ × { 𝐴 } ) ∩ dom ( 𝑤 ∈ ℂ ↦ 𝑤 ) ) ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑦 ) · ( ( 𝑤 ∈ ℂ ↦ 𝑤 ) ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) )
63 32 41 62 3eqtrrd ⊢ ( 𝐴 ∈ ℂ → ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) = ( ( ℂ × { 𝐴 } ) ∘f · ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) )
64 63 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ( ℂ D ( ( ℂ × { 𝐴 } ) ∘f · ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) )
65 eqid ⊢ ( 𝑦 ∈ ℂ ↦ 𝑦 ) = ( 𝑦 ∈ ℂ ↦ 𝑦 )
66 65 57 fmpti ⊢ ( 𝑦 ∈ ℂ ↦ 𝑦 ) : ℂ ⟶ ℂ
67 66 a1i ⊢ ( 𝐴 ∈ ℂ → ( 𝑦 ∈ ℂ ↦ 𝑦 ) : ℂ ⟶ ℂ )
68 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
69 21 a1i ⊢ ( ⊤ → ℂ ∈ { ℝ , ℂ } )
70 69 dvmptid ⊢ ( ⊤ → ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℂ ↦ 1 ) )
71 70 mptru ⊢ ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℂ ↦ 1 )
72 71 dmeqi ⊢ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) = dom ( 𝑦 ∈ ℂ ↦ 1 )
73 ax-1cn ⊢ 1 ∈ ℂ
74 73 rgenw ⊢ ∀ 𝑦 ∈ ℂ 1 ∈ ℂ
75 eqid ⊢ ( 𝑦 ∈ ℂ ↦ 1 ) = ( 𝑦 ∈ ℂ ↦ 1 )
76 75 fmpt ⊢ ( ∀ 𝑦 ∈ ℂ 1 ∈ ℂ ↔ ( 𝑦 ∈ ℂ ↦ 1 ) : ℂ ⟶ ℂ )
77 74 76 mpbi ⊢ ( 𝑦 ∈ ℂ ↦ 1 ) : ℂ ⟶ ℂ
78 77 fdmi ⊢ dom ( 𝑦 ∈ ℂ ↦ 1 ) = ℂ
79 72 78 eqtri ⊢ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) = ℂ
80 79 a1i ⊢ ( 𝐴 ∈ ℂ → dom ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) = ℂ )
81 22 67 68 80 dvcmulf ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( ( ℂ × { 𝐴 } ) ∘f · ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) = ( ( ℂ × { 𝐴 } ) ∘f · ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) )
82 64 81 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ( ( ℂ × { 𝐴 } ) ∘f · ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) )
83 82 dmeqd ⊢ ( 𝐴 ∈ ℂ → dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = dom ( ( ℂ × { 𝐴 } ) ∘f · ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) )
84 ovexd ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ∈ V )
85 offval3 ⊢ ( ( ( ℂ × { 𝐴 } ) ∈ V ∧ ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ∈ V ) → ( ( ℂ × { 𝐴 } ) ∘f · ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) = ( 𝑤 ∈ ( dom ( ℂ × { 𝐴 } ) ∩ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) ) ) )
86 37 84 85 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( ( ℂ × { 𝐴 } ) ∘f · ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) = ( 𝑤 ∈ ( dom ( ℂ × { 𝐴 } ) ∩ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) ) ) )
87 86 dmeqd ⊢ ( 𝐴 ∈ ℂ → dom ( ( ℂ × { 𝐴 } ) ∘f · ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) = dom ( 𝑤 ∈ ( dom ( ℂ × { 𝐴 } ) ∩ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) ) ) )
88 43 80 ineq12d ⊢ ( 𝐴 ∈ ℂ → ( dom ( ℂ × { 𝐴 } ) ∩ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) = ( ℂ ∩ ℂ ) )
89 88 51 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( dom ( ℂ × { 𝐴 } ) ∩ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) = ℂ )
90 89 mpteq1d ⊢ ( 𝐴 ∈ ℂ → ( 𝑤 ∈ ( dom ( ℂ × { 𝐴 } ) ∩ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ℂ ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) ) ) )
91 90 dmeqd ⊢ ( 𝐴 ∈ ℂ → dom ( 𝑤 ∈ ( dom ( ℂ × { 𝐴 } ) ∩ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) ) ) = dom ( 𝑤 ∈ ℂ ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) ) ) )
92 eqid ⊢ ( 𝑤 ∈ ℂ ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ℂ ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) ) )
93 fvconst2g ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) = 𝐴 )
94 71 fveq1i ⊢ ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) = ( ( 𝑦 ∈ ℂ ↦ 1 ) ‘ 𝑤 )
95 94 a1i ⊢ ( 𝑤 ∈ ℂ → ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) = ( ( 𝑦 ∈ ℂ ↦ 1 ) ‘ 𝑤 ) )
96 eqidd ⊢ ( 𝑤 ∈ ℂ → ( 𝑦 ∈ ℂ ↦ 1 ) = ( 𝑦 ∈ ℂ ↦ 1 ) )
97 eqidd ⊢ ( ( 𝑤 ∈ ℂ ∧ 𝑦 = 𝑤 ) → 1 = 1 )
98 73 a1i ⊢ ( 𝑤 ∈ ℂ → 1 ∈ ℂ )
99 96 97 45 98 fvmptd ⊢ ( 𝑤 ∈ ℂ → ( ( 𝑦 ∈ ℂ ↦ 1 ) ‘ 𝑤 ) = 1 )
100 95 99 eqtrd ⊢ ( 𝑤 ∈ ℂ → ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) = 1 )
101 100 adantl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) = 1 )
102 93 101 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) ) = ( 𝐴 · 1 ) )
103 mulcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 · 1 ) ∈ ℂ )
104 73 103 mpan2 ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) ∈ ℂ )
105 104 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 𝐴 · 1 ) ∈ ℂ )
106 102 105 eqeltrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) ) ∈ ℂ )
107 92 106 dmmptd ⊢ ( 𝐴 ∈ ℂ → dom ( 𝑤 ∈ ℂ ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) ) ) = ℂ )
108 91 107 eqtrd ⊢ ( 𝐴 ∈ ℂ → dom ( 𝑤 ∈ ( dom ( ℂ × { 𝐴 } ) ∩ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ) ↦ ( ( ( ℂ × { 𝐴 } ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) ‘ 𝑤 ) ) ) = ℂ )
109 83 87 108 3eqtrd ⊢ ( 𝐴 ∈ ℂ → dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ℂ )
110 22 22 2 4 28 109 dvcof ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( sin ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ) = ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∘f · ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ) )
111 23 a1i ⊢ ( 𝐴 ∈ ℂ → ( ℂ D sin ) = cos )
112 coscn ⊢ cos ∈ ( ℂ –cn→ ℂ )
113 112 a1i ⊢ ( 𝐴 ∈ ℂ → cos ∈ ( ℂ –cn→ ℂ ) )
114 111 113 eqeltrd ⊢ ( 𝐴 ∈ ℂ → ( ℂ D sin ) ∈ ( ℂ –cn→ ℂ ) )
115 33 mptex ⊢ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ∈ V
116 115 a1i ⊢ ( 𝐴 ∈ ℂ → ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ∈ V )
117 coexg ⊢ ( ( ( ℂ D sin ) ∈ ( ℂ –cn→ ℂ ) ∧ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ∈ V ) → ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∈ V )
118 114 116 117 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∈ V )
119 ovexd ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∈ V )
120 offval3 ⊢ ( ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∈ V ∧ ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∈ V ) → ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∘f · ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑤 ∈ ( dom ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∩ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ) ↦ ( ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) ) ) )
121 118 119 120 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∘f · ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑤 ∈ ( dom ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∩ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ) ↦ ( ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) ) ) )
122 4 frnd ⊢ ( 𝐴 ∈ ℂ → ran ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ⊆ ℂ )
123 122 28 sseqtrrd ⊢ ( 𝐴 ∈ ℂ → ran ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ⊆ dom ( ℂ D sin ) )
124 dmcosseq ⊢ ( ran ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ⊆ dom ( ℂ D sin ) → dom ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = dom ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) )
125 123 124 syl ⊢ ( 𝐴 ∈ ℂ → dom ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = dom ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) )
126 ovex ⊢ ( 𝐴 · 𝑦 ) ∈ V
127 eqid ⊢ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) )
128 126 127 dmmpti ⊢ dom ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) = ℂ
129 128 a1i ⊢ ( 𝐴 ∈ ℂ → dom ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) = ℂ )
130 125 129 eqtrd ⊢ ( 𝐴 ∈ ℂ → dom ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ℂ )
131 130 109 ineq12d ⊢ ( 𝐴 ∈ ℂ → ( dom ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∩ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ) = ( ℂ ∩ ℂ ) )
132 131 51 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( dom ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∩ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ) = ℂ )
133 132 mpteq1d ⊢ ( 𝐴 ∈ ℂ → ( 𝑤 ∈ ( dom ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∩ dom ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ) ↦ ( ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ℂ ↦ ( ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) ) ) )
134 11 coscld ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( cos ‘ ( 𝐴 · 𝑤 ) ) ∈ ℂ )
135 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → 𝐴 ∈ ℂ )
136 134 135 mulcomd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( ( cos ‘ ( 𝐴 · 𝑤 ) ) · 𝐴 ) = ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑤 ) ) ) )
137 136 mpteq2dva ⊢ ( 𝐴 ∈ ℂ → ( 𝑤 ∈ ℂ ↦ ( ( cos ‘ ( 𝐴 · 𝑤 ) ) · 𝐴 ) ) = ( 𝑤 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑤 ) ) ) ) )
138 23 coeq1i ⊢ ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ( cos ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) )
139 138 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ( cos ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) )
140 139 fveq1d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) = ( ( cos ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) )
141 4 ffund ⊢ ( 𝐴 ∈ ℂ → Fun ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) )
142 141 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → Fun ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) )
143 10 128 eleqtrrdi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → 𝑤 ∈ dom ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) )
144 fvco ⊢ ( ( Fun ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ∧ 𝑤 ∈ dom ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) → ( ( cos ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) = ( cos ‘ ( ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ‘ 𝑤 ) ) )
145 142 143 144 syl2anc ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( ( cos ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) = ( cos ‘ ( ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ‘ 𝑤 ) ) )
146 12 fveq2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( cos ‘ ( ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ‘ 𝑤 ) ) = ( cos ‘ ( 𝐴 · 𝑤 ) ) )
147 140 145 146 3eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) = ( cos ‘ ( 𝐴 · 𝑤 ) ) )
148 simpl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → 𝐴 ∈ ℂ )
149 0cnd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → 0 ∈ ℂ )
150 22 68 dvmptc ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝐴 ) ) = ( 𝑦 ∈ ℂ ↦ 0 ) )
151 simpr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
152 73 a1i ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → 1 ∈ ℂ )
153 71 a1i ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ 𝑦 ) ) = ( 𝑦 ∈ ℂ ↦ 1 ) )
154 22 148 149 150 151 152 153 dvmptmul ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( ( 0 · 𝑦 ) + ( 1 · 𝐴 ) ) ) )
155 151 mul02d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 0 · 𝑦 ) = 0 )
156 148 mulid2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 1 · 𝐴 ) = 𝐴 )
157 155 156 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 0 · 𝑦 ) + ( 1 · 𝐴 ) ) = ( 0 + 𝐴 ) )
158 148 addid2d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 0 + 𝐴 ) = 𝐴 )
159 157 158 eqtrd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 0 · 𝑦 ) + ( 1 · 𝐴 ) ) = 𝐴 )
160 159 mpteq2dva ⊢ ( 𝐴 ∈ ℂ → ( 𝑦 ∈ ℂ ↦ ( ( 0 · 𝑦 ) + ( 1 · 𝐴 ) ) ) = ( 𝑦 ∈ ℂ ↦ 𝐴 ) )
161 154 160 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ 𝐴 ) )
162 161 adantr ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) = ( 𝑦 ∈ ℂ ↦ 𝐴 ) )
163 eqidd ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) ∧ 𝑦 = 𝑤 ) → 𝐴 = 𝐴 )
164 162 163 10 135 fvmptd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) = 𝐴 )
165 147 164 oveq12d ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) ) = ( ( cos ‘ ( 𝐴 · 𝑤 ) ) · 𝐴 ) )
166 165 mpteq2dva ⊢ ( 𝐴 ∈ ℂ → ( 𝑤 ∈ ℂ ↦ ( ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) ) ) = ( 𝑤 ∈ ℂ ↦ ( ( cos ‘ ( 𝐴 · 𝑤 ) ) · 𝐴 ) ) )
167 8 fveq2d ⊢ ( 𝑦 = 𝑤 → ( cos ‘ ( 𝐴 · 𝑦 ) ) = ( cos ‘ ( 𝐴 · 𝑤 ) ) )
168 167 oveq2d ⊢ ( 𝑦 = 𝑤 → ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) = ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑤 ) ) ) )
169 168 cbvmptv ⊢ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑤 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑤 ) ) ) )
170 169 a1i ⊢ ( 𝐴 ∈ ℂ → ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑤 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑤 ) ) ) ) )
171 137 166 170 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( 𝑤 ∈ ℂ ↦ ( ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) · ( ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ‘ 𝑤 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) )
172 121 133 171 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ( ( ℂ D sin ) ∘ ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ∘f · ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) )
173 20 110 172 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( sin ‘ ( 𝐴 · 𝑦 ) ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝐴 · ( cos ‘ ( 𝐴 · 𝑦 ) ) ) ) )