Theorem dvcmul

Description: The product rule when one argument is a constant. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 10-Feb-2015)

	Ref	Expression
Hypotheses	dvcmul.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
	dvcmul.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
	dvcmul.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	dvcmul.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
	dvcmul.c	⊢ ( 𝜑 → 𝐶 ∈ dom ( 𝑆 D 𝐹 ) )
Assertion	dvcmul	⊢ ( 𝜑 → ( ( 𝑆 D ( ( 𝑆 × { 𝐴 } ) ∘f · 𝐹 ) ) ‘ 𝐶 ) = ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvcmul.s	⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2		dvcmul.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
3		dvcmul.a	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4		dvcmul.x	⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
5		dvcmul.c	⊢ ( 𝜑 → 𝐶 ∈ dom ( 𝑆 D 𝐹 ) )
6		fconst6g	⊢ ( 𝐴 ∈ ℂ → ( 𝑆 × { 𝐴 } ) : 𝑆 ⟶ ℂ )
7	3 6	syl	⊢ ( 𝜑 → ( 𝑆 × { 𝐴 } ) : 𝑆 ⟶ ℂ )
8		ssidd	⊢ ( 𝜑 → 𝑆 ⊆ 𝑆 )
9		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
10	1 9	syl	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
11	10 2 4	dvbss	⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) ⊆ 𝑋 )
12	11 5	sseldd	⊢ ( 𝜑 → 𝐶 ∈ 𝑋 )
13	4 12	sseldd	⊢ ( 𝜑 → 𝐶 ∈ 𝑆 )
14		fconst6g	⊢ ( 𝐴 ∈ ℂ → ( ℂ × { 𝐴 } ) : ℂ ⟶ ℂ )
15	3 14	syl	⊢ ( 𝜑 → ( ℂ × { 𝐴 } ) : ℂ ⟶ ℂ )
16		ssidd	⊢ ( 𝜑 → ℂ ⊆ ℂ )
17		dvconst	⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( ℂ × { 𝐴 } ) ) = ( ℂ × { 0 } ) )
18	3 17	syl	⊢ ( 𝜑 → ( ℂ D ( ℂ × { 𝐴 } ) ) = ( ℂ × { 0 } ) )
19	18	dmeqd	⊢ ( 𝜑 → dom ( ℂ D ( ℂ × { 𝐴 } ) ) = dom ( ℂ × { 0 } ) )
20		c0ex	⊢ 0 ∈ V
21	20	fconst	⊢ ( ℂ × { 0 } ) : ℂ ⟶ { 0 }
22	21	fdmi	⊢ dom ( ℂ × { 0 } ) = ℂ
23	19 22	eqtrdi	⊢ ( 𝜑 → dom ( ℂ D ( ℂ × { 𝐴 } ) ) = ℂ )
24	10 23	sseqtrrd	⊢ ( 𝜑 → 𝑆 ⊆ dom ( ℂ D ( ℂ × { 𝐴 } ) ) )
25		dvres3	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ ( ℂ × { 𝐴 } ) : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D ( ℂ × { 𝐴 } ) ) ) ) → ( 𝑆 D ( ( ℂ × { 𝐴 } ) ↾ 𝑆 ) ) = ( ( ℂ D ( ℂ × { 𝐴 } ) ) ↾ 𝑆 ) )
26	1 15 16 24 25	syl22anc	⊢ ( 𝜑 → ( 𝑆 D ( ( ℂ × { 𝐴 } ) ↾ 𝑆 ) ) = ( ( ℂ D ( ℂ × { 𝐴 } ) ) ↾ 𝑆 ) )
27		xpssres	⊢ ( 𝑆 ⊆ ℂ → ( ( ℂ × { 𝐴 } ) ↾ 𝑆 ) = ( 𝑆 × { 𝐴 } ) )
28	10 27	syl	⊢ ( 𝜑 → ( ( ℂ × { 𝐴 } ) ↾ 𝑆 ) = ( 𝑆 × { 𝐴 } ) )
29	28	oveq2d	⊢ ( 𝜑 → ( 𝑆 D ( ( ℂ × { 𝐴 } ) ↾ 𝑆 ) ) = ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) )
30	18	reseq1d	⊢ ( 𝜑 → ( ( ℂ D ( ℂ × { 𝐴 } ) ) ↾ 𝑆 ) = ( ( ℂ × { 0 } ) ↾ 𝑆 ) )
31		xpssres	⊢ ( 𝑆 ⊆ ℂ → ( ( ℂ × { 0 } ) ↾ 𝑆 ) = ( 𝑆 × { 0 } ) )
32	10 31	syl	⊢ ( 𝜑 → ( ( ℂ × { 0 } ) ↾ 𝑆 ) = ( 𝑆 × { 0 } ) )
33	30 32	eqtrd	⊢ ( 𝜑 → ( ( ℂ D ( ℂ × { 𝐴 } ) ) ↾ 𝑆 ) = ( 𝑆 × { 0 } ) )
34	26 29 33	3eqtr3d	⊢ ( 𝜑 → ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) = ( 𝑆 × { 0 } ) )
35	20	fconst2	⊢ ( ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) : 𝑆 ⟶ { 0 } ↔ ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) = ( 𝑆 × { 0 } ) )
36	34 35	sylibr	⊢ ( 𝜑 → ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) : 𝑆 ⟶ { 0 } )
37	36	fdmd	⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) = 𝑆 )
38	13 37	eleqtrrd	⊢ ( 𝜑 → 𝐶 ∈ dom ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) )
39	7 8 2 4 1 38 5	dvmul	⊢ ( 𝜑 → ( ( 𝑆 D ( ( 𝑆 × { 𝐴 } ) ∘f · 𝐹 ) ) ‘ 𝐶 ) = ( ( ( ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) ‘ 𝐶 ) · ( 𝐹 ‘ 𝐶 ) ) + ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · ( ( 𝑆 × { 𝐴 } ) ‘ 𝐶 ) ) ) )
40	34	fveq1d	⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) ‘ 𝐶 ) = ( ( 𝑆 × { 0 } ) ‘ 𝐶 ) )
41	20	fvconst2	⊢ ( 𝐶 ∈ 𝑆 → ( ( 𝑆 × { 0 } ) ‘ 𝐶 ) = 0 )
42	13 41	syl	⊢ ( 𝜑 → ( ( 𝑆 × { 0 } ) ‘ 𝐶 ) = 0 )
43	40 42	eqtrd	⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) ‘ 𝐶 ) = 0 )
44	43	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) ‘ 𝐶 ) · ( 𝐹 ‘ 𝐶 ) ) = ( 0 · ( 𝐹 ‘ 𝐶 ) ) )
45	2 12	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
46	45	mul02d	⊢ ( 𝜑 → ( 0 · ( 𝐹 ‘ 𝐶 ) ) = 0 )
47	44 46	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) ‘ 𝐶 ) · ( 𝐹 ‘ 𝐶 ) ) = 0 )
48		fvconst2g	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ 𝑆 ) → ( ( 𝑆 × { 𝐴 } ) ‘ 𝐶 ) = 𝐴 )
49	3 13 48	syl2anc	⊢ ( 𝜑 → ( ( 𝑆 × { 𝐴 } ) ‘ 𝐶 ) = 𝐴 )
50	49	oveq2d	⊢ ( 𝜑 → ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · ( ( 𝑆 × { 𝐴 } ) ‘ 𝐶 ) ) = ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · 𝐴 ) )
51		dvfg	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
52	1 51	syl	⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
53	52 5	ffvelcdmd	⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ∈ ℂ )
54	53 3	mulcomd	⊢ ( 𝜑 → ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · 𝐴 ) = ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
55	50 54	eqtrd	⊢ ( 𝜑 → ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · ( ( 𝑆 × { 𝐴 } ) ‘ 𝐶 ) ) = ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
56	47 55	oveq12d	⊢ ( 𝜑 → ( ( ( ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) ‘ 𝐶 ) · ( 𝐹 ‘ 𝐶 ) ) + ( ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) · ( ( 𝑆 × { 𝐴 } ) ‘ 𝐶 ) ) ) = ( 0 + ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) ) )
57	3 53	mulcld	⊢ ( 𝜑 → ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) ∈ ℂ )
58	57	addlidd	⊢ ( 𝜑 → ( 0 + ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) ) = ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
59	39 56 58	3eqtrd	⊢ ( 𝜑 → ( ( 𝑆 D ( ( 𝑆 × { 𝐴 } ) ∘f · 𝐹 ) ) ‘ 𝐶 ) = ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )