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 e. CC -> ( CC _D ( y e. CC |-> ( sin ` ( A x. y ) ) ) ) = ( y e. CC |-> ( A x. ( cos ` ( A x. y ) ) ) ) )

Proof

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