Metamath Proof Explorer

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 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℂ )
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 ffvelrnd ⊢ ( 𝜑 → ( ( 𝑆 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 addid2d ⊢ ( 𝜑 → ( 0 + ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) ) = ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )
59 39 56 58 3eqtrd ⊢ ( 𝜑 → ( ( 𝑆 D ( ( 𝑆 × { 𝐴 } ) ∘f · 𝐹 ) ) ‘ 𝐶 ) = ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝐶 ) ) )