Metamath Proof Explorer

Theorem dvcosax

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

Ref Expression
Assertion dvcosax 
|- ( A e. CC -> ( CC _D ( x e. CC |-> ( cos ` ( A x. x ) ) ) ) = ( x e. CC |-> ( A x. -u ( sin ` ( A x. x ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mulcl 
 |-  ( ( A e. CC /\ x e. CC ) -> ( A x. x ) e. CC )
2 eqidd 
 |-  ( A e. CC -> ( x e. CC |-> ( A x. x ) ) = ( x e. CC |-> ( A x. x ) ) )
3 cosf 
 |-  cos : CC --> CC
4 3 a1i 
 |-  ( A e. CC -> cos : CC --> CC )
5 4 feqmptd 
 |-  ( A e. CC -> cos = ( y e. CC |-> ( cos ` y ) ) )
6 fveq2 
 |-  ( y = ( A x. x ) -> ( cos ` y ) = ( cos ` ( A x. x ) ) )
7 1 2 5 6 fmptco 
 |-  ( A e. CC -> ( cos o. ( x e. CC |-> ( A x. x ) ) ) = ( x e. CC |-> ( cos ` ( A x. x ) ) ) )
8 7 eqcomd 
 |-  ( A e. CC -> ( x e. CC |-> ( cos ` ( A x. x ) ) ) = ( cos o. ( x e. CC |-> ( A x. x ) ) ) )
9 8 oveq2d 
 |-  ( A e. CC -> ( CC _D ( x e. CC |-> ( cos ` ( A x. x ) ) ) ) = ( CC _D ( cos o. ( x e. CC |-> ( A x. x ) ) ) ) )
10 cnelprrecn 
 |-  CC e. { RR , CC }
11 10 a1i 
 |-  ( A e. CC -> CC e. { RR , CC } )
12 1 fmpttd 
 |-  ( A e. CC -> ( x e. CC |-> ( A x. x ) ) : CC --> CC )
13 dvcos 
 |-  ( CC _D cos ) = ( x e. CC |-> -u ( sin ` x ) )
14 13 dmeqi 
 |-  dom ( CC _D cos ) = dom ( x e. CC |-> -u ( sin ` x ) )
15 dmmptg 
 |-  ( A. x e. CC -u ( sin ` x ) e. CC -> dom ( x e. CC |-> -u ( sin ` x ) ) = CC )
16 sincl 
 |-  ( x e. CC -> ( sin ` x ) e. CC )
17 16 negcld 
 |-  ( x e. CC -> -u ( sin ` x ) e. CC )
18 15 17 mprg 
 |-  dom ( x e. CC |-> -u ( sin ` x ) ) = CC
19 14 18 eqtri 
 |-  dom ( CC _D cos ) = CC
20 19 a1i 
 |-  ( A e. CC -> dom ( CC _D cos ) = CC )
21 simpl 
 |-  ( ( A e. CC /\ x e. CC ) -> A e. CC )
22 0red 
 |-  ( ( A e. CC /\ x e. CC ) -> 0 e. RR )
23 id 
 |-  ( A e. CC -> A e. CC )
24 11 23 dvmptc 
 |-  ( A e. CC -> ( CC _D ( x e. CC |-> A ) ) = ( x e. CC |-> 0 ) )
25 simpr 
 |-  ( ( A e. CC /\ x e. CC ) -> x e. CC )
26 1red 
 |-  ( ( A e. CC /\ x e. CC ) -> 1 e. RR )
27 11 dvmptid 
 |-  ( A e. CC -> ( CC _D ( x e. CC |-> x ) ) = ( x e. CC |-> 1 ) )
28 11 21 22 24 25 26 27 dvmptmul 
 |-  ( A e. CC -> ( CC _D ( x e. CC |-> ( A x. x ) ) ) = ( x e. CC |-> ( ( 0 x. x ) + ( 1 x. A ) ) ) )
29 28 dmeqd 
 |-  ( A e. CC -> dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) = dom ( x e. CC |-> ( ( 0 x. x ) + ( 1 x. A ) ) ) )
30 dmmptg 
 |-  ( A. x e. CC ( ( 0 x. x ) + ( 1 x. A ) ) e. _V -> dom ( x e. CC |-> ( ( 0 x. x ) + ( 1 x. A ) ) ) = CC )
31 ovex 
 |-  ( ( 0 x. x ) + ( 1 x. A ) ) e. _V
32 31 a1i 
 |-  ( x e. CC -> ( ( 0 x. x ) + ( 1 x. A ) ) e. _V )
33 30 32 mprg 
 |-  dom ( x e. CC |-> ( ( 0 x. x ) + ( 1 x. A ) ) ) = CC
34 29 33 eqtrdi 
 |-  ( A e. CC -> dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) = CC )
35 11 11 4 12 20 34 dvcof 
 |-  ( A e. CC -> ( CC _D ( cos o. ( x e. CC |-> ( A x. x ) ) ) ) = ( ( ( CC _D cos ) o. ( x e. CC |-> ( A x. x ) ) ) oF x. ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) )
36 dvcos 
 |-  ( CC _D cos ) = ( y e. CC |-> -u ( sin ` y ) )
37 36 a1i 
 |-  ( A e. CC -> ( CC _D cos ) = ( y e. CC |-> -u ( sin ` y ) ) )
38 fveq2 
 |-  ( y = ( A x. x ) -> ( sin ` y ) = ( sin ` ( A x. x ) ) )
39 38 negeqd 
 |-  ( y = ( A x. x ) -> -u ( sin ` y ) = -u ( sin ` ( A x. x ) ) )
40 1 2 37 39 fmptco 
 |-  ( A e. CC -> ( ( CC _D cos ) o. ( x e. CC |-> ( A x. x ) ) ) = ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) )
41 40 oveq1d 
 |-  ( A e. CC -> ( ( ( CC _D cos ) o. ( x e. CC |-> ( A x. x ) ) ) oF x. ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) = ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) oF x. ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) )
42 cnex 
 |-  CC e. _V
43 42 mptex 
 |-  ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) e. _V
44 ovex 
 |-  ( CC _D ( x e. CC |-> ( A x. x ) ) ) e. _V
45 offval3 
 |-  ( ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) e. _V /\ ( CC _D ( x e. CC |-> ( A x. x ) ) ) e. _V ) -> ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) oF x. ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) = ( y e. ( dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) i^i dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) |-> ( ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) ` y ) x. ( ( CC _D ( x e. CC |-> ( A x. x ) ) ) ` y ) ) ) )
46 43 44 45 mp2an 
 |-  ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) oF x. ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) = ( y e. ( dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) i^i dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) |-> ( ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) ` y ) x. ( ( CC _D ( x e. CC |-> ( A x. x ) ) ) ` y ) ) )
47 46 a1i 
 |-  ( A e. CC -> ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) oF x. ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) = ( y e. ( dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) i^i dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) |-> ( ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) ` y ) x. ( ( CC _D ( x e. CC |-> ( A x. x ) ) ) ` y ) ) ) )
48 1 sincld 
 |-  ( ( A e. CC /\ x e. CC ) -> ( sin ` ( A x. x ) ) e. CC )
49 48 negcld 
 |-  ( ( A e. CC /\ x e. CC ) -> -u ( sin ` ( A x. x ) ) e. CC )
50 49 ralrimiva 
 |-  ( A e. CC -> A. x e. CC -u ( sin ` ( A x. x ) ) e. CC )
51 dmmptg 
 |-  ( A. x e. CC -u ( sin ` ( A x. x ) ) e. CC -> dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) = CC )
52 50 51 syl 
 |-  ( A e. CC -> dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) = CC )
53 52 34 ineq12d 
 |-  ( A e. CC -> ( dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) i^i dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) = ( CC i^i CC ) )
54 inidm 
 |-  ( CC i^i CC ) = CC
55 53 54 eqtrdi 
 |-  ( A e. CC -> ( dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) i^i dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) = CC )
56 simpr 
 |-  ( ( A e. CC /\ y e. ( dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) i^i dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) ) -> y e. ( dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) i^i dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) )
57 55 adantr 
 |-  ( ( A e. CC /\ y e. ( dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) i^i dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) ) -> ( dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) i^i dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) = CC )
58 56 57 eleqtrd 
 |-  ( ( A e. CC /\ y e. ( dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) i^i dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) ) -> y e. CC )
59 eqidd 
 |-  ( y e. CC -> ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) = ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) )
60 oveq2 
 |-  ( x = y -> ( A x. x ) = ( A x. y ) )
61 60 fveq2d 
 |-  ( x = y -> ( sin ` ( A x. x ) ) = ( sin ` ( A x. y ) ) )
62 61 negeqd 
 |-  ( x = y -> -u ( sin ` ( A x. x ) ) = -u ( sin ` ( A x. y ) ) )
63 62 adantl 
 |-  ( ( y e. CC /\ x = y ) -> -u ( sin ` ( A x. x ) ) = -u ( sin ` ( A x. y ) ) )
64 id 
 |-  ( y e. CC -> y e. CC )
65 negex 
 |-  -u ( sin ` ( A x. y ) ) e. _V
66 65 a1i 
 |-  ( y e. CC -> -u ( sin ` ( A x. y ) ) e. _V )
67 59 63 64 66 fvmptd 
 |-  ( y e. CC -> ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) ` y ) = -u ( sin ` ( A x. y ) ) )
68 67 adantl 
 |-  ( ( A e. CC /\ y e. CC ) -> ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) ` y ) = -u ( sin ` ( A x. y ) ) )
69 28 adantr 
 |-  ( ( A e. CC /\ y e. CC ) -> ( CC _D ( x e. CC |-> ( A x. x ) ) ) = ( x e. CC |-> ( ( 0 x. x ) + ( 1 x. A ) ) ) )
70 oveq2 
 |-  ( x = y -> ( 0 x. x ) = ( 0 x. y ) )
71 70 oveq1d 
 |-  ( x = y -> ( ( 0 x. x ) + ( 1 x. A ) ) = ( ( 0 x. y ) + ( 1 x. A ) ) )
72 mul02 
 |-  ( y e. CC -> ( 0 x. y ) = 0 )
73 mullid 
 |-  ( A e. CC -> ( 1 x. A ) = A )
74 72 73 oveqan12rd 
 |-  ( ( A e. CC /\ y e. CC ) -> ( ( 0 x. y ) + ( 1 x. A ) ) = ( 0 + A ) )
75 addlid 
 |-  ( A e. CC -> ( 0 + A ) = A )
76 75 adantr 
 |-  ( ( A e. CC /\ y e. CC ) -> ( 0 + A ) = A )
77 74 76 eqtrd 
 |-  ( ( A e. CC /\ y e. CC ) -> ( ( 0 x. y ) + ( 1 x. A ) ) = A )
78 71 77 sylan9eqr 
 |-  ( ( ( A e. CC /\ y e. CC ) /\ x = y ) -> ( ( 0 x. x ) + ( 1 x. A ) ) = A )
79 simpr 
 |-  ( ( A e. CC /\ y e. CC ) -> y e. CC )
80 simpl 
 |-  ( ( A e. CC /\ y e. CC ) -> A e. CC )
81 69 78 79 80 fvmptd 
 |-  ( ( A e. CC /\ y e. CC ) -> ( ( CC _D ( x e. CC |-> ( A x. x ) ) ) ` y ) = A )
82 68 81 oveq12d 
 |-  ( ( A e. CC /\ y e. CC ) -> ( ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) ` y ) x. ( ( CC _D ( x e. CC |-> ( A x. x ) ) ) ` y ) ) = ( -u ( sin ` ( A x. y ) ) x. A ) )
83 mulcl 
 |-  ( ( A e. CC /\ y e. CC ) -> ( A x. y ) e. CC )
84 83 sincld 
 |-  ( ( A e. CC /\ y e. CC ) -> ( sin ` ( A x. y ) ) e. CC )
85 84 negcld 
 |-  ( ( A e. CC /\ y e. CC ) -> -u ( sin ` ( A x. y ) ) e. CC )
86 85 80 mulcomd 
 |-  ( ( A e. CC /\ y e. CC ) -> ( -u ( sin ` ( A x. y ) ) x. A ) = ( A x. -u ( sin ` ( A x. y ) ) ) )
87 82 86 eqtrd 
 |-  ( ( A e. CC /\ y e. CC ) -> ( ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) ` y ) x. ( ( CC _D ( x e. CC |-> ( A x. x ) ) ) ` y ) ) = ( A x. -u ( sin ` ( A x. y ) ) ) )
88 58 87 syldan 
 |-  ( ( A e. CC /\ y e. ( dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) i^i dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) ) -> ( ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) ` y ) x. ( ( CC _D ( x e. CC |-> ( A x. x ) ) ) ` y ) ) = ( A x. -u ( sin ` ( A x. y ) ) ) )
89 55 88 mpteq12dva 
 |-  ( A e. CC -> ( y e. ( dom ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) i^i dom ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) |-> ( ( ( x e. CC |-> -u ( sin ` ( A x. x ) ) ) ` y ) x. ( ( CC _D ( x e. CC |-> ( A x. x ) ) ) ` y ) ) ) = ( y e. CC |-> ( A x. -u ( sin ` ( A x. y ) ) ) ) )
90 41 47 89 3eqtrd 
 |-  ( A e. CC -> ( ( ( CC _D cos ) o. ( x e. CC |-> ( A x. x ) ) ) oF x. ( CC _D ( x e. CC |-> ( A x. x ) ) ) ) = ( y e. CC |-> ( A x. -u ( sin ` ( A x. y ) ) ) ) )
91 9 35 90 3eqtrd 
 |-  ( A e. CC -> ( CC _D ( x e. CC |-> ( cos ` ( A x. x ) ) ) ) = ( y e. CC |-> ( A x. -u ( sin ` ( A x. y ) ) ) ) )
92 oveq2 
 |-  ( y = x -> ( A x. y ) = ( A x. x ) )
93 92 fveq2d 
 |-  ( y = x -> ( sin ` ( A x. y ) ) = ( sin ` ( A x. x ) ) )
94 93 negeqd 
 |-  ( y = x -> -u ( sin ` ( A x. y ) ) = -u ( sin ` ( A x. x ) ) )
95 94 oveq2d 
 |-  ( y = x -> ( A x. -u ( sin ` ( A x. y ) ) ) = ( A x. -u ( sin ` ( A x. x ) ) ) )
96 95 cbvmptv 
 |-  ( y e. CC |-> ( A x. -u ( sin ` ( A x. y ) ) ) ) = ( x e. CC |-> ( A x. -u ( sin ` ( A x. x ) ) ) )
97 91 96 eqtrdi 
 |-  ( A e. CC -> ( CC _D ( x e. CC |-> ( cos ` ( A x. x ) ) ) ) = ( x e. CC |-> ( A x. -u ( sin ` ( A x. x ) ) ) ) )