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 (y \in ℂ⟼ \sin A y)}{d_{ℂ} y} = (y \in ℂ ⟼ A \cos A y)$

Proof

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

Metamath Proof Explorer

Theorem dvsinax

Proof