Metamath Proof Explorer

Theorem dvmptcmul

Description: Function-builder for derivative, product rule for constant multiplier. (Contributed by Mario Carneiro, 1-Sep-2014) (Revised by Mario Carneiro, 11-Feb-2015)

Ref Expression
Hypotheses dvmptadd.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmptadd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvmptadd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
dvmptadd.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
dvmptcmul.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
Assertion dvmptcmul ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐶 · 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐶 · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 dvmptadd.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvmptadd.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
3 dvmptadd.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
4 dvmptadd.da ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
5 dvmptcmul.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
6 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
7 0cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ∈ ℂ )
8 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐶 ∈ ℂ )
9 0cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 0 ∈ ℂ )
10 1 5 dvmptc ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑆 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑆 ↦ 0 ) )
11 4 dmeqd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
12 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 )
13 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝑋 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
14 12 13 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = 𝑋 )
15 11 14 eqtrd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = 𝑋 )
16 dvbsss ⊢ dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ⊆ 𝑆
17 15 16 eqsstrrdi ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
18 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
19 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
20 19 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
21 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
22 1 21 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
23 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
24 20 22 23 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
25 topontop ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top )
26 24 25 syl ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top )
27 toponuni ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
28 24 27 syl ⊢ ( 𝜑 → 𝑆 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
29 17 28 sseqtrd ⊢ ( 𝜑 → 𝑋 ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
30 eqid ⊢ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
31 30 ntrss2 ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top ∧ 𝑋 ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ⊆ 𝑋 )
32 26 29 31 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ⊆ 𝑋 )
33 2 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) : 𝑋 ⟶ ℂ )
34 22 33 17 18 19 dvbssntr ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) ⊆ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) )
35 15 34 eqsstrrd ⊢ ( 𝜑 → 𝑋 ⊆ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) )
36 32 35 eqssd ⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) = 𝑋 )
37 1 8 9 10 17 18 19 36 dvmptres2 ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
38 1 6 7 37 2 3 4 dvmptmul ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐶 · 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 0 · 𝐴 ) + ( 𝐵 · 𝐶 ) ) ) )
39 2 mul02d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 0 · 𝐴 ) = 0 )
40 39 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 0 · 𝐴 ) + ( 𝐵 · 𝐶 ) ) = ( 0 + ( 𝐵 · 𝐶 ) ) )
41 1 2 3 4 dvmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
42 41 6 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 · 𝐶 ) ∈ ℂ )
43 42 addlidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 0 + ( 𝐵 · 𝐶 ) ) = ( 𝐵 · 𝐶 ) )
44 41 6 mulcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 · 𝐶 ) = ( 𝐶 · 𝐵 ) )
45 40 43 44 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 0 · 𝐴 ) + ( 𝐵 · 𝐶 ) ) = ( 𝐶 · 𝐵 ) )
46 45 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 0 · 𝐴 ) + ( 𝐵 · 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐶 · 𝐵 ) ) )
47 38 46 eqtrd ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐶 · 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐶 · 𝐵 ) ) )