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 𝐹 ) ) )