Theorem dvmptmulf

Description: Function-builder for derivative, product rule. A version of dvmptmul using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	dvmptmulf.ph	$$⊢Ⅎx\phi$$
	dvmptmulf.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
	dvmptmulf.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
	dvmptmulf.b	$$⊢\left(\phi \wedge x\in X\right)\to B\in V$$
	dvmptmulf.ab	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}=\left(x\in X⟼B\right)$$
	dvmptmulf.c	$$⊢\left(\phi \wedge x\in X\right)\to C\in ℂ$$
	dvmptmulf.d	$$⊢\left(\phi \wedge x\in X\right)\to D\in W$$
	dvmptmulf.cd	$$⊢\phi \to \frac{d\left(x\in X⟼C\right)}{d_{S}x}=\left(x\in X⟼D\right)$$
Assertion	dvmptmulf	$$⊢\phi \to \frac{d\left(x\in X⟼AC\right)}{d_{S}x}=\left(x\in X⟼BC+DA\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvmptmulf.ph	$$⊢Ⅎx\phi$$
2		dvmptmulf.s	$$⊢\phi \to S\in \left\{ℝ,ℂ\right\}$$
3		dvmptmulf.a	$$⊢\left(\phi \wedge x\in X\right)\to A\in ℂ$$
4		dvmptmulf.b	$$⊢\left(\phi \wedge x\in X\right)\to B\in V$$
5		dvmptmulf.ab	$$⊢\phi \to \frac{d\left(x\in X⟼A\right)}{d_{S}x}=\left(x\in X⟼B\right)$$
6		dvmptmulf.c	$$⊢\left(\phi \wedge x\in X\right)\to C\in ℂ$$
7		dvmptmulf.d	$$⊢\left(\phi \wedge x\in X\right)\to D\in W$$
8		dvmptmulf.cd	$$⊢\phi \to \frac{d\left(x\in X⟼C\right)}{d_{S}x}=\left(x\in X⟼D\right)$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}yAC$$
10		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌A$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}x\times$$
12		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌C$$
13	10 11 12	nfov	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌A⦋y/x⦌C$$
14		csbeq1a	$$⊢x=y\to A=⦋y/x⦌A$$
15		csbeq1a	$$⊢x=y\to C=⦋y/x⦌C$$
16	14 15	oveq12d	$$⊢x=y\to AC=⦋y/x⦌A⦋y/x⦌C$$
17	9 13 16	cbvmpt	$$⊢\left(x\in X⟼AC\right)=\left(y\in X⟼⦋y/x⦌A⦋y/x⦌C\right)$$
18	17	oveq2i	$$⊢\frac{d\left(x\in X⟼AC\right)}{d_{S}x}=\frac{d\left(y\in X⟼⦋y/x⦌A⦋y/x⦌C\right)}{d_{S}y}$$
19	18	a1i	$$⊢\phi \to \frac{d\left(x\in X⟼AC\right)}{d_{S}x}=\frac{d\left(y\in X⟼⦋y/x⦌A⦋y/x⦌C\right)}{d_{S}y}$$
20		nfv	$$⊢Ⅎxy\in X$$
21	1 20	nfan	$$⊢Ⅎx\left(\phi \wedge y\in X\right)$$
22	10	nfel1	$$⊢Ⅎx⦋y/x⦌A\in ℂ$$
23	21 22	nfim	$$⊢Ⅎx\left(\left(\phi \wedge y\in X\right)\to ⦋y/x⦌A\in ℂ\right)$$
24		eleq1w	$$⊢x=y\to \left(x\in X\leftrightarrow y\in X\right)$$
25	24	anbi2d	$$⊢x=y\to \left(\left(\phi \wedge x\in X\right)\leftrightarrow \left(\phi \wedge y\in X\right)\right)$$
26	14	eleq1d	$$⊢x=y\to \left(A\in ℂ\leftrightarrow ⦋y/x⦌A\in ℂ\right)$$
27	25 26	imbi12d	$$⊢x=y\to \left(\left(\left(\phi \wedge x\in X\right)\to A\in ℂ\right)\leftrightarrow \left(\left(\phi \wedge y\in X\right)\to ⦋y/x⦌A\in ℂ\right)\right)$$
28	23 27 3	chvarfv	$$⊢\left(\phi \wedge y\in X\right)\to ⦋y/x⦌A\in ℂ$$
29		nfcv	$$⊢\underset{\_}{Ⅎ}xy$$
30	29	nfcsb1	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
31		nfcv	$$⊢\underset{\_}{Ⅎ}xV$$
32	30 31	nfel	$$⊢Ⅎx⦋y/x⦌B\in V$$
33	21 32	nfim	$$⊢Ⅎx\left(\left(\phi \wedge y\in X\right)\to ⦋y/x⦌B\in V\right)$$
34		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
35	34	eleq1d	$$⊢x=y\to \left(B\in V\leftrightarrow ⦋y/x⦌B\in V\right)$$
36	25 35	imbi12d	$$⊢x=y\to \left(\left(\left(\phi \wedge x\in X\right)\to B\in V\right)\leftrightarrow \left(\left(\phi \wedge y\in X\right)\to ⦋y/x⦌B\in V\right)\right)$$
37	33 36 4	chvarfv	$$⊢\left(\phi \wedge y\in X\right)\to ⦋y/x⦌B\in V$$
38		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
39		csbeq1a	$$⊢y=x\to ⦋y/x⦌A=⦋x/y⦌⦋y/x⦌A$$
40		csbcow	$$⊢⦋x/y⦌⦋y/x⦌A=⦋x/x⦌A$$
41		csbid	$$⊢⦋x/x⦌A=A$$
42	40 41	eqtri	$$⊢⦋x/y⦌⦋y/x⦌A=A$$
43	42	a1i	$$⊢y=x\to ⦋x/y⦌⦋y/x⦌A=A$$
44	39 43	eqtrd	$$⊢y=x\to ⦋y/x⦌A=A$$
45	10 38 44	cbvmpt	$$⊢\left(y\in X⟼⦋y/x⦌A\right)=\left(x\in X⟼A\right)$$
46	45	oveq2i	$$⊢\frac{d\left(y\in X⟼⦋y/x⦌A\right)}{d_{S}y}=\frac{d\left(x\in X⟼A\right)}{d_{S}x}$$
47	46	a1i	$$⊢\phi \to \frac{d\left(y\in X⟼⦋y/x⦌A\right)}{d_{S}y}=\frac{d\left(x\in X⟼A\right)}{d_{S}x}$$
48		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
49	48 30 34	cbvmpt	$$⊢\left(x\in X⟼B\right)=\left(y\in X⟼⦋y/x⦌B\right)$$
50	49	a1i	$$⊢\phi \to \left(x\in X⟼B\right)=\left(y\in X⟼⦋y/x⦌B\right)$$
51	47 5 50	3eqtrd	$$⊢\phi \to \frac{d\left(y\in X⟼⦋y/x⦌A\right)}{d_{S}y}=\left(y\in X⟼⦋y/x⦌B\right)$$
52	12	nfel1	$$⊢Ⅎx⦋y/x⦌C\in ℂ$$
53	21 52	nfim	$$⊢Ⅎx\left(\left(\phi \wedge y\in X\right)\to ⦋y/x⦌C\in ℂ\right)$$
54	15	eleq1d	$$⊢x=y\to \left(C\in ℂ\leftrightarrow ⦋y/x⦌C\in ℂ\right)$$
55	25 54	imbi12d	$$⊢x=y\to \left(\left(\left(\phi \wedge x\in X\right)\to C\in ℂ\right)\leftrightarrow \left(\left(\phi \wedge y\in X\right)\to ⦋y/x⦌C\in ℂ\right)\right)$$
56	53 55 6	chvarfv	$$⊢\left(\phi \wedge y\in X\right)\to ⦋y/x⦌C\in ℂ$$
57	29	nfcsb1	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌D$$
58		nfcv	$$⊢\underset{\_}{Ⅎ}xW$$
59	57 58	nfel	$$⊢Ⅎx⦋y/x⦌D\in W$$
60	21 59	nfim	$$⊢Ⅎx\left(\left(\phi \wedge y\in X\right)\to ⦋y/x⦌D\in W\right)$$
61		csbeq1a	$$⊢x=y\to D=⦋y/x⦌D$$
62	61	eleq1d	$$⊢x=y\to \left(D\in W\leftrightarrow ⦋y/x⦌D\in W\right)$$
63	25 62	imbi12d	$$⊢x=y\to \left(\left(\left(\phi \wedge x\in X\right)\to D\in W\right)\leftrightarrow \left(\left(\phi \wedge y\in X\right)\to ⦋y/x⦌D\in W\right)\right)$$
64	60 63 7	chvarfv	$$⊢\left(\phi \wedge y\in X\right)\to ⦋y/x⦌D\in W$$
65		nfcv	$$⊢\underset{\_}{Ⅎ}yC$$
66		eqcom	$$⊢x=y\leftrightarrow y=x$$
67	66	imbi1i	$$⊢\left(x=y\to C=⦋y/x⦌C\right)\leftrightarrow \left(y=x\to C=⦋y/x⦌C\right)$$
68		eqcom	$$⊢C=⦋y/x⦌C\leftrightarrow ⦋y/x⦌C=C$$
69	68	imbi2i	$$⊢\left(y=x\to C=⦋y/x⦌C\right)\leftrightarrow \left(y=x\to ⦋y/x⦌C=C\right)$$
70	67 69	bitri	$$⊢\left(x=y\to C=⦋y/x⦌C\right)\leftrightarrow \left(y=x\to ⦋y/x⦌C=C\right)$$
71	15 70	mpbi	$$⊢y=x\to ⦋y/x⦌C=C$$
72	12 65 71	cbvmpt	$$⊢\left(y\in X⟼⦋y/x⦌C\right)=\left(x\in X⟼C\right)$$
73	72	oveq2i	$$⊢\frac{d\left(y\in X⟼⦋y/x⦌C\right)}{d_{S}y}=\frac{d\left(x\in X⟼C\right)}{d_{S}x}$$
74	73	a1i	$$⊢\phi \to \frac{d\left(y\in X⟼⦋y/x⦌C\right)}{d_{S}y}=\frac{d\left(x\in X⟼C\right)}{d_{S}x}$$
75		nfcv	$$⊢\underset{\_}{Ⅎ}yD$$
76	75 57 61	cbvmpt	$$⊢\left(x\in X⟼D\right)=\left(y\in X⟼⦋y/x⦌D\right)$$
77	76	a1i	$$⊢\phi \to \left(x\in X⟼D\right)=\left(y\in X⟼⦋y/x⦌D\right)$$
78	74 8 77	3eqtrd	$$⊢\phi \to \frac{d\left(y\in X⟼⦋y/x⦌C\right)}{d_{S}y}=\left(y\in X⟼⦋y/x⦌D\right)$$
79	2 28 37 51 56 64 78	dvmptmul	$$⊢\phi \to \frac{d\left(y\in X⟼⦋y/x⦌A⦋y/x⦌C\right)}{d_{S}y}=\left(y\in X⟼⦋y/x⦌B⦋y/x⦌C+⦋y/x⦌D⦋y/x⦌A\right)$$
80	30 11 12	nfov	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B⦋y/x⦌C$$
81		nfcv	$$⊢\underset{\_}{Ⅎ}x+$$
82	57 11 10	nfov	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌D⦋y/x⦌A$$
83	80 81 82	nfov	$$⊢\underset{\_}{Ⅎ}x\left(⦋y/x⦌B⦋y/x⦌C+⦋y/x⦌D⦋y/x⦌A\right)$$
84		nfcv	$$⊢\underset{\_}{Ⅎ}y\left(BC+DA\right)$$
85	66	imbi1i	$$⊢\left(x=y\to B=⦋y/x⦌B\right)\leftrightarrow \left(y=x\to B=⦋y/x⦌B\right)$$
86		eqcom	$$⊢B=⦋y/x⦌B\leftrightarrow ⦋y/x⦌B=B$$
87	86	imbi2i	$$⊢\left(y=x\to B=⦋y/x⦌B\right)\leftrightarrow \left(y=x\to ⦋y/x⦌B=B\right)$$
88	85 87	bitri	$$⊢\left(x=y\to B=⦋y/x⦌B\right)\leftrightarrow \left(y=x\to ⦋y/x⦌B=B\right)$$
89	34 88	mpbi	$$⊢y=x\to ⦋y/x⦌B=B$$
90	89 71	oveq12d	$$⊢y=x\to ⦋y/x⦌B⦋y/x⦌C=BC$$
91	66	imbi1i	$$⊢\left(x=y\to D=⦋y/x⦌D\right)\leftrightarrow \left(y=x\to D=⦋y/x⦌D\right)$$
92		eqcom	$$⊢D=⦋y/x⦌D\leftrightarrow ⦋y/x⦌D=D$$
93	92	imbi2i	$$⊢\left(y=x\to D=⦋y/x⦌D\right)\leftrightarrow \left(y=x\to ⦋y/x⦌D=D\right)$$
94	91 93	bitri	$$⊢\left(x=y\to D=⦋y/x⦌D\right)\leftrightarrow \left(y=x\to ⦋y/x⦌D=D\right)$$
95	61 94	mpbi	$$⊢y=x\to ⦋y/x⦌D=D$$
96	95 44	oveq12d	$$⊢y=x\to ⦋y/x⦌D⦋y/x⦌A=DA$$
97	90 96	oveq12d	$$⊢y=x\to ⦋y/x⦌B⦋y/x⦌C+⦋y/x⦌D⦋y/x⦌A=BC+DA$$
98	83 84 97	cbvmpt	$$⊢\left(y\in X⟼⦋y/x⦌B⦋y/x⦌C+⦋y/x⦌D⦋y/x⦌A\right)=\left(x\in X⟼BC+DA\right)$$
99	98	a1i	$$⊢\phi \to \left(y\in X⟼⦋y/x⦌B⦋y/x⦌C+⦋y/x⦌D⦋y/x⦌A\right)=\left(x\in X⟼BC+DA\right)$$
100	19 79 99	3eqtrd	$$⊢\phi \to \frac{d\left(x\in X⟼AC\right)}{d_{S}x}=\left(x\in X⟼BC+DA\right)$$