Metamath Proof Explorer

Theorem dvcmulf

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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
dvcmulf.df ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
Assertion dvcmulf ( 𝜑 → ( 𝑆 D ( ( 𝑆 × { 𝐴 } ) ∘f · 𝐹 ) ) = ( ( 𝑆 × { 𝐴 } ) ∘f · ( 𝑆 D 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 dvcmul.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
2 dvcmul.f ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ℂ )
3 dvcmul.a ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
4 dvcmulf.df ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) = 𝑋 )
5 fconstg ⊢ ( 𝐴 ∈ ℂ → ( 𝑋 × { 𝐴 } ) : 𝑋 ⟶ { 𝐴 } )
6 3 5 syl ⊢ ( 𝜑 → ( 𝑋 × { 𝐴 } ) : 𝑋 ⟶ { 𝐴 } )
7 3 snssd ⊢ ( 𝜑 → { 𝐴 } ⊆ ℂ )
8 6 7 fssd ⊢ ( 𝜑 → ( 𝑋 × { 𝐴 } ) : 𝑋 ⟶ ℂ )
9 c0ex ⊢ 0 ∈ V
10 9 fconst ⊢ ( 𝑋 × { 0 } ) : 𝑋 ⟶ { 0 }
11 recnprss ⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
12 1 11 syl ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
13 fconstg ⊢ ( 𝐴 ∈ ℂ → ( 𝑆 × { 𝐴 } ) : 𝑆 ⟶ { 𝐴 } )
14 3 13 syl ⊢ ( 𝜑 → ( 𝑆 × { 𝐴 } ) : 𝑆 ⟶ { 𝐴 } )
15 14 7 fssd ⊢ ( 𝜑 → ( 𝑆 × { 𝐴 } ) : 𝑆 ⟶ ℂ )
16 ssidd ⊢ ( 𝜑 → 𝑆 ⊆ 𝑆 )
17 dvbsss ⊢ dom ( 𝑆 D 𝐹 ) ⊆ 𝑆
18 17 a1i ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) ⊆ 𝑆 )
19 4 18 eqsstrrd ⊢ ( 𝜑 → 𝑋 ⊆ 𝑆 )
20 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
21 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
22 20 21 dvres ⊢ ( ( ( 𝑆 ⊆ ℂ ∧ ( 𝑆 × { 𝐴 } ) : 𝑆 ⟶ ℂ ) ∧ ( 𝑆 ⊆ 𝑆 ∧ 𝑋 ⊆ 𝑆 ) ) → ( 𝑆 D ( ( 𝑆 × { 𝐴 } ) ↾ 𝑋 ) ) = ( ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) ↾ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ) )
23 12 15 16 19 22 syl22anc ⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑆 × { 𝐴 } ) ↾ 𝑋 ) ) = ( ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) ↾ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ) )
24 19 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ↾ 𝑋 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
25 fconstmpt ⊢ ( 𝑆 × { 𝐴 } ) = ( 𝑥 ∈ 𝑆 ↦ 𝐴 )
26 25 reseq1i ⊢ ( ( 𝑆 × { 𝐴 } ) ↾ 𝑋 ) = ( ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ↾ 𝑋 )
27 fconstmpt ⊢ ( 𝑋 × { 𝐴 } ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
28 24 26 27 3eqtr4g ⊢ ( 𝜑 → ( ( 𝑆 × { 𝐴 } ) ↾ 𝑋 ) = ( 𝑋 × { 𝐴 } ) )
29 28 oveq2d ⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑆 × { 𝐴 } ) ↾ 𝑋 ) ) = ( 𝑆 D ( 𝑋 × { 𝐴 } ) ) )
30 19 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ 0 ) ↾ 𝑋 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
31 fconstg ⊢ ( 𝐴 ∈ ℂ → ( ℂ × { 𝐴 } ) : ℂ ⟶ { 𝐴 } )
32 3 31 syl ⊢ ( 𝜑 → ( ℂ × { 𝐴 } ) : ℂ ⟶ { 𝐴 } )
33 32 7 fssd ⊢ ( 𝜑 → ( ℂ × { 𝐴 } ) : ℂ ⟶ ℂ )
34 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
35 dvconst ⊢ ( 𝐴 ∈ ℂ → ( ℂ D ( ℂ × { 𝐴 } ) ) = ( ℂ × { 0 } ) )
36 3 35 syl ⊢ ( 𝜑 → ( ℂ D ( ℂ × { 𝐴 } ) ) = ( ℂ × { 0 } ) )
37 36 dmeqd ⊢ ( 𝜑 → dom ( ℂ D ( ℂ × { 𝐴 } ) ) = dom ( ℂ × { 0 } ) )
38 9 fconst ⊢ ( ℂ × { 0 } ) : ℂ ⟶ { 0 }
39 38 fdmi ⊢ dom ( ℂ × { 0 } ) = ℂ
40 37 39 eqtrdi ⊢ ( 𝜑 → dom ( ℂ D ( ℂ × { 𝐴 } ) ) = ℂ )
41 12 40 sseqtrrd ⊢ ( 𝜑 → 𝑆 ⊆ dom ( ℂ D ( ℂ × { 𝐴 } ) ) )
42 dvres3 ⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ ( ℂ × { 𝐴 } ) : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D ( ℂ × { 𝐴 } ) ) ) ) → ( 𝑆 D ( ( ℂ × { 𝐴 } ) ↾ 𝑆 ) ) = ( ( ℂ D ( ℂ × { 𝐴 } ) ) ↾ 𝑆 ) )
43 1 33 34 41 42 syl22anc ⊢ ( 𝜑 → ( 𝑆 D ( ( ℂ × { 𝐴 } ) ↾ 𝑆 ) ) = ( ( ℂ D ( ℂ × { 𝐴 } ) ) ↾ 𝑆 ) )
44 xpssres ⊢ ( 𝑆 ⊆ ℂ → ( ( ℂ × { 𝐴 } ) ↾ 𝑆 ) = ( 𝑆 × { 𝐴 } ) )
45 12 44 syl ⊢ ( 𝜑 → ( ( ℂ × { 𝐴 } ) ↾ 𝑆 ) = ( 𝑆 × { 𝐴 } ) )
46 45 oveq2d ⊢ ( 𝜑 → ( 𝑆 D ( ( ℂ × { 𝐴 } ) ↾ 𝑆 ) ) = ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) )
47 36 reseq1d ⊢ ( 𝜑 → ( ( ℂ D ( ℂ × { 𝐴 } ) ) ↾ 𝑆 ) = ( ( ℂ × { 0 } ) ↾ 𝑆 ) )
48 xpssres ⊢ ( 𝑆 ⊆ ℂ → ( ( ℂ × { 0 } ) ↾ 𝑆 ) = ( 𝑆 × { 0 } ) )
49 12 48 syl ⊢ ( 𝜑 → ( ( ℂ × { 0 } ) ↾ 𝑆 ) = ( 𝑆 × { 0 } ) )
50 47 49 eqtrd ⊢ ( 𝜑 → ( ( ℂ D ( ℂ × { 𝐴 } ) ) ↾ 𝑆 ) = ( 𝑆 × { 0 } ) )
51 43 46 50 3eqtr3d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) = ( 𝑆 × { 0 } ) )
52 fconstmpt ⊢ ( 𝑆 × { 0 } ) = ( 𝑥 ∈ 𝑆 ↦ 0 )
53 51 52 eqtrdi ⊢ ( 𝜑 → ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) = ( 𝑥 ∈ 𝑆 ↦ 0 ) )
54 20 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
55 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
56 54 12 55 sylancr ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
57 topontop ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top )
58 56 57 syl ⊢ ( 𝜑 → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top )
59 toponuni ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
60 56 59 syl ⊢ ( 𝜑 → 𝑆 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
61 19 60 sseqtrd ⊢ ( 𝜑 → 𝑋 ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
62 eqid ⊢ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
63 62 ntrss2 ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top ∧ 𝑋 ⊆ ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ⊆ 𝑋 )
64 58 61 63 syl2anc ⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ⊆ 𝑋 )
65 12 2 19 21 20 dvbssntr ⊢ ( 𝜑 → dom ( 𝑆 D 𝐹 ) ⊆ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) )
66 4 65 eqsstrrd ⊢ ( 𝜑 → 𝑋 ⊆ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) )
67 64 66 eqssd ⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) = 𝑋 )
68 53 67 reseq12d ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) ↾ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ) = ( ( 𝑥 ∈ 𝑆 ↦ 0 ) ↾ 𝑋 ) )
69 fconstmpt ⊢ ( 𝑋 × { 0 } ) = ( 𝑥 ∈ 𝑋 ↦ 0 )
70 69 a1i ⊢ ( 𝜑 → ( 𝑋 × { 0 } ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
71 30 68 70 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑆 × { 𝐴 } ) ) ↾ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝑋 ) ) = ( 𝑋 × { 0 } ) )
72 23 29 71 3eqtr3d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑋 × { 𝐴 } ) ) = ( 𝑋 × { 0 } ) )
73 72 feq1d ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑋 × { 𝐴 } ) ) : 𝑋 ⟶ { 0 } ↔ ( 𝑋 × { 0 } ) : 𝑋 ⟶ { 0 } ) )
74 10 73 mpbiri ⊢ ( 𝜑 → ( 𝑆 D ( 𝑋 × { 𝐴 } ) ) : 𝑋 ⟶ { 0 } )
75 74 fdmd ⊢ ( 𝜑 → dom ( 𝑆 D ( 𝑋 × { 𝐴 } ) ) = 𝑋 )
76 1 8 2 75 4 dvmulf ⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑋 × { 𝐴 } ) ∘f · 𝐹 ) ) = ( ( ( 𝑆 D ( 𝑋 × { 𝐴 } ) ) ∘f · 𝐹 ) ∘f + ( ( 𝑆 D 𝐹 ) ∘f · ( 𝑋 × { 𝐴 } ) ) ) )
77 sseqin2 ⊢ ( 𝑋 ⊆ 𝑆 ↔ ( 𝑆 ∩ 𝑋 ) = 𝑋 )
78 19 77 sylib ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑋 ) = 𝑋 )
79 78 mpteq1d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑆 ∩ 𝑋 ) ↦ ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) ) )
80 14 ffnd ⊢ ( 𝜑 → ( 𝑆 × { 𝐴 } ) Fn 𝑆 )
81 2 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑋 )
82 1 19 ssexd ⊢ ( 𝜑 → 𝑋 ∈ V )
83 eqid ⊢ ( 𝑆 ∩ 𝑋 ) = ( 𝑆 ∩ 𝑋 )
84 fvconst2g ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑆 × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
85 3 84 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑆 × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
86 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
87 80 81 1 82 83 85 86 offval ⊢ ( 𝜑 → ( ( 𝑆 × { 𝐴 } ) ∘f · 𝐹 ) = ( 𝑥 ∈ ( 𝑆 ∩ 𝑋 ) ↦ ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) ) )
88 6 ffnd ⊢ ( 𝜑 → ( 𝑋 × { 𝐴 } ) Fn 𝑋 )
89 inidm ⊢ ( 𝑋 ∩ 𝑋 ) = 𝑋
90 fvconst2g ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
91 3 90 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑋 × { 𝐴 } ) ‘ 𝑥 ) = 𝐴 )
92 88 81 82 82 89 91 86 offval ⊢ ( 𝜑 → ( ( 𝑋 × { 𝐴 } ) ∘f · 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · ( 𝐹 ‘ 𝑥 ) ) ) )
93 79 87 92 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑆 × { 𝐴 } ) ∘f · 𝐹 ) = ( ( 𝑋 × { 𝐴 } ) ∘f · 𝐹 ) )
94 93 oveq2d ⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑆 × { 𝐴 } ) ∘f · 𝐹 ) ) = ( 𝑆 D ( ( 𝑋 × { 𝐴 } ) ∘f · 𝐹 ) ) )
95 78 mpteq1d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝑆 ∩ 𝑋 ) ↦ ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) ) )
96 dvfg ⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
97 1 96 syl ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ )
98 4 feq2d ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) : dom ( 𝑆 D 𝐹 ) ⟶ ℂ ↔ ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ ) )
99 97 98 mpbid ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) : 𝑋 ⟶ ℂ )
100 99 ffnd ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) Fn 𝑋 )
101 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) = ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) )
102 80 100 1 82 83 85 101 offval ⊢ ( 𝜑 → ( ( 𝑆 × { 𝐴 } ) ∘f · ( 𝑆 D 𝐹 ) ) = ( 𝑥 ∈ ( 𝑆 ∩ 𝑋 ) ↦ ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) ) )
103 0cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 0 ∈ ℂ )
104 ovexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · 𝐴 ) ∈ V )
105 72 oveq1d ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑋 × { 𝐴 } ) ) ∘f · 𝐹 ) = ( ( 𝑋 × { 0 } ) ∘f · 𝐹 ) )
106 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
107 mul02 ⊢ ( 𝑥 ∈ ℂ → ( 0 · 𝑥 ) = 0 )
108 107 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 0 · 𝑥 ) = 0 )
109 82 2 106 106 108 caofid2 ⊢ ( 𝜑 → ( ( 𝑋 × { 0 } ) ∘f · 𝐹 ) = ( 𝑋 × { 0 } ) )
110 105 109 eqtrd ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑋 × { 𝐴 } ) ) ∘f · 𝐹 ) = ( 𝑋 × { 0 } ) )
111 110 69 eqtrdi ⊢ ( 𝜑 → ( ( 𝑆 D ( 𝑋 × { 𝐴 } ) ) ∘f · 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ 0 ) )
112 fvexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ∈ V )
113 3 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
114 99 feqmptd ⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
115 27 a1i ⊢ ( 𝜑 → ( 𝑋 × { 𝐴 } ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
116 82 112 113 114 115 offval2 ⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) ∘f · ( 𝑋 × { 𝐴 } ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · 𝐴 ) ) )
117 82 103 104 111 116 offval2 ⊢ ( 𝜑 → ( ( ( 𝑆 D ( 𝑋 × { 𝐴 } ) ) ∘f · 𝐹 ) ∘f + ( ( 𝑆 D 𝐹 ) ∘f · ( 𝑋 × { 𝐴 } ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 0 + ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · 𝐴 ) ) ) )
118 99 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ∈ ℂ )
119 118 113 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · 𝐴 ) ∈ ℂ )
120 119 addlidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 0 + ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · 𝐴 ) ) = ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · 𝐴 ) )
121 118 113 mulcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · 𝐴 ) = ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
122 120 121 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 0 + ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · 𝐴 ) ) = ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) )
123 122 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( 0 + ( ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) · 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) ) )
124 117 123 eqtrd ⊢ ( 𝜑 → ( ( ( 𝑆 D ( 𝑋 × { 𝐴 } ) ) ∘f · 𝐹 ) ∘f + ( ( 𝑆 D 𝐹 ) ∘f · ( 𝑋 × { 𝐴 } ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · ( ( 𝑆 D 𝐹 ) ‘ 𝑥 ) ) ) )
125 95 102 124 3eqtr4d ⊢ ( 𝜑 → ( ( 𝑆 × { 𝐴 } ) ∘f · ( 𝑆 D 𝐹 ) ) = ( ( ( 𝑆 D ( 𝑋 × { 𝐴 } ) ) ∘f · 𝐹 ) ∘f + ( ( 𝑆 D 𝐹 ) ∘f · ( 𝑋 × { 𝐴 } ) ) ) )
126 76 94 125 3eqtr4d ⊢ ( 𝜑 → ( 𝑆 D ( ( 𝑆 × { 𝐴 } ) ∘f · 𝐹 ) ) = ( ( 𝑆 × { 𝐴 } ) ∘f · ( 𝑆 D 𝐹 ) ) )