# 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 ${⊢}{A}\in ℂ\to \frac{d\left({y}\in ℂ⟼\mathrm{sin}{A}{y}\right)}{{d}_{ℂ}{y}}=\left({y}\in ℂ⟼{A}\mathrm{cos}{A}{y}\right)$

### Proof

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